-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_formula_iff_onTheory_models_equivSentence {φ : L.Formula α} :
    T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ ↑M ⊨ Formula.equivSentence φ

Tactic:
have : (L.lhomWithConstants α).IsExpansionOn M := LHom.isExpansionOn_reduct _ _

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : (L.lhomWithConstants α).IsExpansionOn ↑M
⊢ ↑M ⊨ Formula.equivSentence φ

Proof state:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this✝ : (constantsOn α).Structure ↑M := constantsOn.structure v
this : ↑M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Tactic:
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)

Result:
no goals

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝¹ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this✝ : (L.lhomWithConstants α).IsExpansionOn ↑M
this : ↑M ⊨ T
⊢ φ.Realize fun a => ↑(L.con a)

Tactic:
let M' := Theory.ModelType.of T M

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝¹ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this✝ : (L.lhomWithConstants α).IsExpansionOn ↑M
this : ↑M ⊨ T
M' : T.ModelType := ModelType.of T ↑M
⊢ φ.Realize fun a => ↑(L.con a)

Proof state:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this : (constantsOn α).Structure ↑M := constantsOn.structure v
⊢ φ.Realize v

Tactic:
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance

Result:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this✝ : (constantsOn α).Structure ↑M := constantsOn.structure v
this : ↑M ⊨ (L.lhomWithConstants α).onTheory T
⊢ φ.Realize v

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
⊢ ↑M ⊨ Formula.equivSentence φ

Tactic:
letI := (L.lhomWithConstants α).reduct M

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
⊢ ↑M ⊨ Formula.equivSentence φ

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝¹ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this✝ : (L.lhomWithConstants α).IsExpansionOn ↑M
this : ↑M ⊨ T
M' : T.ModelType := ModelType.of T ↑M
⊢ φ.Realize fun a => ↑(L.con a)

Tactic:
exact h M' (fun a => (L.con a : M)) _

Result:
no goals

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : (L.lhomWithConstants α).IsExpansionOn ↑M
⊢ φ.Realize fun a => ↑(L.con a)

Tactic:
have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝¹ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this✝ : (L.lhomWithConstants α).IsExpansionOn ↑M
this : ↑M ⊨ T
⊢ φ.Realize fun a => ↑(L.con a)

Proof state:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
⊢ φ.Realize v

Tactic:
letI : (constantsOn α).Structure M := constantsOn.structure v

Result:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
this : (constantsOn α).Structure ↑M := constantsOn.structure v
⊢ φ.Realize v

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : (L.lhomWithConstants α).IsExpansionOn ↑M
⊢ ↑M ⊨ Formula.equivSentence φ

Tactic:
rw [Formula.realize_equivSentence]

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
this✝ : L.Structure ↑M := (L.lhomWithConstants α).reduct ↑M
this : (L.lhomWithConstants α).IsExpansionOn ↑M
⊢ φ.Realize fun a => ↑(L.con a)

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
⊢ T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ

Tactic:
refine ⟨fun h => models_sentence_iff.2 (fun M => ?_),
  fun h => models_formula_iff.2 (fun M v => ?_)⟩

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
⊢ ↑M ⊨ Formula.equivSentence φ

case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
⊢ φ.Realize v