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

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ ∀ x ∈ A, ∀ x_1 ∈ A, x⁻¹ * x_1 = z → ∃ y ∈ A, ∃ a ∈ A, y * a⁻¹ = z

Tactic:
rintro x hx y hy rfl

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
have ⟨t, ht⟩ : (x • A ∩ y • A).Nonempty := by
  rw [← card_pos]
  linarith [big_intersection hx hy]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : t ∈ x •> A ∩ y •> A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : (∃ y ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
obtain ⟨⟨z, hz, hzxwy⟩, w, hw, rfl⟩ := ht

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 0 < #(x •> A ∩ y •> A)

Tactic:
linarith [big_intersection hx hy]

Result:
no goals

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

Tactic:
rw [← card_pos]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 0 < #(x •> A ∩ y •> A)

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
refine ⟨z, hz, w, hw, ?_⟩

Result:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z * w⁻¹ = x⁻¹ * y

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

Tactic:
intro z

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ z ∈ A⁻¹ * A → z ∈ A * A⁻¹

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
z : G
hz : z ∈ A
w : G
hw : w ∈ A
hzxwy : x * z = y * w
⊢ z * w⁻¹ = x⁻¹ * y

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, ← hzxwy, inv_mul_cancel_left]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : t ∈ x •> A ∩ y •> A
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Tactic:
simp only [mem_inter, mem_smul_finset, smul_eq_mul] at ht

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
x : G
hx : x ∈ A
y : G
hy : y ∈ A
t : G
ht : (∃ y ∈ A, x * y = t) ∧ ∃ y_1 ∈ A, y * y_1 = t
⊢ ∃ y_1 ∈ A, ∃ a ∈ A, y_1 * a⁻¹ = x⁻¹ * y

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ z ∈ A⁻¹ * A → z ∈ A * A⁻¹

Tactic:
simp only [mem_mul, forall_exists_index, exists_and_left, and_imp, mem_inv,
  exists_exists_and_eq_and]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
z : G
⊢ ∀ x ∈ A, ∀ x_1 ∈ A, x⁻¹ * x_1 = z → ∃ y ∈ A, ∃ a ∈ A, y * a⁻¹ = z