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) : ℚ)
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
⊢ ∑ i ∈ A⁻¹ * A, 1 / 2 * (↑(#A) : ℚ) = 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ)

Tactic:
simp only [sum_const, nsmul_eq_mul, mul_comm]

Premises used: mul_comm, nsmul_eq_mul, Finset.sum_const
-- 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
⊢ 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2

Tactic:
have : ((1 / 2 : ℚ) * #A) * #(A⁻¹ * A) < (#A : ℚ) ^ 2 := by
    rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₂, Nat.cast_sum]
    refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_
    simp only [sum_const, nsmul_eq_mul, mul_comm]
-- 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
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
rw : (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)
⊢ #(A⁻¹ * A) < 2 * #A

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

Premises used: Nat.cast_mul, Nat.cast_lt, Nat.cast_two
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 3 / 2 * (↑(#A) : ℚ)
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
this : 1 / 2 * (↑(#A) : ℚ) * (↑(#(A⁻¹ * A)) : ℚ) < HPow.hPow (α := ℚ) (β := ℕ) (↑(#A) : ℚ) 2
nlinarith : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 1 = 1
nlinarith₁ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₂ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₃ nlinarith₄ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
nlinarith₅ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 * HPow.hPow (α := ℚ) (β := ℕ) 1 2 = 2
nlinarith₆ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → GT.gt (α := ℚ) 2 0
nlinarith₇ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → 2 / 2 = 1
nlinarith₈ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 1 2 = 2
nlinarith₉ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → HMul.hMul (α := ℚ) 2 1 = 2
nlinarith₁₀ : HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) → GT.gt (α := ℚ) 2 0
nlinarith₁₁ :
  HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ) ≤ (↑(#(A⁻¹ * A)) : ℚ) →
    HMul.hMul (α := ℚ) 1 1 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) * HMul.hMul (α := ℚ) 1 (↑(#(A⁻¹ * A)) : ℚ) -
          2 * HPow.hPow (β := ℕ) (HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ)) 2 +
        (0 -
          HSub.hSub (α := ℚ) 0 (↑(#A) : ℚ) *
            (HMul.hMul (α := ℚ) 1 2 * HMul.hMul (α := ℚ) 1 (↑(#A) : ℚ) - HMul.hMul (α := ℚ) 1 (↑(#(A⁻¹ * A)) : ℚ))) =
      0
⊢ (↑(#(A⁻¹ * A)) : ℚ) < HMul.hMul (α := ℚ) 2 (↑(#A) : ℚ)

Tactic:
nlinarith
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
rw : A ⊆ a •> A⁻¹ * A
⊢ A ⊆ a •> (A⁻¹ * A)

Tactic:
rw [← smul_mul_assoc]

Premises used: smul_mul_assoc
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ 1 ∈ a •> A⁻¹

Tactic:
simp [← inv_smul_mem_iff, inv_mem_inv ha]

Premises used: Finset.inv_smul_mem_iff, Finset.inv_mem_inv
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A

Tactic:
exact subset_mul_right _ (by simp [← inv_smul_mem_iff, inv_mem_inv ha])

Premises used: Finset.subset_mul_right
-- 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
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
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.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
rw₄ rw₅ : (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A

Tactic:
rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]

Premises used: coe_mul_coe, Finset.coe_mul, Finset.coe_inj, 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) : ℚ)
a : G
ha : a ∈ A
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A

Tactic:
have h₁ : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
    rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- 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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
rw : a •> ((A⁻¹ * A) <• a) = (a •> (A⁻¹ * A) * (A⁻¹ * A)) <• a
rw₁ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A * (A⁻¹ * A)) <• a
rw₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) <• a
rw₃ rw₄ : a •> (A⁻¹ * A) <• a = a •> (A⁻¹ * A) <• a
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]

Premises used: smul_mul_assoc, mul_smul_comm, SMulCommClass.smul_comm
-- 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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
have h₂ : a • op a • (A⁻¹ * A) = (a • (A⁻¹ * A)) * (op a • (A⁻¹ * A)) := by
    rw [mul_smul_comm, smul_mul_assoc, h₁, smul_comm]
-- 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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
rw : A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> ((A⁻¹ * A) <• a)

Tactic:
rw [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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
mul_subset_mul (A_subset_aH a ha) ?_

Premises used: _private.0.Finset.A_subset_aH, Finset.mul_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) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
refine : A ⊆ (A⁻¹ * A) <• a
⊢ A * A ⊆ a •> (A⁻¹ * A) * (A⁻¹ * A) <• a

Tactic:
refine mul_subset_mul (A_subset_aH a ha) ?_

Premises used: _private.0.Finset.A_subset_aH, Finset.mul_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) : ℚ)
a : G
ha : a ∈ A
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
rw : A ⊆ A * A⁻¹ <• a
⊢ A ⊆ (A⁻¹ * A) <• a

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

Premises used: Finset.mul_inv_eq_inv_mul_of_doubling_lt_two, _private.0.Finset.weaken_doubling, mul_smul_comm
-- 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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ 1 ∈ A⁻¹ <• a

Tactic:
simp [← inv_smul_mem_iff, inv_mem_inv ha]

Premises used: Finset.inv_smul_mem_iff, Finset.inv_mem_inv
-- 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
h₁ : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
h₂ : a •> ((A⁻¹ * A) <• a) = a •> (A⁻¹ * A) * (A⁻¹ * A) <• a
⊢ A ⊆ A * A⁻¹ <• a

Tactic:
exact subset_mul_left _ (by simp [← inv_smul_mem_iff, inv_mem_inv ha])

Premises used: Finset.subset_mul_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) : ℚ)
a : G
ha : a ∈ A
z : G
hz : z ∈ a •> ((A⁻¹ * A) <• a)
⊢ ∃ (a_1 : G), (∃ a ∈ A, ∃ z ∈ A, a⁻¹ * z = a_1) ∧ a * (a_1 * a) = z

Tactic:
simp only [mem_smul_finset, smul_eq_mul_unop, unop_op, smul_eq_mul, mem_mul, mem_inv,
    exists_exists_and_eq_and] at hz

Premises used: exists_exists_and_eq_and, Finset.mem_smul_finset, MulOpposite.unop_op, Finset.mem_inv, smul_eq_mul, MulOpposite.smul_eq_mul_unop, 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 : G
hz : ∃ (a_1 : G), (∃ a ∈ A, ∃ z ∈ A, a⁻¹ * z = a_1) ∧ a * (a_1 * a) = z
obtain : ∀ (b : G) (hb : b ∈ A) (c : G) (hc : c ∈ A) (hz : a * (b⁻¹ * c * a) = z), z ∈ A * A
⊢ z ∈ A * A

Tactic:
obtain ⟨d, ⟨b, hb, c, hc, rfl⟩, hz⟩ := hz

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) : ℚ)
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⁻¹
rw : (↑(A⁻¹ * A * (A⁻¹ * A)) : Set G) = (↑(A⁻¹ * A) : Set G)
rw₁ : (↑(A⁻¹ * A) : Set G) * (↑(A⁻¹ * A) : Set G) = (↑(A⁻¹ * A) : Set G)
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.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
rw₄ rw₅ : (↑(A.invMulSubgroup h) : Set G) = (↑(A.invMulSubgroup h) : Set G)
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A

Tactic:
rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]

Premises used: coe_mul_coe, Finset.coe_mul, Finset.coe_inj, 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) : ℚ)
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⁻¹
⊢ A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A

