-- 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 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 ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
this : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b
⊢ (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b ∈ s'.mulSpan

Tactic:
exact prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
obtain ⟨s', hs', hs'max⟩ :=
  exists_maximal (s.powerset.filter fun s' : Finset α ↦ MulDissociated (s' : Set α))
    ⟨∅, mem_filter.2 ⟨empty_mem_powerset _, by simp⟩⟩

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' ∈ 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

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'
⊢ a ∈ s'.mulSpan

Tactic:
exact subset_mulSpan ha'

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
⊢ MulDissociated ↑∅

Tactic:
simp

Result:
no goals

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' ⊆ s ∧ MulDissociated ↑s'
hs'max : ∀ x ⊆ s, MulDissociated ↑x → ¬s' ⊂ x
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
refine ⟨s', hs'.1, hs _ hs'.1 hs'.2, fun a ha ↦ ?_⟩

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
a : α
ha : a ∈ s
⊢ a ∈ s'.mulSpan

Proof state:
α : 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 ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
⊢ a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b

Tactic:
rw [prod_erase_eq_div hau, htu.2.2, div_div_self']

Result:
no goals

Proof state:
case neg
α : 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 ⊆ s'
hu : u ⊆ s'
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∉ u
⊢ a ∈ s'.mulSpan

Tactic:
cases not_mulDissociated_iff_exists_disjoint.2 ⟨t, u, ht, hu, htu⟩ hs'.2

Result:
no goals

Proof state:
α : 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 = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b

Tactic:
rw [prod_erase_eq_div hat, htu.2.2, div_div_self']

Result:
no goals

Proof state:
case neg.intro.intro.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
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
⊢ a ∈ s'.mulSpan

Tactic:
by_cases hat : a ∈ t

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
⊢ a ∈ s'.mulSpan

case neg
α : 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

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 ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
⊢ a ∈ s'.mulSpan

Tactic:
have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
  rw [prod_erase_eq_div hau, 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 ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
this : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b
⊢ a ∈ s'.mulSpan