Theorem: LoVe.about_Impl (LoVe/Homework/Homework3.lean)

State before:
⊢ ∀ (a b : Prop), ¬a ∨ b → a → b
Tactic:
intros a b hor ha
State after:
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b

State before:
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b
Tactic:
apply Or.elim hor
State after:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b

case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b

State before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b

case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
{ intro hna
  apply False.elim
  apply hna
  exact ha }
State after:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b

State before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
{ intro hb
  exact hb }
State after:
no goals

State before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ ¬a → b
Tactic:
intro hna
State after:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ b

State before:
case left
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ b
Tactic:
apply False.elim
State after:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ False

State before:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ False
Tactic:
apply hna
State after:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ a

State before:
case left.h
a b : Prop
hor : ¬a ∨ b
ha : a
hna : ¬a
⊢ a
Tactic:
exact ha
State after:
no goals

State before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
⊢ b → b
Tactic:
intro hb
State after:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
hb : b
⊢ b

State before:
case right
a b : Prop
hor : ¬a ∨ b
ha : a
hb : b
⊢ b
Tactic:
exact hb
State after:
no goals