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_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)) + #(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)
-- 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)) : ℚ)
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)
⊢ 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

Premises used: Nat.cast_inj, Nat.cast_add
-- 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)) : ℚ)
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)) : ℚ)
rw : #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A
⊢ LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)

Tactic:
rw [Nat.cast_le, ← inter_union_distrib_left]

Premises used: Finset.inter_union_distrib_left, Nat.cast_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)) : ℚ)
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)) : ℚ)
⊢ #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A

Tactic:
card_le_card inter_subset_left

Premises used: Finset.card_le_card, Finset.inter_subset_left
-- 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)) : ℚ)
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)) : ℚ)
⊢ #(A ∩ ((c * d) •> A ∪ (a * b)⁻¹ •> A)) ≤ #A

Tactic:
exact card_le_card inter_subset_left

Premises used: Finset.card_le_card, Finset.inter_subset_left
-- 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)) : ℚ)
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) : ℚ)

Tactic:
have : (#((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)) : ℚ) ≤ #A := by
        rw [Nat.cast_le, ← inter_union_distrib_left]
        exact card_le_card inter_subset_left
-- 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)) : ℚ)
have : ∀ (t : G) (ht : t ∈ A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)), a * b * (c * d) ∈ A⁻¹ * A
⊢ a * b * (c * d) ∈ A⁻¹ * A

Tactic:
have ⟨t, ht⟩ : ((A ∩ (c * d) • A) ∩ (A ∩ (a * b)⁻¹ • A)).Nonempty := by
      rw [← card_pos, ← Nat.cast_pos (α := ℚ)]
      have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)
      rw [← Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this
      have : (#((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)) : ℚ) ≤ #A := by
        rw [Nat.cast_le, ← inter_union_distrib_left]
        exact card_le_card inter_subset_left
      linarith
-- 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)) : ℚ)
t : G
ht : t ∈ A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)
⊢ t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A

Tactic:
simp only [inter_inter_inter_comm, inter_self, mem_inter, ← inv_smul_mem_iff, inv_inv,
      smul_eq_mul, mul_assoc, mul_inv_rev] at ht

Premises used: Finset.inv_smul_mem_iff, Finset.inter_self, mul_assoc, Finset.inter_inter_inter_comm, inv_inv, mul_inv_rev, smul_eq_mul, Finset.mem_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)) : ℚ)
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
rw : ∃ y ∈ A, ∃ z ∈ A⁻¹, y * z = a * b * (c * d)
⊢ a * b * (c * d) ∈ A⁻¹ * A

Tactic:
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), mem_mul]

Premises used: Finset.mul_inv_eq_inv_mul_of_doubling_lt_two, _private.0.Finset.weaken_doubling, 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_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)) : ℚ)
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
⊢ a * b * t ∈ A

Tactic:
simp [ht, mul_assoc]

Premises used: mul_assoc
-- 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)) : ℚ)
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
⊢ ((c * d)⁻¹ * t)⁻¹ ∈ A⁻¹ ∧ a * b * t * ((c * d)⁻¹ * t)⁻¹ = a * b * (c * d)

Tactic:
simp [ht, mul_assoc]

Premises used: mul_assoc
-- 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)) : ℚ)
t : G
ht : t ∈ A ∧ d⁻¹ * (c⁻¹ * t) ∈ A ∧ a * (b * t) ∈ A
⊢ ∃ y ∈ A, ∃ z ∈ A⁻¹, y * z = a * b * (c * d)

Tactic:
exact ⟨a * b * t, by simp [ht, mul_assoc], ((c * d)⁻¹ * t)⁻¹, by simp [ht, mul_assoc]⟩
-- 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) : ℚ)
have : ∀ (x : G) (hx : x ∈ A), 1 ∈ (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ 1 ∈ (↑A⁻¹ : Set G) * (↑A : Set G)

Tactic:
have ⟨x, hx⟩ : A.Nonempty := nonempty_of_doubling 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_1 y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
hx : x ∈ A
⊢ x ∈ (↑A : Set G) ∧ Eq.{u_1 + 1} (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x⁻¹ x) 1

Tactic:
simp [hx]
-- 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 : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
hx : x ∈ A
⊢ 1 ∈ (↑A⁻¹ : Set G) * (↑A : Set G)

Tactic:
exact ⟨x⁻¹, inv_mem_inv hx, x, by simp [hx]⟩
-- 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 : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
simp : ∀ (x_2 : G), x_2⁻¹ ∈ A → ∀ x_3 ∈ A, x_2 * x_3 = x → ∃ (x_4 : G), x_4⁻¹ ∈ A ∧ ∃ y ∈ A, x_4 * y = x⁻¹
⊢ x ∈ (↑A⁻¹ : Set G) * (↑A : Set G) → x⁻¹ ∈ (↑A⁻¹ : Set G) * (↑A : Set G)

Tactic:
simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, mem_coe,
      and_imp]

Premises used: and_imp, forall_exists_index, Finset.coe_inv, Finset.mem_coe, Set.mem_mul, Set.mem_inv
-- 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 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ b⁻¹⁻¹ ∈ A

Tactic:
simpa using hb
-- 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 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ b⁻¹ * a⁻¹ = (a * b)⁻¹

