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 : ι → ℕ
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
h : hs.fract (s := s) x = hs.base (s := s)
h₁ : 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

Tactic:
refine ⟨?_, i, hi, ?_⟩
-- 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 + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + 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)
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 : hs.fract (s := s) (x + z') = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + z)
h :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + y + 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) + (↑i : ι → ℕ) + y)),
    hs.fract (s := s) x = hs.base (s := s)
h₂ :
  ∀ (heq : hs.fract (s := s) x = hs.fract (s := s) (hs.base (s := s) + (↑i : ι → ℕ))),
    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 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_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)
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
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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z), 0 < hs.floor (s := s) x i
⊢ 0 < hs.floor (s := s) x i

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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z
h : ∀ (n : ℕ) (heq : x + z' = hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z), 0 < hs.floor (s := s) x i
⊢ 0 < hs.floor (s := s) x i

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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z
⊢ hs.floor (s := s) (x + z') i = hs.floor (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
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 + z') i = hs.floor (s := s) (hs.base (s := s) + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + 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',
          add_assoc hs.base, ← succ_nsmul', hs.floor_add_nsmul_self, hs.floor_base, zero_add] at heq

Premises used: Set.mem_singleton, _private.0.IsProperLinearSet.base, 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, zero_add, succ_nsmul', 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)
hi : (↑i : ι → ℕ) ∉ hs.periods (s := s)
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) : ℤ)
⊢ 0 < hs.floor (s := s) x i

Tactic:
simp [heq]
-- 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)),
      ⋃ (_ :
        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:
.biUnion (toFinite _) fun i hi => .proj' ?_

Premises used: IsSemilinearSet.biUnion, Set.toFinite, 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))
    (hi :
      Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
        {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i),
    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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + x ∘ Sum.inr + z}
⊢ 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})

Tactic:
refine .biUnion (toFinite _) fun i hi => .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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + 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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + (x ∘ Sum.inl) ∘ Sum.inr + 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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + a ∘ Sum.inr + 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
a :
  IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ |
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (a ∘ Sum.inl) ∘ Sum.inl + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + 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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
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 + x ∘ Sum.inr =
          hs.base (s := s) + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (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 + z' = hs.base (s := s) + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + 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 : (↑(hs.basisSet (s := s)) : Type u_3)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
a :
  IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (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 + a ∘ Sum.inr =
          hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
a :
  ∀ (this : Fintype ι),
    IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
      {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
        ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
          hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols (fromCols 1 0) 0) 1 *ᵥ x) =
        hs.base (s := s) + (↑i : ι → ℕ) + fromCols (fromCols (fromCols 0 1) 1) 0 *ᵥ x}

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

Premises used: _private.0.IsProperLinearSet.base, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, HAdd.hAdd, 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
h :
  ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
    ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
      HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols (fromCols 1 0) 0) 1 *ᵥ x)
h₁ :
  ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
    hs.base (s := s) + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x ∘ Sum.inl) ∘ Sum.inr =
      hs.base (s := s) + (↑i : ι → ℕ) + fromCols (fromCols (fromCols 0 1) 1) 0 *ᵥ x
⊢ IsSemilinearSet.{u_3} (M := ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ)
    {a : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ |
      ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr =
        hs.base (s := s) + (↑i : ι → ℕ) + ((a ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (a ∘ Sum.inl) ∘ Sum.inr}

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

Premises used: _private.0.IsProperLinearSet.base, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, HAdd.hAdd, 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr =
    HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols (fromCols 1 0) 0) 1 *ᵥ x)

Tactic:
simp [add_assoc, fromCols_mulVec]

Premises used: add_assoc, 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)
hi :
  Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
    {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i
this : Fintype ι
x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base (s := s) + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x ∘ Sum.inl) ∘ Sum.inr =
    hs.base (s := s) + (↑i : ι → ℕ) + fromCols (fromCols (fromCols 0 1) 1) 0 *ᵥ x

Tactic:
simp [add_assoc, fromCols_mulVec]

Premises used: add_assoc, Matrix.fromCols_mulVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ IsSemilinearSet (hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s)))

Tactic:
hs.isSemilinearSet_setOfFractNe.union <|
      hs.isSemilinearSet_setOfFloorNeg.union <| hs.isSemilinearSet_setOfFloorPos

Premises used: _private.0.IsProperLinearSet.isSemilinearSet_setOfFloorNeg, _private.0.IsProperLinearSet.isSemilinearSet_setOfFractNe, _private.0.IsProperLinearSet.isSemilinearSet_setOfFloorPos, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
h : sᶜ = hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
⊢ IsSemilinearSet sᶜ

Tactic:
convert!
    hs.isSemilinearSet_setOfFractNe.union <|
      hs.isSemilinearSet_setOfFloorNeg.union <| hs.isSemilinearSet_setOfFloorPos using 1

Premises used: _private.0.IsProperLinearSet.isSemilinearSet_setOfFloorNeg, _private.0.IsProperLinearSet.isSemilinearSet_setOfFractNe, _private.0.IsProperLinearSet.isSemilinearSet_setOfFloorPos, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
h : ∀ (x : ι → ℕ), x ∈ sᶜ ↔ x ∈ hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))
⊢ sᶜ = hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))

Tactic:
ext