Theorem: LO.Propositional.Superintuitionistic.Kripke.complete! (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
⊢ 𝔽(Ax(𝓓)) ⊧ p → 𝓓 ⊢! p
Tactic:
intro h
State after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ 𝓓 ⊢! p

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ 𝓓 ⊢! p
Tactic:
apply deducible_of_validOnCanonicelModel.mp
State after:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ CanonicalModel 𝓓 ⊧ p

State before:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : Inhabited α
𝓓 : DeductionParameter α
inst✝³ : 𝓓.IncludeEFQ
inst✝² : Encodable α
p : Formula α
inst✝¹ : Consistent 𝓓
inst✝ : Canonical 𝓓
h : 𝔽(Ax(𝓓)) ⊧ p
⊢ CanonicalModel 𝓓 ⊧ p
Tactic:
exact h Canonical.realize _ _
State after:
no goals