awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
refine : #(a •> (A⁻¹ * A)) < 2 * #A
⊢ #(l ∪ r) < 2 * #A

Tactic:
refine (card_le_card lr).trans_lt ?_

Premises used: Finset.card_le_card, LE.le.trans_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) : ℚ)
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
rw : #(A⁻¹ * A) < 2 * #A
⊢ #(a •> (A⁻¹ * A)) < 2 * #A

Tactic:
rw [card_smul_finset]

Premises used: Finset.card_smul_finset
-- 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 : 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) < 2 * #A

Tactic:
weak_invMulSubgroup_bound h

Premises used: _private.0.Finset.weak_invMulSubgroup_bound
-- 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 : 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) < 2 * #A

Tactic:
exact weak_invMulSubgroup_bound h

Premises used: _private.0.Finset.weak_invMulSubgroup_bound
-- 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 : 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

Tactic:
have : #(l ∪ r) < 2 * #A := by
    refine (card_le_card lr).trans_lt ?_
    rw [card_smul_finset]
    exact weak_invMulSubgroup_bound 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) : ℚ)
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
rw : 0 < #(l ∩ r)
⊢ (l ∩ r).Nonempty

Tactic:
rw [← card_pos]

Premises used: Finset.card_pos
-- 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 : 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
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
⊢ 0 < #(l ∩ r)

Tactic:
linarith [card_inter_add_card_union l r]

Premises used: Finset.card_inter_add_card_union
-- 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 : 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
have : ∀ (t : G) (ht : t ∈ l ∩ r), z ∈ A * A
⊢ z ∈ A * A

Tactic:
have ⟨t, ht⟩ : (l ∩ r).Nonempty := by
    rw [← card_pos]
    linarith [card_inter_add_card_union l r]
-- 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 : 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
⊢ 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

Premises used: Finset.inv_smul_mem_iff, Finset.mem_inv', 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
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
rw : ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z
⊢ z ∈ A * A

Tactic:
rw [mem_mul]

Premises used: 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) : ℚ)
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
⊢ t * (t⁻¹ * z) = z

Tactic:
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 : 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
⊢ ∃ y ∈ A, ∃ z_1 ∈ A, y * z_1 = z

Tactic:
exact ⟨t, ht.1, t⁻¹ * z, ht.2, by simp⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
(subgroup_strong_bound_right h a ha).antisymm (subgroup_strong_bound_left h a ha)

Premises used: _private.0.Finset.subgroup_strong_bound_right, HasSubset.Subset.antisymm, _private.0.Finset.subgroup_strong_bound_left
-- 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) : ℚ)
obtain : ∀ (a : G) (ha : a ∈ A), #(A⁻¹ * A) = #(A * A)
⊢ #(A⁻¹ * A) = #(A * A)

Tactic:
obtain ⟨a, ha⟩ := nonempty_of_doubling h

Premises used: _private.0.Finset.nonempty_of_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) : ℚ)
a : G
ha : a ∈ A
simp_rw : #(A⁻¹ * A) = #(a •> ((A⁻¹ * 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]

Premises used: Finset.card_smul_finset, Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
subset_antisymm ?_ ?_

Premises used: subset_antisymm
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
refine_2 : (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a

Tactic:
refine subset_antisymm ?_ ?_

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

Tactic:
rw [subset_smul_finset_iff, ← op_inv]

Premises used: Finset.subset_smul_finset_iff, MulOpposite.op_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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⁻¹

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
grw grw₁ : A * (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹
⊢ a •> (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹

Tactic:
grw [smul_finset_subset_mul (by simpa)]

Premises used: Finset.smul_finset_subset_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
simp_rw : (↑A : Set G) * ((↑A⁻¹ : Set G) * (↑A : Set G)) * (↑A⁻¹ : Set G) = (↑A⁻¹ : Set G) * (↑A : Set G)
⊢ A * (A⁻¹ * A) * A⁻¹ = A⁻¹ * A

Tactic:
simp_rw [← coe_inj, coe_mul]

Premises used: Finset.coe_mul, Finset.coe_inj
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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)
rw₅ 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)

Tactic:
rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]

