awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z' = hs.base (s := s) + z
⊢ hs.floor (s := s) x i < 0
have heq₁ : hs.floor (s := s) (x + (↑i : ι → ℕ) + n • (↑i : ι → ℕ) + z') i = hs.floor (s := s) (hs.base (s := s) + z) i
Tactic: apply congr_arg (hs.floor · i) 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 : ι → ℕ
i : (↑(hs.basisSet (s := s)) : Type u_3)
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 • (↑i : ι → ℕ) + z') i = hs.floor (s := s) (hs.base (s := s) + z) i
⊢ hs.floor (s := s) x i < 0
have heq₁ : 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',
          hs.floor_base, add_assoc x, ← succ_nsmul', hs.floor_add_nsmul_self,
          ← eq_neg_iff_add_eq_zero] 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 ι
⊢ 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})
have refine : ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
  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 + (↑i : ι → ℕ) + x ∘ Sum.inr + z' = hs.base (s := s) + z}
Tactic: refine .iUnion fun i => .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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z})
have 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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite (finite_singleton _)) (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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 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 + (↑i : ι → ℕ) + a ∘ Sum.inr + z' = hs.base (s := s) + z}
have 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 + (↑i : ι → ℕ) + (x ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + x ∘ 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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 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 + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr})
have a : IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
  {a : (ι ⊕ ι) ⊕ ι → ℕ |
    ∃ (z' : ι → ℕ),
      Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
        (a ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ IsSemilinearSet.{u_3} (M := (ι ⊕ ι) ⊕ ι → ℕ)
    {a : (ι ⊕ ι) ⊕ ι → ℕ |
      ∃ (z' : ι → ℕ),
        Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
          (a ∘ Sum.inl) ∘ Sum.inl + (↑i : ι → ℕ) + (a ∘ Sum.inl) ∘ Sum.inr + z' = hs.base (s := s) + a ∘ Sum.inr}
have 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 + (↑i : ι → ℕ) + ((x ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + x ∘ Sum.inr =
        hs.base (s := s) + (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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 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})
have 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}
Tactic: apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (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 : (↑(hs.basisSet (s := s)) : Type u_3)
⊢ 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}
have 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}
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 : (↑(hs.basisSet (s := s)) : Type u_3)
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}
have 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
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ 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}
have h₁ : ∀ (x : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ),
  hs.base (s := s) + (x ∘ Sum.inl) ∘ Sum.inr = hs.base (s := s) + fromCols (fromCols (fromCols 0 0) 1) 0 *ᵥ x
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
-- 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.setOfFloorPos (s := s))
have 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}
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
-- 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.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}
⊢ IsSemilinearSet (hs.setOfFloorPos (s := s))
have 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})
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
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ 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}
have 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
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.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
have 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
Tactic: simp only [setOfFloorPos, 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.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
have 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
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.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
⊢ (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
have 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
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.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
have h : Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) (((hs.floor (s := s) x i).toNat - 1) • (↑i : ι → ℕ))
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, ?_, ?_⟩