awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
P : Type u_3
Q : Type u_4
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
inst_3 : L.Structure Q
f : M ↪ₑ[L] N
A : Set M
n : ℕ
φ : (withConstants.{u_5, u_6, u_1} L (↑A : Type u_1)).Formula (Fin n)
x : Fin n → M
h :
  Eq (α := (↑A : Type u_1) ⊕ Fin n → f.toEmbedding.withConstants A)
    (Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : f.toEmbedding.withConstants A)) ((⇑f : (a : M) → N) ∘ x))
    ((⇑f : (a : M) → N) ∘ Sum.elim (fun (a : (↑A : Type u_1)) ↦ (↑(L.con a) : M)) x)
⊢ φ.Realize (M := f.toEmbedding.withConstants A) ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x

Tactic:
simpa only [Formula.Realize, ← BoundedFormula.realize_constantsVarsEquiv, h] using
    f.map_formula
      (BoundedFormula.constantsVarsEquiv φ)
      (Sum.elim (fun a ↦ ↑(L.con a)) x)

Premises used: FirstOrder.Language.BoundedFormula.constantsVarsEquiv, FirstOrder.Language.con, FirstOrder.Language.constantMap, FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv, FirstOrder.Language.ElementaryEmbedding.map_formula, DFunLike.coe, FirstOrder.Language.Formula.Realize, Sum.elim
-- 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
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    φ.Realize x

Tactic:
_root_.trans ?_
        ((realize_iff_of_model_completeTheory M N
              (((L.lhomWithConstants M).onBoundedFormula φ).subst
                  (Constants.term ∘ Sum.inr ∘ x)).alls).trans
          ?_)

Premises used: FirstOrder.Language.BoundedFormula.alls, trans, FirstOrder.Language.Constants.term, Function.comp, FirstOrder.Language.realize_iff_of_model_completeTheory, FirstOrder.Language.BoundedFormula.subst, Sum.inr, Iff.trans, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.LHom.onBoundedFormula
-- 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) ↔
    N ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x))
refine_2 :
  M ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) ↔
    φ.Realize x
⊢ Formula.Realize.{u_6, u_7, u_5, 0} (M := N) φ (Function.comp (β := L[[M]].Constants) constantMap Sum.inr ∘ x) ↔
    φ.Realize x

Tactic:
refine
      _root_.trans ?_
        ((realize_iff_of_model_completeTheory M N
              (((L.lhomWithConstants M).onBoundedFormula φ).subst
                  (Constants.term ∘ Sum.inr ∘ x)).alls).trans
          ?_)

Premises used: FirstOrder.Language.BoundedFormula.alls, trans, FirstOrder.Language.Constants.term, Function.comp, FirstOrder.Language.realize_iff_of_model_completeTheory, FirstOrder.Language.BoundedFormula.subst, Sum.inr, Iff.trans, FirstOrder.Language.lhomWithConstants, FirstOrder.Language.LHom.onBoundedFormula
-- 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_2 :
  BoundedFormula.Realize.{u_6, u_7, u_1, 0} (M := M) φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default
⊢ M ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) ↔
    φ.Realize x

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

Premises used: FirstOrder.Language.LHom.realize_onBoundedFormula, FirstOrder.Language.Sentence.Realize, Unique.forall_iff, FirstOrder.Language.BoundedFormula.realize_subst, FirstOrder.Language.BoundedFormula.realize_alls, FirstOrder.Language.Formula.Realize
-- 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
⊢ BoundedFormula.Realize.{u_6, u_7, u_1, 0} (M := M) φ
      (fun (a : Fin n) ↦ Term.realize (L := L[[M]]) (α := Empty) default ((Constants.term ∘ Sum.inr ∘ x) a)) default ↔
    BoundedFormula.Realize φ x default

Tactic:
rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
h :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x

Tactic:
φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)

Premises used: trans, FirstOrder.Language.Formula.realize_relabel_sumInr, Iff.trans, Iff.symm
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
h :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x

Tactic:
exact φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)

Premises used: trans, FirstOrder.Language.Formula.realize_relabel_sumInr, Iff.trans, Iff.symm
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
suffices :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs
⊢ ∀ {n : ℕ} (φ : L.Formula (Fin n)) (x : Fin n → M),
    Formula.Realize.{u_5, u_6, u_2, 0} (M := N) φ ((⇑f : (a : M) → N) ∘ x) ↔ φ.Realize x

Tactic:
suffices h : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
      φ.Realize (f ∘ default) (f ∘ xs) ↔ φ.Realize default xs by
    intro n φ x
    exact φ.realize_relabel_sumInr.symm.trans (_root_.trans (h n _ _) φ.realize_relabel_sumInr)
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
⊢ ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      φ.Realize default xs

Tactic:
fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_

Premises used: FirstOrder.Language.BoundedFormula.recOn
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (L := L) (M := N) (α := Empty) BoundedFormula.falsum
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (L := L) (α := Empty) BoundedFormula.falsum default xs

Tactic:
fun {_} _ => Iff.rfl

