awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
⊢ 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))
have 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
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]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
⊢ M ⊨ BoundedFormula.alls (((L.lhomWithConstants M).onBoundedFormula φ).subst (Constants.term ∘ Sum.inr ∘ x)) ↔
    φ.Realize x
have 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
Tactic: simp_rw [Sentence.Realize, BoundedFormula.realize_alls, BoundedFormula.realize_subst,
        LHom.realize_onBoundedFormula, Formula.Realize, Unique.forall_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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.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
have 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
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)
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
have refine_1 : ∀ (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: refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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))
refine_1 :
  ∀ (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
⊢ ∀ (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
have refine_2 : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → 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: refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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))
refine_1 :
  ∀ (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
refine_2 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → 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
⊢ ∀ (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
have refine_3 : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n))
  (xs : Fin n → 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: refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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))
refine_1 :
  ∀ (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
refine_2 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (t₁ t₂ : L.Term (Empty ⊕ Fin n)) (xs : Fin n → 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
refine_3 :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (Empty ⊕ Fin n))
    (xs : Fin n → 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
⊢ ∀ (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
have refine_4 : ∀ (n : ℕ) (φ : L.BoundedFormula Empty n) {n : ℕ} (f₁ f₂ : L.BoundedFormula Empty n)
  (f₁_ih :
    ∀ (xs : Fin n → 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 → 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 → 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: refine fun n φ => φ.recOn ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
⊢ 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
have 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)
Tactic: simp only [BoundedFormula.Realize, ← Sum.comp_elim, HomClass.realize_term]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
⊢ (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)
have 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
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))]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
⊢ (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
have 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
Tactic: rw [Function.comp_assoc, map_rel f]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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
have 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
Tactic: rw [Function.comp_assoc, map_rel f]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → 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
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
have refine_5 : (∀ (a : N),
    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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
  ∀ (a : M),
    BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
Tactic: simp only [BoundedFormula.realize_all]
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → 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
xs : Fin n → M
⊢ (∀ (a : N),
      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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
    ∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have refine_5 : ∀
  (h :
    ∀ (a : N),
      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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a))
  (a : M), BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
Tactic: refine ⟨fun h a => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.ElementaryMaps (goal)
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_1 : ℕ
φ_1 : L.BoundedFormula Empty n_1
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih :
  ∀ (xs : Fin (n + 1) → 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
xs : Fin n → M
refine_5 :
  ∀
    (h :
      ∀ (a : N),
        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)
          (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a))
    (a : M),
    BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
⊢ (∀ (a : N),
      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)
        (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) ↔
    ∀ (a : M),
      BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)
have refine_5₁ : (∀ (a : M),
    BoundedFormula.Realize.{u_5, u_6, u_1, 0} (M := M) φ default (Fin.snoc (α := fun (a : Fin n.succ) ↦ M) xs a)) →
  ∀ (a : N),
    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)
      (Fin.snoc (α := fun (a : Fin n.succ) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
Tactic: refine ⟨fun h a => ?_, ?_⟩