awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
φ : L.BoundedFormula α n
hA : φ.IsAtomic
inst_3 : L.HomClass F M N
f : F
hInj : Function.Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
v : α → M
xs : Fin n → M
equal :
  ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    (t₁ =' t₂).Realize v xs →
      Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
have rel : ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  (R.boundedFormula ts).Realize v xs →
    Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
Tactic: induction hA with
  | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term, hInj.eq_iff,
    imp_self]
  | rel R ts =>
    simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
    exact HomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)
⊢ Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    (R.boundedFormula ts).Realize v xs
have of_isAtomic : (RelMap.{u, v, u_2} (M := N) R fun (i : Fin l) ↦ (f : (a : M) → N) (Term.realize (Sum.elim v xs) (ts i))) ↔
  RelMap.{u, v, u_1} (M := M) R fun (i : Fin l) ↦ Term.realize (Sum.elim v xs) (ts i)
Tactic: simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
hA : φ_1.IsAtomic
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ_1.Realize v xs
have of_isAtomic : ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
  Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    (t₁ =' t₂).Realize v xs
Tactic: induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
xs : Fin n → M
φ_1 : L.BoundedFormula α n
hA : φ_1.IsAtomic
of_isAtomic :
  ∀ (t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n)),
    Realize.{u, v, u_2, u'} (M := N) (t₁ =' t₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
      (t₁ =' t₂).Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ_1.Realize v xs
have of_isAtomic₁ : ∀ {l : ℕ} (R : L.Relations l) (ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n)),
  Realize.{u, v, u_2, u'} (M := N) (R.boundedFormula ts) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    (R.boundedFormula ts).Realize v xs
Tactic: induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have falsum : Realize.{u, v, u_2, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
  Realize.{u, v, u_1, u'} (L := L) BoundedFormula.falsum v xs
Tactic: induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]
Cleared hypotheses: hQF
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
falsum :
  Realize.{u, v, u_2, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    Realize.{u, v, u_1, u'} (L := L) BoundedFormula.falsum v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have of_isAtomic : ∀ {φ : L.BoundedFormula α n} (hA : φ.IsAtomic),
  Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
Tactic: induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]
Cleared hypotheses: hQF
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
falsum :
  Realize.{u, v, u_2, u'} (L := L) (M := N) BoundedFormula.falsum ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
    Realize.{u, v, u_1, u'} (L := L) BoundedFormula.falsum v xs
of_isAtomic :
  ∀ {φ : L.BoundedFormula α n} (hA : φ.IsAtomic),
    Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ.Realize v xs
have imp : ∀ {φ₁ φ₂ : L.BoundedFormula α n},
  φ₁.IsQF →
    φ₂.IsQF →
      ∀ (ihφ : Realize.{u, v, u_2, u'} (M := N) φ₁ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₁.Realize v xs)
        (ihψ :
          Realize.{u, v, u_2, u'} (M := N) φ₂ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔ φ₂.Realize v xs),
        Realize.{u, v, u_2, u'} (M := N) (φ₁ ⟹ φ₂) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) ↔
          (φ₁ ⟹ φ₂).Realize v xs
Tactic: induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]
Cleared hypotheses: hQF
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
⊢ (∀ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)) →
    ∀ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
have all : ∀
  (h :
    ∀ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a))
  (a : M),
  Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))
Tactic: refine fun h a => ih ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h_1 : φ_1.IsUniversal
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ_1.Realize v xs
xs : Fin n_1 → M
h :
  ∀ (a : N),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
a : M
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))
have all : Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
  (snoc (α := fun (i : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
Tactic: rw [Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs
have of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
  Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs
Tactic: induction hU with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | all _ ih =>
    simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)
Cleared hypotheses: hU, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hU : φ.IsUniversal
f : F
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
    Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs
⊢ Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs
have all : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
  φ.IsUniversal →
    ∀
      (ih :
        ∀ {xs : Fin (n + 1) → M},
          Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → φ.Realize v xs)
      {xs : Fin n → M},
      Realize.{u, v, u_2, u'} (M := N) (∀' φ) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs) → (∀' φ).Realize v xs
Tactic: induction hU with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | all _ ih =>
    simp only [realize_all, Nat.succ_eq_add_one]
    refine fun h a => ih ?_
    rw [Fin.comp_snoc]
    exact h (f a)
Cleared hypotheses: hU, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
⊢ (∃' φ_1).Realize v xs → Realize.{u, v, u_2, u'} (M := N) (∃' φ_1) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
have ex : (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
  ∃ (a : N),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
Tactic: simp only [realize_ex, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
⊢ (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
    ∃ (a : N),
      Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
        (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) a)
have ex : (∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)) →
  ∀ (a : M) (ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)),
    Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
      (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
Tactic: refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
f : F
v : α → M
n_1 : ℕ
φ_1 : L.BoundedFormula α (n_1 + 1)
h : φ_1.IsExistential
ih :
  ∀ {xs : Fin (n_1 + 1) → M},
    φ_1.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
xs : Fin n_1 → M
h_1 : ∃ (a : M), φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
a : M
ha : φ_1.Realize v (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a)
⊢ Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
    (snoc (α := fun (a : Fin (n_1 + 1)) ↦ N) ((⇑f : (a : M) → N) ∘ xs) ((f : (a : M) → N) a))
have ex : Realize.{u, v, u_2, u'} (M := N) φ_1 ((⇑f : (a : M) → N) ∘ v)
  (Function.comp.{1, u_1 + 1, u_2 + 1} (β := M) (⇑f : (a : M) → N) (snoc (α := fun (a : Fin (n_1 + 1)) ↦ M) xs a))
Tactic: rw [← Fin.comp_snoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hE : φ.IsExistential
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
have of_isQF : ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
  φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
Tactic: induction hE with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | ex _ ih =>
    simp only [realize_ex, Nat.succ_eq_add_one]
    refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
    rw [← Fin.comp_snoc]
    exact ih ha
Cleared hypotheses: hE, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
α : Type u'
n : ℕ
M : Type u_1
inst : L.Structure M
N : Type u_2
inst_1 : L.Structure N
F : Type u_3
inst_2 : FunLike F M N
inst_3 : EmbeddingLike F M N
inst_4 : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hE : φ.IsExistential
f : F
v : α → M
xs : Fin n → M
of_isQF :
  ∀ {n : ℕ} {φ : L.BoundedFormula α n} (hQF : φ.IsQF) {xs : Fin n → M},
    φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
⊢ φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
have ex : ∀ {n : ℕ} {φ : L.BoundedFormula α (n + 1)},
  φ.IsExistential →
    ∀
      (ih :
        ∀ {xs : Fin (n + 1) → M},
          φ.Realize v xs → Realize.{u, v, u_2, u'} (M := N) φ ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs))
      {xs : Fin n → M},
      (∃' φ).Realize v xs → Realize.{u, v, u_2, u'} (M := N) (∃' φ) ((⇑f : (a : M) → N) ∘ v) ((⇑f : (a : M) → N) ∘ xs)
Tactic: induction hE with
  | of_isQF hQF => simp [hQF.realize_embedding]
  | ex _ ih =>
    simp only [realize_ex, Nat.succ_eq_add_one]
    refine fun ⟨a, ha⟩ => ⟨f a, ?_⟩
    rw [← Fin.comp_snoc]
    exact ih ha
Cleared hypotheses: hE, xs
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
⊢ M ⊨ T
have simp : ∀ φ ∈ T, M ⊨ φ
Tactic: simp only [model_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
⊢ ∀ φ ∈ T, M ⊨ φ
have refine : ∀ (φ : L.Sentence) (hφ : φ ∈ T),
  BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
Tactic: refine fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst_1 : L.Structure N
inst_2 : N ⊨ T
f : M ↪[L] N
φ : L.Sentence
hφ : φ ∈ T
⊢ BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑f : (a : M) → N) default)
have rw : BoundedFormula.Realize.{u, v, u_1, 0} (M := N) φ default default
Tactic: rw [Subsingleton.elim (f ∘ default) default, Subsingleton.elim (f ∘ default) default]
-- Lean 4 proof step from Mathlib.ModelTheory.Complexity (goal)
Goal:
L : Language
T : L.Theory
hT : T.IsUniversal
φ : L.Sentence
hφ : BoundedFormula.IsUniversal φ
⊢ ∀ ⦃φ_1 : L.Sentence⦄, φ_1 ∈ Insert.insert φ T → BoundedFormula.IsUniversal φ_1
have simp : ∀ a ∈ T, BoundedFormula.IsUniversal a
Tactic: simp only [Set.mem_insert_iff, forall_eq_or_imp, hφ, true_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
L' : Language
inst_1 : L'.Structure M
h : A.Definable L s
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
⊢ A.Definable L' s
have obtain : ∀ (ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α), A.Definable L' (setOf ψ.Realize)
Tactic: obtain ⟨ψ, rfl⟩ := h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ A.Definable L' (setOf ψ.Realize)
have refine : Eq (α := Set (α → M)) (setOf ψ.Realize) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize)
Tactic: refine ⟨(φ.addConstants A).onFormula ψ, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
L' : Language
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : (withConstants.{u, v, w} L (↑A : Type w)).Formula α
⊢ Eq (α := Set (α → M)) (setOf ψ.Realize) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize)
have h : ∀ (x : α → M),
  Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf (LHom.onFormula (LHom.addConstants (↑A : Type w) φ) ψ).Realize) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ A.Definable L s ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
have rw : (∃ (b : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
    s =
      setOf
        (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
          ((Equiv.symm BoundedFormula.constantsVarsEquiv :
              (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
            b))) ↔
  ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
    s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
Tactic: rw [Definable, Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)]
-- Lean 4 proof step from Mathlib.ModelTheory.Definability (goal)
Goal:
M : Type w
A : Set M
L : Language
inst : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ (b : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
      s =
        setOf
          (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
            ((Equiv.symm BoundedFormula.constantsVarsEquiv :
                (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
              b))) ↔
    ∃ (φ : L.Formula (Sum.{w, u₁} (↑A : Type w) α)),
      s = {v : α → M | φ.Realize (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
have refine : ∀ (φ : L.BoundedFormula (Sum.{w, u₁} (↑A : Type w) α) 0),
  Eq (α := Set (α → M))
    (setOf
      (Formula.Realize (L := withConstants.{u, v, w} L (↑A : Type w))
        ((Equiv.symm BoundedFormula.constantsVarsEquiv :
            (a : L.BoundedFormula ((↑A : Type w) ⊕ α) 0) → L[[(↑A : Type w)]].BoundedFormula α 0)
          φ)))
    {v : α → M | Formula.Realize φ (Sum.elim (Subtype.val (p := fun (x : M) ↦ x ∈ A)) v)}
Tactic: refine exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = ·) ?_))