awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 - ψ
⊢ 0 < 2 - K
have linarith : 2 - K ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [Real.goldenRatio_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 - ψ
linarith linarith₁ : 2 - K ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ 0 < 2 - K
have linarith₂ : 2 - K ≤ 0 → K - φ + (2 - K - 0) + (φ - 2) = 0
Tactic: linarith [Real.goldenRatio_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 - ψ
⊢ ∃ (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)
have hK₂' : 0 < 2 - K
Tactic: have hK₂' : 0 < 2 - K := by linarith [Real.goldenRatio_lt_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
Tactic: have const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ)) := by positivity
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 - ψ))
⊢ ∃ (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)
have inl : ∀ (hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ))
  (hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
  ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
    (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)
Tactic: obtain rfl | A_nonempty := A.eq_empty_or_nonempty
Cleared hypotheses: A, hA₁, hA₂
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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 - ψ))
inl :
  ∀ (hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ))
    (hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)),
    ∃ (H : Subgroup G) (x : Fintype ↥H) (Z : Finset G),
      (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ (↑H : Set G) * (↑Z : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)
⊢ ∃ (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)
have inr : ∀ (A_nonempty : A.Nonempty),
  ∃ (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: obtain rfl | A_nonempty := A.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
hK₁ : 1 < K
hKφ : K < φ
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
hA₁ : (↑(#(HMul.hMul (α := Finset G) ∅⁻¹ ∅)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
hA₂ : (↑(#(HMul.hMul (α := Finset G) ∅ ∅⁻¹)) : ℝ) ≤ K * (↑(card.{u_1} (α := G) ∅) : ℝ)
⊢ (↑(card.{u_1} (α := G) ∅) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧
    (↑⊥ : Set G) * (↑∅ : Set G) = (↑∅ : Set G) * (↑∅⁻¹ : Set G)
have simp : 0 ≤ (2 - K) * K / ((φ - K) * (K - ψ))
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have S_nonempty : S.Nonempty
Tactic: have S_nonempty : S.Nonempty := by simpa [S]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have this : Finite.{u_1 + 1} ↥H
Tactic: have : Finite H := by simpa [H] using stabilizer_finite (by simpa) S.finite_toSet
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ ∃ (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)
have inr : ∀ (val : Fintype ↥H),
  ∃ (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: cases nonempty_fintype H
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 : 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)
have H_mul_S : (↑H : Set G) * (↑S : Set G) = (↑S : Set G)
Tactic: have H_mul_S : (H : Set G) * S = S := by simp [H, ← stabilizer_coe_finset]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
⊢ ∃ (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)
have inr : ∀ (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 : 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: obtain ⟨Z, hZ⟩ := exists_subset_mul_eq_mul_injOn H S
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 : 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)
have H_mul_Z : (↑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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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 : 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)
have H_toFinset_mul_Z : (↑H : Set G).toFinset * Z = S
Tactic: have H_toFinset_mul_Z : Set.toFinset H * Z = S := by simpa [← Finset.coe_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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
⊢ ∃ (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)
have card_H_mul_card_Z : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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)
have inr : (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
Tactic: refine ⟨H, inferInstance, Z, ?_, mod_cast H_mul_Z⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹ ≤
    ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹
have hb : 0 < (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹ ≤
    ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹
have hba : LE.le (α := ℝ) 0 (↑(#S) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
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) : ℝ)
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))
have this₁ : Ne (α := ℝ) (↑(#S) : ℝ) 0
Tactic: have : (#S : ℝ) ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
have _ : (↑(#Z) : ℝ) = (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) : ℝ))⁻¹
⊢ (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
have _₁ : (HDiv.hDiv (α := ℝ) (↑(Fintype.card.{u_1} ↥H) : ℝ) (↑(#S) : ℝ))⁻¹ ≤
  ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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) : ℝ))⁻¹
⊢ (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
have _₂ : ((φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) / (↑(#S) : ℝ))⁻¹ = (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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
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
⊢ (↑(#Z) : ℝ) ≤ (2 - K) * K / ((φ - K) * (K - ψ))
have inr : (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑(Fintype.card.{u_1} ↥H) : ℝ)
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]