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 : Set G) * (↑Z : Set G) = (↑S : Set G)

Tactic:
have H_mul_Z : (H : Set G) * Z = S := by simp [hZ.2.1, H_mul_S]
-- 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 : Set G).toFinset * Z = S

Tactic:
simpa [← Finset.coe_inj]

Premises used: Finset.coe_inj
-- 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 : Set G).toFinset * Z = S

Tactic:
have H_toFinset_mul_Z : Set.toFinset H * Z = S := by simpa [← Finset.coe_inj]
-- 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
⊢ Fintype.card.{u_1} ↥H * #Z = #S

Tactic:
simpa [card_mul_eq_mul_card_of_injOn_opSMul hZ.2.2] using congr_arg _ H_toFinset_mul_Z

Premises used: _private.0.Finset.card_mul_eq_mul_card_of_injOn_opSMul, congr_arg, And.right
-- 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
⊢ Fintype.card.{u_1} ↥H * #Z = #S

Tactic:
have card_H_mul_card_Z : Fintype.card H * #Z = #S := by
    simpa [card_mul_eq_mul_card_of_injOn_opSMul hZ.2.2] using congr_arg _ H_toFinset_mul_Z
-- 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
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
⟨H, inferInstance, Z, ?_, mod_cast H_mul_Z⟩

Premises used: HMul.hMul, congrArg, cast, inferInstance, Finset.coe_mul._simp_2, Inv.inv, SetLike.coe, And.intro, Exists.intro, Eq.symm, Eq
-- 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
inr : (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
refine ⟨H, inferInstance, Z, ?_, mod_cast H_mul_Z⟩
-- 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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
⊢ (↑(#Z) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹

Tactic:
simp [← card_H_mul_card_Z]
-- 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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
hb : 0 < (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ)
hba : LE.le (α := ℝ) 0 (↑(#S) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹ ≤
    ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹

Tactic:
gcongr
-- 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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
⊢ Ne (α := ℝ) (↑(#S) : ℝ) 0

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_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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
⊢ Ne (α := ℝ) (↑(#S) : ℝ) 0

Tactic:
have : (#S : ℝ) ≠ 0 := 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
this_2 : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
this : Ne (α := ℝ) (↑(#S) : ℝ) 0
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
simp [this]
-- 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
this : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
_ : (↑(#Z) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹
_₁ :
  (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹ ≤
    ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹
_₂ : ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))
⊢ (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
calc
          (#Z : ℝ)
      _ = (Fintype.card H / #S : ℝ)⁻¹ := by simp [← card_H_mul_card_Z]
      _ ≤ (((φ - K) * (K - ψ) / ((2 - K) * K) * #S) / #S)⁻¹ := by gcongr
      _ = (2 - K) * K / ((φ - K) * (K - ψ)) := by
        have : (#S : ℝ) ≠ 0 := by positivity
        simp [this]

Premises used: HMul.hMul, HSub.hSub, Membership.mem, Real.goldenConj, Fintype.card, Real.goldenRatio, Subtype, HDiv.hDiv, Nat.cast, 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
inr : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
⊢ (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
suffices ((φ - K) * (K - ψ)) / ((2 - K) * K) * #S ≤ Fintype.card H by
    calc
          (#Z : ℝ)
      _ = (Fintype.card H / #S : ℝ)⁻¹ := by simp [← card_H_mul_card_Z]
      _ ≤ (((φ - K) * (K - ψ) / ((2 - K) * K) * #S) / #S)⁻¹ := by gcongr
      _ = (2 - K) * K / ((φ - K) * (K - ψ)) := by
        have : (#S : ℝ) ≠ 0 := by positivity
        simp [this]
-- 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
z : G
⊢ r z⁻¹ = r z

Tactic:
simp [r, inv_inv]

Premises used: inv_inv
-- 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
⊢ ∀ (z : G), r z⁻¹ = r z

Tactic:
have r_inv z : r z⁻¹ = r z := by simp [r, inv_inv]
-- 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
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ)

Tactic:
?_
-- 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
⊢ LE.le (α := ℝ) (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)

Tactic:
?_
-- 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
⊢ Eq (α := ℝ) (↑(#(↑H : Set G).toFinset) : ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ)

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
inr : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ)
inr₁ : LE.le (α := ℝ) (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)

Tactic:
calc
        (φ - K) * (K - ψ) / ((2 - K) * K) * #S
    _ ≤ #{z ∈ S | (K - 1) * #A < r z} := ?_
    _ ≤ #(H : Set G).toFinset := ?_
    _ = Fintype.card H := by simp

Premises used: HMul.hMul, HSub.hSub, Membership.mem, Real.goldenConj, Fintype.card, Real.goldenRatio, Subtype, Set.toFinset, SetLike.coe, 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
inr :
  let l := #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)});
  ∀ (hk : l = #({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})),
    (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ)

Tactic:
set l : ℕ := #{z ∈ S | (K - 1) * #A < r z} with hk

Premises used: HSub.hSub, OfNat.ofNat