Theorem: LO.FirstOrder.ModelsTheory.of_provably_subtheory (Logic/FirstOrder/Completeness/Lemmata.lean)

State before:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
⊢ ∀ ⦃f : Sentence L⦄, f ∈ T → inst✝.toStruc ⊧ f
Tactic:
intro p hp
State after:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
⊢ inst✝.toStruc ⊧ p

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

State before:
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U V : Theory L
x✝ : T ≼ U
h : M ⊧ₘ* U
p : Sentence L
hp : p ∈ T
this : U ⊢ p
⊢ inst✝.toStruc ⊧ p
Tactic:
exact consequence_iff'.{u, w}.mp (sound! ⟨this⟩) M
State after:
no goals