-- Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
@[to_additive]
lemma pow_ssubset_pow_succ_of_pow_ne_closure (hX₁ : (1 : G) ∈ X) (hX : X.Nontrivial)
    (hXclosure : (X ^ n : Set G) ≠ closure (X : Set G)) : X ^ n ⊂ X ^ (n + 1)

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x y : G
hx : x ∈ ↑X
hy : y ∈ ↑X
⊢ x * y ∈ ↑X

Tactic:
norm_cast at *

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x y : G
hx : x ∈ X
hy : y ∈ X
⊢ x * y ∈ X

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ X

Tactic:
rw [this]

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ x⁻¹ • X

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
⊢ ↑X = ↑(closure ↑X)

Tactic:
let Xgp : Subgroup G :=
{ carrier := X
  mul_mem' := fun {x y} hx hy ↦ by
    norm_cast at *
    simpa [← hXn, ← sq] using mul_mem_mul hx hy
  one_mem' := hX₁
  inv_mem' := fun {x} hx ↦ by
    dsimp at *
    norm_cast at *
    have : x • X ⊆ X := by
      simpa [← hXn, add_assoc, ← sq] using smul_finset_subset_mul (t := X) hx
    have : x • X = X := eq_of_subset_of_card_le this (card_smul_finset ..).ge
    rw [← eq_inv_smul_iff] at this
    rw [this]
    simpa [mem_inv_smul_finset_iff] }

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
Xgp : Subgroup G := { carrier := ↑X, mul_mem' := ⋯, one_mem' := hX₁, inv_mem' := ⋯ }
⊢ ↑X = ↑(closure ↑X)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ (X ^ n) ^ 1 = (X ^ n) ^ (1 + 1)

Tactic:
simp [hXn, ← pow_mul, mul_two]

Result:
no goals

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
Xgp : Subgroup G := { carrier := ↑X, mul_mem' := ⋯, one_mem' := hX₁, inv_mem' := ⋯ }
⊢ ↑X = ↑(closure ↑X)

Tactic:
exact subset_closure.antisymm <| (closure_le Xgp).2 subset_rfl

Result:
no goals

Proof state:
case inr.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
hXn : ∀ (d : ℕ), X ^ (n + d) = X ^ n
⊢ ↑X ^ n = ↑(closure (↑X ^ n))

Tactic:
exact mod_cast this (one_mem_pow hX₁) (hX.pow hn) one_ne_zero
  (by simp [hXn, ← pow_mul, mul_two]) (by simp [hXn, ← pow_mul, mul_two])

Result:
no goals

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x y : G
hx : x ∈ X
hy : y ∈ X
⊢ x * y ∈ X

Tactic:
simpa [← hXn, ← sq] using mul_mem_mul hx hy

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : ↑X ^ 0 ≠ ↑(closure ↑X)
⊢ X ^ 0 ⊂ X ^ (0 + 1)

Tactic:
simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff]
  using hX.not_subset_singleton

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
⊢ X ^ (n + 0) = X ^ n

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ ↑X
⊢ x⁻¹ ∈ ↑X

Tactic:
norm_cast at *

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
⊢ x⁻¹ ∈ X

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hXclosure : ↑X ^ n ≠ ↑(closure ↑X)
hn : n ≠ 0
⊢ X ^ n ≠ X ^ (n + 1)

Tactic:
contrapose! hXclosure with hXn

Result:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
⊢ ↑X ^ n = ↑(closure ↑X)

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : x • X = X
⊢ x⁻¹ ∈ X

Tactic:
rw [← eq_inv_smul_iff] at this

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : True
hXn : X = X ^ 2
x : G
hx : x ∈ X
this✝ : x • X ⊆ X
this : X = x⁻¹ • X
⊢ x⁻¹ ∈ X

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
d : ℕ
hd : X ^ (n + d) = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n

Tactic:
rw [pow_add, pow_one] at hXn

Result:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ n * X
hn₁ : ¬n = 1
this :
  ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
    1 ∈ X → X.Nontrivial → n ≠ 0 → X ^ n = X ^ (n + 1) → n = 1 → ↑X = ↑(closure ↑X)
d : ℕ
hd : X ^ (n + d) = X ^ n
⊢ X ^ (n + (d + 1)) = X ^ n

Proof state:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n✝ : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
n : ℕ
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : n ≠ 0
hXn : X ^ n = X ^ (n + 1)
hn₁ : n = 1
⊢ ↑X ^ n = ↑(closure (↑X ^ n))

Tactic:
subst hn₁

Result:
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : DecidableEq G✝
X✝ : Finset G✝
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
hn : 1 ≠ 0
hXn : X ^ 1 = X ^ (1 + 1)
⊢ ↑X ^ 1 = ↑(closure (↑X ^ 1))