awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
refine :
  Eq (α := Set (ι → K))
    {x : ι → K |
      ∀ p ∈ (↑S : Set (MvPolynomial ι K)), Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
    {v : ι → K |
      Formula.Realize (L := ring) (α :=
        Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)
        (BoundedFormula.iInf fun (i : ↥S) ↦
          Term.equal
            (Term.relabel
              (Sum.map
                (fun (p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ)))
                      x)
                    (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
                      (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
                    ⋯)
                id)
              (termOfFreeCommRing (p' i)))
            0)
        (Sum.elim
          (Subtype.val (p := fun (x : K) ↦
            Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
          v)}
⊢ ∃ (φ :
    ring.Formula
      (Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)),
    Eq (α := Set (ι → K))
      {x : ι → K |
        ∀ p ∈ (↑S : Set (MvPolynomial ι K)),
          Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
      {v : ι → K |
        φ.Realize
          (Sum.elim
            (Subtype.val (p := fun (x : K) ↦
              Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
            v)}

Tactic:
refine ⟨BoundedFormula.iInf
      (fun i : S => Term.equal
        ((termOfFreeCommRing (p' i)).relabel
          (Sum.map (fun p => ⟨p.1.1.coeff p.2.1, by
            simp only [Set.mem_iUnion]
            exact ⟨p.1.1, p.1.2, Set.mem_image_of_mem _ p.2.2⟩⟩) id)) 0), ?_⟩
-- Module: Mathlib.ModelTheory.Algebra.Ring.Definability
Goal:
ι : Type u_1
K : Type u_2
inst : Field K
inst_1 : CompatibleRing K
S : Finset (MvPolynomial ι K)
p' : ↥S → FreeCommRing ((i : ↥S) × ↥(↑i : MvPolynomial ι K).support ⊕ ι) :=
  genericPolyMap fun (p : ↥S) ↦ (↑p : MvPolynomial ι K).support
this_1 : DecidableEq ι := Classical.decEq ι
this : DecidableEq K := Classical.decEq K
⊢ Eq (α := Set (ι → K))
    {x : ι → K |
      ∀ p ∈ (↑S : Set (MvPolynomial ι K)), Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial ι K) → K) p : K) (0 : K)}
    {v : ι → K |
      Formula.Realize (L := ring) (α :=
        Sum.{u_2, u_1} (↑(⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) : Type u_2) ι)
        (BoundedFormula.iInf fun (i : ↥S) ↦
          Term.equal
            (Term.relabel
              (Sum.map
                (fun (p : (i : ↥S) × ↥(↑i : MvPolynomial ι K).support) ↦
                  Subtype.mk (p := fun (x : K) ↦
                    Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ)))
                      x)
                    (coeff (↑(p.snd (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : ι →₀ ℕ)
                      (↑(p.fst (β := fun (i : ↥S) ↦ ↥(↑i : MvPolynomial ι K).support)) : MvPolynomial ι K))
                    ⋯)
                id)
              (termOfFreeCommRing (p' i)))
            0)
        (Sum.elim
          (Subtype.val (p := fun (x : K) ↦
            Membership.mem (γ := Set K) (⋃ p ∈ S, (fun (m : ι →₀ ℕ) ↦ coeff m p) '' (↑p.support : Set (ι →₀ ℕ))) x))
          v)}

Tactic:
simp [Formula.Realize, Term.equal, Function.comp_def, p', MvPolynomial.aeval_eq_eval₂Hom]

Premises used: FirstOrder.Language.Term.equal, Function.comp_def, MvPolynomial.aeval_eq_eval₂Hom, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
p : FreeCommRing α
⊢ Eq.{u_1 + 1} (α := FreeCommRing α) (Term.realize (L := ring) FreeCommRing.of (-1)) (-1)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
p : FreeCommRing α
a : α
⊢ Term.realize (L := ring) FreeCommRing.of (var a) = FreeCommRing.of a

Tactic:
simp [Term.realize]

Premises used: FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
p x y : FreeCommRing α
h : ∃ (t : ring.Term α), Term.realize FreeCommRing.of t = x
h_1 : ∃ (t : ring.Term α), Term.realize FreeCommRing.of t = y
t₁ : ring.Term α
ht₁ : Term.realize FreeCommRing.of t₁ = x
t₂ : ring.Term α
ht₂ : Term.realize FreeCommRing.of t₂ = y
⊢ Term.realize FreeCommRing.of (t₁ + t₂) = x + y

Tactic:
simp_all
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
p x y : FreeCommRing α
h : ∃ (t : ring.Term α), Term.realize FreeCommRing.of t = x
h_1 : ∃ (t : ring.Term α), Term.realize FreeCommRing.of t = y
t₁ : ring.Term α
ht₁ : Term.realize FreeCommRing.of t₁ = x
t₂ : ring.Term α
ht₂ : Term.realize FreeCommRing.of t₂ = y
⊢ Term.realize FreeCommRing.of (t₁ * t₂) = x * y

Tactic:
simp_all
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
rw :
  ((((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) ⋯)) :
    R)
| ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      p :
    R)

Tactic:
rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]

Premises used: Classical.choose_spec, _private.0.FirstOrder.Ring.exists_term_realize_eq_freeCommRing
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
conv_rhs :
  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) ⋯))
⊢ Term.realize (L := ring) v (sorry p) =
    (((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
        (a : FreeCommRing α) → R)
      p

Tactic:
conv_rhs => rw [← Classical.choose_spec (exists_term_realize_eq_freeCommRing p)]

Premises used: Classical.choose_spec, _private.0.FirstOrder.Ring.exists_term_realize_eq_freeCommRing
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : α
var : Term.realize (L := ring) v (sorry p) = v a
⊢ 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 (L := ring) FreeCommRing.of (Language.var a))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih :
  ∀ (a_1 : Fin 2),
    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 (a a_1))
func :
  Term.realize (L := ring) v (sorry p) =
    HAdd.hAdd (α := R) (β := R)
      ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a 0)) :
        R)
      ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a 1)) :
        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 (Language.func ringFunc.add a))

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 2 → ring.Term α
ih :
  ∀ (a_1 : Fin 2),
    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 (a a_1))
