-- 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 x : G), x ∈ A → ∀ x_1 ∈ A, x⁻¹ * x_1 = a → 1 / 2 * ↑(#A) < ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a) (A ×ˢ A)))

Tactic:
rintro _ a ha b 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))
a : G
ha : a ∈ A
b : G
hb : b ∈ A
⊢ 1 / 2 * ↑(#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
this✝ : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
this : 0 < ↑(#A)
⊢ ↑(#(A⁻¹ * A)) < 2 * ↑(#A)

Tactic:
nlinarith

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

Tactic:
simp only [sum_const, nsmul_eq_mul, mul_comm]

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

Tactic:
have h₁ : ∀ x ∈ A, ∀ y ∈ A, (1 / 2 : ℚ) * #A < #((x • A) ∩ (y • A)) := by
  intro x hx y hy
  have := big_intersection hx hy
  rw [← Nat.cast_le (α := ℚ), Nat.cast_mul, Nat.cast_add, Nat.cast_two] at this
  linarith

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⁻¹ * 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
⊢ Set.InjOn (fun t => (a⁻¹ * t, b⁻¹ * t)) ↑(a •> A ∩ b •> A)

Tactic:
simp [Set.InjOn]

Result:
no goals

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

Tactic:
have h₀ : A.Nonempty := nonempty_of_doubling h

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
⊢ #(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
⊢ ↑(#(a •> A ∩ b •> A)) ≤ ↑(#(filter (fun xy => xy.1 * xy.2⁻¹ = a⁻¹ * b) (A ×ˢ A)))

Tactic:
rw [Nat.cast_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)))
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, y⁻¹ = b⁻¹

Tactic:
simp [hb]

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 ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))

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

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

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

Tactic:
have h₂ : ∀ a ∈ A⁻¹ * A, (1 / 2 : ℚ) * #A < #{xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a} := by
  simp only [mem_mul, mem_product, Prod.forall, and_imp, mem_inv, exists_exists_and_eq_and,
    forall_exists_index]
  rintro _ a ha b hb rfl
  refine (h₁ a ha b hb).trans_le ?_
  rw [Nat.cast_le]
  refine card_le_card_of_injOn (fun t => (a⁻¹ * t, b⁻¹ * t)) ?_ (by simp [Set.InjOn])
  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]
  rintro c hc d hd h
  rw [mul_assoc, mul_inv_cancel_left, ← h, inv_mul_cancel_left]
  simp [hd, hc]

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⁻¹ * 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:
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
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⁻¹

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

Tactic:
exact ⟨a, ha, b⁻¹, by simp [hb], rfl⟩

Result:
no goals