-- 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
⊢ 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 ⊆ 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

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

Tactic:
by_cases ha' : a ∈ s'

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'
⊢ 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'
⊢ 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 ⊆ ↑(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

Tactic:
exact prod_div_prod_mem_mulSpan
  ((subset_insert_iff_of_not_mem <| disjoint_left.1 htu.1 hat).1 hu) (subset_insert_iff.1 ht)

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 ⊆ ↑(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:
rw [coe_subset, subset_insert_iff_of_not_mem hat] at ht

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

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

Tactic:
by_cases hau : a ∈ u

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
⊢ 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 ⊆ 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

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 ⊆ ↑(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:
rw [coe_subset, subset_insert_iff_of_not_mem hau] at hu

Result:
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

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

Tactic:
obtain ⟨t, u, ht, hu, htu⟩ := not_mulDissociated_iff_exists_disjoint.1 fun h ↦
  hs'max _ (insert_subset_iff.2 ⟨ha, hs'.1⟩) h <| ssubset_insert ha'

Result:
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