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

State before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
Tactic:
simp [ValidOnFrameClass.iff_models, ValidOnFrameClass]
State after:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ∃ x ∈ 𝔽(𝗘𝗙𝗤), ¬ValidOnFrame x (p ⋎ (p ⟶ ⊥))

State before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, ∃ x ∈ 𝔽(𝗘𝗙𝗤), ¬ValidOnFrame x (p ⋎ (p ⟶ ⊥))
Tactic:
existsi (atom default), (LEMCounterexampleModel).Frame
State after:
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))

State before:
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤) ∧ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
constructor
State after:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)

case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))

State before:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)

case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
. apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr;
  trivial;
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
. simp [ValidOnFrame];
  existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary;
  apply noLEM_atom;
State after:
no goals

State before:
case left
α : Type
inst✝ : Inhabited α
⊢ LEMCounterexampleModel.Frame ∈ 𝔽(𝗘𝗙𝗤)
Tactic:
apply iff_definability_memAxiomSetFrameClass AxiomSet.EFQ.definability |>.mpr
State after:
case left
α : Type
inst✝ : Inhabited α
⊢ True

State before:
case left
α : Type
inst✝ : Inhabited α
⊢ True
Tactic:
trivial
State after:
no goals

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnFrame LEMCounterexampleModel.Frame (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
simp [ValidOnFrame]
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ x,
    ∃ (x_1 : ∀ {w₁ w₂ : LEMCounterexampleModel.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ¬ValidOnModel { Frame := LEMCounterexampleModel.Frame, Valuation := x, hereditary := x_1 }
          (atom default ⋎ (atom default ⟶ ⊥))

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ∃ x,
    ∃ (x_1 : ∀ {w₁ w₂ : LEMCounterexampleModel.Frame.World}, w₁ ≺ w₂ → ∀ {a : α}, x w₁ a → x w₂ a),
      ¬ValidOnModel { Frame := LEMCounterexampleModel.Frame, Valuation := x, hereditary := x_1 }
          (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
existsi (LEMCounterexampleModel).Valuation, LEMCounterexampleModel.hereditary
State after:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))

State before:
case right
α : Type
inst✝ : Inhabited α
⊢ ¬ValidOnModel
      { Frame := LEMCounterexampleModel.Frame, Valuation := LEMCounterexampleModel.Valuation, hereditary := ⋯ }
      (atom default ⋎ (atom default ⟶ ⊥))
Tactic:
apply noLEM_atom
State after:
no goals