-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
theorem doubling_lt_three_halves (h : #(A * A) < (3 / 2 : ℚ) * #A) :
    ∃ (H : Subgroup G) (_ : Fintype H), Fintype.card H < (3 / 2 : ℚ) * #A ∧ ∀ a ∈ A,
      (A : Set G) ⊆ a • H ∧ a •> (H : Set G) = H <• a

Proof state:
case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• 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

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)

Tactic:
simp [← Nat.card_eq_fintype_card, invMulSubgroup, ← coe_mul, ← coe_inv, H]

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Nat.card { x // x ∈ A⁻¹ * A }) < 3 / 2 * ↑(#A)

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Nat.card { x // x ∈ A⁻¹ * A }) < 3 / 2 * ↑(#A)

Tactic:
rwa [Nat.card_eq_finsetCard, card_inv_mul_of_doubling_lt_three_halves h]

Result:
no goals

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

Tactic:
exact_mod_cast A_subset_aH a ha

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a

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

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A)

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

case refine_3
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ a •> ↑H = ↑H <• a

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

Tactic:
rw [invMulSubgroup_eq_inv_mul]

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

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a

Tactic:
let H := invMulSubgroup A h

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
⊢ ∃ H x, ↑(Fintype.card ↥H) < 3 / 2 * ↑(#A) ∧ ∀ a ∈ A, ↑A ⊆ a •> ↑H ∧ a •> ↑H = ↑H <• a