Theorem: LO.FirstOrder.models_of_subtheory (Logic/FirstOrder/Basic/Soundness.lean)

State before:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
⊢ inst✝¹.toStruc ⊧ p
Tactic:
have : T ⊢ p := System.Subtheory.prf (System.byAxm hp)
State after:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
this : T ⊢ p
⊢ inst✝¹.toStruc ⊧ p

State before:
L : Language
T U : Theory L
inst✝² : U ≼ T
M : Type u_1
inst✝¹ : Structure L M
inst✝ : Nonempty M
hM : M ⊧ₘ* T
p : Sentence L
hp : p ∈ U
this : T ⊢ p
⊢ inst✝¹.toStruc ⊧ p
Tactic:
exact sound this hM
State after:
no goals