Premises used: coe_mul_coe, mul_assoc, Finset.invMulSubgroup_eq_mul_inv, 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
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⁻¹ * 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]

Premises used: HMul.hMul, Finset.op_smul_finset_subset_mul, Inv.inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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_2 : a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A
⊢ (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)

Tactic:
rw [subset_smul_finset_iff]

Premises used: Finset.subset_smul_finset_iff
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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
grw grw₁ : A⁻¹ * (A⁻¹ * A * A) ⊆ A⁻¹ * (A⁻¹ * A * A)
⊢ A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)

Tactic:
grw [op_smul_finset_subset_mul (by simpa)]

Premises used: Finset.op_smul_finset_subset_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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⁻¹ * (A * A⁻¹ * A) = A * A⁻¹
⊢ A⁻¹ * (A⁻¹ * A * A) = 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
a : G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
ha : a ∈ A
simp_rw : (↑A⁻¹ : Set G) * ((↑A : Set G) * (↑A⁻¹ : Set G) * (↑A : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹

Tactic:
simp_rw [← coe_inj, coe_mul]

Premises used: Finset.coe_mul, Finset.coe_inj
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
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⁻¹ : Set G) * ((↑A : Set G) * (↑(A.invMulSubgroup h) : Set G)) = (↑A : Set G) * (↑A⁻¹ : Set G)
rw₂ : (↑A⁻¹ : Set G) * (↑A : Set G) * (↑(A.invMulSubgroup h) : 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.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
rw₅ 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)

Tactic:
rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]

Premises used: coe_mul_coe, mul_assoc, Finset.invMulSubgroup_eq_mul_inv, 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
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⁻¹ * A
⊢ a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A

Tactic:
calc
      a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * (A⁻¹ * A) <• a := smul_finset_subset_mul (by simpa)
      _ ⊆ A⁻¹ * ((A⁻¹ * A) * A) := by grw [op_smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]
        simp_rw [← coe_inj, coe_mul]
        rw [mul_assoc, ← invMulSubgroup_eq_inv_mul _ h, ← mul_assoc,
          ← invMulSubgroup_eq_inv_mul _ h, ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe]

Premises used: HMul.hMul, Inv.inv, HSMul.hSMul, MulOpposite.op, Finset.smul_finset_subset_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 : Subgroup G := A.invMulSubgroup h
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H),
    (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ) ∧
      ∀ a ∈ A, (↑A : Set G) ⊆ a •> (↑H : Set G) ∧ a •> (↑H : Set G) = (↑H : Set G) <• a

Tactic:
⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩

