Theorem: LO.Propositional.Superintuitionistic.Kripke.unprovable_bot (Logic/Propositional/Superintuitionistic/Kripke/Soundness.lean)

State before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
⊢ 𝓓 ⊬! ⊥
Tactic:
intro h
State after:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
h : 𝓓 ⊢! ⊥
⊢ False

State before:
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
ne : IsNonempty 𝔽(Ax(𝓓))
h : 𝓓 ⊢! ⊥
⊢ False
Tactic:
obtain ⟨F, hF⟩ := ne
State after:
case mk.intro
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
h : 𝓓 ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(𝓓))
⊢ False

State before:
case mk.intro
α : Type u_1
inst✝ : Inhabited α
𝓓 : DeductionParameter α
h : 𝓓 ⊢! ⊥
F : Frame
hF : F ∈ 𝔽(Ax(𝓓))
⊢ False
Tactic:
simpa using sound! h hF
State after:
no goals