awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
⊢ 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)
have 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
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)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ IsSemilinearSet (hs.setOfFractNe (s := s))
have 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}
Tactic: convert_to IsSemilinearSet (⋃ u ∈ hs.fundamentalDomain \ {hs.base}, { x |
    ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = u + y }) using 1
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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}
⊢ IsSemilinearSet (hs.setOfFractNe (s := s))
have 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})
Tactic: convert_to IsSemilinearSet (⋃ u ∈ hs.fundamentalDomain \ {hs.base}, { x |
    ∃ y ∈ closure hs.basisSet, ∃ y' ∈ closure hs.basisSet, x + y' = u + y }) using 1
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ 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}
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
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
have 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
Tactic: simp only [setOfFractNe, mem_iUnion, mem_setOf_eq, exists_prop]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ 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
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
have h : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
  (∑ i : (↑hs.basisSet : Type u_3), (hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))
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, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℕ))
⊢ ∃ 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
have h₁ : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s)))
  (∑ i : (↑hs.basisSet : Type u_3), (-hs.floor (s := s) x i).toNat • (↑i : ι → ℕ))
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, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℕ))
⊢ ∃ 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
have 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 : ι → ℕ)
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, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
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 ≠ hs.base (s := s)
have heq₁ : hs.fract (s := s) (x + y') = hs.fract (s := s) (u + y)
Tactic: apply congr_arg hs.fract at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
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 ≠ hs.base (s := s)
have heq₁ : 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
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ hs.fract (s := s) x ≠ hs.base (s := s)
have h : u ≠ hs.base (s := s)
Tactic: rwa [heq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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})
have 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}
Tactic: refine .biUnion hs.finite_fundamentalDomain.diff fun i hi => .proj' ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
⊢ 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})
have apply : 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 Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet) (LinearMap.funLeft ℕ ℕ Sum.inr)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ ι → ℕ)
    {a : ι ⊕ ι → ℕ |
      ∃ (y' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s))) y' ∧
          a ∘ Sum.inl + y' = i + a ∘ Sum.inr}
have 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}
Tactic: apply IsSemilinearSet.proj'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
⊢ 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})
have a : IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
  {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)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
have a : ∀ (this : Fintype ι),
  IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
have h : ∀ (x : (ι ⊕ ι) ⊕ ι → ℕ),
  (x ∘ Sum.inl) ∘ Sum.inl + x ∘ Sum.inr = HAdd.hAdd (α := ι → ℕ) 0 (fromCols (fromCols 1 0) 1 *ᵥ x)
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
have h₁ : ∀ (x : (ι ⊕ ι) ⊕ ι → ℕ), i + (x ∘ Sum.inl) ∘ Sum.inr = i + fromCols (fromCols 0 1) 0 *ᵥ x
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain (s := s) \ {hs.base (s := s)}
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
have a : ∀ (this : Fintype ι),
  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]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ IsSemilinearSet (hs.setOfFloorNeg (s := s))
have 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}
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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}
⊢ IsSemilinearSet (hs.setOfFloorNeg (s := s))
have 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})
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ 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}
have 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
Tactic: ext x