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 y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet (s := s)
hi : (↑i : ι → ℕ) ∉ t
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) y
mem :
  ∀ (y : ι → ℕ) (hy : y ∈ t),
    Eq (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      (0 : ℚ)
⊢ Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
    (0 : ℚ)
have zero : Eq (α := ℚ)
  ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) 0 : ι → ℚ) :
          (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
        (a : (↑hs.basisSet : Type u_3)) → ℚ)
      i :
    ℚ)
  (0 : ℚ)
Tactic: induction hy using AddSubmonoid.closure_induction with
  | mem y hy =>
    rw [← hs.basis_apply ⟨y, ht hy⟩]
    simpa [Finsupp.single_apply, ← Subtype.val_inj] using ne_of_mem_of_not_mem hy hi
  | zero => simp
  | add _ _ _ _ ih₁ ih₂ => simp [ih₁, ih₂]
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet (s := s)
hi : (↑i : ι → ℕ) ∉ t
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) y
mem :
  ∀ (y : ι → ℕ) (hy : y ∈ t),
    Eq (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      (0 : ℚ)
zero :
  Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) 0 : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
    (0 : ℚ)
⊢ Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
    (0 : ℚ)
have add : ∀ (x y : ι → ℕ),
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) x →
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) y →
      ∀
        (ih₁ :
          Eq (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)
            (0 : ℚ))
        (ih₂ :
          Eq (α := ℚ)
            ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                      ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
                    (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                  (a : (↑hs.basisSet : Type u_3)) → ℚ)
                i :
              ℚ)
            (0 : ℚ)),
        Eq (α := ℚ)
          ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ) :
                  (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                (a : (↑hs.basisSet : Type u_3)) → ℚ)
              i :
            ℚ)
          (0 : ℚ)
Tactic: induction hy using AddSubmonoid.closure_induction with
  | mem y hy =>
    rw [← hs.basis_apply ⟨y, ht hy⟩]
    simpa [Finsupp.single_apply, ← Subtype.val_inj] using ne_of_mem_of_not_mem hy hi
  | zero => simp
  | add _ _ _ _ ih₁ ih₂ => simp [ih₁, ih₂]
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet (s := s)
hi : (↑i : ι → ℕ) ∉ t
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) y
⊢ hs.floor (s := s) (x + y) i = hs.floor (s := s) x i
have suffices : Eq (α := ℚ)
  ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) :
          (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
        (a : (↑hs.basisSet : Type u_3)) → ℚ)
      i :
    ℚ)
  (0 : ℚ)
Tactic: classical
  suffices hs.basis.repr (toRatVec y) i = 0 by
    simp [floor, this]
  induction hy using AddSubmonoid.closure_induction with
  | mem y hy =>
    rw [← hs.basis_apply ⟨y, ht hy⟩]
    simpa [Finsupp.single_apply, ← Subtype.val_inj] using ne_of_mem_of_not_mem hy hi
  | zero => simp
  | add _ _ _ _ ih₁ ih₂ => simp [ih₁, ih₂]
-- 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 : 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 : ι → ℕ)
have rw : 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: rw [← toRatVec_mono]
-- 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 (α := ι → ℚ)
    ((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 : ι → ℕ)) :
      ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ) :
      ι → ℚ)
Tactic: simp only [floor, 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 : ι → ℕ
⊢ ∑ 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 : ι → ℕ) : ι → ℚ) :
        ι → ℚ)
have 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 : ι → ℚ)
Tactic: rw [← sub_le_iff_le_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 : ι → ℕ
| 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 : ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ)
Tactic: enter [1, 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 (β := ι → ℚ)
      (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 : ι → ℕ) : ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ)
Tactic: rw [← Nat.cast_smul_eq_nsmul ℤ, ← Nat.cast_smul_eq_nsmul ℤ, ← sub_smul,
      Int.toNat_sub_toNat_neg, ← Int.cast_smul_eq_zsmul ℚ]
-- 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 (α := ι → ℚ)
    (∑ 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 : ι → ℚ)
have 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 : ι → ℕ) : ι → ℚ)
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 ℚ]
-- 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 (α := ι → ℚ)
    (∑ 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 : ι → ℚ)
have 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 : ι → ℚ)
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 ℚ]
-- 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 (α := ι → ℚ)
    (∑ 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 : ι → ℚ)
have 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)) : ι → ℚ)
Tactic: trans 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 : ι → ℕ
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)) : ι → ℚ)
⊢ 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 : ι → ℚ)
have trans₁ : HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ) ≤
  (toRatVec : (a : ι → ℕ) → ι → ℚ) x
Tactic: trans toRatVec x - toRatVec hs.base