Theorem: Smt.Reconstruct.Prop.equivElim1 (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:
rewrite [h]
State after:
P Q : Prop
h : P = Q
⊢ ¬Q ∨ Q

State before:
P Q : Prop
h : P = Q
⊢ ¬Q ∨ Q
Tactic:
cases Classical.em Q with
| inl q  => exact Or.inr q
| inr nq => exact Or.inl nq
State after:
no goals

State before:
case inl
P Q : Prop
h : P = Q
q : Q
⊢ ¬Q ∨ Q
Tactic:
exact Or.inr q
State after:
no goals

State before:
case inr
P Q : Prop
h : P = Q
nq : ¬Q
⊢ ¬Q ∨ Q
Tactic:
exact Or.inl nq
State after:
no goals