Theorem: LoVe.BackwardProofs.Peirce_of_EM (LoVe/Labs/Lab2Solution.lean)

State before:
⊢ ExcludedMiddle → Peirce
Tactic:
rw [ExcludedMiddle]
State after:
⊢ (∀ (a : Prop), a ∨ ¬a) → Peirce

State before:
⊢ (∀ (a : Prop), a ∨ ¬a) → Peirce
Tactic:
rw [Peirce]
State after:
⊢ (∀ (a : Prop), a ∨ ¬a) → ∀ (a b : Prop), ((a → b) → a) → a

State before:
⊢ (∀ (a : Prop), a ∨ ¬a) → ∀ (a b : Prop), ((a → b) → a) → a
Tactic:
intro hem
State after:
hem : ∀ (a : Prop), a ∨ ¬a
⊢ ∀ (a b : Prop), ((a → b) → a) → a

State before:
hem : ∀ (a : Prop), a ∨ ¬a
⊢ ∀ (a b : Prop), ((a → b) → a) → a
Tactic:
intro a b haba
State after:
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a

State before:
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a
Tactic:
apply Or.elim (hem a)
State after:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a

case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a

State before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a

case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
{ intro ha
  assumption }
State after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a

State before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
{ intro hna
  apply haba
  intro ha
  apply False.elim
  apply hna
  assumption }
State after:
no goals

State before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ a → a
Tactic:
intro ha
State after:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
ha : a
⊢ a

State before:
case left
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
ha : a
⊢ a
Tactic:
assumption
State after:
no goals

State before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
⊢ ¬a → a
Tactic:
intro hna
State after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a

State before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a
Tactic:
apply haba
State after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a → b

State before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
⊢ a → b
Tactic:
intro ha
State after:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ b

State before:
case right
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ b
Tactic:
apply False.elim
State after:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ False

State before:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ False
Tactic:
apply hna
State after:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ a

State before:
case right.h
hem : ∀ (a : Prop), a ∨ ¬a
a b : Prop
haba : (a → b) → a
hna : ¬a
ha : a
⊢ a
Tactic:
assumption
State after:
no goals