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_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)
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * (↑(#S) : ℝ) ≤ (↑l : ℝ)
have _₁ : (2 - K) * K * (↑l : ℝ) / ((2 - K) * K) = (↑l : ℝ)
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
-- 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
⊢ LE.le (α := ℝ) (↑(#({z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)})) : ℝ) (↑(#(↑H : Set G).toFinset) : ℝ)
have inr : {z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)} ⊆ (↑H : Set G).toFinset
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 : 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
⊢ {z ∈ S | (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)} ⊆ (↑H : Set G).toFinset
have inr : ∀ ⦃x : G⦄, x ∈ S → (K - 1) * (↑(#A) : ℝ) < (↑(r x) : ℝ) → x ∈ H
Tactic: simp only [subset_iff, mem_filter, Set.mem_toFinset, SetLike.mem_coe, and_imp]
-- 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
z : G
hz : z ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)
⊢ z ∈ H
have inr : ∀ ⦃b : G⦄, b ∈ S → z •> b ∈ S
Tactic: rw [mem_stabilizer_finset']
-- 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
z : G
hz : z ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)
w : G
hw : w ∈ S
⊢ z •> w ∈ S
have hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(r w) : ℝ)
Tactic: have hrw : (2 - K) * #A ≤ r w := by
      simpa [card_mul_inv_eq_convolution_inv] using le_card_mul_inv_eq hA₁ (by simpa)
-- 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
z : G
hz : z ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z) : ℝ)
w : G
hw : w ∈ S
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(r w) : ℝ)
⊢ z •> w ∈ S
have inr : ∀ (hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z⁻¹) : ℝ)) ⦃w : G⦄ (hw : w ∈ S) (hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(r w) : ℝ)),
  z •> w ∈ S
Tactic: rw [← r_inv] at hrz
Cleared hypotheses: hrz, w, hw, hrw
-- 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
z : G
hz : z ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z⁻¹) : ℝ)
w : G
hw : w ∈ S
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(r w) : ℝ)
⊢ z •> w ∈ S
have hrz₁ : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
Tactic: simp only [r, ← card_inter_smul] at hrz hrw
Cleared hypotheses: hrz, hrw
-- 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
z : G
hz : z ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(r z⁻¹) : ℝ)
w : G
hw : w ∈ S
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(r w) : ℝ)
hrz₁ : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
⊢ z •> w ∈ S
have hrw₁ : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
Tactic: simp only [r, ← card_inter_smul] at hrz hrw
Cleared hypotheses: hrz, hrw
-- 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
⊢ LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have a : A ∩ z⁻¹ •> A ⊆ z⁻¹ •> A
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 : 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
a : A ∩ z⁻¹ •> A ⊆ z⁻¹ •> A
⊢ LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have a₁ : A ∩ w •> A ⊆ w •> A
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 : 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have this₁ : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
Tactic: have : (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) : ℝ) ≤ #(z⁻¹ •> A ∩ w •> A) := by
        gcongr <;> exact inter_subset_right
-- 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
⊢ LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) (↑(#A) : ℝ)
have a : A ∩ z⁻¹ •> A ∪ A ∩ w •> A ⊆ A
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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have this₁ : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) (↑(#A) : ℝ)
Tactic: have : (#((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) ≤ #A := by
        gcongr; exact union_subset inter_subset_left inter_subset_left
-- 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this_2 : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
this : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) (↑(#A) : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have this₁ : HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) =
  HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A)) : ℝ) (↑(#(A ∩ w •> A)) : ℝ)
Tactic: have :
          (#((A ∩ z⁻¹ •> A) ∩ (A ∩ w •> A)) + #((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) =
            #(A ∩ z⁻¹ •> A) + #(A ∩ w •> A) := mod_cast card_inter_add_card_union ..
-- 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this_2 : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
this_3 : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) (↑(#A) : ℝ)
this :
  HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A)) : ℝ) (↑(#(A ∩ w •> A)) : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have linarith : LE.le (α := ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ) 0 → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- 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
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * (↑(#A) : ℝ) < (↑(#(A ∩ z⁻¹ •> A)) : ℝ)
hrw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(A ∩ w •> A)) : ℝ)
this_2 : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
this_3 : LE.le (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) (↑(#A) : ℝ)
this :
  HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) =
    HAdd.hAdd (α := ℝ) (↑(#(A ∩ z⁻¹ •> A)) : ℝ) (↑(#(A ∩ w •> A)) : ℝ)
linarith linarith₁ linarith₂ : LE.le (α := ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ) 0 → HMul.hMul (α := ℝ) 1 1 = 1
⊢ LT.lt (α := ℝ) 0 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)
have linarith₃ : LE.le (α := ℝ) (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ) 0 →
  (1 * K - HMul.hMul (α := ℝ) 1 1) * HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ) - HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A)) : ℝ) +
              ((2 - K) * (↑(#A) : ℝ) - (↑(#(A ∩ w •> A)) : ℝ)) +
            (HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) -
              HMul.hMul (α := ℝ) 1 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ)) +
          (HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) - HMul.hMul (α := ℝ) 1 (↑(#A) : ℝ)) +
        -(HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) : ℝ) +
              HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) : ℝ) -
            (HMul.hMul (α := ℝ) 1 (↑(#(A ∩ z⁻¹ •> A)) : ℝ) + HMul.hMul (α := ℝ) 1 (↑(#(A ∩ w •> A)) : ℝ))) +
      (HMul.hMul (α := ℝ) 1 (↑(#(z⁻¹ •> A ∩ w •> A)) : ℝ) - HMul.hMul (α := ℝ) 1 0) =
    0
Tactic: linarith