-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
rw rw₁ rw₂ : ∀ (hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)), IsProperSemilinearSet s
rw₃ : ∀ (a : M) (t : Finset M), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
h :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (a : M) (t : Finset M) (hn : t.card = n), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
h₁ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))),
    IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
pos :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (hindep : LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
neg neg₁ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (hindep : ¬LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
neg₂ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (hindep :
      ∃ t_1 ⊆ t, ∃ (f : M → ℕ), Eq (α := M) (∑ i ∈ t_1, f i • id i) (∑ i ∈ t \ t_1, f i • id i) ∧ ∃ i ∈ t_1, 0 < f i),
    IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
neg₃ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (heq : Eq (α := M) (∑ i ∈ t', f i • id i) (∑ i ∈ t \ t', f i • id i))
    (i : M) (hi : i ∈ t') (hfi : 0 < f i), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
neg₄ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (i : M) (hi : i ∈ t') (hfi : 0 < f i)
    (heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)),
    IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
h₂ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (i : M) (hi : i ∈ t') (hfi : 0 < f i)
    (heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)),
    a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
      ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)
neg₅ neg₆ :
  ∀ (a : M) (t : Finset M)
    (ih :
      ∀ m < t.card,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (i : M) (hi : i ∈ t') (hfi : 0 < f i)
    (heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)),
    IsProperSemilinearSet.{u_1} (M := M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
⊢ IsProperSemilinearSet s

Tactic:
classical
  rw [isLinearSet_iff] at hs
  rcases hs with ⟨a, t, rfl⟩
  induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
  subst hn
  by_cases hindep : LinearIndepOn ℕ id (t : Set M)
  · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
  rw [not_linearIndepOn_finset_iffₒₛ] at hindep
  rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
  simp only [Function.id_def] at heq
  convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
  · ext x
    simp only [mem_vadd_set, SetLike.mem_coe]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [mem_closure_finset] at hy
      rcases hy with ⟨g, -, rfl⟩
      induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
      subst hn
      by_cases! hfg : ∀ j ∈ t', f j ≤ g j
      · convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
        conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
        simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
        congr! 2 with j hj
        rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
      · rcases hfg with ⟨j, hj, hgj⟩
        simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
        refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
        rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
    · simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
      rintro ⟨j, hj, k, hk, y, hy, rfl⟩
      refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
      rw [add_assoc]
  · exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl

Premises used: Finset.filter_notMem_eq_sdiff, Function.id_def, AddSubmonoid.mem_closure_finset, Set.mem_vadd_set, isLinearSet_iff, Finset.sum_add_distrib, add_assoc, Set.mem_iUnion, add_right_comm, Finset.sum_union, Finset.mem_range, add_left_cancel_iff, Disjoint.symm, add_smul, SetLike.mem_coe, vadd_eq_add, ite_smul, Finset.sdiff_disjoint, Finset.filter_mem_eq_inter, not_linearIndepOn_finset_iffₒₛ, Finset.sum_ite, rfl