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 ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HAdd.hAdd (β := ι → ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ))
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ)
                      (∑ i : ↥Finset.univ,
                        f (↑(↑i : (↑hs.basisSet : Type u_3)) : ι → ℕ) • (↑(↑i : (↑hs.basisSet : Type u_3)) : ι → ℕ)) :
                    ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ) =
    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 :
          ℚ) +
      (↑(f (↑i : ι → ℕ)) : ℤ)

Tactic:
simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply]

Premises used: nsmul_eq_mul, Finsupp.single_apply, _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
simp :
  Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ)
                      (x + ∑ j : (↑hs.basisSet : Type u_3), f (↑j : ι → ℕ) • (↑j : ι → ℕ)) :
                    ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ) =
    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 :
          ℚ) +
      (↑(f (↑i : ι → ℕ)) : ℤ)
simp₁ :
  Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HAdd.hAdd (β := ι → ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ))
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ)
                      (∑ i : ↥Finset.univ,
                        f (↑(↑i : (↑hs.basisSet : Type u_3)) : ι → ℕ) • (↑(↑i : (↑hs.basisSet : Type u_3)) : ι → ℕ)) :
                    ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ) =
    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 :
          ℚ) +
      (↑(f (↑i : ι → ℕ)) : ℤ)
⊢ hs.floor (s := s) (x + ∑ j : (↑hs.basisSet : Type u_3), f (↑j : ι → ℕ) • (↑j : ι → ℕ)) i =
    hs.floor (s := s) x i + (↑(f (↑i : ι → ℕ)) : ℤ)

Tactic:
classical
  simp only [floor]
  rw [map_add, ← sub_add_eq_add_sub, ← Finset.sum_coe_sort]
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply]

Premises used: _private.0.IsProperLinearSet.floor, map_add, nsmul_eq_mul, Finsupp.single_apply, _private.0.IsProperLinearSet.basis_apply, sub_add_eq_add_sub, Finset.sum_coe_sort
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
hab :
  LE.le (α := ℚ)
    ((((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 :
      ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
⊢ 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 :
        ℚ) ≤
    Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)

Tactic:
apply Int.floor_le_floor

Premises used: Int.floor_le_floor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
hab :
  LE.le (α := ℚ) (0 : ℚ)
    ((((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 :
      ℚ)
⊢ LE.le (α := ℚ)
    ((((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 :
      ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + y) : ι → ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)

Tactic:
simp_rw [map_add, add_sub_right_comm, map_add, Finsupp.add_apply, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, Finsupp.add_apply, map_add, add_sub_right_comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hy : ∃ (a : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ), y = ∑ i : (↑hs.basisSet : Type u_3), a i • (↑i : ι → ℕ)
hab :
  ∀ (f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ),
    LE.le (α := ℚ) (0 : ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                ((toRatVec : (a : ι → ℕ) → ι → ℚ) (∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) : ι → ℚ) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
⊢ LE.le (α := ℚ) (0 : ℚ)
    ((((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 :
      ℚ)

Tactic:
rcases hy with ⟨f, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ
hab :
  LE.le (α := ℚ) 0
    (∑ c : (↑hs.basisSet : Type u_3),
      (((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (f c • (↑c : ι → ℕ)) : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i)
⊢ LE.le (α := ℚ) (0 : ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (∑ i : (↑hs.basisSet : Type u_3), f i • (↑i : ι → ℕ)) : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)

Tactic:
simp_rw [map_sum, Finsupp.coe_finsetSum, Finset.sum_apply]

Premises used: Finset.sum_apply, map_sum, Finsupp.coe_finsetSum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ
hab :
  ∀ (i_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i_1 →
      LE.le (α := ℚ) (0 : ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (f i_1 • (↑i_1 : ι → ℕ)) : ι → ℚ) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)
⊢ LE.le (α := ℚ) 0
    (∑ c : (↑hs.basisSet : Type u_3),
      (((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) (f c • (↑c : ι → ℕ)) : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i)

Tactic:
apply Finset.sum_nonneg

Premises used: Finset.sum_nonneg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
f : (↑(hs.basisSet (s := s)) : Type u_3) → ℕ
⊢ ∀ (i_1 : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i_1 →
      LE.le (α := ℚ) (0 : ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (f i_1 • (↑i_1 : ι → ℕ)) : ι → ℚ) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)

Tactic:
simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply, ite_nonneg]

Premises used: ite_nonneg, nsmul_eq_mul, Finsupp.single_apply, _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
this :
  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 : ℚ)
⊢ hs.floor (s := s) (x + y) i = hs.floor (s := s) x i

Tactic:
simp [floor, this]

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 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
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 : ℚ)
⊢ hs.floor (s := s) (x + y) i = hs.floor (s := s) x i

Tactic:
suffices hs.basis.repr (toRatVec y) i = 0 by
    simp [floor, this]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y_1 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet (s := s)
hi : (↑i : ι → ℕ) ∉ t
y : ι → ℕ
hy : y ∈ t
mem :
  Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ)
                  (Subtype.mk (p := fun (x : ι → ℕ) ↦ x ∈ hs.basisSet (s := s)) 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 : ℚ)

Tactic:
rw [← hs.basis_apply ⟨y, ht hy⟩]

Premises used: Subtype.mk, _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x y_1 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet (s := s)
hi : (↑i : ι → ℕ) ∉ t
y : ι → ℕ
hy : y ∈ t
⊢ Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ)
                  (Subtype.mk (p := fun (x : ι → ℕ) ↦ x ∈ hs.basisSet (s := s)) y ⋯) :
                ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
    (0 : ℚ)

Tactic:
simpa [Finsupp.single_apply, ← Subtype.val_inj] using ne_of_mem_of_not_mem hy hi

Premises used: Subtype.val_inj, ne_of_mem_of_not_mem, Finsupp.single_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ 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:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
x_1 y_1 : ι → ℕ
hx : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) x_1
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure t) y_1
ih₁ :
  Eq (α := ℚ)
    ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
              ((toRatVec : (a : ι → ℕ) → ι → ℚ) x_1 : ι → ℚ) :
            (↑(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_1 : ι → ℚ) :
            (↑(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_1 + y_1) : ι → ℚ) :
            (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
          (a : (↑hs.basisSet : Type u_3)) → ℚ)
        i :
      ℚ)
    (0 : ℚ)

Tactic:
simp [ih₁, ih₂]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 : ℚ)
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 : ℚ)
⊢ 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:
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₂]

Premises used: Subtype.val_inj, ne_of_mem_of_not_mem, Finsupp.single_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
suffices suffices₁ 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 : ℚ)
⊢ hs.floor (s := s) (x + y) i = hs.floor (s := s) x i

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₂]

Premises used: Subtype.val_inj, ne_of_mem_of_not_mem, Finsupp.single_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℕ)) :
      ι → ℚ)
⊢ ∑ 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 [← toRatVec_mono]

Premises used: _private.0.toRatVec_mono