awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ LE.le.{u_3} (α := ι → ℚ)
    (∑ x_1 : (↑hs.basisSet : Type u_3),
      HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        (↑(Int.floor (α := ℚ)
              ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  x_1 :
                ℚ)) :
          ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))
    (∑ i : (↑hs.basisSet : Type u_3),
      HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ))

Tactic:
Finset.sum_le_sum fun i _ => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
refine :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i →
      HSMul.hSMul (α := ℚ) (β := ι → ℚ)
          (↑(Int.floor (α := ℚ)
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                          (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                        (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                      (a : (↑hs.basisSet : Type u_3)) → ℚ)
                    i :
                  ℚ)) :
            ℚ)
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) ≤
        HSMul.hSMul (α := ℚ) (β := ι → ℚ)
          ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              i :
            ℚ)
          ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
⊢ LE.le.{u_3} (α := ι → ℚ)
    (∑ x_1 : (↑hs.basisSet : Type u_3),
      HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        (↑(Int.floor (α := ℚ)
              ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  x_1 :
                ℚ)) :
          ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))
    (∑ i : (↑hs.basisSet : Type u_3),
      HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ))

Tactic:
refine Finset.sum_le_sum fun i _ => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
h : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
rw :
  HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      (↑(Int.floor (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)) :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) ≤
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)
⊢ HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      (↑(Int.floor (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)) :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) ≤
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)

Tactic:
rw [basis_apply]

Premises used: _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
h : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
⊢ HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      (↑(Int.floor (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)) :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) ≤
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)

Tactic:
smul_le_smul_of_nonneg_right (Int.floor_le _) (toRatVec_nonneg _)

Premises used: smul_le_smul_of_nonneg_right, _private.0.toRatVec_nonneg, Int.floor_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
h : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
⊢ HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      (↑(Int.floor (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)) :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) ≤
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)

Tactic:
exact smul_le_smul_of_nonneg_right (Int.floor_le _) (toRatVec_nonneg _)

Premises used: smul_le_smul_of_nonneg_right, _private.0.toRatVec_nonneg, Int.floor_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) ≤
    (toRatVec : (a : ι → ℕ) → ι → ℚ) x

Tactic:
simp [toRatVec_nonneg]

Premises used: _private.0.toRatVec_nonneg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
simp :
  x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) -
        ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) +
      ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
⊢ x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    hs.fract (s := s) x + ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
simp only [fract]

Premises used: _private.0.IsProperLinearSet.fract
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
rw rw₁ :
  x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
⊢ x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) -
        ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) +
      ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
rw [tsub_add_cancel_of_le (hs.floor_toNat_sum_le x)]

Premises used: _private.0.IsProperLinearSet.floor_toNat_sum_le, tsub_add_cancel_of_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
rw :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ)
          (x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
        ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ)
          (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
        ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
⊢ (toRatVec : (a : ι → ℕ) → ι → ℚ)
      (x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) -
        ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
rw [← map_tsub_of_le _ _ _ (hs.floor_toNat_sum_le x)]

Premises used: _private.0.IsProperLinearSet.floor_toNat_sum_le, map_tsub_of_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
simp :
  HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
        (∑ x_1 : (↑hs.basisSet : Type u_3),
            HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) :
          ι → ℚ) -
      ∑ x_1 : (↑hs.basisSet : Type u_3),
        HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ)
          (x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
        ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ)
          (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
        ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
simp only [map_add, map_sum, map_nsmul]

Premises used: map_add, map_sum, map_nsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
rw :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      (∑ x_1 : (↑hs.basisSet : Type u_3),
          (HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
            HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
        ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
⊢ HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
        (∑ x_1 : (↑hs.basisSet : Type u_3),
            HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) :
          ι → ℚ) -
      ∑ x_1 : (↑hs.basisSet : Type u_3),
        HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
rw [← sub_add_eq_add_sub, sub_add, ← Finset.sum_sub_distrib]

Premises used: sub_add, Finset.sum_sub_distrib, sub_add_eq_add_sub
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
h :
  ∀ (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
      HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      (∑ x_1 : (↑hs.basisSet : Type u_3),
          (HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
            HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
        ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
enter [1, 2, 2, _]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
x_1 : (↑(hs.basisSet (s := s)) : Type u_3)
h : HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
| HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
    HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]

Premises used: sub_smul, Int, Nat.cast_smul_eq_nsmul, Int.toNat_sub_toNat_neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
h :
  ∀ (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      (∑ x_1 : (↑hs.basisSet : Type u_3),
          (HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
            HSMul.hSMul (β := ι → ℚ) (-hs.floor (s := s) x x_1).toNat
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
        ι → ℚ) =
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
enter [1, 2, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]

Premises used: sub_smul, Int, Nat.cast_smul_eq_nsmul, Int.toNat_sub_toNat_neg