-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
private lemma weak_invMulSubgroup_bound (h : #(A * A) < (3 / 2 : ℚ) * #A) :
    #(A⁻¹ * A) < 2 * #A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A)))

Tactic:
refine (h₁ a ha b hb).trans_le ?_

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ ↑(#(a •> A ∩ b •> A)) ≤ ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A)))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ (A⁻¹ * A).Nonempty

Tactic:
simp [h₀]

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₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ ∀ a_1 ∈ a •> A ∩ b •> A, (fun t => (a⁻¹ * t, b⁻¹ * t)) a_1 ∈ filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A)

Tactic:
simp only [mem_inter, mem_product, and_imp, Prod.forall, mem_filter, mul_inv_rev, inv_inv,
  exists_and_left, exists_eq_left, forall_exists_index, smul_eq_mul,
  forall_apply_eq_imp_iff₂, inv_mul_cancel_left, inv_mul_cancel_right, mem_smul_finset]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ ∀ a_1 ∈ A, ∀ x ∈ A, b * x = a * a_1 → (a_1 ∈ A ∧ b⁻¹ * (a * a_1) ∈ A) ∧ a_1 * (a_1⁻¹ * a⁻¹ * b) = a⁻¹ * b

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))

Tactic:
have := big_intersection hx hy

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
x : G
hx : x ∈ A
y : G
hy : y ∈ A
this : 2 * #A ≤ #(x •> A ∩ y •> A) + #(A * A)
⊢ 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h✝ : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
c : G
hc : c ∈ A
d : G
hd : d ∈ A
h : b * d = a * c
⊢ (c ∈ A ∧ b⁻¹ * (a * c) ∈ A) ∧ c * (c⁻¹ * a⁻¹ * b) = a⁻¹ * b

Tactic:
rw [mul_assoc, mul_inv_cancel_left, ← h, inv_mul_cancel_left]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h✝ : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
c : G
hc : c ∈ A
d : G
hd : d ∈ A
h : b * d = a * c
⊢ (c ∈ A ∧ d ∈ A) ∧ a⁻¹ * b = a⁻¹ * b

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ #(a •> A ∩ b •> A) ≤ #(filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A))

Tactic:
refine card_le_card_of_injOn (fun t => (a⁻¹ * t, b⁻¹ * t)) ?_ (by simp [Set.InjOn])

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ ∀ a_1 ∈ a •> A ∩ b •> A, (fun t => (a⁻¹ * t, b⁻¹ * t)) a_1 ∈ filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2

Tactic:
rw [← Nat.cast_pow, sq, ← card_product, card_eq_sum_card_fiberwise h₃, Nat.cast_sum]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) <
    ∑ x ∈ A⁻¹ * A,
      ↑(#(filter
            (fun a =>
              (match a with
                | (x, y) => x * y⁻¹) =
                x)
            (A ×ˢ A)))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ 0 < ↑(#A)

Tactic:
simpa [card_pos]

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₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
have : (0 : ℚ) < #A := by simpa [card_pos]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
h₃ :
  ∀ x ∈ A ×ˢ A,
    (fun x =>
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this✝ : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
this : 0 < ↑(#A)
⊢ #(A⁻¹ * A) < 2 * #A