Theorem: and_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 intro
P Q R : Prop
h1 : P
h2 : Q
⊢ Q ∧ P

State before:
case intro
P Q R : Prop
h1 : P
h2 : Q
⊢ Q ∧ P
Tactic:
constructor
State after:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q

case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P

State before:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q

case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
. exact h2
State after:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P

State before:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
. exact h1
State after:
no goals

State before:
case intro.left
P Q R : Prop
h1 : P
h2 : Q
⊢ Q
Tactic:
exact h2
State after:
no goals

State before:
case intro.right
P Q R : Prop
h1 : P
h2 : Q
⊢ P
Tactic:
exact h1
State after:
no goals