-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
obtain :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ∈ {s' ∈ s.powerset | MulDissociated (↑s' : Set α)}) s'),
    ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
obtain₁ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'),
    ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
obtain₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
    a ∈ s'.mulSpan
pos :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∈ s'), a ∈ s'.mulSpan
neg neg₁ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s'), a ∈ s'.mulSpan
neg₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α))
    (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)) (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)),
    a ∈ s'.mulSpan
pos₁ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α))
    (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)) (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a))
    (hat : a ∈ t), a ∈ s'.mulSpan
neg₃ neg₄ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : (↑t : Set α) ⊆ (↑(insert a s') : Set α))
    (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)) (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a))
    (hat : a ∉ t), a ∈ s'.mulSpan
neg₅ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : t ⊆ s') (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α))
    (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)) (hat : a ∉ t), a ∈ s'.mulSpan
pos₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : t ⊆ s') (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α))
    (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)) (hat : a ∉ t) (hau : a ∈ u), a ∈ s'.mulSpan
neg₆ neg₇ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s') (t u : Finset α) (ht : t ⊆ s') (hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α))
    (htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)) (hat : a ∉ t) (hau : a ∉ u), a ∈ s'.mulSpan
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
classical
  obtain ⟨s', hs'⟩ :=
    (s.powerset.filter fun s' : Finset α ↦ MulDissociated (s' : Set α)).exists_maximal
      ⟨∅, mem_filter.2 ⟨empty_mem_powerset _, by simp⟩⟩
  simp only [mem_filter, mem_powerset] at hs'
  refine ⟨s', hs'.1.1, hs _ hs'.1.1 hs'.1.2, fun a ha ↦ ?_⟩
  by_cases ha' : a ∈ s'
  · exact subset_mulSpan ha'
  obtain ⟨t, u, ht, hu, htu⟩ := not_mulDissociated_iff_exists_disjoint.1 fun h ↦
    hs'.not_gt ⟨insert_subset_iff.2 ⟨ha, hs'.1.1⟩, h⟩ <| ssubset_insert ha'
  by_cases hat : a ∈ t
  · have : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b := by
      rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
    rw [this]
    exact prod_div_prod_mem_mulSpan
      ((subset_insert_iff_of_notMem <| disjoint_left.1 htu.1 hat).1 hu) (subset_insert_iff.1 ht)
  rw [coe_subset, subset_insert_iff_of_notMem hat] at ht
  by_cases hau : a ∈ u
  · have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
      rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
    rw [this]
    exact prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)
  · rw [coe_subset, subset_insert_iff_of_notMem hau] at hu
    cases not_mulDissociated_iff_exists_disjoint.2 ⟨t, u, ht, hu, htu⟩ hs'.1.2

Premises used: Finset.mem_powerset, Finset.mem_filter, Finset.coe_subset