awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
f : presburger.Functions l
k : Fin l → ℕ
u : Fin l → α → ℕ
ih : ∀ (a : Fin l) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
func :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α) (k : Fin 0 → ℕ) (u : Fin 0 → α → ℕ)
    (ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
func₁ :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α) (k : Fin 0 → ℕ) (u : Fin 0 → α → ℕ)
    (ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
have func₂ : ∀ (ts : Fin 2 → presburger[[(↑A : Type)]].Term α) (k : Fin 2 → ℕ) (u : Fin 2 → α → ℕ)
  (ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
  ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v
Tactic: cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
Cleared hypotheses: l, ts, f, k, u, ih
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
have func : ∀ (v : α → ℕ),
  (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
    (↑f : ℕ) + 0 ⬝ᵥ v
Tactic: refine ⟨f, 0, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
v : α → ℕ
⊢ (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
    (↑f : ℕ) + 0 ⬝ᵥ v
have func : Eq (α := ℕ) (↑(presburger.con f) : ℕ) (↑f : ℕ)
Tactic: rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions l
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inr f) fun (i : Fin l) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
have func : ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v)
  (f : (constantsOn (↑A : Type)).Functions 0),
  ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
Tactic: cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: l, ts, ih, f
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions l
func :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v)
    (f : (constantsOn (↑A : Type)).Functions 0),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inr f) fun (i : Fin l) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
have func₁ : ∀ (n : ℕ) (ts : Fin (n + 1) → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin (n + 1)), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v)
  (f : (constantsOn (↑A : Type)).Functions (n + 1)),
  ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := n + 1) (Sum.inr f) fun (i : Fin (n + 1)) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v
Tactic: cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: l, ts, ih, f
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
f : presburger[[(↑A : Type)]].Functions l
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
have func : ∀ (f : presburger.Functions l),
  ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
Tactic: cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
f : presburger[[(↑A : Type)]].Functions l
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
func :
  ∀ (f : presburger.Functions l),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
have func₁ : ∀ (f : (constantsOn (↑A : Type)).Functions l),
  ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inr f) fun (i : Fin l) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v
Tactic: cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have var : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (var i) = k + u ⬝ᵥ v
Tactic: induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
Tactic: induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have func : ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
  ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (func f ts) = k + u ⬝ᵥ v
Tactic: induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
func :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (Language.func f ts) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have func₁ : ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
  ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
Tactic: induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have var : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (var i) = k + u ⬝ᵥ v
Tactic: classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
Tactic: classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have func : ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
  ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (func f ts) = k + u ⬝ᵥ v
Tactic: classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
func :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (Language.func f ts) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v
have func₁ : ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
  (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
  ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
Tactic: classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
⊢ IsSemilinearSet (M := α → ℕ) (setOf φ.Realize)
have h : Eq (α := Set (α → ℕ)) (setOf φ.Realize)
  (image (α := α ⊕ Fin 0 → ℕ) (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
    {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
Tactic: convert! (isSemilinearSet_boundedFormula_realize φ).image (LinearMap.funLeft ℕ ℕ e.symm)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
⊢ Eq (α := Set (α → ℕ)) (setOf φ.Realize)
    (image (α := α ⊕ Fin 0 → ℕ) (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
      {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
have h : ∀ (x : α → ℕ),
  Membership.mem (γ := Set (α → ℕ)) (setOf φ.Realize) x ↔
    Membership.mem (γ := Set (α → ℕ))
      (image (α := α ⊕ Fin 0 → ℕ)
        (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
        {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ Membership.mem (γ := Set (α → ℕ)) (setOf φ.Realize) x ↔
    Membership.mem (γ := Set (α → ℕ))
      (image (α := α ⊕ Fin 0 → ℕ)
        (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
        {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
      x
have h : φ.Realize x ↔
  ∃ (x_1 : α ⊕ Fin 0 → ℕ),
    BoundedFormula.Realize φ (x_1 ∘ Sum.inl) (x_1 ∘ Sum.inr) ∧
      (LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ) x_1 = x
Tactic: simp only [mem_setOf_eq, mem_image]