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 : ι → ℕ
⊢ x ∈ hs.setOfFloorNeg (s := s) ↔
    Membership.mem (γ := Set (ι → ℕ))
      (⋃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
        {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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z})
      x
have h : (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ↔
  ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
Tactic: simp only [setOfFloorNeg, mem_iUnion, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ↔
    ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
have h : (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) →
  ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
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 : ι → ℕ
h :
  (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) →
    ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
⊢ (hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ↔
    ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
have h₁ : (∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z) →
  hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), 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 : ι → ℕ
hx : hs.fract (s := s) x = hs.base (s := s)
i : (↑(hs.basisSet (s := s)) : Type u_3)
hi : hs.floor (s := s) x i < 0
⊢ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
have h : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)})
  (((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
Tactic: refine ⟨i, ((- 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 : hs.floor (s := s) x i < 0
h :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)})
    (((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
⊢ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + 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, ((- 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 : hs.floor (s := s) x i < 0
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)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + 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, ((- 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 : hs.floor (s := s) x i < 0
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)) (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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
have h₃ : x + (↑i : ι → ℕ) + ((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ) +
    ∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ) =
  hs.base (s := s) + ∑ j ∈ Finset.erase Finset.univ i, (hs.floor (s := s) x j).toNat • (↑j : ι → ℕ)
Tactic: refine ⟨i, ((- 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 : hs.floor (s := s) x i < 0
⊢ 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 : hs.floor (s := s) x i < 0
⊢ 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 : hs.floor (s := s) x i < 0
⊢ x + (↑i : ι → ℕ) + ((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ) +
      ∑ j ∈ Finset.erase Finset.univ i, (-hs.floor (s := s) x j).toNat • (↑j : ι → ℕ) =
    hs.base (s := s) + ∑ 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 x, ← succ_nsmul',
          tsub_add_cancel_of_le
            ((Int.le_toNat (neg_pos.2 hi).le).2 (le_neg.1 (Int.cast_le_neg_one_of_neg hi))),
          add_assoc x,
          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 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)
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
⊢ hs.fract (s := s) x = hs.base (s := s) ∧ ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0
have h : hs.fract (s := s) x = hs.base (s := s)
Tactic: refine ⟨?_, 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 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + 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)), hs.floor (s := s) x i < 0
have h₁ : hs.floor (s := s) x i < 0
Tactic: refine ⟨?_, i, ?_⟩
-- 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)
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
⊢ hs.fract (s := s) x = hs.base (s := s)
have heq₁ : hs.fract (s := s) (x + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + 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)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)
⊢ hs.fract (s := s) x = hs.base (s := s)
have h : ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ) + y) = hs.fract (s := s) (hs.base (s := s) + 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)
h :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ) + y) = hs.fract (s := s) (hs.base (s := s) + 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 + (↑i : ι → ℕ)) = hs.fract (s := s) (hs.base (s := s) + 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)
h :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ) + y) = hs.fract (s := s) (hs.base (s := s) + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ)) = hs.fract (s := s) (hs.base (s := s) + 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) + 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)
h :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ) + y) = hs.fract (s := s) (hs.base (s := s) + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ)) = hs.fract (s := s) (hs.base (s := s) + 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) + 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))), 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)
h :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ) + y) = hs.fract (s := s) (hs.base (s := s) + z)),
    hs.fract (s := s) x = hs.base (s := s)
h₁ :
  ∀ (heq : hs.fract (s := s) (x + (↑i : ι → ℕ)) = hs.fract (s := s) (hs.base (s := s) + 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) + 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))), 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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)
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
⊢ hs.floor (s := s) x i < 0
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z), hs.floor (s := s) x i < 0
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)
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 + (↑i : ι → ℕ) + y + z' = hs.base (s := s) + z
⊢ hs.floor (s := s) x i < 0
have h : ∀ (n : ℕ) (heq : x + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z' = hs.base (s := s) + z), hs.floor (s := s) x i < 0
Tactic: rcases hy with ⟨n, rfl⟩
Cleared hypotheses: y, hy, heq