awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
K : ℝ
A 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)) : ℝ)
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
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#(a •> A ∩ b •> A)) : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ HMul.hMul (α := ℝ) 2 (↑(#A) : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑(#(a •> A ∩ b •> A)) : ℝ) (↑(#(B * A)) : ℝ)

Tactic:
have : 2 * (#A : ℝ) ≤ #(a •> A ∩ b •> A) + #(B * A) := mod_cast big_intersection ha hb
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℝ)
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
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#(a •> A ∩ b •> A)) : ℝ)

Tactic:
linarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x

Tactic:
simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx

Premises used: exists_exists_and_eq_and, Finset.mem_inv, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
obtain :
  ∀ (a : G) (ha : a ∈ B) (b : G) (hb : b ∈ B),
    (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
rw : (2 - K) * (↑(#A) : ℝ) ≤ (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) ≤ (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)

Tactic:
rw [card_mul_inv_eq_convolution_inv]

Premises used: Finset.card_mul_inv_eq_convolution_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ) ≤ (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)

Tactic:
simpa [card_smul_inter_smul] using le_card_smul_inter_smul hA ha hb

Premises used: _private.0.Finset.le_card_smul_inter_smul, Finset.card_smul_inter_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ ∃ a ∈ B, ∃ z ∈ B, a⁻¹ * z = x

Tactic:
simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx

Premises used: exists_exists_and_eq_and, Finset.mem_inv, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
obtain :
  ∀ (a : G) (ha : a ∈ B) (b : G) (hb : b ∈ B),
    (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x})) : ℝ)

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
rw : (2 - K) * (↑(#A) : ℝ) < (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)
⊢ (2 - K) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a⁻¹ * b})) : ℝ)

Tactic:
rw [card_mul_inv_eq_convolution_inv]

Premises used: Finset.card_mul_inv_eq_convolution_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℝ) < (↑(A.convolution A⁻¹ (a⁻¹ * b)) : ℝ)

Tactic:
simpa [card_smul_inter_smul] using lt_card_smul_inter_smul hA ha hb

Premises used: Finset.card_smul_inter_smul, _private.0.Finset.lt_card_smul_inter_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
simp : ∀ x ∈ A, ∀ x_1 ∈ A, x⁻¹ * x_1 = z → ∃ y ∈ A, ∃ a ∈ A, y * a⁻¹ = z
⊢ z ∈ A⁻¹ * A → z ∈ A * A⁻¹

Tactic:
simp only [mem_mul, forall_exists_index, and_imp, mem_inv,
    exists_exists_and_eq_and]

Premises used: and_imp, forall_exists_index, exists_exists_and_eq_and, Finset.mem_inv, Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ (x •> A ∩ y •> A).Nonempty

Tactic:
simpa using lt_card_smul_inter_smul (K := 2) (mod_cast h) hx hy

Premises used: _private.0.Finset.lt_card_smul_inter_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
have : ∀ (t : G) (ht : t ∈ x •> A ∩ y •> A), ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y
⊢ ∃ 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
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t

Tactic:
simp only [mem_inter, mem_smul_finset, smul_eq_mul] at ht

Premises used: Finset.mem_smul_finset, smul_eq_mul, Finset.mem_inter
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
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
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
obtain ⟨⟨z, hz, hzxwy⟩, w, hw, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
⟨z, hz, w, hw, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
refine : z * w⁻¹ = x⁻¹ * y
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
refine ⟨z, hz, w, hw, ?_⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)
rw₃ rw₄ : z = z
⊢ z * w⁻¹ = x⁻¹ * y

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)

Premises used: _private.0.Finset.mul_inv_eq_inv_mul_of_doubling_lt_two_aux, Finset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
refine : A * A⁻¹ ⊆ A⁻¹ * A
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
refine Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)

Premises used: _private.0.Finset.mul_inv_eq_inv_mul_of_doubling_lt_two_aux, Finset.Subset.antisymm
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ #(A⁻¹ * A⁻¹) < 2 * #A⁻¹

Tactic:
simpa [← mul_inv_rev] using h

Premises used: mul_inv_rev
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ ⊆ A⁻¹ * A

Tactic:
simpa using
    mul_inv_eq_inv_mul_of_doubling_lt_two_aux (A := A⁻¹) (by simpa [← mul_inv_rev] using h)

