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

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

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)

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)))
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
have h₃ : ∀ x ∈ A ×ˢ A, (fun ⟨x, y⟩ => x * y⁻¹) x ∈ A⁻¹ * A := by
  rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h)]
  simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]
  intro a b ha hb
  exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩

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

Tactic:
simp only [mem_product, Prod.forall, mem_mul, and_imp, mem_inv]

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)))
⊢ ∀ (a b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = 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))
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)))

Tactic:
refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₂).trans_eq' ?_

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

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]

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
⊢ #(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))
h₂ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))
⊢ ∀ (a b : G), a ∈ A → b ∈ A → ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = a * b⁻¹

Tactic:
intro a b ha hb

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)))
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, ∃ z, (∃ y ∈ A, y⁻¹ = z) ∧ y * z = 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_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

Tactic:
rintro c hc d hd h

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 ∧ b⁻¹ * (a * c) ∈ A) ∧ c * (c⁻¹ * 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
c : G
hc : c ∈ A
d : G
hd : d ∈ A
h : b * d = a * c
⊢ (c ∈ A ∧ d ∈ A) ∧ a⁻¹ * b = a⁻¹ * b

Tactic:
simp [hd, hc]

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

Tactic:
linarith

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

Tactic:
rw [← Nat.cast_le (α := ℚ), Nat.cast_mul, Nat.cast_add, Nat.cast_two] at this

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