awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Algebra.Ring.FreeCommRing (goal)
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of
        (Classical.choose (p := fun (x : ring.Term α) ↦ Term.realize FreeCommRing.of x = p) ⋯))
have induction : ∀ (x : ring.Term α),
  Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      (Term.realize FreeCommRing.of x)
Tactic: induction Classical.choose (exists_term_realize_eq_freeCommRing p) with
  | var _ => simp
  | func f a ih =>
    cases f <;>
    simp [ih]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
⊢ Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M)
have zero : Term.realize (L := presburger) v (↑0 : presburger.Term α) = (↑0 : M)
Tactic: induction n with simp [*]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
zero : Term.realize (L := presburger) v (↑0 : presburger.Term α) = (↑0 : M)
⊢ Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M)
have succ : ∀ (n : ℕ),
  Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M) →
    Term.realize (L := presburger) v (↑(n + 1) : presburger.Term α) = (↑(n + 1) : M)
Tactic: induction n with simp [*]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
t : presburger.Term α
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
⊢ Term.realize v (n • t) = n • Term.realize v t
have zero : Term.realize v (HSMul.hSMul (α := ℕ) 0 t) = HSMul.hSMul (α := ℕ) 0 (Term.realize v t)
Tactic: induction n with simp [*, add_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
t : presburger.Term α
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
zero : Term.realize v (HSMul.hSMul (α := ℕ) 0 t) = HSMul.hSMul (α := ℕ) 0 (Term.realize v t)
⊢ Term.realize v (n • t) = n • Term.realize v t
have succ : ∀ (n : ℕ), Term.realize v (n • t) = n • Term.realize v t → Term.realize v ((n + 1) • t) = (n + 1) • Term.realize v t
Tactic: induction n with simp [*, add_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
have rhs : ∑ i ∈ s, Term.realize v (f i)
Tactic: rhs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| ∑ i ∈ s, Term.realize v (f i)
have rw : List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
Tactic: rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
have rw : List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
Tactic: rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
⊢ Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
have conv : Term.realize v (List.map f s.toList).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
Tactic: conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
⊢ Term.realize v (List.map f s.toList).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
have generalize : ∀ (l : List β), Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
Tactic: generalize s.toList = l
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
l : List β
⊢ Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
have nil : Term.realize v (List.map f []).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) [])
Tactic: induction l with simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
l : List β
nil : Term.realize v (List.map f []).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) [])
⊢ Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
have cons : ∀ (head : β) (tail : List β),
  Term.realize v (List.map f tail).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) tail) →
    Term.realize v (List.map f (head :: tail)).sum =
      List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) (head :: tail))
Tactic: induction l with simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
⊢ Term.realize v (sum s f) = ∑ i ∈ s, Term.realize v (f i)
have simp : Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
Tactic: classical
  simp only [sum]
  conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
  generalize s.toList = l
  induction l with simp [*]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
simp : Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
⊢ Term.realize v (sum s f) = ∑ i ∈ s, Term.realize v (f i)
have simp₁ : Term.realize v (List.map f s.toList).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
Tactic: classical
  simp only [sum]
  conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
  generalize s.toList = l
  induction l with simp [*]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Basic (goal)
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
simp : Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)
simp₁ : Term.realize v (List.map f s.toList).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
⊢ Term.realize v (sum s f) = ∑ i ∈ s, Term.realize v (f i)
have simp₂ : ∀ (l : List β), Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
Tactic: classical
  simp only [sum]
  conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]
  generalize s.toList = l
  induction l with simp [*]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : IsLinearSet s
⊢ A.Definable presburger s
have hs₁ : ∃ (a : α → ℕ) (t : Finset (α → ℕ)), s = a +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ))
Tactic: rw [isLinearSet_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : ∃ (a : α → ℕ) (t : Finset (α → ℕ)), s = a +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ))
⊢ A.Definable presburger s
have rcases : ∀ (v : α → ℕ) (t : Finset (α → ℕ)),
  A.Definable presburger (v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)))
Tactic: rcases hs with ⟨v, t, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
⊢ A.Definable presburger (v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)))
have refine : v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) =
  setOf
    (Formula.Realize (L := presburger[[(↑A : Type)]])
      (Formula.iExs (↥t)
        (Formula.iInf fun (i : α) ↦
          Term.equal (var (Sum.inl i))
            (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                (presburger.sum Finset.univ fun (x : ↥t) ↦
                  HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                    (var (Sum.inr (Sum.inr x))))).varsToConstants)))
Tactic: refine ⟨Formula.iExs t (Formula.iInf fun i : α =>
    (Term.var (Sum.inl i)).equal
      (Term.varsToConstants
        ((v i : presburger.Term _) + presburger.sum Finset.univ fun x : t =>
          x.1 i • Term.var (Sum.inr (Sum.inr x))))), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
⊢ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) =
    setOf
      (Formula.Realize (L := presburger[[(↑A : Type)]])
        (Formula.iExs (↥t)
          (Formula.iInf fun (i : α) ↦
            Term.equal (var (Sum.inl i))
              (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                  (presburger.sum Finset.univ fun (x : ↥t) ↦
                    HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                      (var (Sum.inr (Sum.inr x))))).varsToConstants)))
have h : ∀ (x : α → ℕ),
  x ∈ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) ↔
    Membership.mem (γ := Set (α → ℕ))
      (setOf
        (Formula.Realize (L := presburger[[(↑A : Type)]])
          (Formula.iExs (↥t)
            (Formula.iInf fun (i : α) ↦
              Term.equal (var (Sum.inl i))
                (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (presburger.sum Finset.univ fun (x : ↥t) ↦
                      HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                        (var (Sum.inr (Sum.inr x))))).varsToConstants))))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
