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 B : Finset G
a b : G
hA : (↑(#(B * A)) : ℝ) < K * (↑(#A) : ℝ)
ha : a ∈ B
hb : b ∈ B
this : HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#(a •> A ∩ b •> A)) : ℝ)
have linarith : (↑(#(a •> A ∩ b •> A)) : ℝ) ≤ (2 - K) * (↑(#A) : ℝ) →
  (↑(#(B * A)) : ℝ) - K * (↑(#A) : ℝ) +
        (HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) - HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)) +
      ((↑(#(a •> A ∩ b •> A)) : ℝ) - (2 - K) * (↑(#A) : ℝ)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : (↑(#(B * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hx : x ∈ B⁻¹ * B
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)
have hx₁ : ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x
Tactic: simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : (↑(#(B * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
hx : ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)
have obtain : ∀ (a : G) (ha : a ∈ B) (b : G) (hb : b ∈ B), (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
hA : (↑(#(B * A)) : ℝ) ≤ K * (↑(#A) : ℝ)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
have rw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)
Tactic: rw [card_mul_inv_eq_convolution_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : (↑(#(B * A)) : ℝ) < K * (↑(#A) : ℝ)
hx : x ∈ B⁻¹ * B
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)
have hx₁ : ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x
Tactic: simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : (↑(#(B * A)) : ℝ) < K * (↑(#A) : ℝ)
hx : ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)
have obtain : ∀ (a : G) (ha : a ∈ B) (b : G) (hb : b ∈ B), (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A B : Finset G
hA : (↑(#(B * A)) : ℝ) < K * (↑(#A) : ℝ)
a : G
ha : a ∈ B
b : G
hb : b ∈ B
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
have rw : (2 - K) * (↑(#A) : ℝ) < (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)
Tactic: rw [card_mul_inv_eq_convolution_inv]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ z ∈ A⁻¹ * A → z ∈ A * A⁻¹
have simp : ∀ x ∈ A, ∀ x_1 ∈ A, x⁻¹ * x_1 = z → ∃ y ∈ A, ∃ a ∈ A, y * a⁻¹ = z
Tactic: simp only [mem_mul, forall_exists_index, and_imp, mem_inv,
    exists_exists_and_eq_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
have have : ∀ (t : G) (ht : t ∈ x •> A ∩ y •> A), ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
Tactic: have ⟨t, ht⟩ : (x • A ∩ y • A).Nonempty := by
    simpa using lt_card_smul_inter_smul (K := 2) (mod_cast h) hx hy
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : t ∈ x •> A ∩ y •> A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
have ht₁ : (∃ y ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t
Tactic: simp only [mem_inter, mem_smul_finset, smul_eq_mul] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : (∃ y ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
have obtain : ∀ (z : G) (hz : z ∈ A) (w : G) (hw : w ∈ A) (hzxwy : x * z = y * w), ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
Tactic: obtain ⟨⟨z, hz, hzxwy⟩, w, hw, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
have refine : z * w⁻¹ = x⁻¹ * y
Tactic: refine ⟨z, hz, w, hw, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z * w⁻¹ = x⁻¹ * y
have rw : z = x⁻¹ * y * w
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
rw : z = x⁻¹ * y * w
⊢ z * w⁻¹ = x⁻¹ * y
have rw₁ : z = x⁻¹ * (y * w)
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
rw : z = x⁻¹ * y * w
rw₁ : z = x⁻¹ * (y * w)
⊢ z * w⁻¹ = x⁻¹ * y
have rw₂ : z = x⁻¹ * (x * z)
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
rw : z = x⁻¹ * y * w
rw₁ : z = x⁻¹ * (y * w)
rw₂ : z = x⁻¹ * (x * z)
⊢ z * w⁻¹ = x⁻¹ * y
have rw₃ : z = z
Tactic: rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ = A⁻¹ * A
have refine : A * A⁻¹ ⊆ A⁻¹ * A
Tactic: refine Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ #(A * A) < 2 * #A
have rw : (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
Tactic: rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₃ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 2 0
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 2 0
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₄ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) →
  HSub.hSub (α := ℚ) 0 (↑(#(A * A)) : ℚ) + 3 * (HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) - (↑(#(A * A)) : ℚ)) +
      2 * (HMul.hMul (α := ℚ) 2 (↑(#(A * A)) : ℚ) - HMul.hMul (α := ℚ) 1 3 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) =
    0
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
linarith₃ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 2 0
linarith₄ :
  HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) →
    HSub.hSub (α := ℚ) 0 (↑(#(A * A)) : ℚ) + 3 * (HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) - (↑(#(A * A)) : ℚ)) +
        2 * (HMul.hMul (α := ℚ) 2 (↑(#(A * A)) : ℚ) - HMul.hMul (α := ℚ) 1 3 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) =
      0
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 3 0
Tactic: linarith only [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ A.Nonempty
have by_contra! : ∀ (h : (↑(#(HMul.hMul (α := Finset G) ∅ ∅)) : ℚ) < 3 / 2 * (↑(card.{u_1} (α := G) ∅) : ℚ)), False
Tactic: by_contra! rfl
Cleared hypotheses: A, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a b c d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ ∀ {a b : G},
    a ∈ (↑A⁻¹ : Set G) * (↑A : Set G) → b ∈ (↑A⁻¹ : Set G) * (↑A : Set G) → a * b ∈ (↑A⁻¹ : Set G) * (↑A : Set G)
have norm_cast : ∀ {a b : G}, a ∈ A⁻¹ * A → b ∈ A⁻¹ * A → a * b ∈ A⁻¹ * A
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a b c d x_1 y_1 : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
have a₁ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔
  (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)
Tactic: convert! lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a b c d x_1 y_1 : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔
    (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)
have a₁ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔ 1 / 2 * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a b c d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ ∀ {a b : G}, a ∈ A⁻¹ * A → b ∈ A⁻¹ * A → a * b ∈ A⁻¹ * A
have h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
Tactic: have h₁ x (hx : x ∈ A) y (hy : y ∈ A) : (1 / 2 : ℚ) * #A < #(x • A ∩ y • A) := by
      convert! lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy
      norm_num
      simp [← Rat.cast_lt (K := ℝ)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b c_1 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a c : G
ha : a ∈ A⁻¹ * A
hc : c ∈ A⁻¹ * A
⊢ a * c ∈ A⁻¹ * A
have ha₁ : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a
Tactic: simp only [mem_mul, mem_inv'] at ha hc
Cleared hypotheses: ha, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b c_1 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a c : G
ha : a ∈ A⁻¹ * A
hc : c ∈ A⁻¹ * A
ha₁ : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a
⊢ a * c ∈ A⁻¹ * A
have hc₁ : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
Tactic: simp only [mem_mul, mem_inv'] at ha hc
Cleared hypotheses: ha, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b c_1 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a c : G
ha : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a
hc : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
⊢ a * c ∈ A⁻¹ * A
have obtain : ∀ (a : G) (ha : a⁻¹ ∈ A) (b : G) (hb : b ∈ A), a * b * c ∈ A⁻¹ * A
Tactic: obtain ⟨a, ha, b, hb, rfl⟩ := ha
Cleared hypotheses: a, 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_1 B S : Finset G
a_1 b_1 c_1 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
c : G
hc : ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ a * b * c ∈ A⁻¹ * A
have obtain : ∀ (c : G) (hc : c⁻¹ ∈ A) (d : G) (hd : d ∈ A), a * b * (c * d) ∈ A⁻¹ * A
Tactic: obtain ⟨c, hc, d, hd, rfl⟩ := hc
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
have refine : LE.le (α := ℚ) (↑(#(b •> A ∩ a⁻¹ •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
Tactic: refine (h₁ b hb _ ha).trans_le ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
⊢ LE.le (α := ℚ) (↑(#(b •> A ∩ a⁻¹ •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
have rw : LE.le (α := ℚ) (↑(#(b⁻¹ •> (b •> A ∩ a⁻¹ •> A))) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
Tactic: rw [← card_smul_finset b⁻¹]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
⊢ a * b * (c * d) ∈ A⁻¹ * A
have h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
Tactic: have h₂ : (1 / 2 : ℚ) * #A < #(A ∩ (a * b)⁻¹ • A) := by
      refine (h₁ b hb _ ha).trans_le ?_
      rw [← card_smul_finset b⁻¹]
      simp [smul_smul, smul_finset_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
have refine : LE.le (α := ℚ) (↑(#(c⁻¹ •> A ∩ d •> A)) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)
Tactic: refine (h₁ _ hc d hd).trans_le ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ LE.le (α := ℚ) (↑(#(c⁻¹ •> A ∩ d •> A)) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)
have rw : LE.le (α := ℚ) (↑(#(c •> (c⁻¹ •> A ∩ d •> A))) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)
Tactic: rw [← card_smul_finset c]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ a * b * (c * d) ∈ A⁻¹ * A
have h₃ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
Tactic: have h₃ : (1 / 2 : ℚ) * #A < #(A ∩ (c * d) • A) := by
      refine (h₁ _ hc d hd).trans_le ?_
      rw [← card_smul_finset c]
      simp [smul_smul, smul_finset_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
h₃ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
⊢ (A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)).Nonempty
have rw : LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
Tactic: rw [← card_pos, ← Nat.cast_pos (α := ℚ)]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
h₃ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have this : #(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)) + #(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A) =
  #(A ∩ (c * d) •> A) + #(A ∩ (a * b)⁻¹ •> A)
Tactic: have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.VerySmallDoubling (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
h₃ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
this :
  #(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)) + #(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A) =
    #(A ∩ (c * d) •> A) + #(A ∩ (a * b)⁻¹ •> A)
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have this₁ : HAdd.hAdd (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
    (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) =
  HAdd.hAdd (α := ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
Tactic: rw [← Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this
Cleared hypotheses: 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_1 B S : Finset G
a_1 b_1 c_1 d_1 x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₁ : ∀ (x : G) (hx : x ∈ A) (y : G) (hy : y ∈ A), 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
h₃ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)
this :
  HAdd.hAdd (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
      (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) =
    HAdd.hAdd (α := ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
have rw : #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A
Tactic: rw [Nat.cast_le, ← inter_union_distrib_left]