awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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)) : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have this₁ : 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
-- 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_1 :
  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)) : ℚ)
this : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have linarith : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 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_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_1 :
  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)) : ℚ)
this : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
linarith : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have linarith₁ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
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_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_1 :
  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)) : ℚ)
this : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
linarith : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
linarith₁ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have linarith₂ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 2 1 = 2
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_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_1 :
  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)) : ℚ)
this : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
linarith : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
linarith₁ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 2 1 = 2
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have linarith₃ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → GT.gt (α := ℚ) 2 0
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_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_1 :
  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)) : ℚ)
this : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) (↑(#A) : ℚ)
linarith : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
linarith₁ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 2 1 = 2
linarith₃ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → GT.gt (α := ℚ) 2 0
linarith₄ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
linarith₅ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₆ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 2 1 = 2
linarith₇ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → GT.gt (α := ℚ) 2 0
linarith₈ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → 2 / 2 = 1
linarith₉ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₁₀ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → HMul.hMul (α := ℚ) 2 1 = 2
linarith₁₁ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 → GT.gt (α := ℚ) 2 0
⊢ LT.lt (α := ℚ) 0 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ)
have linarith₁₂ : LE.le (α := ℚ) (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) 0 →
  HMul.hMul (α := ℚ) 1 1 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) - HMul.hMul (α := ℚ) 2 (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ) +
            (HMul.hMul (α := ℚ) 1 1 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) -
              HMul.hMul (α := ℚ) 2 (↑(#(A ∩ (c * d) •> A)) : ℚ)) +
          2 *
            -(HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) +
                  HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) -
                (HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (c * d) •> A)) : ℚ) +
                  HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (a * b)⁻¹ •> A)) : ℚ))) +
        2 *
          (HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (c * d) •> A ∪ A ∩ (a * b)⁻¹ •> A)) : ℚ) - HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) +
      2 * (HMul.hMul (α := ℚ) 1 (↑(#(A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A))) : ℚ) - HMul.hMul (α := ℚ) 1 0) =
    0
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_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 * b * (c * d) ∈ A⁻¹ * A
have have : ∀ (t : G) (ht : t ∈ A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> 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
-- 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)) : ℚ)
t : G
ht : t ∈ A ∩ (c * d) •> A ∩ (A ∩ (a * b)⁻¹ •> A)
⊢ a * b * (c * d) ∈ A⁻¹ * A
have ht₁ : 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
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
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 * (c * d) ∈ A⁻¹ * A
have rw : ∃ y ∈ A, ∃ z ∈ A⁻¹, y * z = a * b * (c * d)
Tactic: rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), mem_mul]
-- 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) : ℚ)
⊢ 1 ∈ (↑A⁻¹ : Set G) * (↑A : Set G)
have have : ∀ (x : G) (hx : x ∈ A), 1 ∈ (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: have ⟨x, hx⟩ : A.Nonempty := nonempty_of_doubling 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_1 y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
x : G
⊢ x ∈ (↑A⁻¹ : Set G) * (↑A : Set G) → x⁻¹ ∈ (↑A⁻¹ : Set G) * (↑A : Set G)
have 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⁻¹
Tactic: simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ (↑(A.invMulSubgroup h) : Set G) = (↑A : Set G) * (↑A⁻¹ : Set G)
have rw : (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [invMulSubgroup_eq_inv_mul, eq_comm]
-- 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 : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have norm_cast : A * A⁻¹ = 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ #(A * A) < 2 * #A
have qify : (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
Tactic: qify at 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)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → 2 / 2 = 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
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
-- 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
-- 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
-- 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)) : ℚ) +
        2 * (HMul.hMul (α := ℚ) 2 (↑(#(A * A)) : ℚ) - HMul.hMul (α := ℚ) 1 3 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) +
      3 * (HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) - (↑(#(A * A)) : ℚ)) =
    0
Tactic: linarith
-- 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)) : ℚ) +
          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
⊢ (↑(#(A * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
have linarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A * A)) : ℚ) → GT.gt (α := ℚ) 3 0
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_1 B S : Finset G
a b c d x y : G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ Fintype ↥(A.invMulSubgroup h)
have simp : Fintype ↥(A⁻¹ * A)
Tactic: simp only [invMulSubgroup, ← coe_mul, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,
    mem_coe]
-- 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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ #(A⁻¹ * A) < 2 * #A
have h₀ : A.Nonempty
Tactic: have h₀ : A.Nonempty := nonempty_of_doubling 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) : ℚ)
h₀ : A.Nonempty
a : G
ha : a ∈ A⁻¹ * A
⊢ 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ)
have 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: convert! lt_card_mul_inv_eq (by simpa using Rat.cast_strictMono (K := ℝ) h) ha
-- 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) : ℚ)
h₀ : A.Nonempty
a : G
ha : 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})) : ℝ)
have a₁ : 1 / 2 * (↑(#A) : ℚ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a})) : ℚ) ↔
  1 / 2 * (↑(#A) : ℝ) < (↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
h₀ : A.Nonempty
⊢ #(A⁻¹ * A) < 2 * #A
have h₁ : ∀ (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 := ℝ)]
-- 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) : ℚ)
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
have rw : ∀ 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)]
-- 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) : ℚ)
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⁻¹
have simp : ∀ (a b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ (z : G), (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹
Tactic: simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]
-- 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)) : ℚ) < 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⁻¹ * A) < 2 * #A
have h₂ : ∀ 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⟩
-- 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) : ℚ)
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
⊢ 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
have rw : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) <
  ∑ x ∈ A⁻¹ * A,
    (↑(#({a ∈ A ×ˢ A |
            (match (motive := G × G → G) a with
              | (x, y) => x * y⁻¹) =
              x})) :
      ℚ)
Tactic: rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₂, Nat.cast_sum]
-- 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) : ℚ)
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
⊢ 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) <
    ∑ x ∈ A⁻¹ * A,
      (↑(#({a ∈ A ×ˢ A |
              (match (motive := G × G → G) a with
                | (x, y) => x * y⁻¹) =
                x})) :
        ℚ)
have refine : ∑ i ∈ A⁻¹ * A, 1 / 2 * (↑(#A) : ℚ) = 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ)
Tactic: refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_