Theorem: Smt.Reconstruct.Prop.notEquivElim1 (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, Classical.em Q with
| Or.inl p, _ => Or.inl p
| _, Or.inl q => Or.inr q
| Or.inr np, Or.inr nq =>
  absurd (propext (Iff.intro (λ p => absurd p np) (λ q => absurd q nq))) h
State after:
no goals