Theorem: LoVe.ForwardProofs.And_swap_tactical (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
a b : Prop
⊢ a ∧ b → b ∧ a
Tactic:
intro hab
State after:
a b : Prop
hab : a ∧ b
⊢ b ∧ a

State before:
a b : Prop
hab : a ∧ b
⊢ b ∧ a
Tactic:
apply And.intro
State after:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a

State before:
case left
a b : Prop
hab : a ∧ b
⊢ b

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.right
State after:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a

State before:
case left.self
a b : Prop
hab : a ∧ b
⊢ ?left.a ∧ b

case left.a
a b : Prop
hab : a ∧ b
⊢ Prop

case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
exact hab
State after:
case right
a b : Prop
hab : a ∧ b
⊢ a

State before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
apply And.left
State after:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop

State before:
case right.self
a b : Prop
hab : a ∧ b
⊢ a ∧ ?right.b

case right.b
a b : Prop
hab : a ∧ b
⊢ Prop
Tactic:
exact hab
State after:
no goals