Theorem: LO.Modal.Standard.Kripke.realize_axiomset_of_self_canonicalModel (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ CanonicalModel L ⊧* Ax(L)
Tactic:
apply Semantics.realizeSet_iff.mpr
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ Ax(L) → CanonicalModel L ⊧ f

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
⊢ ∀ ⦃f : Formula α⦄, f ∈ Ax(L) → CanonicalModel L ⊧ f
Tactic:
intro p hp
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ CanonicalModel L ⊧ p

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ CanonicalModel L ⊧ p
Tactic:
apply iff_valid_on_canonicalModel_deducible.mpr
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Tactic:
exact ⟨Deduction.maxm hp⟩
State after:
no goals