func :
  Term.realize (L := ring) v (sorry p) =
    HMul.hMul (α := R) (β := R)
      ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a 0)) :
        R)
      ((((FreeCommRing.lift : (a : α → R) → FreeCommRing α →+* R) v : RingHom.{u_1, u_2} (FreeCommRing α) R) :
            (a : FreeCommRing α) → R)
          (Term.realize FreeCommRing.of (a 1)) :
        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 (Language.func ringFunc.mul a))

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 1 → ring.Term α
ih :
  ∀ (a_1 : Fin 1),
    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 (a a_1))
func :
  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 (a 0))
⊢ 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 (Language.func ringFunc.neg a))

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih :
  ∀ (a_1 : Fin 0),
    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 (a a_1))
func : Term.realize (L := ring) v (sorry p) = 0
⊢ 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 (Language.func ringFunc.zero a))

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
a : Fin 0 → ring.Term α
ih :
  ∀ (a_1 : Fin 0),
    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 (a a_1))
func : Term.realize (L := ring) v (sorry p) = 1
⊢ 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 (Language.func ringFunc.one a))

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
Goal:
α : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : CompatibleRing R
p : FreeCommRing α
v : α → R
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)
⊢ 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) ⋯))

Tactic:
induction Classical.choose (exists_term_realize_eq_freeCommRing p) with
  | var _ => simp
  | func f a ih =>
    cases f <;>
    simp [ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, _private.0.FirstOrder.Ring.exists_term_realize_eq_freeCommRing, Classical.choose
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := presburger.Term α) (↑0 : presburger.Term α) 0

Tactic:
rfl

Premises used: Nat.unaryCast, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
n : ℕ
⊢ (↑(n + 1) : presburger.Term α) = HAdd.hAdd (α := presburger.Term α) (↑n : presburger.Term α) 1

Tactic:
rfl

Premises used: Nat.unaryCast, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
t : presburger.Term α
⊢ HSMul.hSMul (α := ℕ) 0 t = 0

Tactic:
rfl

Premises used: FirstOrder.Language.Constants.term, nsmulRec, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
t : presburger.Term α
n : ℕ
⊢ (n + 1) • t = n • t + t

Tactic:
rfl

Premises used: nsmulRec, FirstOrder.Language.Functions.apply₂, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
M : Type u_2
inst : Zero M
inst_1 : One M
inst_2 : Add M
v : Fin 0 → M
⊢ Structure.funMap (L := presburger) presburgerFunc.zero v = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
M : Type u_2
inst : Zero M
inst_1 : One M
inst_2 : Add M
v : Fin 0 → M
⊢ Structure.funMap (L := presburger) presburgerFunc.one v = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
M : Type u_2
inst : Zero M
inst_1 : One M
inst_2 : Add M
v : Fin 2 → M
⊢ Structure.funMap (L := presburger) presburgerFunc.add v = v 0 + v 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : Zero M
inst_1 : One M
inst_2 : Add M
⊢ Term.realize (L := presburger) v 0 = 0

Tactic:
rfl

Premises used: FirstOrder.Language.Term.realize, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : Zero M
inst_1 : One M
inst_2 : Add M
⊢ Term.realize (L := presburger) v 1 = 1

