awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
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 : ι → ℕ))
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 : ι → ℕ)
⊢ ∃ (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:
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, ?_, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 {(↑i : ι → ℕ)})
    (((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))

Tactic:
nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _

Premises used: Set.mem_singleton, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Subtype.val
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 {(↑i : ι → ℕ)})
    (((-hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))

Tactic:
exact nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _

Premises used: Set.mem_singleton, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Subtype.val
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 : ι → ℕ))

Tactic:
sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Premises used: _private.0.IsProperLinearSet.floor, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Int.toNat, sum_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 :
  ∀ (j : (↑(hs.basisSet (s := s)) : Type u_3)) (hj : j ∈ Finset.erase Finset.univ i),
    (↑j : ι → ℕ) ∈ hs.basisSet (s := s) \ {(↑i : ι → ℕ)}
⊢ 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 sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
j : (↑(hs.basisSet (s := s)) : Type u_3)
hj : j ∈ Finset.erase Finset.univ i
⊢ (↑j : ι → ℕ) ∈ hs.basisSet (s := s) \ {(↑i : ι → ℕ)}

Tactic:
simpa [Subtype.val_inj] using hj

Premises used: Subtype.val_inj
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 : ι → ℕ))

Tactic:
sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _

Premises used: _private.0.IsProperLinearSet.floor, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Int.toNat, sum_mem, Neg.neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 :
  ∀ (j : (↑(hs.basisSet (s := s)) : Type u_3)) (hj : j ∈ Finset.erase Finset.univ i),
    (↑j : ι → ℕ) ∈ hs.basisSet (s := s) \ {(↑i : ι → ℕ)}
⊢ 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 sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 :
  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 : ι → ℕ)
⊢ 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:
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]

Premises used: Iff.mpr, Finset.mem_univ, Int.cast_le_neg_one_of_neg, Int.le_toNat, Finset.univ, neg_pos, add_assoc, _private.0.IsProperLinearSet.floor, le_neg, tsub_add_cancel_of_le, LT.lt.le, Finset.add_sum_erase, Finset.sum_erase_add, zero_nsmul, succ_nsmul', Iff.mp, HSMul.hSMul, Int.toNat, Int.toNat_eq_zero, add_zero, Finset.erase, Subtype.val, Finset.sum, Neg.neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 + ∑ 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:
hs.add_floor_neg_toNat_sum_eq x

Premises used: _private.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 + ∑ 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:
exact hs.add_floor_neg_toNat_sum_eq x

Premises used: _private.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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

Tactic:
⟨?_, i, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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)
h₁ : hs.floor (s := s) x i < 0
⊢ 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:
refine ⟨?_, i, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + y + z') = hs.fract (s := s) (hs.base (s := s) + z)

Tactic:
apply congr_arg hs.fract at heq

Premises used: _private.0.IsProperLinearSet.fract, congr_arg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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)
h₄ h₅ h₆ h₇ : ∀ (heq : hs.fract (s := s) x = hs.base (s := s)), 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

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.diff_subset, AddSubmonoid.mem_closure_of_mem, _private.0.IsProperLinearSet.fract_add_of_mem_closure, _private.0.IsProperLinearSet.fract_base, AddSubmonoid.closure_mono, Subtype.property
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 :
  ∀ (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
⊢ hs.floor (s := s) x i < 0

Tactic:
rw [mem_closure_singleton] at hy

Premises used: AddSubmonoid.mem_closure_singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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
h : ∀ (n : ℕ) (heq : x + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z' = hs.base (s := s) + z), hs.floor (s := s) x i < 0
⊢ hs.floor (s := s) x i < 0

Tactic:
rcases hy with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z' = hs.base (s := s) + z
⊢ hs.floor (s := s) (x + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z') i = hs.floor (s := s) (hs.base (s := s) + z) i

Tactic:
apply congr_arg (hs.floor · i) at heq

Premises used: _private.0.IsProperLinearSet.floor, congr_arg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z') i = hs.floor (s := s) (hs.base (s := s) + z) i
⊢ 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',
          hs.floor_base, add_assoc x, ← succ_nsmul', hs.floor_add_nsmul_self,
          ← eq_neg_iff_add_eq_zero] at heq

Premises used: Set.mem_singleton, Set.diff_subset, _private.0.IsProperLinearSet.floor_add_of_mem_closure, _private.0.IsProperLinearSet.floor_add_nsmul_self, add_assoc, Set.notMem_diff_of_mem, _private.0.IsProperLinearSet.floor_base, succ_nsmul', eq_neg_iff_add_eq_zero, Subtype.val
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 i = -(↑(n + 1) : ℤ)
⊢ hs.floor (s := s) x i < 0

Tactic:
simpa [heq] using neg_one_lt_zero.trans_le (Nat.cast_nonneg _)

Premises used: Nat.cast_nonneg, LT.lt.trans_le, neg_one_lt_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    (⋃ (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})

Tactic:
.iUnion fun i => .proj' ?_

Premises used: IsSemilinearSet.iUnion, IsSemilinearSet.proj'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
refine :
  ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
    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 + (↑i : ι → ℕ) + x ∘ Sum.inr + z' = hs.base (s := s) + z}
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    (⋃ (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})

Tactic:
refine .iUnion fun i => .proj' ?_
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z}
⊢ 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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z})

Tactic:
apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite (finite_singleton _)) (LinearMap.funLeft ℕ ℕ Sum.inr)

Premises used: _private.0.Nat.isSemilinearSet_preimage, _private.0.Nat.isSemilinearSet_inter, IsSemilinearSet.closure_of_finite, Sum.inr, LinearMap.funLeft, Nat, Set.finite_singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
a :
  IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {x : (ι ⊕ ι) ⊕ ι → ℕ |
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (x ∘ Sum.inr) ∧
        ∃ (z' : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
            (x ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (x ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + x ∘ Sum.inr}
⊢ 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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z}

Tactic:
apply IsSemilinearSet.proj'

Premises used: IsSemilinearSet.proj'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
a :
  IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ |
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (a ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    ({a : (ι ⊕ ι) ⊕ ι → ℕ |
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (a ∘ Sum.inr)} ∩
      {a : (ι ⊕ ι) ⊕ ι → ℕ |
        ∃ (z' : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
            (a ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr})

Tactic:
apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (LinearMap.funLeft ℕ ℕ Sum.inr)

Premises used: _private.0.Nat.isSemilinearSet_preimage, _private.0.Nat.isSemilinearSet_inter, IsSemilinearSet.closure_of_finite, Set.Finite.diff, _private.0.IsProperLinearSet.finite_basisSet, Sum.inr, LinearMap.funLeft, Nat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
a :
  IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (x ∘ Sum.inr) ∧
        ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr =
          hs.base (s := s) + (x ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ |
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (a ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr}

Tactic:
apply IsSemilinearSet.proj'

Premises used: IsSemilinearSet.proj'