Premises used: inferInstance, 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)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
H : Subgroup G := A.invMulSubgroup h
refine_1 : (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
refine_2 : ∀ (a : G) (ha : a ∈ A), (↑A : Set G) ⊆ a •> (↑H : Set G)
refine_3 : ∀ (a : G) (ha : a ∈ A), a •> (↑H : Set G) = (↑H : Set G) <• a
⊢ ∃ (H : Subgroup G) (x : Fintype ↥H),
    (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ) ∧
      ∀ a ∈ A, (↑A : Set G) ⊆ a •> (↑H : Set G) ∧ a •> (↑H : Set G) = (↑H : Set G) <• a

Tactic:
refine ⟨H, inferInstance, ?_, fun a ha ↦ ⟨?_, ?_⟩⟩
-- 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 : Subgroup G := A.invMulSubgroup h
refine_1 : (↑(Nat.card.{u_1} ↥(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ (↑(Fintype.card.{u_1} ↥H) : ℚ) < 3 / 2 * (↑(#A) : ℚ)

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

Premises used: Subgroup.mem_mk, Finset.invMulSubgroup, Finset.coe_mul, Subsemigroup.mem_mk, Submonoid.mem_mk, Finset.mem_coe, Nat.card_eq_fintype_card
-- 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 : Subgroup G := A.invMulSubgroup h
refine_1 : (↑(#(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
⊢ (↑(Nat.card.{u_1} ↥(A⁻¹ * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)

Tactic:
rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]

Premises used: Nat.card_eq_finsetCard, Finset.card_inv_mul_of_doubling_lt_three_halves
-- 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 : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
refine_2 : (↑A : Set G) ⊆ a •> ((↑A⁻¹ : Set G) * (↑A : Set G))
⊢ (↑A : Set G) ⊆ a •> (↑H : Set G)

Tactic:
rw [invMulSubgroup_eq_inv_mul]

Premises used: 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) : ℚ)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ (↑A : Set G) ⊆ a •> ((↑A⁻¹ : Set G) * (↑A : Set G))

Tactic:
exact_mod_cast A_subset_aH a ha

Premises used: _private.0.Finset.A_subset_aH
-- 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 : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> (↑H : Set G) = (↑H : Set G) <• a

Tactic:
simpa [H, invMulSubgroup_eq_inv_mul, ← coe_inv, ← coe_mul, ← coe_smul_finset]
      using smul_inv_mul_eq_inv_mul_opSMul h ha

Premises used: Finset.smul_inv_mul_eq_inv_mul_opSMul, Finset.coe_mul, Finset.coe_smul_finset, Finset.coe_inv, Finset.invMulSubgroup_eq_inv_mul
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ (↑H : Set G)
hx : (↑H : Set G) <• x = c
⊢ x ∈ c

Tactic:
simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]

Premises used: SetLike.mem_coe, mul_inv_cancel, OneMemClass.one_mem, mem_rightCoset_iff
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ (↑H : Set G)
refine : ∀ (hx : x ∈ c), (↑H : Set G) <• x = c
⊢ x ∈ c ↔ (↑H : Set G) <• x = c

Tactic:
refine ⟨fun hx => ?_, fun hx =>
    by simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]⟩
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ (↑H : Set G)
hx : x ∈ c
obtain :
  ∀ (a : G) (hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x),
    (↑H : Set G) <• x = (fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }
⊢ (↑H : Set G) <• x = c

Tactic:
obtain ⟨⟨a⟩, rfl⟩ := hc

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
change : (↑H : Set G) <• x = (↑H : Set G) <• a
⊢ (↑H : Set G) <• x = (fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }

Tactic:
change _ = _ <• _
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
ha : x * a⁻¹ ∈ H
⊢ (↑H : Set G) <• x = (↑H : Set G) <• a

Tactic:
rw [eq_comm, smul_eq_iff_eq_inv_smul, ← op_inv, op_smul_op_smul, rightCoset_mem_rightCoset]

Premises used: op_smul_op_smul, eq_comm, rightCoset_mem_rightCoset, smul_eq_iff_eq_inv_smul, MulOpposite.op_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x a : G
hx : Membership.mem (γ := Set G) ((fun (m : Gᵐᵒᵖ) ↦ m •> (↑H : Set G)) { unop' := a }) x
ha : x <• a⁻¹ ∈ H
ha₁ : (op a)⁻¹ •> x ∈ H
ha₂ : (op a)⁻¹ •> x ∈ (↑H : Set G)
ha₃ ha₄ ha₅ ha₆ : x ∈ (↑H : Set G) <• a
⊢ x * a⁻¹ ∈ H

Tactic:
rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]

Premises used: op_smul_eq_mul, SetLike.mem_coe, Set.mem_smul_set_iff_inv_smul_mem, MulOpposite.op_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
x y : G
⊢ x ∈ (↑H : Set G) <• y ↔ (↑H : Set G) <• x = (↑H : Set G) <• y

Tactic:
op_smul_eq_iff_mem (mem_orbit _ _)

Premises used: MulAction.mem_orbit, _private.0.Finset.op_smul_eq_iff_mem