-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
/-- A `1`-approximate subgroup is the same thing as a subgroup. -/
@[to_additive (attr := simp)
"A `1`-approximate subgroup is the same thing as a subgroup."]
lemma isApproximateSubgroup_one {A : Set G} :
    IsApproximateSubgroup 1 (A : Set G) ↔ ∃ H : Subgroup G, H = A where
  mp hA

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ x⁻¹ ∈ A

Tactic:
simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ x • A

Tactic:
assumption

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
⊢ x⁻¹ • (A * A) ⊆ A

Tactic:
rwa [← subset_smul_set_iff]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ x * x ∈ A

Tactic:
rw [← hA.inv_eq_self]

Result:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ x * x ∈ A⁻¹

Proof state:
case intro.intro.intro.inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
rw [Finset.coe_singleton, singleton_smul, sq] at hKA

Result:
case intro.intro.intro.inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A * A ⊆ x • A
⊢ ∃ x, A * A ⊆ x • A

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x✝ : G
hx : x✝ ∈ { carrier := A, mul_mem' := ⋯, one_mem' := ⋯ }.carrier
⊢ x✝⁻¹ ∈ { carrier := A, mul_mem' := ⋯, one_mem' := ⋯ }.carrier

Tactic:
dsimp

Result:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x✝ : G
hx : x✝ ∈ { carrier := A, mul_mem' := ⋯, one_mem' := ⋯ }.carrier
⊢ x✝⁻¹ ∈ A

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hK : ↑(#K) ≤ 1
hKA : A ^ 2 ⊆ ↑K • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
simp only [Nat.cast_le_one, Finset.card_le_one_iff_subset_singleton,
  Finset.subset_singleton_iff] at hK

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hKA : A ^ 2 ⊆ ↑K • A
hK : ∃ x, K = ∅ ∨ K = {x}
⊢ ∃ x, A * A ⊆ x • A

Proof state:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsApproximateSubgroup 1 ↑H

Tactic:
exact .subgroup

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ x * x ∈ A⁻¹

Tactic:
simpa using hx' (smul_mem_smul_set (mul_mem_mul hx_inv hA.one_mem))

Result:
no goals

Proof state:
case intro.intro.intro.inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A * A ⊆ x • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
use x

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
⊢ A * A ⊆ A

Tactic:
have hx' : x ⁻¹ • (A * A) ⊆ A := by rwa [← subset_smul_set_iff]

Result:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ A * A ⊆ A

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
⊢ (∃ H, ↑H = A) → IsApproximateSubgroup 1 A

Tactic:
rintro ⟨H, rfl⟩

Result:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsApproximateSubgroup 1 ↑H

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
this : A * A ⊆ A
x✝ : G
hx : x✝ ∈ { carrier := A, mul_mem' := ⋯, one_mem' := ⋯ }.carrier
⊢ x✝⁻¹ ∈ A

Tactic:
rwa [← hA.inv_eq_self, inv_mem_inv]

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ A * A ⊆ A

Tactic:
have hx_inv : x⁻¹ ∈ A := by
  simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))

Result:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ A * A ⊆ A

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
obtain ⟨K, hK, hKA⟩ := hA.sq_covBySMul

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hK : ↑(#K) ≤ 1
hKA : A ^ 2 ⊆ ↑K • A
⊢ ∃ x, A * A ⊆ x • A

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ A

Tactic:
calc A * A ⊆ x • A := by assumption
  _ = x⁻¹ • (x * x) • A := by simp [sq, smul_smul]
  _ ⊆ x⁻¹ • (A • A) := smul_set_mono (smul_set_subset_smul hx_sq)
  _ ⊆ A := hx'

Result:
no goals

Proof state:
case intro.intro.intro.inl
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑∅ • A
⊢ ∃ x, A * A ⊆ x • A

Tactic:
simp [hA.nonempty.ne_empty] at hKA

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ ∃ H, ↑H = A

Tactic:
suffices A * A ⊆ A from
  let H : Subgroup G :=
    { carrier := A
      one_mem' := hA.one_mem
      inv_mem' hx := by dsimp; rwa [← hA.inv_eq_self, inv_mem_inv]
      mul_mem' hx hy := this (mul_mem_mul hx hy) }
  ⟨H, rfl⟩

Result:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
⊢ A * A ⊆ A

Proof state:
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ x • A = x⁻¹ • (x * x) • A

Tactic:
simp [sq, smul_smul]

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
K : Finset G
hKA : A ^ 2 ⊆ ↑K • A
hK : ∃ x, K = ∅ ∨ K = {x}
⊢ ∃ x, A * A ⊆ x • A

Tactic:
obtain ⟨x, rfl | rfl⟩ := hK

Result:
case intro.intro.intro.inl
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑∅ • A
⊢ ∃ x, A * A ⊆ x • A

case intro.intro.intro.inr
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hKA : A ^ 2 ⊆ ↑{x} • A
⊢ ∃ x, A * A ⊆ x • A

Proof state:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
⊢ A * A ⊆ A

Tactic:
have hx_sq : x * x ∈ A := by
  rw [← hA.inv_eq_self]
  simpa using hx' (smul_mem_smul_set (mul_mem_mul hx_inv hA.one_mem))

Result:
case intro
G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ A