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.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:
⟨hs.fract x, ⟨hs.fract_mem_fundamentalDomain x, hx⟩, ∑ i, (hs.floor x i).toNat • i.1,
        ?_, ∑ i, (-hs.floor x i).toNat • i.1, ?_, ?_⟩

Premises used: Finset.univ, _private.0.IsProperLinearSet.floor, _private.0.IsProperLinearSet.fract, _private.0.IsProperLinearSet.fract_mem_fundamentalDomain, And.intro, Exists.intro, HSMul.hSMul, Int.toNat, 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)
h :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))
h₁ :
  Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))
h₂ :
  x + ∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ) =
    hs.fract (s := s) x + ∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ)
⊢ ∃ 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:
refine ⟨hs.fract x, ⟨hs.fract_mem_fundamentalDomain x, hx⟩, ∑ i, (hs.floor x i).toNat • i.1,
        ?_, ∑ i, (-hs.floor x i).toNat • i.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)
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))

Tactic:
sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

Premises used: _private.0.IsProperLinearSet.floor, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Int.toNat, sum_mem, Subtype.property
-- 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)
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))

Tactic:
exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

Premises used: nsmul_mem, AddSubmonoid.mem_closure_of_mem, 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)
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))

Tactic:
sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

Premises used: _private.0.IsProperLinearSet.floor, nsmul_mem, AddSubmonoid.mem_closure_of_mem, Int.toNat, sum_mem, Neg.neg, Subtype.property
-- 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)
⊢ Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
    (∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))

Tactic:
exact sum_mem fun i _ => nsmul_mem (mem_closure_of_mem i.2) _

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

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

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 u : ι → ℕ
hu : u ∈ hs.fundamentalDomain (s := s)
hu' : u ∉ {hs.base (s := s)}
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
y' : ι → ℕ
hy' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y'
heq : x + y' = u + y
⊢ hs.fract (s := s) (x + y') = hs.fract (s := s) (u + y)

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 u : ι → ℕ
hu : u ∈ hs.fundamentalDomain (s := s)
hu' : u ∉ {hs.base (s := s)}
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
y' : ι → ℕ
hy' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y'
heq : hs.fract (s := s) (x + y') = hs.fract (s := s) (u + y)
⊢ hs.fract (s := s) x = u

Tactic:
rw [hs.fract_add_of_mem_closure hy', hs.fract_add_of_mem_closure hy,
        hs.fract_eq_self_of_mem_fundamentalDomain hu] at heq

Premises used: _private.0.IsProperLinearSet.fract_eq_self_of_mem_fundamentalDomain, _private.0.IsProperLinearSet.fract_add_of_mem_closure
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x u : ι → ℕ
hu : u ∈ hs.fundamentalDomain (s := s)
hu' : u ∉ {hs.base (s := s)}
y : ι → ℕ
hy : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y
y' : ι → ℕ
hy' : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y'
heq : hs.fract (s := s) x = u
h h₁ h₂ h₃ : u ≠ hs.base (s := s)
⊢ hs.fract (s := s) x ≠ hs.base (s := s)

Tactic:
rwa [heq]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ 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})

Tactic:
.biUnion hs.finite_fundamentalDomain.diff fun i hi => .proj' ?_

Premises used: IsSemilinearSet.biUnion, _private.0.IsProperLinearSet.finite_fundamentalDomain, Set.Finite.diff, IsSemilinearSet.proj'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
refine :
  ∀ (i : ι → ℕ) (hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}),
    IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
      {x : ι ⊕ ι → ℕ |
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) (x ∘ Sum.inr) ∧
          ∃ (y' : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧
              x ∘ Sum.inl + y' = i + x ∘ Sum.inr}
⊢ 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})

Tactic:
refine .biUnion hs.finite_fundamentalDomain.diff fun i hi => .proj' ?_
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
apply :
  IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    {a : ι ⊕ ι → ℕ |
      ∃ (y' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧
          a ∘ Sum.inl + y' = i + a ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    ({a : ι ⊕ ι → ℕ | Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) (a ∘ Sum.inr)} ∩
      {a : ι ⊕ ι → ℕ |
        ∃ (y' : ι → ℕ),
          Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧
            a ∘ Sum.inl + y' = i + a ∘ Sum.inr})

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

Premises used: _private.0.Nat.isSemilinearSet_preimage, _private.0.Nat.isSemilinearSet_inter, IsSemilinearSet.closure_of_finite, _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 : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
a :
  IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {x : (ι ⊕ ι) ⊕ ι → ℕ |
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) (x ∘ Sum.inr) ∧
        (x ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr = i + (x ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    {a : ι ⊕ ι → ℕ |
      ∃ (y' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧
          a ∘ Sum.inl + y' = i + a ∘ Sum.inr}

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

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

Premises used: _private.0.Nat.isSemilinearSet_preimage, _private.0.Nat.isSemilinearSet_inter, IsSemilinearSet.closure_of_finite, _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 : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
a :
  ∀ (this : Fintype ι),
    IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
      {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (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 : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
this : Fintype ι
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {x : (ι ⊕ ι) ⊕ ι → ℕ |
      HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols 1 0) 1 *ᵥ x) = i + fromCols (fromCols 0 1) 0 *ᵥ x}

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

Premises used: Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
this : Fintype ι
h :
  ∀ (x : (ι ⊕ ι) ⊕ ι → ℕ),
    (x ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr = HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols 1 0) 1 *ᵥ x)
h₁ : ∀ (x : (ι ⊕ ι) ⊕ ι → ℕ), i + (x ∘ Sum.inl) ∘ Sum.inr = i + fromCols (fromCols 0 1) 0 *ᵥ x
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}

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

Premises used: Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
this : Fintype ι
x : (ι ⊕ ι) ⊕ ι → ℕ
⊢ (x ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr = HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols 1 0) 1 *ᵥ x)

Tactic:
simp [fromCols_mulVec]

Premises used: Matrix.fromCols_mulVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
this : Fintype ι
x : (ι ⊕ ι) ⊕ ι → ℕ
⊢ i + (x ∘ Sum.inl) ∘ Sum.inr = i + fromCols (fromCols 0 1) 0 *ᵥ x

Tactic:
simp [fromCols_mulVec]

Premises used: Matrix.fromCols_mulVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
a a₁ a₂ :
  ∀ (this : Fintype ι),
    IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
      {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}

Tactic:
classical
    haveI := Fintype.ofFinite ι
    convert!
      Nat.isSemilinearSet_setOf_mulVec_eq (κ := (ι ⊕ ι) ⊕ ι) 0 i
        (Matrix.fromCols (Matrix.fromCols 1 0) 1) (Matrix.fromCols (Matrix.fromCols 0 1) 0) using
      4 <;> simp [fromCols_mulVec]

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

Tactic:
convert_to IsSemilinearSet (⋃ i : hs.basisSet, { x | ∃ y ∈ closure {i.1},
    ∃ z ∈ closure (hs.basisSet \ {i.1}), ∃ z' ∈ closure (hs.basisSet \ {i.1}),
      x + i.1 + y + z' = hs.base + 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.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
⊢ hs.setOfFloorNeg (s := s) =
    ⋃ (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:
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)), 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
⊢ 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

Tactic:
simp only [setOfFloorNeg, mem_iUnion, mem_setOf_eq]

Premises used: _private.0.IsProperLinearSet.setOfFloorNeg, Set.mem_iUnion, Set.mem_setOf_eq
-- 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)), 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
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
⊢ (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
-- 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
⊢ ∃ (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:
⟨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, ?_, ?_⟩

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