Theorem: LO.Propositional.Superintuitionistic.Kripke.noLEM_atom (Logic/Propositional/Superintuitionistic/Kripke/LEM.lean)

State before:
α : Type
a : α
⊢ ¬LEMCounterexampleModel ⊧ atom a ⋎ ~atom a
Tactic:
simp [ValidOnModel.iff_models, Satisfies.iff_models, ValidOnModel, Satisfies, LEMCounterexampleModel]
State after:
α : Type
a : α
⊢ ∃ x, ¬x = 1 ∧ x ≺ 1

State before:
α : Type
a : α
⊢ ∃ x, ¬x = 1 ∧ x ≺ 1
Tactic:
use 0
State after:
case h
α : Type
a : α
⊢ ¬0 = 1 ∧ 0 ≺ 1

State before:
case h
α : Type
a : α
⊢ ¬0 = 1 ∧ 0 ≺ 1
Tactic:
aesop
State after:
no goals