-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  hs.setOfFloorPos (s := s) =
    ⋃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      ⋃ (_ :
        Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
          {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i),
        {x : ι → ℕ |
          ∃ (y : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
              ∃ (z : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
                  ∃ (z' : ι → ℕ),
                    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                      x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z}
convert_to convert_to₁ :
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    (⋃ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
      ⋃ (_ :
        Membership.mem (γ := Set (↑(hs.basisSet (s := s)) : Type u_3))
          {i : (↑(hs.basisSet (s := s)) : Type u_3) | (↑i : ι → ℕ) ∉ hs.periods (s := s)} i),
        {x : ι → ℕ |
          ∃ (y : ι → ℕ),
            Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure {(↑i : ι → ℕ)}) y ∧
              ∃ (z : ι → ℕ),
                Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z ∧
                  ∃ (z' : ι → ℕ),
                    Membership.mem (γ := AddSubmonoid (ι → ℕ)) (closure (hs.basisSet (s := s) \ {(↑i : ι → ℕ)})) z' ∧
                      x + z' = hs.base (s := s) + (↑i : ι → ℕ) + y + z})
⊢ IsSemilinearSet (hs.setOfFloorPos (s := s))

Tactic:
classical
  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
  · ext x
    simp only [setOfFloorPos, mem_iUnion, mem_setOf_eq, exists_prop]
    constructor
    · intro ⟨hx, i, hi, hi'⟩
      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, ?_, ?_⟩
      · exact nsmul_mem (mem_closure_of_mem (mem_singleton i.1)) _
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · refine sum_mem fun j hj => nsmul_mem (mem_closure_of_mem ?_) _
        simpa [Subtype.val_inj] using hj
      · rw [add_assoc hs.base, ← succ_nsmul',
          tsub_add_cancel_of_le ((Int.le_toNat hi'.le).2 (Int.add_one_le_of_lt hi')),
          add_assoc hs.base,
          Finset.add_sum_erase _ (fun j => (hs.floor x j).toNat • j.1) (Finset.mem_univ i),
          ← add_zero (Finset.sum (Finset.univ.erase i) _),
          ← zero_nsmul i.1, ← Int.toNat_eq_zero.2 (neg_neg_iff_pos.2 hi').le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x
    · intro ⟨i, hi, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, hi, ?_⟩
      · apply congr_arg hs.fract at heq
        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
      · rw [mem_closure_singleton] at hy
        rcases hy with ⟨n, rfl⟩
        apply congr_arg (hs.floor · i) at heq
        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
        simp [heq]
  · refine .biUnion (toFinite _) fun i hi => .proj' ?_
    rw [setOf_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite (finite_singleton _)) (LinearMap.funLeft ℕ ℕ Sum.inr)
    apply IsSemilinearSet.proj'
    rw [setOf_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (LinearMap.funLeft ℕ ℕ Sum.inr)
    apply IsSemilinearSet.proj'
    rw [setOf_and]
    apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet.diff) (LinearMap.funLeft ℕ ℕ Sum.inr)
    haveI := Fintype.ofFinite ι
    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
      <;> simp [add_assoc, fromCols_mulVec]

Premises used: _private.0.IsProperLinearSet.base, Set.setOf_and, _private.0.IsProperLinearSet.floor_add_nsmul_self, Subtype.val_inj, add_assoc, _private.0.IsProperLinearSet.setOfFloorPos, setOf, Set.mem_iUnion, _private.0.Nat.isSemilinearSet_preimage, _private.0.IsProperLinearSet.fract, _private.0.Nat.isSemilinearSet_inter, Membership.mem, Exists, IsSemilinearSet.closure_of_finite, _private.0.IsProperLinearSet.floor_base, Set.mem_setOf_eq, exists_prop, zero_add, Set.Finite.diff, _private.0.IsProperLinearSet.finite_basisSet, congr_arg, SDiff.sdiff, And, HAdd.hAdd, Sum.inr, IsSemilinearSet, LinearMap.funLeft, Nat, AddSubmonoid.closure, succ_nsmul', AddSubmonoid.mem_closure_singleton, Singleton.singleton, Subtype.val, Eq, Set.finite_singleton, IsSemilinearSet.proj', Set.iUnion, Matrix.fromCols_mulVec, _private.0.IsProperLinearSet.basisSet, _private.0.IsProperLinearSet.fract_base, rfl