-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
lemma smul_inv_mul_eq_inv_mul_opSMul (h : #(A * A) < (3 / 2 : ℚ) * #A) (ha : a ∈ A) :
    a •> (A⁻¹ * A) = (A⁻¹ * A) <• a

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A * (↑A⁻¹ * ↑A) * ↑A⁻¹ = ↑A⁻¹ * ↑A

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

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) = (A⁻¹ * A) <• a

Tactic:
refine subset_antisymm ?_ ?_

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a

case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ A⁻¹ * A * A

Tactic:
exact op_smul_finset_subset_mul (by simpa)

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : 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 gcongr; exact 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]

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a

Tactic:
rw [subset_smul_finset_iff, ← op_inv]

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) <• a⁻¹ ⊆ A⁻¹ * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹

Tactic:
simp_rw [← coe_inj, coe_mul]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * ↑A⁻¹ * ↑A) = ↑A * ↑A⁻¹

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a ∈ A

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ a •> (A⁻¹ * A)

Tactic:
rw [subset_smul_finset_iff]

Result:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a⁻¹ •> ((A⁻¹ * A) <• a) ⊆ A⁻¹ * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A⁻¹ * (↑A * ↑A⁻¹ * ↑A) = ↑A * ↑A⁻¹

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

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A * A) = A⁻¹ * A

Tactic:
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two <| weaken_doubling h]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A * A⁻¹ * A) = A * A⁻¹

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a⁻¹ ∈ A⁻¹

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A * (A⁻¹ * A) * A⁻¹ = A⁻¹ * A

Tactic:
simp_rw [← coe_inj, coe_mul]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ ↑A * (↑A⁻¹ * ↑A) * ↑A⁻¹ = ↑A⁻¹ * ↑A

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : 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 gcongr; exact 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]

Result:
no goals

Proof state:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ A * (A⁻¹ * A)

Tactic:
exact smul_finset_subset_mul (by simpa)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) * A⁻¹ ⊆ A * (A⁻¹ * A) * A⁻¹

Tactic:
gcongr

Result:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ A * (A⁻¹ * A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ A⁻¹ * (A⁻¹ * A) <• a ⊆ A⁻¹ * (A⁻¹ * A * A)

Tactic:
gcongr

Result:
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ (A⁻¹ * A) <• a ⊆ A⁻¹ * A * A