-- Mathlib/Geometry/Group/Growth/LinearLowerBound.lean
@[to_additive]
lemma pow_right_strictMonoOn (hX₁ : 1 ∈ X) (hX : X.Nontrivial) :
    StrictMonoOn (fun n ↦ X ^ n) {n | (X ^ (n - 1) : Set G) ≠ closure (X : Set G)}

Proof state:
case intro.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
hmn : 0 ≤ n
hm : ↑X ^ (0 - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Tactic:
simp [eq_comm (a := (1 : Set _)), coe_set_eq_one, -Set.subset_singleton_iff,
  hX.coe.not_subset_singleton] at hm

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m) * ↑X ^ (m - 1)

Tactic:
rw [← pow_add]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m + (m - 1))

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
⊢ False

Tactic:
apply hn

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Proof state:
case intro.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Tactic:
calc (X : Set G) ^ (n - 1)
_ = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; omega
_ = closure (X : Set G) := by rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]

Result:
no goals

Proof state:
case e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ n - 1 = n - m + (m - 1)

Tactic:
omega

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - m) * ↑X ^ (m - 1) = ↑(closure ↑X)

Tactic:
rw [hm, Set.pow_mul_subgroupClosure hX.nonempty.to_set]

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Tactic:
obtain rfl | hm₀ := m.eq_zero_or_pos

Result:
case intro.inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
hmn : 0 ≤ n
hm : ↑X ^ (0 - 1) = ↑(closure ↑X)
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

case intro.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑(closure ↑X)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ ↑X ^ (n - 1) = ↑X ^ (n - m + (m - 1))

Tactic:
congr 1

Result:
case e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
hm₀ : m > 0
⊢ n - 1 = n - m + (m - 1)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
⊢ ∀ ⦃x : ℕ⦄,
    x ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)} →
      ∀ ⦃y : ℕ⦄, y ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)} → Set.Icc x y ⊆ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}

Tactic:
rintro - - n hn m ⟨-, hmn⟩ hm

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
n : ℕ
hn : n ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}
m : ℕ
hmn : m ≤ n
hm : ↑X ^ (m - 1) = ↑(closure ↑X)
⊢ False

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
⊢ StrictMonoOn (fun n => X ^ n) {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}

Tactic:
refine strictMonoOn_of_lt_add_one ⟨?_⟩ fun n _ _ hn ↦
  pow_ssubset_pow_succ_of_pow_ne_closure hX₁ hX hn

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
X : Finset G
hX₁ : 1 ∈ X
hX : X.Nontrivial
⊢ ∀ ⦃x : ℕ⦄,
    x ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)} →
      ∀ ⦃y : ℕ⦄, y ∈ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)} → Set.Icc x y ⊆ {n | ↑X ^ (n - 1) ≠ ↑(closure ↑X)}