Theorem: LO.Modal.Standard.Kripke.unprovable_bot (Logic/Modal/Standard/Kripke/Soundness.lean)

State before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
⊢ L ⊬! ⊥
Tactic:
intro h
State after:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FrameClass.IsNonempty 𝔽(Ax(L))
h : L ⊢! ⊥
⊢ False

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

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