awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
refine :
  (∃ (t : Finset α),
      (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)) →
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
refine not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩

Premises used: not_mulDissociated, Iff.intro, Iff.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩

Premises used: Iff.mpr, sdiff_ne_sdiff_iff, SDiff.sdiff, And.intro, Exists.intro, Finset.prod_sdiff_eq_prod_sdiff_iff, disjoint_sdiff_sdiff
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
refine_1 : (↑(t \ u) : Set α) ⊆ s
refine_2 : (↑(u \ t) : Set α) ⊆ s
⊢ ∃ (t : Finset α) (u : Finset α),
    (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
refine_1 : (↑t : Set α) \ (↑u : Set α) ⊆ s
⊢ (↑(t \ u) : Set α) ⊆ s

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
refine_2 : (↑u : Set α) \ (↑t : Set α) ⊆ s
⊢ (↑(u \ t) : Set α) ⊆ s

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑t : Set α) \ (↑u : Set α) ⊆ s

Tactic:
diff_subset.trans ‹_›

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑t : Set α) \ (↑u : Set α) ⊆ s

Tactic:
exact diff_subset.trans ‹_›

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑u : Set α) \ (↑t : Set α) ⊆ s

Tactic:
diff_subset.trans ‹_›

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
t : Finset α
ht : (↑t : Set α) ⊆ s
u : Finset α
hu : (↑u : Set α) ⊆ s
htu : t ≠ u
h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)
⊢ (↑u : Set α) \ (↑t : Set α) ⊆ s

Tactic:
exact diff_subset.trans ‹_›

Premises used: Set.diff_subset, HasSubset.Subset.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
refine :
  (∃ (t : Finset α),
      (↑t : Set α) ⊆ s ∧ ∃ (u : Finset α), (↑u : Set α) ⊆ s ∧ t ≠ u ∧ Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)) →
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
refine₁ :
  ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s) (u : Finset α) (hu : (↑u : Set α) ⊆ s) (htu : t ≠ u)
    (h : Eq (α := α) (∏ x ∈ t, x) (∏ x ∈ u, x)),
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
⊢ ¬MulDissociated s ↔
    ∃ (t : Finset α) (u : Finset α),
      (↑t : Set α) ⊆ s ∧ (↑u : Set α) ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
classical
  refine not_mulDissociated.trans
    ⟨?_, fun ⟨t, u, ht, hu, _, htune, htusum⟩ ↦ ⟨t, ht, u, hu, htune, htusum⟩⟩
  rintro ⟨t, ht, u, hu, htu, h⟩
  refine ⟨t \ u, u \ t, ?_, ?_, disjoint_sdiff_sdiff, sdiff_ne_sdiff_iff.2 htu,
    Finset.prod_sdiff_eq_prod_sdiff_iff.2 h⟩ <;> push_cast <;> exact diff_subset.trans ‹_›

Premises used: Set.diff_subset, not_mulDissociated, HasSubset.Subset.trans, Iff.intro, Iff.trans
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : CommGroup β
s : Set α
e : β ≃* α
⊢ MulDissociated.{u_2} (α := β) ((⇑e : (a : β) → α) ⁻¹' s) ↔ MulDissociated s

Tactic:
simp [MulDissociated, InjOn, ← e.finsetCongr.forall_congr_right, ← e.apply_eq_iff_eq,
    (Finset.map_injective _).eq_iff]

Premises used: MulDissociated, MulEquiv.apply_eq_iff_eq, Function.Injective.eq_iff, MulEquiv.toEquiv, Equiv.finsetCongr, Finset.map_injective, Set.InjOn, Equiv.forall_congr_right
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
s : Set α
⊢ MulDissociated s⁻¹ ↔ MulDissociated s

Tactic:
(MulEquiv.inv α).mulDissociated_preimage

Premises used: MulEquiv.inv, MulEquiv.mulDissociated_preimage
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
⊢ a ∈ s.mulSpan ↔ ∃ (ε : α → ℤ), (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a

Tactic:
simp [mulSpan]

Premises used: Finset.mulSpan
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
inl :
  Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (1 : ℤ)
inr :
  ∀ (hab : a ≠ b),
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
        Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)

Tactic:
obtain rfl | hab := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a : ℤ) (1 : ℤ)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
hab : a ≠ b
⊢ Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (-1 : ℤ) ∨
    Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (0 : ℤ) ∨
      Eq (α := ℤ) (Pi.single (M := fun (a : α) ↦ ℤ) a 1 b : ℤ) (1 : ℤ)

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ ∏ a_1 ∈ s, HPow.hPow (β := ℤ) a_1 (Pi.single (M := fun (a : α) ↦ ℤ) a 1 a_1 : ℤ) = a

