awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ (↑δₘ[A, B] : 𝕜) = HDiv.hDiv (α := 𝕜) (↑(#(A / B)) : 𝕜) (↑(#A) : 𝕜)

Tactic:
simp [divConst]

Premises used: Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
norm_cast : σ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A + B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑σ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A + B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ σ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A + B)) : ℚ≥0)

Tactic:
addConst_mul_card _ _

Premises used: Finset.addConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ σ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A + B)) : ℚ≥0)

Tactic:
exact addConst_mul_card _ _

Premises used: Finset.addConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
norm_cast : δ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A - B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑δ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A - B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ δ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A - B)) : ℚ≥0)

Tactic:
subConst_mul_card _ _

Premises used: Finset.subConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ δ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A - B)) : ℚ≥0)

Tactic:
exact subConst_mul_card _ _

Premises used: Finset.subConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
norm_cast : (↑(#A) : ℚ≥0) * σ[A, B] = (↑(#(A + B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑σ[A, B] : 𝕜) = (↑(#(A + B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ (↑(#A) : ℚ≥0) * σ[A, B] = (↑(#(A + B)) : ℚ≥0)

Tactic:
card_mul_addConst _ _

Premises used: Finset.card_mul_addConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ (↑(#A) : ℚ≥0) * σ[A, B] = (↑(#(A + B)) : ℚ≥0)

Tactic:
exact card_mul_addConst _ _

Premises used: Finset.card_mul_addConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
norm_cast : (↑(#A) : ℚ≥0) * δ[A, B] = (↑(#(A - B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑δ[A, B] : 𝕜) = (↑(#(A - B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ (↑(#A) : ℚ≥0) * δ[A, B] = (↑(#(A - B)) : ℚ≥0)

Tactic:
card_mul_subConst _ _

Premises used: Finset.card_mul_subConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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'
⊢ (↑(#A) : ℚ≥0) * δ[A, B] = (↑(#(A - B)) : ℚ≥0)

Tactic:
exact card_mul_subConst _ _

Premises used: Finset.card_mul_subConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
norm_cast : σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑σₘ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A * B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)

Tactic:
mulConst_mul_card _ _

Premises used: Finset.mulConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ σₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A * B)) : ℚ≥0)

Tactic:
exact mulConst_mul_card _ _

Premises used: Finset.mulConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
norm_cast : δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑δₘ[A, B] : 𝕜) (↑(#A) : 𝕜) = (↑(#(A / B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)

Tactic:
divConst_mul_card _ _

Premises used: Finset.divConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ δₘ[A, B] * (↑(#A) : ℚ≥0) = (↑(#(A / B)) : ℚ≥0)

Tactic:
exact divConst_mul_card _ _

Premises used: Finset.divConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
norm_cast : (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑σₘ[A, B] : 𝕜) = (↑(#(A * B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)

Tactic:
card_mul_mulConst _ _

Premises used: Finset.card_mul_mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ (↑(#A) : ℚ≥0) * σₘ[A, B] = (↑(#(A * B)) : ℚ≥0)

Tactic:
exact card_mul_mulConst _ _

Premises used: Finset.card_mul_mulConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
norm_cast : (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)
⊢ HMul.hMul (α := 𝕜) (↑(#A) : 𝕜) (↑δₘ[A, B] : 𝕜) = (↑(#(A / B)) : 𝕜)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)

Tactic:
card_mul_divConst _ _

Premises used: Finset.card_mul_divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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
⊢ (↑(#A) : ℚ≥0) * δₘ[A, B] = (↑(#(A / B)) : ℚ≥0)

Tactic:
exact card_mul_divConst _ _

Premises used: Finset.card_mul_divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
inl : δₘ[∅] ≤ HPow.hPow (β := ℕ) σₘ[∅] 2
inr : ∀ (hA' : A.Nonempty), δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2
⊢ δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
⊢ δₘ[∅] ≤ HPow.hPow (β := ℕ) σₘ[∅] 2

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
inr :
  δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A] ≤ HPow.hPow (β := ℕ) σₘ[A] 2

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
rw₁ rw₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(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)

Tactic:
rw [← mul_assoc, divConst_mul_card]

Premises used: Finset.divConst_mul_card, mul_assoc
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
norm_cast : #(A / A) * #A ≤ #(A * A) * #(A * A)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A / A) * #A ≤ #(A * A) * #(A * A)

Tactic:
ruzsa_triangle_inequality_div_mul_mul ..

Premises used: Finset.ruzsa_triangle_inequality_div_mul_mul
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A / A) * #A ≤ #(A * A) * #(A * A)

Tactic:
exact ruzsa_triangle_inequality_div_mul_mul ..

Premises used: Finset.ruzsa_triangle_inequality_div_mul_mul
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
rw :
  σₘ[A] * (↑(#A) : ℚ≥0) * (σₘ[A] * (↑(#A) : ℚ≥0)) =
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
rw [← mulConst_mul_card]

Premises used: Finset.mulConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * (↑(#A) : ℚ≥0) * (σₘ[A] * (↑(#A) : ℚ≥0)) =
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
_₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#(A * A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) σₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#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

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Finset.card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
rw₆ rw₇ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A / B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A⁻¹, B] = δₘ[A, B]

Tactic:
rw [mulConst, divConst, card_inv, ← card_inv, mul_inv_rev, inv_inv, inv_mul_eq_div]

Premises used: Finset.card_inv, Finset.mulConst, inv_mul_eq_div, inv_inv, mul_inv_rev, Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
rw₆ rw₇ :
  HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0) = HDiv.hDiv (α := ℚ≥0) (↑(#(A * B)) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ δₘ[A⁻¹, B] = σₘ[A, B]

Tactic:
rw [mulConst, divConst, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]

Premises used: Finset.card_inv, Finset.mulConst, mul_comm, inv_div, div_inv_eq_mul, Finset.divConst
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
inl : σₘ[∅] ≤ HPow.hPow (β := ℕ) δₘ[∅] 2
inr : ∀ (hA' : A.Nonempty), σₘ[A] ≤ HPow.hPow (β := ℕ) δₘ[A] 2
⊢ σₘ[A] ≤ HPow.hPow (β := ℕ) δₘ[A] 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
⊢ σₘ[∅] ≤ HPow.hPow (β := ℕ) δₘ[∅] 2

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
inr :
  σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0) ≤
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A] ≤ HPow.hPow (β := ℕ) δₘ[A] 2

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
rw₁ rw₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(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)

Tactic:
rw [← mul_assoc, mulConst_mul_card]

Premises used: Finset.mulConst_mul_card, mul_assoc
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
norm_cast : #(A * A) * #A ≤ #(A / A) * #(A / A)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A * A)) : ℚ≥0) (↑(#A) : ℚ≥0) ≤ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A * A) * #A ≤ #(A / A) * #(A / A)

Tactic:
ruzsa_triangle_inequality_mul_div_div ..

Premises used: Finset.ruzsa_triangle_inequality_mul_div_div
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A * A) * #A ≤ #(A / A) * #(A / A)

Tactic:
exact ruzsa_triangle_inequality_mul_div_div ..

Premises used: Finset.ruzsa_triangle_inequality_mul_div_div
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
rw :
  δₘ[A] * (↑(#A) : ℚ≥0) * (δₘ[A] * (↑(#A) : ℚ≥0)) =
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
rw [← divConst_mul_card]

Premises used: Finset.divConst_mul_card
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) : ℚ≥0) * (δₘ[A] * (↑(#A) : ℚ≥0)) =
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.DoublingConst
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)
_₂ :
  HMul.hMul (α := ℚ≥0) (↑(#(A / A)) : ℚ≥0) (↑(#(A / A)) : ℚ≥0) =
    HPow.hPow (β := ℕ) δₘ[A] 2 * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#A) : ℚ≥0)
⊢ σₘ[A] * HMul.hMul (α := ℚ≥0) (↑(#A) : ℚ≥0) (↑(#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

Premises used: HMul.hMul, HDiv.hDiv, Nat.cast, Finset.card
-- Module: Mathlib.Combinatorics.Additive.ETransform
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

Tactic:
union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, Set.Mem, setOf, HasSubset.Subset.trans, Finset.union_mul_inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
refine : e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2
⊢ (mulDysonETransform e x).1 * (mulDysonETransform e x).2 ⊆ x.1 * x.2

Tactic:
refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, HasSubset.Subset.trans, Finset.union_mul_inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
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
rw₃ rw₄ : x.1 * x.2 ⊆ x.1 * x.2
⊢ e • x.2 * e⁻¹ • x.1 ⊆ x.1 * x.2

Tactic:
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]

Premises used: smul_mul_assoc, inv_smul_smul, mul_comm, mul_smul_comm
-- Module: Mathlib.Combinatorics.Additive.ETransform
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
rw₅ rw₆ : #x.1 + #x.2 = #x.1 + #x.2
⊢ #(x.1 ∪ e • x.2) + #(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]

Premises used: Finset.smul_finset_inter, Finset.inter_comm, smul_inv_smul, Finset.card_union_add_card_inter, Inter.inter, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
fst : (mulDysonETransform e (mulDysonETransform e x)).1 = (mulDysonETransform e x).1
snd : (mulDysonETransform e (mulDysonETransform e x)).2 = (mulDysonETransform e x).2
⊢ mulDysonETransform e (mulDysonETransform e x) = mulDysonETransform e x

Tactic:
ext : 1
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
fst : x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2

Tactic:
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]

Premises used: Finset.smul_finset_inter, Finset.union_eq_left, Finset.inter_comm, smul_inv_smul
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Tactic:
inter_subset_union

Premises used: Set.Mem, setOf, Finset.inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Tactic:
exact inter_subset_union

Premises used: Finset.inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
snd : x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1

Tactic:
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]

Premises used: Finset.union_comm, inv_smul_smul, Finset.smul_finset_union, Finset.inter_eq_left
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1

Tactic:
inter_subset_union

Premises used: Finset.inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1

Tactic:
exact inter_subset_union

Premises used: Finset.inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
rw : x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2
⊢ e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2

Tactic:
rw [smul_finset_inter, smul_inv_smul, inter_comm]

Premises used: Finset.smul_finset_inter, Finset.inter_comm, smul_inv_smul
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
x : Finset α × Finset α
⊢ mulETransformLeft 1 x = x

Tactic:
simp [mulETransformLeft]

Premises used: Finset.mulETransformLeft
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
x : Finset α × Finset α
⊢ mulETransformRight 1 x = x

Tactic:
simp [mulETransformRight]

Premises used: Finset.mulETransformRight