awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
| ∑ 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 : ι → ℕ) : ι → ℚ) ≤
    HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
have rhs : HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
Tactic: rhs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
have rw : ∑ 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: rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
| ∑ 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 : ι → ℕ) : ι → ℚ) ≤
    HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
have rw : ∑ 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: rhs; rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ ∑ 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 : ι → ℕ) : ι → ℚ) ≤
    HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
have conv : 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: conv => rhs; rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℚ))
have 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 : ι → ℚ)
Tactic: refine Finset.sum_le_sum fun i _ => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 :
        ℚ)
      ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ)
Tactic: rw [basis_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ 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 : ι → ℕ)
have 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 : ι → ℕ)
Tactic: simp only [fract]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ 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 : ι → ℕ)
have 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 : ι → ℕ)
Tactic: rw [tsub_add_cancel_of_le (hs.floor_toNat_sum_le x)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ (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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
Tactic: rw [← map_tsub_of_le _ _ _ (hs.floor_toNat_sum_le x)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ 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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
Tactic: simp only [map_add, map_sum, map_nsmul]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ 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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
Tactic: rw [← sub_add_eq_add_sub, sub_add, ← Finset.sum_sub_distrib]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
| 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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ)
Tactic: enter [1, 2, 2, _]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℕ) : ι → ℚ)
have h : HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
| 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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have h : ∀ (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
  HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
Tactic: enter [1, 2, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg]