-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N_1 : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N_1
inst_2 : L.Structure P
inst_3 : L.Structure Q
N : Type u_5
inst_4 : L.Structure N
inst_5 : L[[M]].Structure N
inst_6 : (L.lhomWithConstants M).IsExpansionOn N
inst_7 : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
refine_1 :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    Formula.Realize (M := N) (α := Empty)
      (BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))) default
refine_1₁ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize (α := Empty)
        (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) default xs
refine_1₂ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₃ :
  Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize φ
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₄ :
  BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x)
      default ↔
    ∀ (xs : Fin 0 → N),
      BoundedFormula.Realize φ
        (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
refine_1₅ :
  BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x)
      default ↔
    BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) default
refine_1₆ :
  BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (fun (x_1 : Fin n) ↦ (↑(Sum.inr (x x_1)) : N)) default ↔
    BoundedFormula.Realize.{u_6, u_7, u_5, 0} (M := N) φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default (Constants.term (Sum.inr (x a)))) default
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))

Tactic:
simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff, Function.comp_def,
        Term.realize_constants]

Premises used: FirstOrder.Language.LHom.realize_onBoundedFormula, FirstOrder.Language.Sentence.Realize, Unique.forall_iff, FirstOrder.Language.BoundedFormula.realize_subst, FirstOrder.Language.Term.realize_constants, Function.comp_def, FirstOrder.Language.BoundedFormula.realize_alls, FirstOrder.Language.Formula.Realize