Tactic:
rfl

Premises used: FirstOrder.Language.Term.realize, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
t₁ t₂ : presburger.Term α
M : Type u_2
v : α → M
inst : Zero M
inst_1 : One M
inst_2 : Add M
⊢ Term.realize v (t₁ + t₂) = Term.realize v t₁ + Term.realize v t₂

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, FirstOrder.Language.Term.realize, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
⊢ Term.realize (L := presburger) v (↑0 : presburger.Term α) = (↑0 : M)

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
h : Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M)
⊢ Term.realize (L := presburger) v (↑(n + 1) : presburger.Term α) = (↑(n + 1) : M)

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
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)
succ :
  ∀ (n : ℕ),
    Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M) →
      Term.realize (L := presburger) v (↑(n + 1) : presburger.Term α) = (↑(n + 1) : M)
⊢ Term.realize (L := presburger) v (↑n : presburger.Term α) = (↑n : M)

Tactic:
induction n with simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
t : presburger.Term α
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
⊢ Term.realize v (HSMul.hSMul (α := ℕ) 0 t) = HSMul.hSMul (α := ℕ) 0 (Term.realize v t)

Tactic:
simp [*, add_nsmul]

Premises used: add_nsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
t : presburger.Term α
M : Type u_2
v : α → M
inst : AddMonoidWithOne M
n : ℕ
h : Term.realize v (n • t) = n • Term.realize v t
⊢ Term.realize v ((n + 1) • t) = (n + 1) • Term.realize v t

Tactic:
simp [*, add_nsmul]

Premises used: add_nsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
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)
succ :
  ∀ (n : ℕ), Term.realize v (n • t) = n • Term.realize v t → Term.realize v ((n + 1) • t) = (n + 1) • Term.realize v t
⊢ Term.realize v (n • t) = n • Term.realize v t

Tactic:
induction n with simp [*, add_nsmul]

Premises used: add_nsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
rhs : ∑ i ∈ s, Term.realize v (f i)
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)

Tactic:
rhs
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
rw : List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
| ∑ i ∈ s, Term.realize v (f i)

Tactic:
rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]

Premises used: Finset.nodup_toList, List.sum_toFinset, Finset.toList_toFinset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
rw : List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)
| Term.realize v (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)

Tactic:
rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]

Premises used: Finset.nodup_toList, List.sum_toFinset, Finset.toList_toFinset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
conv : 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 (List.map f s.toList).sum = ∑ i ∈ s, Term.realize v (f i)

Tactic:
conv => rhs; rw [← s.toList_toFinset, List.sum_toFinset _ s.nodup_toList]

Premises used: Finset.nodup_toList, List.sum_toFinset, Finset.toList_toFinset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
generalize :
  ∀ (l : List β), Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
⊢ Term.realize v (List.map f s.toList).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) s.toList)

Tactic:
generalize s.toList = l

Premises used: Finset.toList
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
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 []).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) [])

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
Goal:
α : Type u_1
M : Type u_2
v : α → M
inst : AddCommMonoidWithOne M
β : Type u_3
s : Finset β
f : β → presburger.Term α
head : β
tail : List β
tail_ih : 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:
simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
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)) [])
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))
⊢ Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)

Tactic:
induction l with simp [*]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Basic
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)
simp₂ : ∀ (l : List β), Term.realize v (List.map f l).sum = List.sum (List.map (fun (i : β) ↦ Term.realize v (f i)) l)
⊢ Term.realize v (sum s f) = ∑ 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 [*]

Premises used: Finset.toList, FirstOrder.Language.presburger.sum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : IsLinearSet s
⊢ ∃ (a : α → ℕ) (t : Finset (α → ℕ)), s = a +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ))

Tactic:
rw [isLinearSet_iff] at hs

Premises used: isLinearSet_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : ∃ (a : α → ℕ) (t : Finset (α → ℕ)), s = a +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ))
rcases :
  ∀ (v : α → ℕ) (t : Finset (α → ℕ)),
    A.Definable presburger (v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)))
⊢ A.Definable presburger s

Tactic:
rcases hs with ⟨v, t, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
⊢ A.Definable presburger (v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)))

Tactic:
⟨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))))), ?_⟩

Premises used: Finset.univ, Set.Definable, FirstOrder.Language.Formula.iInf, Membership.mem, Subtype, FirstOrder.Language.Term.equal, Sum.inl, Nat.cast, FirstOrder.Language.Formula.iExs, FirstOrder.Language.presburger.sum, FirstOrder.Language.Term.var, HAdd.hAdd, Sum.inr, FirstOrder.Language.Term.varsToConstants, Exists.intro, HSMul.hSMul, Subtype.val