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

State before:
α : Type
inst✝ : Inhabited α
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
obtain ⟨p, _⟩ : ∃ (p : Formula α), ¬(𝔽(Ax(𝐈𝐧𝐭))) ⊧ p ⋎ ~p := noLEM_on_frameclass
State after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p

State before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ ∃ p, 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
existsi p
State after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ 𝐈𝐧𝐭 ⊬! p ⋎ ~p

State before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ 𝐈𝐧𝐭 ⊬! p ⋎ ~p
Tactic:
by_contra hC
State after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
⊢ False

State before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
⊢ False
Tactic:
have : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p := sound! hC
State after:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
this : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ False

State before:
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
this : 𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ False
Tactic:
contradiction
State after:
no goals