awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) = HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A⁻¹) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A⁻¹) : ℝ) = (↑(#(A ×ˢ A⁻¹)) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
norm_cast : #(A ×ˢ A⁻¹) = ∑ x ∈ S, r x
⊢ Eq (α := ℝ) (↑(#(A ×ˢ A⁻¹)) : ℝ) (∑ z ∈ S, (↑(r z) : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ #(A ×ˢ A⁻¹) = ∑ x ∈ S, r x

Tactic:
card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2

Premises used: Finset.convolution, Finset.card_eq_sum_card_fiberwise, And.right, And.left, Iff.mp, Finset.mem_product, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ #(A ×ˢ A⁻¹) = ∑ x ∈ S, r x

Tactic:
exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2

Premises used: Finset.card_eq_sum_card_fiberwise, And.right, And.left, Iff.mp, Finset.mem_product, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
norm_cast :
  ∑ x ∈ S, r x =
    HAdd.hAdd (α := ℕ) (∑ x ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r x) : ℝ), r x)
      (∑ x ∈ S with (↑(r x) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), r x)
⊢ ∑ z ∈ S, (↑(r z) : ℝ) =
    HAdd.hAdd (α := ℝ) (∑ z ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ), (↑(r z) : ℝ))
      (∑ z ∈ S with (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), (↑(r z) : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
simp_rw :
  ∑ x ∈ S, r x =
    HAdd.hAdd (α := ℕ) (∑ x ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r x) : ℝ), r x)
      (∑ x ∈ S with ¬(K - 1) * (↑(#A) : ℝ) < (↑(r x) : ℝ), r x)
⊢ ∑ x ∈ S, r x =
    HAdd.hAdd (α := ℕ) (∑ x ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r x) : ℝ), r x)
      (∑ x ∈ S with (↑(r x) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), r x)

Tactic:
simp_rw [← not_lt, sum_filter_add_sum_filter_not]

Premises used: not_lt, Finset.sum_filter_add_sum_filter_not
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
h₁ : ∀ (z : G) (hz : z ∈ {z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)}), r z ≤ #A
h₂ : ∀ (z : G) (hz : z ∈ {z ∈ S | (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ)}), (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ)
⊢ HAdd.hAdd (α := ℝ) (∑ z ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ), (↑(r z) : ℝ))
      (∑ z ∈ S with (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), (↑(r z) : ℝ)) ≤
    HAdd.hAdd (α := ℝ) (∑ z ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ), (↑(#A) : ℝ))
      (∑ z ∈ S with (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), (K - 1) * (↑(#A) : ℝ))

Tactic:
gcongr with z hz z hz
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
z : G
hz : z ∈ {z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)}
⊢ r z ≤ #A

Tactic:
convolution_le_card_left

Premises used: Finset.convolution_le_card_left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
z : G
hz : z ∈ {z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)}
⊢ r z ≤ #A

Tactic:
exact convolution_le_card_left

Premises used: Finset.convolution_le_card_left
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
z : G
hz : z ∈ {z ∈ S | (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ)}
⊢ (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ HAdd.hAdd (α := ℝ) (∑ z ∈ S with (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ), (↑(#A) : ℝ))
      (∑ z ∈ S with (↑(r z) : ℝ) ≤ (K - 1) * (↑(#A) : ℝ), (K - 1) * (↑(#A) : ℝ)) =
    HMul.hMul (α := ℝ) (↑l : ℝ) (↑(#A) : ℝ) + HSub.hSub (α := ℝ) (↑(#S) : ℝ) (↑l : ℝ) * (K - 1) * (↑(#A) : ℝ)

Tactic:
simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]

Premises used: HMul.hMul, mul_assoc, HSub.hSub, Nat.cast, Finset.card_filter_add_card_filter_not, not_lt, LT.lt, Finset.card, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ HMul.hMul (α := ℝ) (↑l : ℝ) (↑(#A) : ℝ) + HSub.hSub (α := ℝ) (↑(#S) : ℝ) (↑l : ℝ) * (K - 1) * (↑(#A) : ℝ) =
    ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)

Tactic:
ring
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)

Tactic:
have ineq : #A * #A ≤ ((2 - K) * l + (K - 1) * #S) * #A := by
      calc
            (#A : ℝ) * #A
        _ = #A * #A⁻¹ := by simp
        _ = #(A ×ˢ A⁻¹) := by simp
        _ = ∑ z ∈ S, ↑(r z) := by
          norm_cast
          exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2
        _ = ∑ z ∈ S with (K - 1) * #A < r z, ↑(r z) + ∑ z ∈ S with r z ≤ (K - 1) * #A, ↑(r z) := by
          norm_cast; simp_rw [← not_lt, sum_filter_add_sum_filter_not]
        _ ≤ ∑ z ∈ S with (K - 1) * #A < r z, ↑(#A)
          + ∑ z ∈ S with r z ≤ (K - 1) * #A, (K - 1) * #A := by
          gcongr with z hz z hz
          · exact convolution_le_card_left
          · simp_all
        _ = l * #A + (#S - l) * (K - 1) * #A := by
          simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]
        _ = ((2 - K) * l + (K - 1) * #S) * #A := by ring
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
ineq : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)
⊢ 0 < #A

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
ineq : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)
⊢ 0 < #A

Tactic:
have : 0 < #A := by positivity
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : (↑(#(A⁻¹ * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hA₂ : (↑(#(A * A⁻¹)) : ℝ) ≤ K * (↑(#A) : ℝ)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this_1 : Finite.{u_1 + 1} ↥H
val : Fintype ↥H
H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Z : Finset G
hZ :
  Z ⊆ S ∧
    (↑H : Set G) * (↑Z : Set G) = (↑H : Set G) * (↑S : Set G) ∧
      Set.InjOn (β := Set G) (fun (x : G) ↦ (↑H : Set G) <• x) (↑Z : Set G)
H_mul_Z : (↑H : Set G) * (↑Z : Set G) = (↑S : Set G)
H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
card_H_mul_card_Z : Fintype.card.{u_1} ↥H * #Z = #S
r : (z : G) → ℕ := fun (z : G) ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
l : ℕ := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})
ineq : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)
this : 0 < #A
hbc : (↑(#A) : ℝ) ≤ (2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)
⊢ K * (↑(#A) : ℝ) ≤ K * ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ))

Tactic:
gcongr