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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ r = z •> A⁻¹
have rw : a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))
Tactic: rw [inter_eq_right, ← this, mul_assoc _ A,
      ← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), subset_smul_finset_iff]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))
have simp : (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹
Tactic: simp only [← mul_assoc, smul_smul]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹
have refine : a⁻¹ * z ∈ A⁻¹ * A * A
Tactic: refine smul_finset_subset_mul ?_
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ z ∈ A * A
have hr : r = z •> A⁻¹
Tactic: have hr : r = z • A⁻¹ := by
    rw [inter_eq_right, ← this, mul_assoc _ A,
      ← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), subset_smul_finset_iff]
    simp only [← mul_assoc, smul_smul]
    refine smul_finset_subset_mul ?_
    simp [← hz, mul_mem_mul, ha, hb, hc]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
⊢ l ∪ r ⊆ a •> (A⁻¹ * A)
have rw : A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)
Tactic: rw [union_subset_iff, hl]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
⊢ z ∈ A * A
have lr : l ∪ r ⊆ a •> (A⁻¹ * A)
Tactic: have lr : l ∪ r ⊆ a • (A⁻¹ * A) := by
    rw [union_subset_iff, hl]
    exact ⟨A_subset_aH a ha, 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
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
⊢ #l = #A
have rw : #A = #A
Tactic: rw [hl]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
⊢ z ∈ A * A
have this₁ : #l = #A
Tactic: have : #l = #A := by rw [hl]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this : #l = #A
⊢ #r = #A
have rw : #(z •> A⁻¹) = #A
Tactic: rw [hr, card_smul_finset, card_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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this : #l = #A
rw : #(z •> A⁻¹) = #A
⊢ #r = #A
have rw₁ : #A⁻¹ = #A
Tactic: rw [hr, card_smul_finset, card_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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this : #l = #A
rw : #(z •> A⁻¹) = #A
rw₁ : #A⁻¹ = #A
⊢ #r = #A
have rw₂ : #A = #A
Tactic: rw [hr, card_smul_finset, card_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) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this : #l = #A
⊢ z ∈ A * A
have this₁ : #r = #A
Tactic: have : #r = #A := by rw [hr, card_smul_finset, card_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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this : #r = #A
⊢ #(l ∪ r) < 2 * #A
have refine : #(a •> (A⁻¹ * A)) < 2 * #A
Tactic: refine (card_le_card lr).trans_lt ?_
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this : #r = #A
⊢ #(a •> (A⁻¹ * A)) < 2 * #A
have rw : #(A⁻¹ * A) < 2 * #A
Tactic: rw [card_smul_finset]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this : #r = #A
⊢ z ∈ A * A
have this₁ : #(l ∪ r) < 2 * #A
Tactic: have : #(l ∪ r) < 2 * #A := by
    refine (card_le_card lr).trans_lt ?_
    rw [card_smul_finset]
    exact weak_invMulSubgroup_bound 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ (l ∩ r).Nonempty
have rw : 0 < #(l ∩ r)
Tactic: rw [← card_pos]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ 0 < #(l ∩ r)
have linarith : #(l ∩ r) ≤ 0 → 2 / 2 = 1
Tactic: linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
linarith : #(l ∩ r) ≤ 0 → 2 / 2 = 1
⊢ 0 < #(l ∩ r)
have linarith₁ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 1 2 = 2
Tactic: linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
linarith : #(l ∩ r) ≤ 0 → 2 / 2 = 1
linarith₁ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 1 2 = 2
⊢ 0 < #(l ∩ r)
have linarith₂ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 2 1 = 2
Tactic: linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
linarith : #(l ∩ r) ≤ 0 → 2 / 2 = 1
linarith₁ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 2 1 = 2
⊢ 0 < #(l ∩ r)
have linarith₃ : #(l ∩ r) ≤ 0 → GT.gt (α := ℚ) 2 0
Tactic: linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
linarith : #(l ∩ r) ≤ 0 → 2 / 2 = 1
linarith₁ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 1 2 = 2
linarith₂ : #(l ∩ r) ≤ 0 → HMul.hMul (α := ℚ) 2 1 = 2
linarith₃ : #(l ∩ r) ≤ 0 → GT.gt (α := ℚ) 2 0
⊢ 0 < #(l ∩ r)
have linarith₄ : #(l ∩ r) ≤ 0 →
  -1 + -HSub.hSub (α := ℤ) (↑(#l) : ℤ) (↑(#A) : ℤ) + -HSub.hSub (α := ℤ) (↑(#r) : ℤ) (↑(#A) : ℤ) +
          (HAdd.hAdd (α := ℤ) (↑(#(l ∪ r)) : ℤ) 1 - HMul.hMul (α := ℤ) 2 (↑(#A) : ℤ)) +
        HSub.hSub (α := ℤ) (↑(#(l ∩ r)) : ℤ) 0 +
      -(HAdd.hAdd (α := ℤ) (↑(#(l ∩ r)) : ℤ) (↑(#(l ∪ r)) : ℤ) - HAdd.hAdd (α := ℤ) (↑(#l) : ℤ) (↑(#r) : ℤ)) =
    0
Tactic: linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ z ∈ A * A
have have : ∀ (t : G) (ht : t ∈ l ∩ r), z ∈ A * A
Tactic: have ⟨t, ht⟩ : (l ∩ r).Nonempty := by
    rw [← card_pos]
    linarith [card_inter_add_card_union l r]
-- 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
t : G
ht : t ∈ l ∩ r
⊢ z ∈ A * A
have ht₁ : t ∈ A ∧ t⁻¹ * z ∈ A
Tactic: simp only [hl, hr, mem_inter, ← inv_smul_mem_iff, smul_eq_mul, mem_inv', mul_inv_rev,
    inv_inv] 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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this_1 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this_2 : #l = #A
this_3 : #r = #A
this : #(l ∪ r) < 2 * #A
t : G
ht : t ∈ A ∧ t⁻¹ * z ∈ A
⊢ z ∈ A * A
have rw : ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z
Tactic: rw [mem_mul]
-- 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) = #(A * A)
have obtain : ∀ (a : G) (ha : a ∈ A), #(A⁻¹ * A) = #(A * A)
Tactic: obtain ⟨a, ha⟩ := 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) : ℚ)
a : G
ha : a ∈ A
⊢ #(A⁻¹ * A) = #(A * A)
have simp_rw : #(A⁻¹ * A) = #(a •> ((A⁻¹ * A) <• a))
Tactic: simp_rw [← smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves h ha, card_smul_finset]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a
have refine_1 : a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a
Tactic: refine subset_antisymm ?_ ?_
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
refine_1 : a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a
have refine_2 : (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)
Tactic: refine subset_antisymm ?_ ?_
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a
have refine_1 : a •> (A⁻¹ * A) <• a⁻¹ ⊆ A⁻¹ * A
Tactic: rw [subset_smul_finset_iff, ← op_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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹
have grw : A * (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹
Tactic: grw [smul_finset_subset_mul (by simpa)]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ A * (A⁻¹ * A) * A⁻¹ = A⁻¹ * A
have simp_rw : (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: simp_rw [← coe_inj, coe_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw₁ : (↑(A.invMulSubgroup h) : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₁ : (↑(A.invMulSubgroup h) : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw₂ : (↑(A.invMulSubgroup h) : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₁ : (↑(A.invMulSubgroup h) : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₂ : (↑(A.invMulSubgroup h) : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₁ : (↑(A.invMulSubgroup h) : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₂ : (↑(A.invMulSubgroup h) : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw₄ : (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
rw : (↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₁ : (↑(A.invMulSubgroup h) : Set G) * (↑A : Set G) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₂ : (↑(A.invMulSubgroup h) : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G)) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₃ : (↑(A.invMulSubgroup h) : Set G) * (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
rw₄ : (↑(A.invMulSubgroup h) : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
have rw₅ : (↑A⁻¹ : Set G) * (↑A : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
Tactic: rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) <• a⁻¹ ⊆ A⁻¹ * A
have a₁ : a •> (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹
Tactic: calc
      a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
a₁ : a •> (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹
⊢ a •> (A⁻¹ * A) <• a⁻¹ ⊆ A⁻¹ * A
have a₂ : A * (A⁻¹ * A) * A⁻¹ = A⁻¹ * A
Tactic: calc
      a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]
-- 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)
have refine_2 : a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A
Tactic: rw [subset_smul_finset_iff]