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 - ψ
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⁻¹) : ℝ)
_₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A⁻¹) : ℝ) = (↑(#(A ×ˢ A⁻¹)) : ℝ)
_₂ : Eq (α := ℝ) (↑(#(A ×ˢ A⁻¹)) : ℝ) (∑ z ∈ S, (↑(r z) : ℝ))
_₃ :
  ∑ 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) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)
have _₄ : 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: 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
-- 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
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⁻¹) : ℝ)
_₁ : HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A⁻¹) : ℝ) = (↑(#(A ×ˢ A⁻¹)) : ℝ)
_₂ : Eq (α := ℝ) (↑(#(A ×ˢ A⁻¹)) : ℝ) (∑ z ∈ S, (↑(r z) : ℝ))
_₃ :
  ∑ 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) : ℝ))
_₄ :
  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) : ℝ))
⊢ HMul.hMul (α := ℝ) (↑(#A) : ℝ) (↑(#A) : ℝ) ≤ ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ)) * (↑(#A) : ℝ)
have _₅ : 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: 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
-- 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
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) : ℝ)})
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
have ineq : 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
-- 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
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) : ℝ)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
have this₁ : 0 < #A
Tactic: have : 0 < #A := 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
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
⊢ K * (↑(#A) : ℝ) ≤ K * ((2 - K) * (↑l : ℝ) + (K - 1) * (↑(#S) : ℝ))
have hbc : (↑(#A) : ℝ) ≤ (2 - K) * (↑l : ℝ) + (K - 1) * (↑(#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
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
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
have ineq₁ : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
Tactic: replace ineq := calc
          (#S : ℝ)
      _ ≤ K * #A := ‹_›
      _ ≤ K * ((2 - K) * l + (K - 1) * #S) := by
        gcongr; exact le_of_mul_le_mul_right ineq <| by positivity
      _ = (2 - K) * K * l + (K - 1) * K * #S := by ring
Cleared hypotheses: ineq
-- 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
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) : ℝ)})
this : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
⊢ (φ - K) * (K - ψ) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
have this₁ : φ * ψ = -1
Tactic: have := Real.goldenRatio_mul_goldenConj
-- 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
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) : ℝ)})
this_2 : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
this : φ * ψ = -1
⊢ (φ - K) * (K - ψ) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
have this₁ : φ + ψ = 1
Tactic: have := Real.goldenRatio_add_goldenConj
-- 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
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) : ℝ)})
this_2 : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
this_3 : φ * ψ = -1
this : φ + ψ = 1
⊢ (φ - K) * (K - ψ) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
have rw : (1 - (K - 1) * K) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
Tactic: rw [show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind]
-- 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
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) : ℝ)})
this_2 : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
this_3 : φ * ψ = -1
this : φ + ψ = 1
⊢ (1 - (K - 1) * K) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
have hab : (1 - (K - 1) * K) * (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ)
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
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) : ℝ)})
this_2 : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
this_3 : φ * ψ = -1
this : φ + ψ = 1
⊢ (1 - (K - 1) * K) * (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ)
have linarith : (2 - K) * K * (↑l : ℝ) < (1 - (K - 1) * K) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith [ineq]
-- 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
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) : ℝ)})
this_2 : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
this_3 : φ * ψ = -1
this : φ + ψ = 1
linarith linarith₁ : (2 - K) * K * (↑l : ℝ) < (1 - (K - 1) * K) * (↑(#S) : ℝ) → HMul.hMul (α := ℝ) 1 1 = 1
⊢ (1 - (K - 1) * K) * (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ)
have linarith₂ : (2 - K) * K * (↑l : ℝ) < (1 - (K - 1) * K) * (↑(#S) : ℝ) →
  (↑(#S) : ℝ) - ((2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)) +
      ((2 - K) * K * (↑l : ℝ) - (1 - (K - 1) * K) * (↑(#S) : ℝ)) =
    0
Tactic: linarith [ineq]
-- 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
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) : ℝ)})
this : 0 < #A
ineq : (↑(#S) : ℝ) ≤ (2 - K) * K * (↑l : ℝ) + (K - 1) * K * (↑(#S) : ℝ)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
have _ : (φ - K) * (K - ψ) * (↑(#S) : ℝ) / ((2 - K) * K) ≤ (2 - K) * K * (↑l : ℝ) / ((2 - K) * K)
Tactic: calc
          (φ - K) * (K - ψ) / ((2 - K) * K) * #S
      _ = (φ - K) * (K - ψ) * #S / ((2 - K) * K) := div_mul_eq_mul_div ..
      _ ≤ (2 - K) * K * l / ((2 - K) * K) := by
        have := Real.goldenRatio_mul_goldenConj
        have := Real.goldenRatio_add_goldenConj
        rw [show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind]
        gcongr ?_ / _
        linarith [ineq]
      _ = l := by field