-- Mathlib/Combinatorics/Additive/Dissociation.lean
/-- If every dissociated subset of `s` has size at most `d`, then `s` is actually generated by a
subset of size at most `d`.

This is a dissociation analog of the fact that a set whose linearly independent subsets all have
size at most `d` is of dimension at most `d` itself. -/
@[to_additive "If every dissociated subset of `s` has size at most `d`, then `s` is actually
generated by a subset of size at most `d`.

This is a dissociation analog of the fact that a set whose linearly independent subspaces all have
size at most `d` is of dimension at most `d` itself."]
lemma exists_subset_mulSpan_card_le_of_forall_mulDissociated
    (hs : ∀ s', s' ⊆ s → MulDissociated (s' : Set α) → s'.card ≤ d) :
    ∃ s', s' ⊆ s ∧ s'.card ≤ d ∧ s ⊆ mulSpan s'

Proof state:
case intro.intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ∈ filter (fun s' => MulDissociated ↑s') s.powerset
hs'max : ∀ x ∈ filter (fun s' => MulDissociated ↑s') s.powerset, ¬s' < x
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
simp only [mem_filter, mem_powerset, lt_eq_subset, and_imp] at hs' hs'max

Result:
case intro.intro
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Proof state:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ a ∈ s'.mulSpan

Tactic:
rw [this]

Result:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b ∈ s'.mulSpan

Proof state:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
⊢ a ∈ s'.mulSpan

Tactic:
have : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b := by
  rw [prod_erase_eq_div hat, htu.2.2, div_div_self']

Result:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : s' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : ↑t ⊆ ↑(insert a s')
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∈ t
this : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b
⊢ a ∈ s'.mulSpan