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 : hs.fract (s := s) x = hs.base (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
h :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)})
    (((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
⊢ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
          ∃ (z : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
              ∃ (z' : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                  x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
have h₁ : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
  (∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
Tactic: refine ⟨i, hi, ((hs.floor x i).toNat - 1) • i.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.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 : ι → ℕ
hx : hs.fract (s := s) x = hs.base (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
h :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)})
    (((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
h₁ :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
    (∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
⊢ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
          ∃ (z : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
              ∃ (z' : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                  x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
have h₂ : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
  (∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
Tactic: refine ⟨i, hi, ((hs.floor x i).toNat - 1) • i.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.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 : ι → ℕ
hx : hs.fract (s := s) x = hs.base (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
h :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)})
    (((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
h₁ :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
    (∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
h₂ :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
    (∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
⊢ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
          ∃ (z : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
              ∃ (z' : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                  x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
have h₃ : x + ∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ) =
  hs.base (s := s) + (↑i : ι → ℕ) + ((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ) +
    ∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ)
Tactic: refine ⟨i, hi, ((hs.floor x i).toNat - 1) • i.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (hs.floor x j).toNat • j.1, ?_,
          ∑ j ∈ Finset.univ.erase i, (- hs.floor x j).toNat • j.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 : ι → ℕ
hx : hs.fract (s := s) x = hs.base (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
    (∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
have h : ∀ (j : (↑(hs.basisSet (s := s)) : Type u_3)) (hj : j ∈ Finset.erase Finset.univ i),
  (↑j : ι → ℕ) ∈ hs.basisSet (s := s) \ {(↑i : ι → ℕ)}
Tactic: refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
-- 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)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)}))
    (∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ))
have h : ∀ (j : (↑(hs.basisSet (s := s)) : Type u_3)) (hj : j ∈ Finset.erase Finset.univ i),
  (↑j : ι → ℕ) ∈ hs.basisSet (s := s) \ {(↑i : ι → ℕ)}
Tactic: refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
-- 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)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ x + ∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ) =
    hs.base (s := s) + (↑i : ι → ℕ) + ((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ) +
      ∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ)
have h : x + ∑ x_1 : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x x_1).toNat • (↑x_1 : ι → ℕ) =
  hs.fract (s := s) x + ∑ x_1 : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x x_1).toNat • (↑x_1 : ι → ℕ)
Tactic: rw [add_assoc hs.base, ← succ_nsmul',
          tsub_add_cancel_of_le ((Int.le_toNat hi'.le).2 (Int.add_one_le_of_lt hi')),
          add_assoc hs.base,
          Finset.add_sum_erase _ (fun j => (hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 (neg_neg_iff_pos.2 hi').le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← 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 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
⊢ hs.fract (s := s) x = hs.base (s := s) ∧
    ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x i
have h : hs.fract (s := s) x = hs.base (s := s)
Tactic: refine ⟨?_, 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 ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
h : hs.fract (s := s) x = hs.base (s := s)
⊢ hs.fract (s := s) x = hs.base (s := s) ∧
    ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x i
have h₁ : 0 < hs.floor (s := s) x i
Tactic: refine ⟨?_, i, hi, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
⊢ hs.fract (s := s) x = hs.base (s := s)
have heq₁ : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
Tactic: apply congr_arg hs.fract at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h : ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)),
  hs.fract (s := s) x = hs.base (s := s)
Tactic: rwa [hs.fract_add_of_mem_closure (closure_mono diff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
h :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)),
    hs.fract (s := s) x = hs.base (s := s)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h₁ : ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y)),
  hs.fract (s := s) x = hs.base (s := s)
Tactic: rwa [hs.fract_add_of_mem_closure (closure_mono diff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
h :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y)),
    hs.fract (s := s) x = hs.base (s := s)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h₂ : ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ))),
  hs.fract (s := s) x = hs.base (s := s)
Tactic: rwa [hs.fract_add_of_mem_closure (closure_mono diff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
h :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y)),
    hs.fract (s := s) x = hs.base (s := s)
h₂ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ))),
    hs.fract (s := s) x = hs.base (s := s)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h₃ : ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s))), hs.fract (s := s) x = hs.base (s := s)
Tactic: rwa [hs.fract_add_of_mem_closure (closure_mono diff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
h :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y)),
    hs.fract (s := s) x = hs.base (s := s)
h₂ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ))),
    hs.fract (s := s) x = hs.base (s := s)
h₃ : ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s))), hs.fract (s := s) x = hs.base (s := s)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h₄ : ∀ (heq : hs.fract (s := s) x = hs.base (s := s)), hs.fract (s := s) x = hs.base (s := s)
Tactic: rwa [hs.fract_add_of_mem_closure (closure_mono diff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq
Cleared hypotheses: heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
⊢ 0 < hs.floor (s := s) x i
have h : ∀ (hy : ∃ (n : ℕ), n • (↑i : ι → ℕ) = y) (z : ι → ℕ)
  (hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z) (z' : ι → ℕ)
  (hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z')
  (heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z), 0 < hs.floor (s := s) x i
Tactic: rw [mem_closure_singleton] at hy
Cleared hypotheses: hy, z, hz, z', hz', heq
-- 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
y : ι → ℕ
hy : ∃ (n : ℕ), n • (↑i : ι → ℕ) = y
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
⊢ 0 < hs.floor (s := s) x i
have h : ∀ (n : ℕ) (heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z), 0 < hs.floor (s := s) x i
Tactic: rcases hy with ⟨n, rfl⟩
Cleared hypotheses: y, hy, heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
n : ℕ
heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z
⊢ 0 < hs.floor (s := s) x i
have heq₁ : hs.floor (s := s) (x + z') i = hs.floor (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z) i
Tactic: apply congr_arg (hs.floor · i) at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
z : ι → ℕ
hz : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z
z' : ι → ℕ
hz' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z'
n : ℕ
heq : hs.floor (s := s) (x + z') i = hs.floor (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z) i
⊢ 0 < hs.floor (s := s) x i
have heq₁ : hs.floor (s := s) x i = (↑(n + 1) : ℤ)
Tactic: rw [hs.floor_add_of_mem_closure diff_subset (notMem_diff_of_mem (mem_singleton i.1)) hz,
          hs.floor_add_of_mem_closure diff_subset (notMem_diff_of_mem (mem_singleton i.1)) hz',
          add_assoc hs.base, ← succ_nsmul', hs.floor_add_nsmul_self, hs.floor_base, zero_add] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    (⋃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      ⋃ (_ :
        Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
          {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i),
        {x : ι → ℕ |
          ∃ (y : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
              ∃ (z : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
                  ∃ (z' : ι → ℕ),
                    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                      x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z})
have refine : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3))
  (hi :
    Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
      {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i),
  IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    {x : ι ⊕ ι → ℕ |
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) (x ∘ Sum.inr) ∧
        ∃ (z : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
            ∃ (z' : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                x ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + x ∘ Sum.inr + z}
Tactic: refine .biUnion (toFinite _) fun i hi => .proj' ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    ({a : ι ⊕ ι → ℕ | Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) (a ∘ Sum.inr)} ∩
      {a : ι ⊕ ι → ℕ |
        ∃ (z : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
            ∃ (z' : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                a ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + z})
have apply : IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
  {a : ι ⊕ ι → ℕ |
    ∃ (z : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
        ∃ (z' : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
            a ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + z}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite (finite_singleton _)) (LinearMap.funLeft ℕ ℕ Sum.inr)