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 : ι → ℕ
conv :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      (∑ x_1 : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((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 : ι → ℚ)
      (∑ 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:
conv =>
    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
-- 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 : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                x_1) :
            ℚ)
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) +
        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) ((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_eq_iff_eq_add, add_assoc, ← sub_eq_iff_eq_add', ← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_assoc, sub_eq_iff_eq_add, sub_eq_iff_eq_add'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
simp :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                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 :
              ℚ))
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                x_1) :
            ℚ)
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ) +
        HSMul.hSMul (β := ι → ℚ) (hs.floor (s := s) x x_1) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))

Tactic:
simp only [floor]

Premises used: _private.0.IsProperLinearSet.floor
-- 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.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)) → ℚ)
              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 :
            ℚ))
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                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 :
              ℚ))
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))

Tactic:
enter [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 (α := ℚ) (β := ι → ℚ)
    ((((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 :
      ℚ)
    ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) x_1 : ι → ℚ)
| 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)) → ℚ)
            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 :
          ℚ))
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ)

Tactic:
rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]

Premises used: Rat, add_smul, Int.fract_add_floor, _private.0.IsProperLinearSet.basis_apply, 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 (α := ℚ) (β := ι → ℚ)
      ((((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 :
        ℚ)
      ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) x_1 : ι → ℚ)
| HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                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 :
              ℚ))
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))

Tactic:
enter [2, 2, _]
    rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]

Premises used: Rat, add_smul, Int.fract_add_floor, _private.0.IsProperLinearSet.basis_apply, 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 :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
            x_1 :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) x_1 : ι → ℚ)
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
                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 :
              ℚ))
          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x_1 : ι → ℕ) : ι → ℚ))

Tactic:
conv =>
    enter [2, 2, _]
    rw [← Int.cast_smul_eq_zsmul ℚ, ← add_smul, Int.fract_add_floor, ← hs.basis_apply]

Premises used: Rat, add_smul, Int.fract_add_floor, _private.0.IsProperLinearSet.basis_apply, Int.cast_smul_eq_zsmul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
rw rw₁ :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) =
    ∑ x_1 : (↑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)) → ℚ)
            x_1 :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) x_1 : ι → ℚ)

Tactic:
rw [hs.basis.sum_repr]

Premises used: _private.0.IsProperLinearSet.basis, Module.Basis.sum_repr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
⊢ ∃ (a : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ), y = ∑ i : (↑hs.basisSet : Type u_3), a i • (↑i : ι → ℕ)

Tactic:
rw [mem_closure_iff_of_fintype] at hy

Premises used: AddSubmonoid.mem_closure_iff_of_fintype
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
hy : ∃ (a : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ), y = ∑ i : (↑hs.basisSet : Type u_3), a i • (↑i : ι → ℕ)
rcases :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
    hs.fract (s := s) (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) = hs.fract (s := s) x
⊢ hs.fract (s := s) (x + y) = hs.fract (s := s) x

Tactic:
rcases hy with ⟨f, t, ht, hf, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ
rw :
  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 + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                            ι → ℚ)
                          ((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 : ι → ℕ) → ι → ℚ) (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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
⊢ hs.fract (s := s) (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) = hs.fract (s := s) x

Tactic:
rw [← toRatVec_inj, hs.toRatVec_fract_eq, hs.toRatVec_fract_eq]

Premises used: _private.0.IsProperLinearSet.toRatVec_fract_eq, _private.0.toRatVec_inj
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ
h :
  ∀ (x_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ x_1 →
      Eq (α := ℚ)
        (Int.fract
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    (HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                        ι → ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              x_1) :
          ℚ)
        (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)) → ℚ)
              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 + ∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) :
                            ι → ℚ)
                          ((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 : ι → ℕ) → ι → ℚ) (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:
congr! 3