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 : ι → ℕ
simp :
  ∑ 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 :
              ℚ)).toNat
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) ≤
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) 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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
⊢ LE.le (α := ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ)
        (x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)) :
      ι → ℚ)

Tactic:
simp only [floor, map_add, map_sum, map_nsmul]

Premises used: _private.0.IsProperLinearSet.floor, 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 :
  LE.le (α := ι → ℚ)
    (∑ 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 :
                  ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
          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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) 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 :
              ℚ)).toNat
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) ≤
    HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) 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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)

Tactic:
rw [← sub_le_iff_le_add, ← Finset.sum_sub_distrib]

Premises used: sub_le_iff_le_add, Finset.sum_sub_distrib
-- 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 (β := ι → ℚ)
        (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 :
              ℚ)).toNat
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
      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 :
                ℚ)).toNat
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
| LE.le (α := ι → ℚ)
    (∑ 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 :
                  ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
          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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)

Tactic:
enter [1, 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 (α := ℚ) (β := ι → ℚ)
    (↑(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 : ι → ℕ) : ι → ℚ)
| 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 :
            ℚ)).toNat
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
    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 :
              ℚ)).toNat
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)

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

Premises used: Rat, sub_smul, Int, Nat.cast_smul_eq_nsmul, Int.toNat_sub_toNat_neg, Int.cast_smul_eq_zsmul
-- 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 (α := ℚ) (β := ι → ℚ)
      (↑(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 : ι → ℕ) : ι → ℚ)
| LE.le (α := ι → ℚ)
    (∑ 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 :
                  ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
          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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)

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

Premises used: Rat, sub_smul, Int, Nat.cast_smul_eq_nsmul, Int.toNat_sub_toNat_neg, Int.cast_smul_eq_zsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
conv :
  LE.le (α := ι → ℚ)
    (∑ 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
⊢ LE.le (α := ι → ℚ)
    (∑ 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 :
                  ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) -
          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 :
                    ℚ)).toNat
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)

Tactic:
conv =>
    enter [1, 2, _]
    rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg, ← Int.cast_smul_eq_zsmul ℚ]

Premises used: Rat, sub_smul, Int, Nat.cast_smul_eq_nsmul, Int.toNat_sub_toNat_neg, Int.cast_smul_eq_zsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
trans :
  ∑ 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)) : ι → ℚ)
trans₁ :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) ≤
    (toRatVec : (a : ι → ℕ) → ι → ℚ) x
⊢ LE.le (α := ι → ℚ)
    (∑ 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)

Tactic:
trans toRatVec x - toRatVec hs.base

Premises used: _private.0.IsProperLinearSet.base, _private.0.toRatVec, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
rhs :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
| ∑ 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)) : ι → ℚ)

Tactic:
rhs
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℚ)
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)

Tactic:
rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]

Premises used: _private.0.IsProperLinearSet.base, _private.0.IsProperLinearSet.basis, HSub.hSub, _private.0.toRatVec, DFunLike.coe, Module.Basis.sum_repr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℚ)
| ∑ 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)) : ι → ℚ)

Tactic:
rhs; rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]

Premises used: _private.0.IsProperLinearSet.base, _private.0.IsProperLinearSet.basis, HSub.hSub, _private.0.toRatVec, DFunLike.coe, Module.Basis.sum_repr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℚ))
⊢ ∑ 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)) : ι → ℚ)

Tactic:
conv => rhs; rw [← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]

Premises used: _private.0.IsProperLinearSet.base, _private.0.IsProperLinearSet.basis, HSub.hSub, _private.0.toRatVec, DFunLike.coe, Module.Basis.sum_repr