English
If H.index ≠ 0, then for every a ∈ G there exists n > 0 with n ≤ H.index and a^n ∈ H.
Русский
Если H.index ≠ 0, то для любого a ∈ G существует n > 0, такое что n ≤ H.index и a^n ∈ H.
LaTeX
$$H.index \neq 0 \Rightarrow \forall a \in G, \exists n > 0, n \le H.index \land a^n \in H$$
Lean4
@[to_additive]
theorem exists_pow_mem_of_index_ne_zero (h : H.index ≠ 0) (a : G) : ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H :=
by
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 cutsat, by cutsat, ?_⟩
rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add, add_comm] at he
rw [← zpow_natCast]
convert he
cutsat
suffices ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H)
by
rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
rcases hne.lt_or_gt with hlt | hlt
· exact ⟨n₁, n₂, hlt, hle₂, he⟩
· exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩
by_contra hc
simp_rw [not_exists] at hc
let f : (Set.Icc 0 H.index) → G ⧸ H := fun n ↦ (a ^ (n : ℕ) : G)
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'
have := (fintypeOfIndexNeZero h).finite
have hcard := Nat.card_le_card_of_injective f hf
simp [← index_eq_card] at hcard