Tactic:
have : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
    rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
rw : (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)
⊢ l = A

Tactic:
rw [inter_eq_left, ← this, subset_smul_finset_iff]

Premises used: Finset.subset_smul_finset_iff, Finset.inter_eq_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) : ℚ)
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
simp : (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * A
⊢ (z * a⁻¹)⁻¹ •> A ⊆ A⁻¹ * A * (A⁻¹ * A)

Tactic:
simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]

Premises used: mul_assoc, inv_inv, mul_inv_rev
-- Module: Mathlib.Combinatorics.Additive.VerySmallDoubling
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq G
A : Finset G
h : (↑(#(A * A)) : ℚ) < 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
⊢ (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * A

Tactic:
smul_finset_subset_mul ?_

Premises used: Set.Mem, setOf, 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) : ℚ)
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
refine : a * a⁻¹ * c⁻¹ * b * a⁻¹ ∈ A⁻¹ * A * A⁻¹
⊢ (a * a⁻¹ * c⁻¹ * b * a⁻¹) •> A ⊆ A⁻¹ * A * A⁻¹ * A

Tactic:
refine smul_finset_subset_mul ?_

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
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
⊢ a * a⁻¹ * c⁻¹ * b * a⁻¹ ∈ A⁻¹ * A * A⁻¹

Tactic:
simp [mul_mem_mul, ha, hb, hc]

Premises used: Finset.mul_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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
⊢ l = A

Tactic:
have hl : l = A := by
    rw [inter_eq_left, ← this, subset_smul_finset_iff]
    simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]
    refine smul_finset_subset_mul ?_
    simp [mul_mem_mul, ha, hb, hc]
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
rw : a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))
⊢ r = z •> 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]

Premises used: Finset.mul_inv_eq_inv_mul_of_doubling_lt_two, Finset.subset_smul_finset_iff, mul_assoc, _private.0.Finset.weaken_doubling, Finset.inter_eq_right
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
simp : (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹
⊢ a⁻¹ •> z •> A⁻¹ ⊆ A⁻¹ * (A * (A * A⁻¹))

Tactic:
simp only [← mul_assoc, smul_smul]

Premises used: mul_assoc, smul_smul
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹

Tactic:
smul_finset_subset_mul ?_

Premises used: Set.Mem, setOf, 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) : ℚ)
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
refine : a⁻¹ * z ∈ A⁻¹ * A * A
⊢ (a⁻¹ * z) •> A⁻¹ ⊆ A⁻¹ * A * A * A⁻¹

Tactic:
refine smul_finset_subset_mul ?_

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
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

Tactic:
simp [← hz, mul_mem_mul, ha, hb, hc]

Premises used: Finset.mul_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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
⊢ 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]
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
rw : A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)
⊢ l ∪ r ⊆ a •> (A⁻¹ * A)

Tactic:
rw [union_subset_iff, hl]

Premises used: Finset.union_subset_iff
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
⊢ A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)

Tactic:
⟨A_subset_aH a ha, inter_subset_left⟩

Premises used: _private.0.Finset.A_subset_aH, And.intro, Finset.inter_subset_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) : ℚ)
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⁻¹
⊢ A ⊆ a •> (A⁻¹ * A) ∧ r ⊆ a •> (A⁻¹ * A)

Tactic:
exact ⟨A_subset_aH a ha, inter_subset_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) : ℚ)
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)

Tactic:
have lr : l ∪ r ⊆ a • (A⁻¹ * A) := by
    rw [union_subset_iff, hl]
    exact ⟨A_subset_aH a ha, inter_subset_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) : ℚ)
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)
rw rw₁ : #A = #A
⊢ #l = #A

Tactic:
rw [hl]
-- 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 : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
⊢ #l = #A

Tactic:
have : #l = #A := by rw [hl]
-- 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 : #l = #A
rw : #(z •> A⁻¹) = #A
rw₁ : #A⁻¹ = #A
rw₂ rw₃ : #A = #A
⊢ #r = #A

Tactic:
rw [hr, card_smul_finset, card_inv]

Premises used: Finset.card_inv, 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 : #l = #A
⊢ #r = #A

Tactic:
have : #r = #A := by rw [hr, card_smul_finset, card_inv]
-- 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:
(card_le_card lr).trans_lt ?_

Premises used: Finset.card_le_card, LE.le.trans_lt