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

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

State before:
α : Type u
L : DeductionParameter α
inst✝ : L.HasNecOnly
ne : FiniteFrameClass.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 : FiniteFrame
hF : F ∈ 𝔽ꟳ(Ax(L))
⊢ False

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