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

State before:
⊢ ∀ {P Q : Prop}, P ∨ Q → Q ∨ P
Tactic:
intros P Q h
State after:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P

State before:
P Q : Prop
h : P ∨ Q
⊢ Q ∨ P
Tactic:
cases h with
| inl hp => exact Or.inr hp
| inr hq => exact Or.inl hq
State after:
no goals

State before:
case inl
P Q : Prop
hp : P
⊢ Q ∨ P
Tactic:
exact Or.inr hp
State after:
no goals

State before:
case inr
P Q : Prop
hq : Q
⊢ Q ∨ P
Tactic:
exact Or.inl hq
State after:
no goals