⊢ x ∈ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) ↔
    Membership.mem (γ := Set (α → ℕ))
      (setOf
        (Formula.Realize (L := presburger[[(↑A : Type)]])
          (Formula.iExs (↥t)
            (Formula.iInf fun (i : α) ↦
              Term.equal (var (Sum.inl i))
                (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (presburger.sum Finset.univ fun (x : ↥t) ↦
                      HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                        (var (Sum.inr (Sum.inr x))))).varsToConstants))))
      x
have h : (∃ (a : ↥t → ℕ), v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x) ↔
  ∃ (i : ↥t → ℕ), ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * i x
Tactic: simp only [mem_vadd_set, SetLike.mem_coe, AddSubmonoid.mem_closure_finset', Finset.univ_eq_attach,
    nsmul_eq_mul, vadd_eq_add, ↓existsAndEq, true_and, mem_setOf_eq, Formula.realize_iExs,
    Formula.realize_iInf, Formula.realize_equal, Term.realize_var, Sum.elim_inl,
    Term.realize_varsToConstants, coe_con, presburger.realize_add, presburger.realize_natCast,
    Nat.cast_id, presburger.realize_sum, presburger.realize_nsmul, Sum.elim_inr, smul_eq_mul]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
⊢ (∃ (a : ↥t → ℕ), v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x) ↔
    ∃ (i : ↥t → ℕ), ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * i x
have h : ∀ (a : ↥t → ℕ),
  v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x ↔ ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
Tactic: congr! with a
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
⊢ v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x ↔ ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
have h : (∀ (x_1 : α), x x_1 = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) x_1) ↔
  ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
Tactic: simp_rw [Eq.comm (b := x), fun x : t => mul_comm (a x : α → ℕ) x, funext_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
⊢ (∀ (x_1 : α), x x_1 = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) x_1) ↔
    ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
have h : ∀ (i : α),
  x i = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) i ↔
    x i = v i + ∑ x ∈ t.attach, (↑x : α → ℕ) i * a x
Tactic: congr! 1 with i
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : IsSemilinearSet s
⊢ A.Definable presburger s
have hs₁ : ∃ (S : Finset (Set (α → ℕ))), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set (α → ℕ)))
Tactic: rw [isSemilinearSet_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : ∃ (S : Finset (Set (α → ℕ))), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set (α → ℕ)))
⊢ A.Definable presburger s
have rcases : ∀ (S : Finset (Set (α → ℕ))) (hS : ∀ t ∈ S, IsLinearSet t), A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
Tactic: rcases hs with ⟨S, hS, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
⊢ A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
have choose : ∀ (φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α) (hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize),
  A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
Tactic: choose φ hφ using fun s : S => (hS s.1 s.2).definable
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
⊢ A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
have refine : ⋃₀ (↑S : Set (Set (α → ℕ))) = setOf (Formula.iSup φ).Realize
Tactic: refine ⟨Formula.iSup φ, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
⊢ ⋃₀ (↑S : Set (Set (α → ℕ))) = setOf (Formula.iSup φ).Realize
have h : ∀ (x : α → ℕ), x ∈ ⋃₀ (↑S : Set (Set (α → ℕ))) ↔ Membership.mem (γ := Set (α → ℕ)) (setOf (Formula.iSup φ).Realize) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
x : α → ℕ
⊢ x ∈ ⋃₀ (↑S : Set (Set (α → ℕ))) ↔ Membership.mem (γ := Set (α → ℕ)) (setOf (Formula.iSup φ).Realize) x
have this : ∀ (s : Set (α → ℕ)) (hs : s ∈ S) (x : α → ℕ),
  Membership.mem (γ := Set (α → ℕ)) (setOf (φ (Subtype.mk (p := fun (x : Set (α → ℕ)) ↦ x ∈ S) s hs)).Realize) x ↔
    x ∈ (↑(Subtype.mk (p := fun (x : Set (α → ℕ)) ↦ x ∈ S) s hs) : Set (α → ℕ))
Tactic: have := fun s hs x => Set.ext_iff.1 (hφ ⟨s, hs⟩).symm x
-- 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 : 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
have func : ∀ (k : Fin l → ℕ) (u : Fin l → α → ℕ) (ih : ∀ (a : Fin l) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ 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
Tactic: choose k u ih using ih
Cleared hypotheses: 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 α
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
have func : ∀ (v : α → ℕ),
  (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
      Term.realize v (ts i)) =
    0 + 0 ⬝ᵥ v
Tactic: refine ⟨0, 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 α
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
have func : ∀ (v : α → ℕ),
  (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
      Term.realize v (ts i)) =
    1 + 0 ⬝ᵥ v
Tactic: refine ⟨1, 0, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
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
have func : ∀ (v : α → ℕ),
  (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
      Term.realize v (ts i)) =
    k 0 + k 1 + (u 0 + u 1) ⬝ᵥ v
Tactic: refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
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
v : α → ℕ
⊢ (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
      Term.realize v (ts i)) =
    k 0 + k 1 + (u 0 + u 1) ⬝ᵥ v
have func : (Structure.funMap (L := presburger) (n := 2) presburgerFunc.add fun (i : Fin 2) ↦ Term.realize v (ts i)) =
  k 0 + u 0 ⬝ᵥ v + (k 1 + u 1 ⬝ᵥ v)
Tactic: rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
-- 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
⊢ ∃ (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 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
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 α
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
⊢ ∃ (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 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
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