-- 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 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:
classical
  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
  · ext x
    simp only [setOfFloorNeg, mem_iUnion, mem_setOf_eq]
    constructor
    · intro ⟨hx, i, hi⟩
      refine ⟨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, ?_, ?_⟩
      · 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 x, ← succ_nsmul',
          tsub_add_cancel_of_le
            ((Int.le_toNat (neg_pos.2 hi).le).2 (le_neg.1 (Int.cast_le_neg_one_of_neg hi))),
          add_assoc x,
          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 hi.le,
          Finset.sum_erase_add _ _ (Finset.mem_univ i), ← hx]
        exact hs.add_floor_neg_toNat_sum_eq x
    · intro ⟨i, y, hy, z, hz, z', hz', heq⟩
      refine ⟨?_, i, ?_⟩
      · 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 (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2),
          hs.fract_add_of_mem_closure (closure_mono diff_subset hz), 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',
          hs.floor_base, add_assoc x, ← succ_nsmul', hs.floor_add_nsmul_self,
          ← eq_neg_iff_add_eq_zero] at heq
        simpa [heq] using neg_one_lt_zero.trans_le (Nat.cast_nonneg _)
  · refine .iUnion fun i => .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 (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) 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
      <;> simp [add_comm _ i.1, add_assoc, fromCols_mulVec]

Premises used: _private.0.IsProperLinearSet.setOfFloorNeg, _private.0.IsProperLinearSet.base, Set.setOf_and, _private.0.IsProperLinearSet.floor_add_nsmul_self, Subtype.val_inj, Nat.cast_nonneg, add_assoc, 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, Set.Finite.diff, _private.0.IsProperLinearSet.finite_basisSet, congr_arg, SDiff.sdiff, And, HAdd.hAdd, Sum.inr, LT.lt.trans_le, IsSemilinearSet, LinearMap.funLeft, Nat, AddSubmonoid.closure, succ_nsmul', neg_one_lt_zero, eq_neg_iff_add_eq_zero, 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