-- Mathlib/ModelTheory/Semantics.lean
theorem realize_equivSentence_symm_con [L[[α]].Structure M]
    [(L.lhomWithConstants α).IsExpansionOn M] (φ : L[[α]].Sentence) :
    ((equivSentence.symm φ).Realize fun a => (L.con a : M)) ↔ φ.Realize M

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔ M ⊨ φ

Tactic:
refine _root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default

Proof state:
case e__v.h.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
val✝ : α
⊢ ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inl val✝) =
    Sum.elim (fun a => ↑(L.con a)) default (Sum.inl val✝)

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default =
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default

Tactic:
congr with (_ | a)

Result:
case e__v.h.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
val✝ : α
⊢ ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inl val✝) =
    Sum.elim (fun a => ↑(L.con a)) default (Sum.inl val✝)

case e__v.h.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
a : Empty
⊢ ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inr a) = Sum.elim (fun a => ↑(L.con a)) default (Sum.inr a)

Proof state:
case e__v.h.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
a : Empty
⊢ ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) (Sum.inr a) = Sum.elim (fun a => ↑(L.con a)) default (Sum.inr a)

Tactic:
cases a

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default

Tactic:
rw [iff_iff_eq]

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default =
    (BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun a => ↑(L.con a)) default) default

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ ((equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ M ⊨ φ

Tactic:
simp only [equivSentence, _root_.Equiv.symm_symm, Equiv.coe_trans, Realize,
  BoundedFormula.realize_relabelEquiv, Function.comp]

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ (BoundedFormula.constantsVarsEquiv φ).Realize ((fun a => ↑(L.con a)) ∘ ⇑(Equiv.sumEmpty α Empty)) default ↔ M ⊨ φ