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 : ι → ℚ
h :
  (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
    ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
⊢ Membership.mem (γ := Set (ι → ℚ))
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))) x ↔
    Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x

Tactic:
simp only [mem_image, mem_range, exists_exists_eq_and]

Premises used: Set.mem_range, Set.mem_image, exists_exists_eq_and
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
h :
  ∀ (x : ι),
    Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) : ι → ℚ)
      ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x : ι → ℚ)
⊢ (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
    ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x

Tactic:
congr!
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
x_1 : ι
h :
  ∀ (x : ι),
    Eq (α := ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x_1 : ι → ℕ) x)
      ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x_1 x)
⊢ Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x_1 : ι → ℕ) : ι → ℚ)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x_1 : ι → ℚ)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
x_1 x_2 : ι
⊢ Eq (α := ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x_1 : ι → ℕ) x_2)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x_1 x_2)

Tactic:
simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]

Premises used: Pi.single_apply, _private.0.toRatVec, Pi.basisFun_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₆ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
h :
  Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
h₁ :
  ∀ (x : ι → ℚ),
    Membership.mem (γ := Set (ι → ℚ))
        (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
        x ↔
      Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
h₂ :
  ∀ (x : ι → ℚ),
    (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
      ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
h₃ :
  ∀ (x : ι → ℚ) (x : ι),
    Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) : ι → ℚ)
      ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x : ι → ℚ)
h₄ :
  ∀ (x : ι → ℚ) (x x_1 : ι),
    Eq (α := ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) x_1)
      ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x x_1)
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤

Tactic:
classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]

Premises used: Set.mem_range, LinearIndepOn.span_image_extend_eq_span_image, Pi.single_apply, Set.image_mono, Rat, Set.subset_union_right, _private.0.linearIndepOn_toRatVec, Set.mem_image, _private.0.IsProperLinearSet.linearIndepOn_periods, _private.0.toRatVec, exists_exists_eq_and, Pi.basisFun_apply, Submodule.span_mono, top_le_iff, Pi.basisFun, Module.Basis.span_eq, _private.0.IsProperLinearSet.basisSet, LE.le.trans'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ Eq (α := ι → ℚ) ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)

Tactic:
simp [basis]

Premises used: _private.0.IsProperLinearSet.basis
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
⊢ hs.fundamentalDomain (s := s).Finite

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
rw :
  LE.le.{u_3} (α := ι → ℚ)
    (∑ 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 : (↑hs.basisSet : Type u_3), (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x : ι → ℕ))
⊢ x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))

Tactic:
rw [mem_Iic, ← toRatVec_mono, map_add, map_sum, ← add_sub_cancel (toRatVec hs.base) (toRatVec x),
    add_le_add_iff_left, ← hs.basis.sum_repr (toRatVec x - toRatVec hs.base)]

Premises used: _private.0.IsProperLinearSet.base, _private.0.IsProperLinearSet.basis, add_le_add_iff_left, HSub.hSub, _private.0.toRatVec_mono, map_add, _private.0.toRatVec, map_sum, add_sub_cancel, Set.mem_Iic, DFunLike.coe, Module.Basis.sum_repr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
⊢ LE.le.{u_3} (α := ι → ℚ)
    (∑ 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 : (↑hs.basisSet : Type u_3), (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x : ι → ℕ))

Tactic:
Finset.sum_le_sum fun i hi => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
refine :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3))
    (hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i),
    HSMul.hSMul (α := ℚ) (β := ι → ℚ)
        ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                  (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                    ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
              (a : (↑hs.basisSet : Type u_3)) → ℚ)
            i :
          ℚ)
        ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ) ≤
      (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ)
⊢ LE.le.{u_3} (α := ι → ℚ)
    (∑ 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 : (↑hs.basisSet : Type u_3), (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑x : ι → ℕ))

Tactic:
refine Finset.sum_le_sum fun i hi => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
rw :
  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 : ι → ℚ) ≤
    (hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i
⊢ HSMul.hSMul (α := ℚ) (β := ι → ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                  ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
              (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
            (a : (↑hs.basisSet : Type u_3)) → ℚ)
          i :
        ℚ)
      ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ) ≤
    (toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ)

Tactic:
rw [← hs.basis_apply i]

Premises used: _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
hb : LE.le (α := ι → ℚ) (0 : ι → ℚ) ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
h :
  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 :
      ℚ)
    (1 : ℚ)
⊢ 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 : ι → ℚ) ≤
    (hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i

Tactic:
apply smul_le_of_le_one_left

Premises used: smul_le_of_le_one_left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
hb : LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)
⊢ LE.le (α := ι → ℚ) (0 : ι → ℚ) ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)

Tactic:
rw [hs.basis_apply]

Premises used: _private.0.IsProperLinearSet.basis_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
⊢ LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)

Tactic:
toRatVec_nonneg _

Premises used: _private.0.toRatVec_nonneg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
⊢ LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)

Tactic:
exact toRatVec_nonneg _

Premises used: _private.0.toRatVec_nonneg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ 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 :
      ℚ)
    (1 : ℚ)

Tactic:
(hx i).2.le

Premises used: LT.lt.le, And.right
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ 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 :
      ℚ)
    (1 : ℚ)

Tactic:
exact (hx i).2.le

Premises used: LT.lt.le, And.right
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ hs.floor (s := s) (hs.base (s := s)) i = 0

Tactic:
simp [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 ι
⊢ hs.fract (s := s) (hs.base (s := s)) = hs.base (s := s)

Tactic:
simp [fract, hs.floor_base]

Premises used: _private.0.IsProperLinearSet.fract, _private.0.IsProperLinearSet.floor_base
-- 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)
n : ℕ
rw :
  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 : ι → ℕ) → ι → ℚ) (n • (↑i : ι → ℕ)) : ι → ℚ)) :
              (↑(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 :
          ℚ) +
      (↑n : ℤ)
⊢ Int.floor (α := ℚ)
      ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (x + n • (↑i : ι → ℕ)) : ι → ℚ)
                  ((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 :
          ℚ) +
      (↑n : ℤ)

Tactic:
rw [map_add, ← sub_add_eq_add_sub]

Premises used: map_add, sub_add_eq_add_sub
-- 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)
n : ℕ
⊢ 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 : ι → ℕ) → ι → ℚ) (n • (↑i : ι → ℕ)) : ι → ℚ)) :
              (↑(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 :
          ℚ) +
      (↑n : ℤ)

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

Premises used: nsmul_eq_mul, _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)
rw :
  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 : ι → ℕ)) : ℤ)
⊢ 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 : ι → ℕ)) : ℤ)

Tactic:
rw [map_add, ← sub_add_eq_add_sub, ← Finset.sum_coe_sort]

Premises used: map_add, sub_add_eq_add_sub, Finset.sum_coe_sort