Theorem: MyNat.or_symm (TheoremProvingLean/inductive_types.lean)

State before:
P Q : Prop
⊢ P ∨ Q → Q ∨ P
Tactic:
intro 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 => apply Or.inr; exact hp
| inr hq =>  apply Or.inl; exact hq
State after:
no goals

State before:
case inl
P Q : Prop
hp : P
⊢ Q ∨ P
Tactic:
apply Or.inr
State after:
case inl.h
P Q : Prop
hp : P
⊢ P

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

State before:
case inr
P Q : Prop
hq : Q
⊢ Q ∨ P
Tactic:
apply Or.inl
State after:
case inr.h
P Q : Prop
hq : Q
⊢ Q

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