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 ι
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 : ι → ℚ)
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have h₄ : ∀ (x : ι → ℚ) (x x_1 : ι),
  Eq (α := ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) x_1)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x x_1)
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ hs.fundamentalDomain (s := s).Finite
have haveI : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
⊢ x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
have 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 : ι → ℕ))
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)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℕ))
have 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 : ι → ℕ)
Tactic: refine Finset.sum_le_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ 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 : ι → ℕ)
have 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
Tactic: rw [← hs.basis_apply i]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ 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
have hb : LE.le (α := ι → ℚ) (0 : ι → ℚ) ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
Tactic: apply smul_le_of_le_one_left
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℚ)
⊢ 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
have 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 : ℚ)
Tactic: apply smul_le_of_le_one_left
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℚ) ((hs.basis (s := s) : (a : (↑hs.basisSet : Type u_3)) → ι → ℚ) i : ι → ℚ)
have hb : LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ)
Tactic: rw [hs.basis_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ hs.fundamentalDomain (s := s).Finite
have haveI : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
Tactic: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  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)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
⊢ hs.fundamentalDomain (s := s).Finite
have haveI₃ : ∀ (this : Fintype ι),
  hs.fundamentalDomain (s := s) ⊆ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
Tactic: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  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)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
haveI₃ :
  ∀ (this : Fintype ι),
    hs.fundamentalDomain (s := s) ⊆ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
⊢ hs.fundamentalDomain (s := s).Finite
have haveI₄ : ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)),
  x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
Tactic: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  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)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
haveI₃ :
  ∀ (this : Fintype ι),
    hs.fundamentalDomain (s := s) ⊆ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
haveI₄ :
  ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)),
    x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
⊢ hs.fundamentalDomain (s := s).Finite
have haveI₅ : ∀ (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: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  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)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), hs.fundamentalDomain (s := s).Finite
haveI₃ :
  ∀ (this : Fintype ι),
    hs.fundamentalDomain (s := s) ⊆ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
haveI₄ :
  ∀ (this : Fintype ι) ⦃x : ι → ℕ⦄ (hx : x ∈ hs.fundamentalDomain (s := s)),
    x ∈ Iic (hs.base (s := s) + ∑ i : (↑hs.basisSet : Type u_3), (↑i : ι → ℕ))
haveI₅ :
  ∀ (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 : ι → ℕ))
⊢ hs.fundamentalDomain (s := s).Finite
have haveI₆ : ∀ (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),
  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: classical
  haveI := Fintype.ofFinite ι
  apply (finite_Iic (hs.base + ∑ i : hs.basisSet, i.1)).subset
  intro x hx
  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)]
  refine Finset.sum_le_sum fun i hi => ?_
  rw [← hs.basis_apply i]
  apply smul_le_of_le_one_left
  · rw [hs.basis_apply]
    exact toRatVec_nonneg _
  · exact (hx i).2.le
-- 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 (s := s)) : Type u_3)
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 : ℤ)
have 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 : ℤ)
Tactic: rw [map_add, ← sub_add_eq_add_sub]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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) →₀ ℚ)
                (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 : ι → ℕ)) : ℤ)
have 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 : ι → ℕ)) : ℤ)
Tactic: rw [map_add, ← sub_add_eq_add_sub, ← Finset.sum_coe_sort]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ hs.floor (s := s) (x + ∑ j : (↑hs.basisSet : Type u_3), f (↑j : ι → ℕ) • (↑j : ι → ℕ)) i =
    hs.floor (s := s) x i + (↑(f (↑i : ι → ℕ)) : ℤ)
have 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 : ι → ℕ)) : ℤ)
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]