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

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

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

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

State before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ a
Tactic:
apply hpeirce a False
State after:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ (a → False) → a

State before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
⊢ (a → False) → a
Tactic:
intro hna
State after:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ a

State before:
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ a
Tactic:
apply False.elim
State after:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ False

State before:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ False
Tactic:
apply hnna
State after:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ ¬a

State before:
case h
hpeirce : ∀ (a b : Prop), ((a → b) → a) → a
a : Prop
hnna : ¬¬a
hna : a → False
⊢ ¬a
Tactic:
exact hna
State after:
no goals