Theorem: LO.Modal.Standard.Kripke.realize_theory_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 ⊧* System.theory 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 ∈ System.theory 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 ∈ System.theory 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 ∈ System.theory 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 ∈ System.theory 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 ∈ System.theory 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 ∈ System.theory L
⊢ L ⊢! p
Tactic:
simpa [System.theory] using hp
State after:
no goals