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 : ι → ℕ
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)
⊢ 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:
simp only [mem_vadd_set, SetLike.mem_coe, vadd_eq_add]

Premises used: Set.mem_vadd_set, SetLike.mem_coe, vadd_eq_add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
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
⊢ (∃ (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
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)

Tactic:
⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩

Premises used: And.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
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
⊢ 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)

Tactic:
refine ⟨?_, fun i => ⟨?_, fun hi => ?_⟩⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
mp : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
⊢ hs.fract (s := s) (hs.base (s := s) + y) = hs.base (s := s)

Tactic:
rw [hs.fract_add_of_mem_closure, hs.fract_base]

Premises used: _private.0.IsProperLinearSet.fract_add_of_mem_closure, _private.0.IsProperLinearSet.fract_base
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y

Tactic:
closure_mono hs.periods_subset_basisSet hy

Premises used: _private.0.IsProperLinearSet.periods_subset_basisSet, AddSubmonoid.closure_mono
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y

Tactic:
exact closure_mono hs.periods_subset_basisSet hy

Premises used: _private.0.IsProperLinearSet.periods_subset_basisSet, AddSubmonoid.closure_mono
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
mp : hs.floor (s := s) (hs.base (s := s)) i ≤ hs.floor (s := s) (hs.base (s := s) + y) i
⊢ 0 ≤ hs.floor (s := s) (hs.base (s := s) + y) i

Tactic:
rw [← hs.floor_base i]

Premises used: _private.0.IsProperLinearSet.floor_base
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
⊢ hs.floor (s := s) (hs.base (s := s)) i ≤ hs.floor (s := s) (hs.base (s := s) + y) i

Tactic:
hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)

Premises used: _private.0.IsProperLinearSet.periods_subset_basisSet, _private.0.IsProperLinearSet.floor_le_floor_add_of_mem_closure, AddSubmonoid.closure_mono
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
⊢ hs.floor (s := s) (hs.base (s := s)) i ≤ hs.floor (s := s) (hs.base (s := s) + y) i

Tactic:
exact hs.floor_le_floor_add_of_mem_closure (closure_mono hs.periods_subset_basisSet hy)

Premises used: _private.0.IsProperLinearSet.periods_subset_basisSet, _private.0.IsProperLinearSet.floor_le_floor_add_of_mem_closure, AddSubmonoid.closure_mono
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
mp₁ mp₂ : Eq (α := ℤ) 0 0
⊢ hs.floor (s := s) (hs.base (s := s) + y) i = 0

Tactic:
rw [hs.floor_add_of_mem_closure hs.periods_subset_basisSet hi hy, hs.floor_base]

Premises used: _private.0.IsProperLinearSet.periods_subset_basisSet, _private.0.IsProperLinearSet.floor_add_of_mem_closure, _private.0.IsProperLinearSet.floor_base
-- 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)
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

Tactic:
⟨∑ 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) _, ?_⟩

Premises used: Finset.univ, _private.0.IsProperLinearSet.floor, Membership.mem, nsmul_mem, _private.0.IsProperLinearSet.periods, AddSubmonoid.mem_closure_of_mem, And.right, And.intro, Exists.intro, Iff.mp, Finset.mem_filter, HSMul.hSMul, Int.toNat, Subtype.val, Finset.filter, Finset.sum, 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)
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)
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
⊢ ∃ (y : ι → ℕ), Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.periods (s := s))) y ∧ hs.base (s := s) + y = 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) _, ?_⟩
-- 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)
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)
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
⊢ 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:
rw [Finset.sum_filter, ← hx₁]

Premises used: Finset.sum_filter
-- 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)
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)
rw : x + ∑ _x : (↑hs.basisSet : Type u_3), 0
| x

Tactic:
rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]

Premises used: Finset.sum_const_zero, add_zero
-- 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)
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)
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
⊢ (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:
conv_rhs =>
      rw [← add_zero x, ← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)]

