awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0)
have norm_cast : #(A / A) * #A ≤ #(A * A) * #(A * A)
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
hA' : A.Nonempty
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw : σₘ[A] * (↑(#A) : ℚ≥0) * (σₘ[A] * (↑(#A) : ℚ≥0)) =
  HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [← 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 : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _ : δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: calc
    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
    _ = _ := by rw [← mulConst_mul_card]; ring
-- 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)
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _₁ : HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0)
Tactic: calc
    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
    _ = _ := by rw [← mulConst_mul_card]; ring
-- 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)
_₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0)
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _₂ : HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0) =
  HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: calc
    _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
    _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
    _ = _ := by rw [← mulConst_mul_card]; ring
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
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, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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) (↑(#(B⁻¹ * A⁻¹⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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)
rw₄ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(B⁻¹ * A⁻¹⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A⁻¹, B] = δₘ[A, B]
have rw₅ : HDiv.hDiv (α := ℚ≥0) (↑(#(B⁻¹ * A)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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)
rw₄ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(B⁻¹ * A⁻¹⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₅ : HDiv.hDiv (α := ℚ≥0) (↑(#(B⁻¹ * A)) : ℚ≥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, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
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, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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) (↑(#(B / A⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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)
rw₄ : HDiv.hDiv (α := ℚ≥0) (↑(#(B / A⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A⁻¹, B] = σₘ[A, B]
have rw₅ : HDiv.hDiv (α := ℚ≥0) (↑(#(B * A)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [mulConst, divConst, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
rw₂ : HDiv.hDiv (α := ℚ≥0) (↑(#(A⁻¹ / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = 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)
rw₄ : HDiv.hDiv (α := ℚ≥0) (↑(#(B / A⁻¹)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
rw₅ : HDiv.hDiv (α := ℚ≥0) (↑(#(B * A)) : ℚ≥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, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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 : CommGroup 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 : CommGroup 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 : CommGroup 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, mulConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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, mulConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0)
have norm_cast : #(A * A) * #A ≤ #(A / A) * #(A / A)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have rw : δₘ[A] * (↑(#A) : ℚ≥0) * (δₘ[A] * (↑(#A) : ℚ≥0)) =
  HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: rw [← divConst_mul_card]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _ : σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: calc
    _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
    _ = _ := by rw [← divConst_mul_card]; ring
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
⊢ σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _₁ : HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0)
Tactic: calc
    _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
    _ = _ := by rw [← divConst_mul_card]; ring
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.DoublingConst (goal)
Goal:
G : Type u_1
inst : CommGroup 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)
_₁ :
  HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0)
⊢ σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
have _₂ : HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0) =
  HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
Tactic: calc
    _ = #(A * A) * (#A : ℚ≥0) := by rw [← mul_assoc, mulConst_mul_card]
    _ ≤ #(A / A) * #(A / A) := by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..
    _ = _ := by rw [← divConst_mul_card]; ring
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2
have refine : e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
Tactic: refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
have rw : e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2
Tactic: rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
have rw₁ : e⁻¹ • e • (x.2 * x.1) ⊆ x.1 * x.2
Tactic: rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2
rw₁ : e⁻¹ • e • (x.2 * x.1) ⊆ x.1 * x.2
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
have rw₂ : x.2 * x.1 ⊆ x.1 * x.2
Tactic: rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : e⁻¹ • (e • x.2 * x.1) ⊆ x.1 * x.2
rw₁ : e⁻¹ • e • (x.2 * x.1) ⊆ x.1 * x.2
rw₂ : x.2 * x.1 ⊆ x.1 * x.2
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
have rw₃ : x.1 * x.2 ⊆ x.1 * x.2
Tactic: rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw₁ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
rw₁ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw₂ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ x.1) = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
rw₁ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
rw₂ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ x.1) = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw₃ : #(x.1 ∪ e • x.2) + #(x.1 ∩ e • x.2) = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
rw₁ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
rw₂ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ x.1) = #x.1 + #x.2
rw₃ : #(x.1 ∪ e • x.2) + #(x.1 ∩ e • x.2) = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw₄ : #x.1 + #(e • x.2) = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : #(x.1 ∪ e • x.2) + #(e • (x.2 ∩ e⁻¹ • x.1)) = #x.1 + #x.2
rw₁ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ e • e⁻¹ • x.1) = #x.1 + #x.2
rw₂ : #(x.1 ∪ e • x.2) + #(e • x.2 ∩ x.1) = #x.1 + #x.2
rw₃ : #(x.1 ∪ e • x.2) + #(x.1 ∩ e • x.2) = #x.1 + #x.2
rw₄ : #x.1 + #(e • x.2) = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(x.2 ∩ e⁻¹ • x.1) = #x.1 + #x.2
have rw₅ : #x.1 + #x.2 = #x.1 + #x.2
Tactic: rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
    card_union_add_card_inter, card_smul_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x
have fst : (mulDysonETransform e (mulDysonETransform e x)).1 = (mulDysonETransform e x).1
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
fst : (mulDysonETransform e (mulDysonETransform e x)).1 = (mulDysonETransform e x).1
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x
have snd : (mulDysonETransform e (mulDysonETransform e x)).2 = (mulDysonETransform e x).2
Tactic: ext : 1