by_cases p
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)