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 ι
i : (↑(hs.basisSet (s := s)) : Type u_3)
a :
  IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base (s := s) + (a ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    ({a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) (a ∘ Sum.inr)} ∩
      {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
          hs.base (s := s) + (a ∘ Sum.inl) ∘ 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 :
  ∀ (this : Fintype ι),
    IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
      {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
          hs.base (s := s) + (a ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base (s := s) + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
haveI := Fintype.ofFinite ι
-- 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)
this : Fintype ι
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      (↑i : ι → ℕ) + fromCols (fromCols (fromCols 1 1) 0) 1 *ᵥ x =
        hs.base (s := s) + fromCols (fromCols (fromCols 0 0) 1) 0 *ᵥ x}

Tactic:
Nat.isSemilinearSet_setOf_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) i.1 hs.base
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 1) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 0) 1) 0)

Premises used: _private.0.IsProperLinearSet.base, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat, Subtype.val
-- 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)
this : Fintype ι
h :
  ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
    ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr =
      (↑i : ι → ℕ) + fromCols (fromCols (fromCols 1 1) 0) 1 *ᵥ x
h₁ :
  ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
    hs.base (s := s) + (x ∘ Sum.inl) ∘ Sum.inr = hs.base (s := s) + fromCols (fromCols (fromCols 0 0) 1) 0 *ᵥ x
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + a ∘ Sum.inr =
        hs.base (s := s) + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
convert!
      Nat.isSemilinearSet_setOf_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) i.1 hs.base
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 1) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 0) 1) 0) using 4

Premises used: _private.0.IsProperLinearSet.base, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat, Subtype.val
-- 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)
this : Fintype ι
x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr =
    (↑i : ι → ℕ) + fromCols (fromCols (fromCols 1 1) 0) 1 *ᵥ x

Tactic:
simp [add_comm _ i.1, add_assoc, fromCols_mulVec]

Premises used: add_assoc, add_comm, Subtype.val, Matrix.fromCols_mulVec
-- 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)
this : Fintype ι
x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base (s := s) + (x ∘ Sum.inl) ∘ Sum.inr = hs.base (s := s) + fromCols (fromCols (fromCols 0 0) 1) 0 *ᵥ x

Tactic:
simp [add_comm _ i.1, add_assoc, fromCols_mulVec]

Premises used: add_assoc, add_comm, Subtype.val, Matrix.fromCols_mulVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  hs.setOfFloorPos (s := s) =
    ⋃ (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}
convert_to :
  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})
⊢ IsSemilinearSet (hs.setOfFloorPos (s := s))

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

Premises used: _private.0.IsProperLinearSet.base, setOf, Membership.mem, Exists, SDiff.sdiff, And, HAdd.hAdd, IsSemilinearSet, AddSubmonoid.closure, Singleton.singleton, Subtype.val, 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.setOfFloorPos (s := s) ↔
      Membership.mem (γ := Set (ι → ℕ))
        (⋃ (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})
        x
⊢ hs.setOfFloorPos (s := s) =
    ⋃ (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}

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.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x 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
⊢ x ∈ hs.setOfFloorPos (s := s) ↔
    Membership.mem (γ := Set (ι → ℕ))
      (⋃ (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})
      x

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

Premises used: _private.0.IsProperLinearSet.setOfFloorPos, Set.mem_iUnion, 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.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x 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
h₁ :
  (∃ (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) →
    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
⊢ (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) ↔
    ∃ (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

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

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

Premises used: Finset.univ, _private.0.IsProperLinearSet.floor, HSub.hSub, And.intro, Exists.intro, HSMul.hSMul, Int.toNat, OfNat.ofNat, 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 : (↑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 : ι → ℕ))
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 : ι → ℕ)
⊢ ∃ (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

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, ?_, ?_⟩
-- 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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ 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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ 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 : (↑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 : ι → ℕ))

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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
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 + ∑ 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:
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]

Premises used: Iff.mpr, Finset.mem_univ, _private.0.IsProperLinearSet.base, neg_neg_iff_pos, Int.le_toNat, Finset.univ, add_assoc, _private.0.IsProperLinearSet.floor, Int.add_one_le_of_lt, tsub_add_cancel_of_le, LT.lt.le, Finset.add_sum_erase, Finset.sum_erase_add, zero_nsmul, succ_nsmul', HSMul.hSMul, Int.toNat, Int.toNat_eq_zero, add_zero, Finset.erase, Subtype.val, Finset.sum
-- 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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ 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 : (↑i : ι → ℕ) ∉ hs.periods (s := s)
hi' : 0 < hs.floor (s := s) x i
⊢ 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)
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

Tactic:
⟨?_, i, hi, ?_⟩

Premises used: And.intro, Exists.intro