Premises used: isEmptyElim, False.elim, Iff.rfl, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
⊢ ∀ {n : ℕ} (xs : Fin n → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (L := L) (M := N) (α := Empty) BoundedFormula.falsum
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (L := L) (α := Empty) BoundedFormula.falsum default xs

Tactic:
exact fun {_} _ => Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
t₁ t₂ : L.Term (Empty ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.equal t₁ t₂)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
    (BoundedFormula.equal t₁ t₂).Realize default xs

Tactic:
simp [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]

Premises used: FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.HomClass.realize_term, Sum.comp_elim
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
refine_3 :
  ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n_1)) (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.rel R ts)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.rel R ts).Realize default xs
⊢ ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n_1)) (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.rel R ts)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (BoundedFormula.rel R ts).Realize default xs

Tactic:
_
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 l : ℕ
R : L.Relations l
ts : Fin l → L.Term (Empty ⊕ Fin n_1)
xs : Fin n_1 → M
refine_3 :
  (RelMap.{u_5, u_6, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim default xs) (ts i))) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim default xs) (ts i)
⊢ BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (BoundedFormula.rel R ts)
      (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
    (BoundedFormula.rel R ts).Realize default xs

Tactic:
simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]

Premises used: FirstOrder.Language.BoundedFormula.Realize, FirstOrder.Language.HomClass.realize_term, Sum.comp_elim
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 l : ℕ
R : L.Relations l
ts : Fin l → L.Term (Empty ⊕ Fin n_1)
xs : Fin n_1 → M
refine_3 :
  (RelMap.{u_5, u_6, u_2} (M := N) R fun (i : Fin l) ↦
      (((⇑f : (a : M) → N) ∘ Term.realize (Sum.elim default xs)) ∘ ts) i) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ (Term.realize (Sum.elim default xs) ∘ ts) i
⊢ (RelMap.{u_5, u_6, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim default xs) (ts i))) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim default xs) (ts i)

Tactic:
simp_rw [← Function.comp_apply (f := (f : M → N)),
      ← Function.comp_apply (f := Term.realize (Sum.elim default xs)),
      ← Function.comp_apply (f := (f : M → N) ∘ Term.realize (Sum.elim default xs))]

Premises used: Function.comp_apply
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 l : ℕ
R : L.Relations l
ts : Fin l → L.Term (Empty ⊕ Fin n_1)
xs : Fin n_1 → M
refine_3 :
  (RelMap.{u_5, u_6, u_2} (M := N) R fun (i : Fin l) ↦
      ((⇑f : (a : M) → N) ∘ Term.realize (Sum.elim default xs) ∘ ts) i) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ (Term.realize (Sum.elim default xs) ∘ ts) i
refine_3₁ refine_3₂ :
  RelMap R (Term.realize (Sum.elim default xs) ∘ ts) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ (Term.realize (Sum.elim default xs) ∘ ts) i
⊢ (RelMap.{u_5, u_6, u_2} (M := N) R fun (i : Fin l) ↦
      (((⇑f : (a : M) → N) ∘ Term.realize (Sum.elim default xs)) ∘ ts) i) ↔
    RelMap.{u_5, u_6, u_1} (M := M) R fun (i : Fin l) ↦ (Term.realize (Sum.elim default xs) ∘ ts) i

Tactic:
rw [Function.comp_assoc, map_rel f]

Premises used: FirstOrder.Language.Embedding.map_rel, Function.comp_assoc
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
refine_4 :
  ∀ (f₁ f₂ : L.BoundedFormula Empty n_1)
    (f₁_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₁.Realize default xs)
    (f₂_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₂.Realize default xs)
    (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs
⊢ ∀ (f₁ f₂ : L.BoundedFormula Empty n_1)
    (f₁_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₁.Realize default xs)
    (f₂_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₂.Realize default xs)
    (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs

Tactic:
_
-- Module: Mathlib.ModelTheory.ElementaryMaps
Goal:
L : Language
M : Type u_1
N : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
        (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) a) →
      ∃ (b : M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) φ default
          (Fin.snoc (α := fun (a : Fin (n + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ x) ((f : (a : M) → N) b))
n : ℕ
φ : L.BoundedFormula Empty n
n_1 : ℕ
f₁ : L.BoundedFormula Empty n_1
refine_4 :
  ∀ (f₂ : L.BoundedFormula Empty n_1)
    (f₁_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₁.Realize default xs)
    (f₂_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₂.Realize default xs)
    (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs
⊢ ∀ (f₂ : L.BoundedFormula Empty n_1)
    (f₁_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₁
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₁.Realize default xs)
    (f₂_ih :
      ∀ (xs : Fin n_1 → M),
        BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) f₂
            (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
          f₂.Realize default xs)
    (xs : Fin n_1 → M),
    BoundedFormula.Realize.{u_5, u_6, u_2, 0} (M := N) (f₁ ⟹ f₂)
        (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) default) ((⇑f : (a : M) → N) ∘ xs) ↔
      (f₁ ⟹ f₂).Realize default xs

Tactic:
_