Premises used: _private.0.Finset.mul_inv_eq_inv_mul_of_doubling_lt_two_aux
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
rw : (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
⊢ #(A * A) < 2 * #A

Tactic:
rw [← Nat.cast_lt (α := ℚ), Nat.cast_mul, Nat.cast_two]

Premises used: Nat.cast_mul, Nat.cast_lt, Nat.cast_two
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
linarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 3 0
linarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 2 0
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)

Tactic:
linarith only [h]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
by_contra! : ∀ (h : (↑(#(HMul.hMul (α := Finset G) ∅ ∅)) : ℚ) < 3 / 2 * (↑(card.{u_1} (α := G) ∅) : ℚ)), False
⊢ A.Nonempty

Tactic:
by_contra! rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
h : (↑(#(HMul.hMul (α := Finset G) ∅ ∅)) : ℚ) < 3 / 2 * (↑(card.{u_1} (α := G) ∅) : ℚ)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℚ)
norm_cast : ∀ {a b : G}, a ∈ A⁻¹ * A → b ∈ A⁻¹ * A → a * b ∈ A⁻¹ * 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)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ (↑(#(A * A)) : ℝ) < HDiv.hDiv (α := ℝ) 3 2 * (↑(#A) : ℝ)

Tactic:
simpa using Rat.cast_strictMono (K := ℝ) h

Premises used: Rat.cast_strictMono
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
a₁ :
  1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔
    (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ)

Tactic:
convert! lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy

Premises used: _private.0.Finset.lt_card_smul_inter_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
a₁ : 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔ 1 / 2 * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(x •> A ∩ y •> A)) : ℚ) ↔
    (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ) ↔ 1 / 2 * (↑(#A) : ℝ) < (↑(#(x •> A ∩ y •> A)) : ℝ)

Tactic:
simp [← Rat.cast_lt (K := ℝ)]

Premises used: Rat.cast_lt
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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) : ℚ)
⊢ ∀ (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 := ℝ)]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a

Tactic:
simp only [mem_mul, mem_inv'] at ha hc

Premises used: Finset.mem_inv', Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
⊢ ∃ (y : G), y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c

Tactic:
simp only [mem_mul, mem_inv'] at ha hc

Premises used: Finset.mem_inv', Finset.mem_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
obtain : ∀ (a : G) (ha : a⁻¹ ∈ A) (b : G) (hb : b ∈ A), a * b * c ∈ A⁻¹ * A
⊢ a * c ∈ A⁻¹ * A

Tactic:
obtain ⟨a, ha, b, hb, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
obtain : ∀ (c : G) (hc : c⁻¹ ∈ A) (d : G) (hd : d ∈ A), a * b * (c * d) ∈ A⁻¹ * A
⊢ a * b * c ∈ A⁻¹ * A

Tactic:
obtain ⟨c, hc, d, hd, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)

Tactic:
(h₁ b hb _ ha).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
refine : LE.le (α := ℚ) (↑(#(b •> A ∩ a⁻¹ •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)

Tactic:
refine (h₁ b hb _ ha).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
rw : LE.le (α := ℚ) (↑(#(b⁻¹ •> (b •> A ∩ a⁻¹ •> A))) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)
⊢ LE.le (α := ℚ) (↑(#(b •> A ∩ a⁻¹ •> A)) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)

Tactic:
rw [← card_smul_finset b⁻¹]

Premises used: Inv.inv, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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⁻¹ •> (b •> A ∩ a⁻¹ •> A))) : ℚ) (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ)

Tactic:
simp [smul_smul, smul_finset_inter]

Premises used: Finset.smul_finset_inter, smul_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)

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]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)

Tactic:
(h₁ _ hc d hd).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)
refine : LE.le (α := ℚ) (↑(#(c⁻¹ •> A ∩ d •> A)) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#(A ∩ (c * d) •> A)) : ℚ)

Tactic:
refine (h₁ _ hc d hd).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)
rw : LE.le (α := ℚ) (↑(#(c •> (c⁻¹ •> A ∩ d •> A))) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)
⊢ LE.le (α := ℚ) (↑(#(c⁻¹ •> A ∩ d •> A)) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)

Tactic:
rw [← card_smul_finset c]

Premises used: Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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 •> (c⁻¹ •> A ∩ d •> A))) : ℚ) (↑(#(A ∩ (c * d) •> A)) : ℚ)

Tactic:
simp [smul_smul, smul_finset_inter]

Premises used: Finset.smul_finset_inter, smul_smul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)

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]
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)) : ℚ)
rw : LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
⊢ (A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)).Nonempty

Tactic:
rw [← card_pos, ← Nat.cast_pos (α := ℚ)]

Premises used: Nat.cast_pos, Finset.card_pos