Theorem: LoVe.BackwardProofs.Or_swap (LoVe/Lectures/LoVe03_BackwardProofs_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 Or.elim hab
State after:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a

case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a

State before:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a

case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
{ intro ha
  exact Or.inr ha }
State after:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a

State before:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
{ intro hb
  exact Or.inl hb }
State after:
no goals

State before:
case left
a b : Prop
hab : a ∨ b
⊢ a → b ∨ a
Tactic:
intro ha
State after:
case left
a b : Prop
hab : a ∨ b
ha : a
⊢ b ∨ a

State before:
case left
a b : Prop
hab : a ∨ b
ha : a
⊢ b ∨ a
Tactic:
exact Or.inr ha
State after:
no goals

State before:
case right
a b : Prop
hab : a ∨ b
⊢ b → b ∨ a
Tactic:
intro hb
State after:
case right
a b : Prop
hab : a ∨ b
hb : b
⊢ b ∨ a

State before:
case right
a b : Prop
hab : a ∨ b
hb : b
⊢ b ∨ a
Tactic:
exact Or.inl hb
State after:
no goals