Theorem: Smt.Reconstruct.Prop.orImplies (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {p q : Prop}, (¬p → q) → p ∨ q
Tactic:
intros p q h
State after:
p q : Prop
h : ¬p → q
⊢ p ∨ q

State before:
p q : Prop
h : ¬p → q
⊢ p ∨ q
Tactic:
exact match Classical.em p with
| Or.inl pp => Or.inl pp
| Or.inr npp => match Classical.em q with
                | Or.inl pq => Or.inr pq
                | Or.inr npq => False.elim (npq (h npp))
State after:
no goals