Theorem: or_swap' (LAMR/Examples/using_lean_as_a_proof_assistant/proof_terms.lean)

State before:
P Q R : Prop
⊢ P ∨ Q → Q ∨ P
Tactic:
intro h
State after:
P Q R : Prop
h : P ∨ Q
⊢ Q ∨ P

State before:
P Q R : Prop
h : P ∨ Q
⊢ Q ∨ P
Tactic:
rcases h with h1 |  h2
State after:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P

case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P

State before:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P

case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
. right; exact h1
State after:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P

State before:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
. left; exact h2
State after:
no goals

State before:
case inl
P Q R : Prop
h1 : P
⊢ Q ∨ P
Tactic:
right
State after:
case inl.h
P Q R : Prop
h1 : P
⊢ P

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

State before:
case inr
P Q R : Prop
h2 : Q
⊢ Q ∨ P
Tactic:
left
State after:
case inr.h
P Q R : Prop
h2 : Q
⊢ Q

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