Theorem: LoVe.BackwardProofs.And_swap_braces (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
⊢ ∀ (a b : Prop), a ∧ b → b ∧ a
Tactic:
intro a b 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:
{ exact And.right hab }
State after:
case right
a b : Prop
hab : a ∧ b
⊢ a

State before:
case right
a b : Prop
hab : a ∧ b
⊢ a
Tactic:
{ exact And.left hab }
State after:
no goals

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

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