-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma exists_pow_mem_of_index_ne_zero (h : H.index ≠ 0) (a : G) :
    ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ n₂ - n₁ ≤ H.index

Tactic:
omega

Result:
no goals

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Tactic:
dsimp only [f] at he

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₁) = ↑(a ^ n₂)
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
    add_comm] at he

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Proof state:
case h.e'_5.h.e'_6
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ ↑(n₂ - n₁) = ↑n₂ + -↑n₁

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ (n₂ - n₁) ∈ H

Tactic:
rw [← zpow_natCast]

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
⊢ Function.Injective f

Tactic:
rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Proof state:
case intro.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
rcases hne.lt_or_lt with hlt | hlt

Result:
case intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₁ < n₂
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

case intro.intro.intro.intro.intro.inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₂ < n₁
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Proof state:
case intro.intro.intro.intro.intro.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hne : n₁ ≠ n₂
hle₁ : n₁ ≤ H.index
hle₂ : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
hlt : n₁ < n₂
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
exact ⟨n₁, n₂, hlt, hle₂, he⟩

Result:
no goals

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Tactic:
have hc' := hc n₁ n₂

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
n₁ : ℕ
h₁ : 0 ≤ n₁
hle₁ : n₁ ≤ H.index
n₂ : ℕ
h₂ : 0 ≤ n₂
hle₂ : n₂ ≤ H.index
he : f ⟨n₁, ⋯⟩ = f ⟨n₂, ⋯⟩
hc' : ¬(n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁))
⊢ ⟨n₁, ⋯⟩ = ⟨n₂, ⋯⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
suffices ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
  rcases this with ⟨n₁, n₂, hlt, hle, he⟩
  refine ⟨n₂ - n₁, by omega, by omega, ?_⟩
  rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
      add_comm] at he
  rw [← zpow_natCast]
  convert he
  omega

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)

Tactic:
by_contra hc

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ¬∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
⊢ False

Tactic:
have hf : Function.Injective f := by
  rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he
  have hc' := hc n₁ n₂
  dsimp only [f] at he
  simpa [hle₁, hle₂, he] using hc'

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
f : ↑(Set.Icc 0 H.index) → G ⧸ H := fun n => ↑(a ^ ↑n)
hf : Function.Injective f
⊢ False

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ a ^ ↑(n₂ - n₁) ∈ H

Tactic:
convert he

Result:
case h.e'_5.h.e'_6
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : a ^ (↑n₂ + -↑n₁) ∈ H
⊢ ↑(n₂ - n₁) = ↑n₂ + -↑n₁

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
refine ⟨n₂ - n₁, by omega, by omega, ?_⟩

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
n₁ n₂ : ℕ
hlt : n₁ < n₂
hle : n₂ ≤ H.index
he : ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ a ^ (n₂ - n₁) ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ¬∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ↑(a ^ n₂) = ↑(a ^ n₁)
⊢ False

Tactic:
simp_rw [not_exists] at hc

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
hc : ∀ (x x_1 : ℕ), ¬(x ≠ x_1 ∧ x ≤ H.index ∧ x_1 ≤ H.index ∧ ↑(a ^ x_1) = ↑(a ^ x))
⊢ False