Tactic:
simp [Pi.single, Function.update, pow_ite, ha]

Premises used: Function.update, pow_ite, Pi.single
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
pos :
  a ∈ t →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
neg :
  a ∉ t →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
by_cases a ∈ t
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∈ t
pos :
  a ∈ u →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
neg :
  a ∉ u →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
by_cases a ∈ u
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∉ t
pos :
  a ∈ u →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
neg :
  a ∉ u →
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
        HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
by_cases a ∈ u
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∈ t
h_1 : a ∈ u
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∈ t
h_1 : a ∉ u
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∉ t
h_1 : a ∈ u
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
h : a ∉ t
h_1 : a ∉ u
⊢ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = -1 ∨
    HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 0 ∨
      HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a = 1

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Additive.Dissociation
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
⊢ ∏ a ∈ s, a ^ HSub.hSub (α := (x : α) → ℤ) (β := (x : α) → ℤ) ((↑t : Set α).indicator 1) ((↑u : Set α).indicator 1) a =
    HDiv.hDiv (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)

Tactic:
simp [prod_div_distrib, zpow_sub,
      ← div_eq_mul_inv, Set.indicator, pow_ite, inter_eq_right.2, *]

Premises used: Iff.mpr, Set.indicator, pow_ite, div_eq_mul_inv, Finset.inter_eq_right, Finset.prod_div_distrib, zpow_sub
-- 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
⊢ MulDissociated (↑∅ : Set α)

Tactic:
simp
-- 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
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

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

Premises used: Iff.mpr, Finset.empty_mem_powerset, Finset.exists_maximal, And.intro, Exists.intro, Finset.mem_filter, EmptyCollection.emptyCollection
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ∈ {s' ∈ s.powerset | MulDissociated (↑s' : Set α)}) s'
⊢ Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'

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

Premises used: Finset.mem_powerset, Finset.mem_filter
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
⟨s', hs'.1.1, hs _ hs'.1.1 hs'.1.2, fun a ha ↦ ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
refine : ∀ (a : α) (ha : a ∈ s), a ∈ s'.mulSpan
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan

Tactic:
refine ⟨s', hs'.1.1, hs _ hs'.1.1 hs'.1.2, fun a ha ↦ ?_⟩
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
pos : ∀ (ha' : a ∈ s'), a ∈ s'.mulSpan
neg : ∀ (ha' : a ∉ s'), a ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan

Tactic:
by_cases ha' : a ∈ s'
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∈ s'
⊢ a ∈ s'.mulSpan

Tactic:
subset_mulSpan ha'

Premises used: Finset.subset_mulSpan
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∈ s'
⊢ a ∈ s'.mulSpan

Tactic:
exact subset_mulSpan ha'

Premises used: Finset.subset_mulSpan
-- 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
s' : Finset α
hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
neg :
  ∀ (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
⊢ a ∈ s'.mulSpan

Tactic:
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'

Premises used: Iff.mpr, Finset.insert_subset_iff, not_mulDissociated_iff_exists_disjoint, And.left, And.intro, Iff.mp, Finset.ssubset_insert, Maximal.not_gt
-- 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
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)
pos : ∀ (hat : a ∈ t), a ∈ s'.mulSpan
neg : ∀ (hat : a ∉ t), a ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan

Tactic:
by_cases hat : a ∈ t
-- 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
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
rw : a = (∏ b ∈ u, b) / ((∏ x ∈ t, x) / a)
rw₁ : a = (∏ b ∈ u, b) / ((∏ a ∈ u, a) / a)
rw₂ rw₃ : a = a
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)

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

Premises used: Finset.prod_erase_eq_div, And.right, div_div_self'
-- 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
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 = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)

Tactic:
have : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b := by
      rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
-- 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
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
this : a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)
pos : HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b) ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan

Tactic:
rw [this]
-- 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
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
this : a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b) ∈ s'.mulSpan

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

Premises used: Finset.subset_insert_iff_of_notMem, Finset.prod_div_prod_mem_mulSpan, And.left, Iff.mp, Finset.disjoint_left, Finset.subset_insert_iff
-- 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
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
this : a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)
⊢ HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b) ∈ s'.mulSpan

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

Premises used: Finset.subset_insert_iff_of_notMem, Finset.prod_div_prod_mem_mulSpan, And.left, Iff.mp, Finset.disjoint_left, Finset.subset_insert_iff