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 : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
⊢ HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ i : (↑hs.basisSet : Type u_3),
          HSMul.hSMul (α := ℚ) (β := ι → ℚ)
            (Int.fract
                ((((Basis.repr (hs.basis (s := s)) : (a : ι → ℚ) → (↑hs.basisSet : Type u_3) →₀ ℚ)
                        (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
                          ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) :
                      (↑(hs.basisSet (s := s)) : Type u_3) →₀ ℚ) :
                    (a : (↑hs.basisSet : Type u_3)) → ℚ)
                  i) :
              ℚ)
            ((toRatVec : (a : ι → ℕ) → ι → ℚ) (↑i : ι → ℕ) : ι → ℚ) :
        ι → ℚ) =
    (toRatVec : (a : ι → ℕ) → ι → ℚ) x
have conv_lhs : HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
    (∑ 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 : ι → ℚ) :
      ι → ℚ) =
  (toRatVec : (a : ι → ℕ) → ι → ℚ) x
Tactic: conv_lhs =>
    enter [2, 2, i]
    rw [Int.fract_eq_self.2 (hx i), ← 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 ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain (s := s)
⊢ HAdd.hAdd (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
      (∑ 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 : ι → ℚ) :
        ι → ℚ) =
    (toRatVec : (a : ι → ℕ) → ι → ℚ) x
have rw : HAdd.hAdd (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)
    (HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.base (s := s)) : ι → ℚ)) =
  (toRatVec : (a : ι → ℕ) → ι → ℚ) x
Tactic: rw [hs.basis.sum_repr]
-- 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 ∈ s ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have nth_rw : x ∈ hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ)) ↔
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: nth_rw 1 [hs.eq_base_vadd_closure_periods]
-- 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 ∈ hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ)) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have simp : (∃ (y : ι → ℕ),
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) ↔
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
-- 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 : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have mp : (∃ (y : ι → ℕ),
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) →
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
mp :
  (∃ (y : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) →
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ (∃ (y : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have mpr : (hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)) →
  ∃ (y : ι → ℕ), Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
⊢ hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i ∧
        ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) (hs.base (s := s) + y) i = 0)
have mp : hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s)
Tactic: refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
mp : hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s)
⊢ hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i ∧
        ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) (hs.base (s := s) + y) i = 0)
have mp₁ : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)), 0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i
Tactic: refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
mp : hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s)
mp₁ : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)), 0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i
⊢ hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i ∧
        ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) (hs.base (s := s) + y) i = 0)
have mp₂ : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)),
  hs.floor (s := s) (hs.base (s := s) + y) i = 0