Tactic:
simp
-- 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 d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
⊢ ∃ (x : G), x⁻¹ ∈ A ∧ ∃ y ∈ A, x * y = (a * b)⁻¹

Tactic:
exact ⟨b⁻¹, by simpa using hb, a⁻¹, ha, by simp⟩
-- 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) : ℚ)
⊢ (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)

Tactic:
rfl

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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
rw : (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)

Tactic:
rw [invMulSubgroup_eq_inv_mul, eq_comm]

Premises used: eq_comm, Finset.invMulSubgroup_eq_inv_mul
-- 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) : ℚ)
norm_cast : A * A⁻¹ = A⁻¹ * A
⊢ (↑A : Set G) * (↑A⁻¹ : Set G) = (↑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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
qify : (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
⊢ #(A * A) < 2 * #A

Tactic:
qify at 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) : ℚ)
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)) : ℚ) +
          2 * (HMul.hMul (α := ℚ) 2 (↑(#(A * A)) : ℚ) - HMul.hMul (α := ℚ) 1 3 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) +
        3 * (HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) - (↑(#(A * A)) : ℚ)) =
      0
linarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 2 0
linarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 3 0
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)

Tactic:
linarith
-- 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) : ℚ)
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
exact mul_inv_eq_inv_mul_of_doubling_lt_two (by qify at h ⊢; linarith)

Premises used: Finset.mul_inv_eq_inv_mul_of_doubling_lt_two
-- 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) : ℚ)
simp : Fintype ↥(A⁻¹ * A)
⊢ Fintype ↥(A.invMulSubgroup h)

Tactic:
simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
    mem_coe]

Premises used: Subgroup.mem_mk, Finset.invMulSubgroup, Finset.coe_mul, Subsemigroup.mem_mk, Submonoid.mem_mk, Finset.mem_coe
-- 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) : ℚ)
⊢ Fintype ↥(A⁻¹ * A)

Tactic:
infer_instance
-- 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) : ℚ)
⊢ A.Nonempty

Tactic:
have h₀ : A.Nonempty := nonempty_of_doubling 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) : ℚ)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
a₁ :
  1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ) ↔
    (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a})) : ℝ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)

Tactic:
convert! lt_card_mul_inv_eq (by simpa using Rat.cast_strictMono (K := ℝ) h) ha

Premises used: _private.0.Finset.lt_card_mul_inv_eq
-- 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) : ℚ)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
a₁ :
  1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ) ↔
    1 / 2 * (↑(#A) : ℝ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℝ)
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ) ↔
    (2 - HDiv.hDiv (α := ℝ) 3 2) * (↑(#A) : ℝ) < (↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = a})) : ℝ)

Tactic:
norm_num
-- 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) : ℚ)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ) ↔
    1 / 2 * (↑(#A) : ℝ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
⊢ ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)

Tactic:
have h₁ a (ha : a ∈ A⁻¹ * A) : (1 / 2 : ℚ) * #A < #{xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a} := by
    convert! lt_card_mul_inv_eq (by simpa using Rat.cast_strictMono (K := ℝ) h) ha
    norm_num
    simp [← Rat.cast_lt (K := ℝ)]
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
rw :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A * A⁻¹
⊢ ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A

Tactic:
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h)]

Premises used: Finset.mul_inv_eq_inv_mul_of_doubling_lt_two, _private.0.Finset.weaken_doubling
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
simp : ∀ (a b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ (z : G), (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹
⊢ ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A * A⁻¹

Tactic:
simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]

Premises used: and_imp, Finset.mem_inv, Prod.forall, Finset.mem_product, 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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, y⁻¹ = b⁻¹

Tactic:
simp [hb]
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, ∃ (z : G), (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹

Tactic:
exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
⊢ ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A

Tactic:
have h₂ : ∀ x ∈ A ×ˢ A, (fun ⟨x, y⟩ => x * y⁻¹) x ∈ A⁻¹ * A := by
    rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h)]
    simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]
    intro a b ha hb
    exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
rw :
  1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) <
    ∑ x ∈ A⁻¹ * A,
      (↑(#({a ∈ A ×ˢ A |
              (match (motive := G × G → G) a with
                | (x, y) => x * y⁻¹) =
                x})) :
        ℚ)
⊢ 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2

Tactic:
rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₂, Nat.cast_sum]

Premises used: Finset.card_product, sq, Finset.card_eq_sum_card_fiberwise, Nat.cast_sum, Nat.cast_pow
-- 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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
⊢ (A⁻¹ * A).Nonempty

Tactic:
simp [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) : ℚ)
h₀ : A.Nonempty
h₁ : ∀ (a : G) (ha : a ∈ A⁻¹ * A), 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun (x : G × G) ↦
          (match (motive := G × G → G) x with
            | (x, y) => x * y⁻¹ :
            G))
        x ∈
      A⁻¹ * A
refine : ∑ i ∈ A⁻¹ * A, 1 / 2 * (↑(#A) : ℚ) = 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ)
⊢ 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) <
    ∑ x ∈ A⁻¹ * A,
      (↑(#({a ∈ A ×ˢ A |
              (match (motive := G × G → G) a with
                | (x, y) => x * y⁻¹) =
                x})) :
        ℚ)

Tactic:
refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_

Premises used: LT.lt.trans_eq', Finset.sum_lt_sum_of_nonempty