-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
let let₁ let₂ : ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
let₃ let₄ :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s), ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
let₅ :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s),
    let g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0});
    ∀ (hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y), ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
let₆ :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s),
    let g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0});
    ∀ (hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y) (a : M) (ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a),
      ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
let₇ :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s),
    let g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0});
    ∀ (hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y) (a : M) (ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a),
      IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}
h :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s),
    let g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0});
    ∀ (hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y) (a : M) (ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a),
      {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)
let₈ let₉ :
  let f : (x : M) → AddSubmonoid M := fun (x : M) ↦
    if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥;
  ∀ (hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s),
    let g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0});
    ∀ (hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y) (a : M) (ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a),
      IsSemilinearSet (a +ᵥ (↑(f a) : Set M))
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}

Tactic:
classical
  let f (x : M) : AddSubmonoid M :=
    if hx : x ∈ s then
      { carrier := { y | x + y ∈ s }
        zero_mem' := by simpa
        add_mem' := by
          intro a b ha hb
          simp only [mem_setOf_eq] at *
          rw [← add_assoc]
          exact hs _ hx _ _ ha hb }
    else ⊥
  have hf : ∀ x ∈ s, ∀ y, y ∈ f x ↔ x + y ∈ s := by simp_all [f]
  let g (x : M) : AddSemigroupIdeal M := .closure (f x \ {0})
  have hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y := by
    intro x hx y hy hxy z hz
    rw [le_iff_exists_add] at hxy
    rcases hxy with ⟨y, rfl⟩
    simp only [AddSemigroupIdeal.mem_closure'', mem_diff, SetLike.mem_coe, mem_singleton_iff,
      g] at hz ⊢
    rcases hz with ⟨y', z, ⟨hz₁, hz₂⟩, rfl⟩
    rw [hf _ hx] at hz₁
    refine ⟨y', z, ⟨?_, hz₂⟩, rfl⟩
    rw [hf _ hy]
    exact hs _ hx _ _ hy hz₁
  rcases exists_maximalFor_of_wellFoundedGT (· ∈ s) g hs' with ⟨a, ha⟩
  refine ⟨a, ha.1, ?_⟩
  convert_to IsSemilinearSet (a +ᵥ (f a : Set M))
  · ext x
    simp only [le_iff_exists_add, mem_setOf_eq, ha.1, ↓reduceDIte, coe_set_mk,
      AddSubsemigroup.coe_set_mk, mem_vadd_set, vadd_eq_add, f]
    grind
  · refine IsSemilinearSet.vadd a (.of_fg (AddSubmonoid.fg_of_subtractive ?_))
    intro x hx y hxy
    rw [hf _ ha.1] at hx
    rw [hf _ ha.1, ← add_assoc] at hxy
    by_cases hy : y = 0
    · simp [hy]
    replace hy : y ∈ g (a + x) := by
      apply AddSemigroupIdeal.subset_closure
      refine Set.mem_diff_of_mem ?_ hy
      rwa [SetLike.mem_coe, hf _ hx]
    apply ha.2 hx (hg _ ha.1 _ hx le_self_add) at hy
    simp only [g, AddSemigroupIdeal.mem_closure'', Set.mem_diff, SetLike.mem_coe,
      Set.notMem_singleton_iff] at hy
    rcases hy with ⟨w, u, ⟨hu₁, hu₂⟩, rfl⟩
    induction w using WellQuasiOrderedLE.to_wellFoundedLT.induction (α := M) generalizing u with
      | _ w ih
    by_cases hw₁ : w = 0
    · simpa [hw₁]
    have hxu : a + x + u ∈ s := hs _ ha.1 _ _ hx (by rwa [hf _ ha.1] at hu₁)
    have hw₂ : w ∈ g (a + x + u) := by
      apply AddSemigroupIdeal.subset_closure
      refine Set.mem_diff_of_mem ?_ hw₁
      rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]
    apply ha.2 hxu (hg _ ha.1 _ hxu (le_add_right le_self_add)) at hw₂
    simp only [g, AddSemigroupIdeal.mem_closure'', Set.mem_diff, SetLike.mem_coe,
      Set.notMem_singleton_iff] at hw₂
    rcases hw₂ with ⟨w', u', ⟨hu'₁, hu'₂⟩, rfl⟩
    rw [add_assoc]
    apply ih
    · exact lt_add_of_pos_right _ (pos_of_ne_zero hu'₂)
    · exact add_mem hu'₁ hu₁
    · simp [hu₂, hu'₂]
    · rwa [← add_assoc w']

Premises used: Set.mem_vadd_set, le_iff_exists_add, add_assoc, reduceDIte, Set.mem_setOf_eq, AddSemigroupIdeal.mem_closure'', WellFoundedLT.induction, Set.notMem_singleton_iff, SetLike.mem_coe, Set.mem_diff, vadd_eq_add, AddSubsemigroup.coe_set_mk, AddSubmonoid.coe_set_mk, rfl