Premises used: Finset.sum_const_zero, add_zero
-- 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)
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 + ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
(hs.add_floor_neg_toNat_sum_eq x).symm

Premises used: _private.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq, Eq.symm
-- 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)
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 : ι → ℕ)
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 : ι → ℕ)
⊢ (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:
convert! (hs.add_floor_neg_toNat_sum_eq x).symm using 3 with i _ i

Premises used: _private.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq, Eq.symm
-- 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)
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 : ι → ℕ)
neg : ∀ (hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)), 0 = (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 : ι → ℕ)

Tactic:
split_ifs with hi
-- 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)
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
hi : (↑i : ι → ℕ) ∈ hs.periods (s := s)
⊢ (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) = (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
simp
-- 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)
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
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
⊢ 0 = (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
simp [(hx₂ i).2 hi]

Premises used: And.right
-- 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)
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
⊢ 0 = (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)

Tactic:
simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]

Premises used: Iff.mpr, neg_nonpos, And.left, Int.toNat_eq_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
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)
mpr 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
⊢ 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)

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)]

Premises used: Set.mem_vadd_set, _private.0.IsProperLinearSet.floor_base, Finset.sum_const_zero, _private.0.IsProperLinearSet.fract_add_of_mem_closure, SetLike.mem_coe, _private.0.IsProperLinearSet.add_floor_neg_toNat_sum_eq, vadd_eq_add, add_zero, Finset.sum_filter, Eq.symm, _private.0.IsProperLinearSet.eq_base_vadd_closure_periods, _private.0.IsProperLinearSet.fract_base, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  hs.setOfFractNe (s := s) =
    ⋃ u ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      {x : ι → ℕ |
        ∃ (y : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
            ∃ (y' : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = u + y}
convert_to :
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    (⋃ u ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      {x : ι → ℕ |
        ∃ (y : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
            ∃ (y' : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = u + y})
⊢ IsSemilinearSet (hs.setOfFractNe (s := s))

Tactic:
convert_to IsSemilinearSet (⋃ u ∈ hs.fundamentalDomain \ {hs.base}, { x |
    ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = u + y }) using 1

Premises used: setOf, Membership.mem, Exists, And, HAdd.hAdd, IsSemilinearSet, AddSubmonoid.closure, Eq, Set.iUnion, _private.0.IsProperLinearSet.basisSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  ∀ (x : ι → ℕ),
    x ∈ hs.setOfFractNe (s := s) ↔
      Membership.mem (γ := Set (ι → ℕ))
        (⋃ u ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
          {x : ι → ℕ |
            ∃ (y : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
                ∃ (y' : ι → ℕ),
                  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = u + y})
        x
⊢ hs.setOfFractNe (s := s) =
    ⋃ u ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      {x : ι → ℕ |
        ∃ (y : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
            ∃ (y' : ι → ℕ),
              Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = u + y}

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
h :
  hs.fract (s := s) x ≠ hs.base (s := s) ↔
    ∃ i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
          ∃ (y' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = i + y
⊢ x ∈ hs.setOfFractNe (s := s) ↔
    Membership.mem (γ := Set (ι → ℕ))
      (⋃ u ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
        {x : ι → ℕ |
          ∃ (y : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
              ∃ (y' : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = u + y})
      x

Tactic:
simp only [setOfFractNe, mem_iUnion, mem_setOf_eq, exists_prop]

Premises used: Set.mem_iUnion, _private.0.IsProperLinearSet.setOfFractNe, Set.mem_setOf_eq, exists_prop
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
h :
  hs.fract (s := s) x ≠ hs.base (s := s) →
    ∃ i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
          ∃ (y' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = i + y
h₁ :
  (∃ i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
          ∃ (y' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = i + y) →
    hs.fract (s := s) x ≠ hs.base (s := s)
⊢ hs.fract (s := s) x ≠ hs.base (s := s) ↔
    ∃ i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)},
      ∃ (y : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y ∧
          ∃ (y' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧ x + y' = i + y

Tactic:
constructor