-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
a₁ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    (a : ι → ℕ) (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
    (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
    IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
a₂ a₃ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty),
    IsSemilinearSet s
a₄ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
    (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}), IsSemilinearSet s
h :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
    (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}),
    s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}
a₅ a₆ :
  ∀ (t : Finset ι)
    (ih :
      ∀ t_1 ⊂ t,
        ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
    {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i) (hs' : s.Nonempty) (x : ι → ℕ)
    (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}),
    IsSemilinearSet.{u_1} (M := ι → ℕ)
      ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j})
⊢ IsSemilinearSet s

Tactic:
classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]

Premises used: Set.mem_union, Function.update, Set.mem_iUnion, Set.mem_setOf_eq, Finset.mem_range, Set.eq_empty_or_nonempty, Pi.le_def, rfl