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 : 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
obtain₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
    a ∈ s'.mulSpan
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have pos : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
  (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
-- 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
obtain₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
    a ∈ s'.mulSpan
pos :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∈ s'), a ∈ s'.mulSpan
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have neg : ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
  (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
-- 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
obtain₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
    a ∈ s'.mulSpan
pos :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∈ s'), a ∈ s'.mulSpan
neg neg₁ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s'), a ∈ s'.mulSpan
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have neg₂ : ∀ (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
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
obtain₂ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s),
    a ∈ s'.mulSpan
pos :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∈ s'), a ∈ s'.mulSpan
neg neg₁ :
  ∀ (s' : Finset α) (hs' : Maximal (fun (x : Finset α) ↦ x ⊆ s ∧ MulDissociated (↑x : Set α)) s') (a : α) (ha : a ∈ s)
    (ha' : a ∉ s'), a ∈ s'.mulSpan
neg₂ :
  ∀ (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
⊢ ∃ s' ⊆ s, #s' ≤ d ∧ s ⊆ s'.mulSpan
have pos₁ : ∀ (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
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.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
have inl : σₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ * B)) : ℚ≥0)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : σₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ * B)) : ℚ≥0)
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
have inr : ∀ (hA : A.Nonempty), σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
have inl : δₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ / B)) : ℚ≥0)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : δₘ[∅, B] * (↑(card.{u_1} (α := G) ∅) : ℚ≥0) = (↑(#(∅ / B)) : ℚ≥0)
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
have inr : ∀ (hA : A.Nonempty), δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
Tactic: obtain rfl | hA := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)
have rw : σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
Tactic: rw [mul_comm, mulConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
⊢ (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)
have rw₁ : Eq (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)
Tactic: rw [mul_comm, mulConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)
have rw : δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
Tactic: rw [mul_comm, divConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
⊢ (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)
have rw₁ : Eq (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#(A / B)) : ℚ≥0)
Tactic: rw [mul_comm, divConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ σₘ[A, B⁻¹] = δₘ[A, B]
have rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = δₘ[A, B]
Tactic: rw [mulConst, divConst, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = δₘ[A, B]
⊢ σₘ[A, B⁻¹] = δₘ[A, B]
have rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = δₘ[A, B]
rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A, B⁻¹] = δₘ[A, B]
have rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ δₘ[A, B⁻¹] = σₘ[A, B]
have rw : δₘ[A, B⁻¹] = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : δₘ[A, B⁻¹] = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A, B⁻¹] = σₘ[A, B]
have rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A / B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
rw : δₘ[A, B⁻¹] = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₁ : HDiv.hDiv (α := ℚ≥0) (↑(#(A / B⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A, B⁻¹] = σₘ[A, B]
have rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, div_inv_eq_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ σₘ[A, B]
have rw : LE.le (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)
Tactic: rw [mulConst, one_le_div₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
rw : LE.le (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#(A * B)) : ℚ≥0)
⊢ 1 ≤ σₘ[A, B]
have rw₁ : LT.lt (α := ℚ≥0) 0 (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, one_le_div₀]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
⊢ 1 ≤ δₘ[A, B]
have rw : 1 ≤ σₘ[A, B⁻¹]
Tactic: rw [← mulConst_inv_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ σₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inl : σₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : σₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
⊢ σₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inr : ∀ (hA' : A.Nonempty), σₘ[A, B] ≤ (↑(#B) : ℚ≥0)
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ σₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inr : (↑(#(A * B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)
Tactic: rw [mulConst, div_le_iff₀' (by positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
⊢ δₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inl : δₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inl : δₘ[∅, B] ≤ (↑(#B) : ℚ≥0)
⊢ δₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inr : ∀ (hA' : A.Nonempty), δₘ[A, B] ≤ (↑(#B) : ℚ≥0)
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
hA' : A.Nonempty
⊢ δₘ[A, B] ≤ (↑(#B) : ℚ≥0)
have inr : (↑(#(A / B)) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#B) : ℚ≥0)
Tactic: rw [divConst, div_le_iff₀' (by positivity)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ σₘ[A, B] ≤ A.dens⁻¹
have rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [dens, inv_div, mulConst]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
have hab : #(A * B) ≤ Fintype.card G
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ δₘ[A, B] ≤ A.dens⁻¹
have rw : HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [dens, inv_div, divConst]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A B : Finset G
inst_2 : Fintype G
⊢ HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HDiv.hDiv (α := ℚ≥0) (↑(Fintype.card G) : ℚ≥0) (↑(#A) : ℚ≥0)
have hab : #(A / B) ≤ Fintype.card G
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ HMul.hMul (α := 𝕜) (↑σ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A + B)) : 𝕜)
have norm_cast : σ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A + B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ HMul.hMul (α := 𝕜) (↑δ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A - B)) : 𝕜)
have norm_cast : δ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A - B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑σ[A, B] : 𝕜) = (↑(#(A + B)) : 𝕜)
have norm_cast : (↑(#A) : ℚ≥0) * σ[A, B] = (↑(#(A + B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G' : Type u_2
inst : AddGroup G'
inst_1 : DecidableEq G'
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G'
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑δ[A, B] : 𝕜) = (↑(#(A - B)) : 𝕜)
have norm_cast : (↑(#A) : ℚ≥0) * δ[A, B] = (↑(#(A - B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G
⊢ HMul.hMul (α := 𝕜) (↑σₘ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A * B)) : 𝕜)
have norm_cast : σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G
⊢ HMul.hMul (α := 𝕜) (↑δₘ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A / B)) : 𝕜)
have norm_cast : δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑σₘ[A, B] : 𝕜) = (↑(#(A * B)) : 𝕜)
have norm_cast : (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
𝕜 : Type u_3
inst_2 : Semifield 𝕜
inst_3 : CharZero 𝕜
A B : Finset G
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑δₘ[A, B] : 𝕜) = (↑(#(A / B)) : 𝕜)
have norm_cast : (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2
have inl : δₘ[∅] ≤ HPow.hPow (β := ℕ) σₘ[∅] 2
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
inl : δₘ[∅] ≤ HPow.hPow (β := ℕ) σₘ[∅] 2
⊢ δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2
have inr : ∀ (hA' : A.Nonempty), δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2
Tactic: obtain rfl | hA' := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2
have inr : δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
  HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw : δₘ[A] * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [← mul_assoc, divConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
rw : δₘ[A] * (↑(#A) : ℚ≥0) * (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw₁ : HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [← mul_assoc, divConst_mul_card]