Theorem: alt_classical_redux.alt_classical_redux_em (TheoremProvingLean/tactics.lean)

State before:
p : Prop
⊢ p ∨ ¬p
Tactic:
suffices ¬¬ (p ∨ ¬ p) by
  apply assumed_dne; assumption
State after:
p : Prop
⊢ ¬¬(p ∨ ¬p)

State before:
p : Prop
⊢ ¬¬(p ∨ ¬p)
Tactic:
intro
State after:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ False

State before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ False
Tactic:
have h : ¬ p ∧ ¬¬p := by
  rw [← de_morgan_1]  assumption
State after:
p : Prop
a✝ : ¬(p ∨ ¬p)
h : ¬p ∧ ¬¬p
⊢ False

State before:
p : Prop
a✝ : ¬(p ∨ ¬p)
h : ¬p ∧ ¬¬p
⊢ False
Tactic:
cases h with
| intro hnp hnnp => contradiction
State after:
no goals

State before:
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ p ∨ ¬p
Tactic:
apply assumed_dne
State after:
case h
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ ¬¬(p ∨ ¬p)

State before:
case h
p : Prop
this : ¬¬(p ∨ ¬p)
⊢ ¬¬(p ∨ ¬p)
Tactic:
assumption
State after:
no goals

State before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬p ∧ ¬¬p
Tactic:
rw [← de_morgan_1]
State after:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬(p ∨ ¬p)

State before:
p : Prop
a✝ : ¬(p ∨ ¬p)
⊢ ¬(p ∨ ¬p)
Tactic:
assumption
State after:
no goals

State before:
case intro
p : Prop
a✝ : ¬(p ∨ ¬p)
hnp : ¬p
hnnp : ¬¬p
⊢ False
Tactic:
contradiction
State after:
no goals