Theorem: my_first_theorem (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
⊢ p ∧ q → q ∧ p
Tactic:
intro hpq
State after:
p q r : Prop
hpq : p ∧ q
⊢ q ∧ p

State before:
p q r : Prop
hpq : p ∧ q
⊢ q ∧ p
Tactic:
cases' hpq with hp hq
State after:
case intro
p q r : Prop
hp : p
hq : q
⊢ q ∧ p

State before:
case intro
p q r : Prop
hp : p
hq : q
⊢ q ∧ p
Tactic:
apply And.intro
State after:
case intro.left
p q r : Prop
hp : p
hq : q
⊢ q

case intro.right
p q r : Prop
hp : p
hq : q
⊢ p

State before:
case intro.left
p q r : Prop
hp : p
hq : q
⊢ q

case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Tactic:
. exact hq
State after:
case intro.right
p q r : Prop
hp : p
hq : q
⊢ p

State before:
case intro.right
p q r : Prop
hp : p
hq : q
⊢ p
Tactic:
. exact hp
State after:
no goals