Tactic: refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
⊢ hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s)
have mp : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
Tactic: rw [hs.fract_add_of_mem_closure, hs.fract_base]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
i : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i
have mp : hs.floor (s := s) (hs.base (s := s)) i ≤ hs.floor (s := s) (hs.base (s := s) + y) i
Tactic: rw [← hs.floor_base i]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
⊢ hs.floor (s := s) (hs.base (s := s) + y) i = 0
have mp : hs.floor (s := s) (hs.base (s := s)) i = 0
Tactic: rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
mp : hs.floor (s := s) (hs.base (s := s)) i = 0
⊢ hs.floor (s := s) (hs.base (s := s) + y) i = 0
have mp₁ : Eq (α := ℤ) 0 0
Tactic: rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_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 : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ ∃ (y : ι → ℕ), Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x
have mpr : hs.base (s := s) +
    ∑ i : (↑hs.basisSet : Type u_3) with (↑i : ι → ℕ) ∈ hs.periods (s := s),
      (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
  x
Tactic: refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).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 : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ hs.base (s := s) +
      ∑ i : (↑hs.basisSet : Type u_3) with (↑i : ι → ℕ) ∈ hs.periods (s := s),
        (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    x
have mpr : (hs.fract (s := s) x +
    ∑ a : (↑hs.basisSet : Type u_3),
      if (↑a : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x a).toNat • (↑a : ι → ℕ) else 0) =
  x
Tactic: rw [Finset.sum_filter, ← hx₁]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
| x
have rw : x + ∑ _x : (↑hs.basisSet : Type u_3), 0
Tactic: rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ (hs.fract (s := s) x +
      ∑ a : (↑hs.basisSet : Type u_3),
        if (↑a : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x a).toNat • (↑a : ι → ℕ) else 0) =
    x
have mpr : (hs.fract (s := s) x +
    ∑ a : (↑hs.basisSet : Type u_3),
      if (↑a : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x a).toNat • (↑a : ι → ℕ) else 0) =
  x + ∑ _x : (↑hs.basisSet : Type u_3), 0
Tactic: conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ (hs.fract (s := s) x +
      ∑ a : (↑hs.basisSet : Type u_3),
        if (↑a : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x a).toNat • (↑a : ι → ℕ) else 0) =
    x + ∑ _x : (↑hs.basisSet : Type u_3), 0
have h : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
  Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i →
    (if (↑i : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) else 0) =
      (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
Tactic: convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
h :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i →
      (if (↑i : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) else 0) =
        (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
⊢ (hs.fract (s := s) x +
      ∑ a : (↑hs.basisSet : Type u_3),
        if (↑a : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x a).toNat • (↑a : ι → ℕ) else 0) =
    x + ∑ _x : (↑hs.basisSet : Type u_3), 0
have h₁ : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
  Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i →
    0 = (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
Tactic: convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
i : (↑(hs.basisSet (s := s)) : Type u_3)
h : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
⊢ (if (↑i : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) else 0) =
    (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
have pos : ∀ (hi : (↑i : ι → ℕ) ∈ hs.periods (s := s)),
  (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) = (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
hx₁ : hs.fract (s := s) x = hs.base (s := s)
hx₂ :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
i : (↑(hs.basisSet (s := s)) : Type u_3)
h : Membership.mem (γ := Finset (↑(hs.basisSet (s := s)) : Type u_3)) Finset.univ i
pos :
  ∀ (hi : (↑i : ι → ℕ) ∈ hs.periods (s := s)),
    (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) = (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
⊢ (if (↑i : ι → ℕ) ∈ hs.periods (s := s) then (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) else 0) =
    (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
have neg : ∀ (hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)), 0 = (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
Tactic: split_ifs with hi
-- 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 ∈ s ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have nth_rw : x ∈ hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ)) ↔
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: classical
  nth_rw 1 [hs.eq_base_vadd_closure_periods]
  simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
  constructor
  · rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
  · intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
nth_rw nth_rw₁ nth_rw₂ :
  x ∈ hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ)) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ x ∈ s ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have nth_rw₃ : (∃ (y : ι → ℕ),
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) ↔
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: classical
  nth_rw 1 [hs.eq_base_vadd_closure_periods]
  simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
  constructor
  · rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
  · intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
nth_rw nth_rw₁ nth_rw₂ :
  x ∈ hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ)) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
nth_rw₃ :
  (∃ (y : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
⊢ x ∈ s ↔
    hs.fract (s := s) x = hs.base (s := s) ∧
      ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
have mp : (∃ (y : ι → ℕ),
    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = x) →
  hs.fract (s := s) x = hs.base (s := s) ∧
    ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)
Tactic: classical
  nth_rw 1 [hs.eq_base_vadd_closure_periods]
  simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
  constructor
  · rintro ⟨y, hy, rfl⟩
    refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
    · rw [hs.fract_add_of_mem_closure, hs.fract_base]
      exact closure_mono hs.periods_subset_basisSet hy
    · rw [← hs.floor_base i]
      exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)
    · rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]
  · intro ⟨hx₁, hx₂⟩
    refine ⟨∑ i : hs.basisSet with i.1 ∈ hs.periods, (hs.floor x i).toNat • i.1,
      sum_mem fun i hi => nsmul_mem (mem_closure_of_mem (Finset.mem_filter.1 hi).2) _, ?_⟩
    rw [Finset.sum_filter, ← hx₁]
    conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]
    convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i
    · split_ifs with hi
      · simp
      · simp [(hx₂ i).2 hi]
    · simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]