awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ 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
have 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
Tactic: by_cases a ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ 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
have 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
Tactic: by_cases a ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ 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
have 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
Tactic: by_cases a ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have obtain : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ∈ {s' ∈ s.powerset | MulDissociated (↑s' : Set α)}) s'),
  ∃ 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⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (hypothesis)
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'
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have hs'₁ : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'
Tactic: simp only [mem_filter, mem_powerset] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
have refine : ∀ (a : α) (ha : a ∈ s), a ∈ s'.mulSpan
Tactic: refine ⟨s', hs'.1.1, hs _ hs'.1.1 hs'.1.2, fun a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ a ∈ s'.mulSpan
have pos : ∀ (ha' : a ∈ s'), a ∈ s'.mulSpan
Tactic: by_cases ha' : a ∈ s'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ a ∈ s'.mulSpan
have neg : ∀ (ha' : a ∉ s'), a ∈ s'.mulSpan
Tactic: by_cases ha' : a ∈ s'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
have 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
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'
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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)
⊢ a ∈ s'.mulSpan
have pos : ∀ (hat : a ∈ t), a ∈ s'.mulSpan
Tactic: by_cases hat : a ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ a ∈ s'.mulSpan
have neg : ∀ (hat : a ∉ t), a ∈ s'.mulSpan
Tactic: by_cases hat : a ∈ t
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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)
have rw : a = (∏ b ∈ u, b) / ((∏ x ∈ t, x) / a)
Tactic: rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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)
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)
have rw₁ : a = (∏ b ∈ u, b) / ((∏ a ∈ u, a) / a)
Tactic: rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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)
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b)
have rw₂ : a = a
Tactic: rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (hypothesis)
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 ∈ s'.mulSpan
have this : 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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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)
⊢ a ∈ s'.mulSpan
have pos : HDiv.hDiv (α := α) (∏ b ∈ u, b) (∏ b ∈ t.erase a, b) ∈ s'.mulSpan
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (hypothesis)
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 ∈ s'.mulSpan
have ht₁ : t ⊆ s'
Tactic: rw [coe_subset, subset_insert_iff_of_notMem hat] at ht
Cleared hypotheses: ht, hu, htu, hat
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ 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
have pos : ∀ (hau : a ∈ u), a ∈ s'.mulSpan
Tactic: by_cases hau : a ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ s'
hu : (↑u : Set α) ⊆ (↑(insert a s') : Set α)
htu : Disjoint t u ∧ t ≠ u ∧ Eq (α := α) (∏ a ∈ t, a) (∏ a ∈ u, a)
hat : a ∉ t
pos : ∀ (hau : a ∈ u), a ∈ s'.mulSpan
⊢ a ∈ s'.mulSpan
have neg : ∀ (hau : a ∉ u), a ∈ s'.mulSpan
Tactic: by_cases hau : a ∈ u
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ 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 = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
have rw : a = (∏ b ∈ t, b) / ((∏ x ∈ u, x) / a)
Tactic: rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ 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
rw : a = (∏ b ∈ t, b) / ((∏ x ∈ u, x) / a)
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
have rw₁ : a = (∏ a ∈ u, a) / ((∏ x ∈ u, x) / a)
Tactic: rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ 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
rw : a = (∏ b ∈ t, b) / ((∏ x ∈ u, x) / a)
rw₁ : a = (∏ a ∈ u, a) / ((∏ x ∈ u, x) / a)
⊢ a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
have rw₂ : a = a
Tactic: rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (hypothesis)
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 ⊆ 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
have this : a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
Tactic: have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
      rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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 ⊆ 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
this : a = HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b)
⊢ a ∈ s'.mulSpan
have pos : HDiv.hDiv (α := α) (∏ b ∈ t, b) (∏ b ∈ u.erase a, b) ∈ s'.mulSpan
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (hypothesis)
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 ⊆ 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
have hu₁ : u ⊆ s'
Tactic: rw [coe_subset, subset_insert_iff_of_notMem hau] at hu
Cleared hypotheses: hu, htu, hat, hau
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : DecidableEq α
inst_2 : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated (↑s' : Set α) → #s' ≤ d
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have obtain : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ∈ {s' ∈ s.powerset | MulDissociated (↑s' : Set α)}) s'),
  ∃ 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
have obtain₁ : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s'),
  ∃ 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Dissociation (goal)
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
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have obtain₂ : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
  a ∈ 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