Subgroup_IsCyclic.lean

import Mathlib

lemma Subgroup.IsCyclic [Group G] [HG : IsCyclic G] (H : Subgroup G)  :
  IsCyclic H
:= by
  haveI := Classical.propDecidable
  obtain ⟨g, Hg : ∀ h, ∃ k, g ^ k = h⟩ := HG
  cases' subsingleton_or_nontrivial H with H0 H0
  · rcases H0 with ⟨H0⟩
    constructor; use 1; intro h; simp
    apply H0
  · obtain ⟨h, Hh⟩ := exists_ne (1 : ↥H)
    obtain ⟨m, Hl⟩ := Hg h
    have : ∃ n : ℕ, g ^ n ∈ H ∧ n ≠ 0 := by
      cases' m with m m'<;> simp at *
      · use m; constructor
        · rw [Hl]; simp
        · intro F; subst m; simp at *; apply Hh; ext; rw [<- Hl]; simp
      · use (m' + 1); constructor
        · rw [<- inv_inv (g ^ (m' + 1))]
          apply inv_mem
          rw [Hl]; simp
        · intro F; rw [F] at Hl; simp at Hl; apply Hh; ext; rw [<- Hl]; simp
    let n := Nat.find this
    have Hn : g ^ n ∈ H := (Nat.find_spec this).1
    have Hn0 : n ≠ 0 := (Nat.find_spec this).2
    have Hle : ∀ (k : ℕ), g ^ k ∈ H ∧ k ≠ 0 → n ≤ k := by
      intro k Hk
      apply Nat.find_le Hk

    constructor
    use ⟨g ^ n, Hn⟩; intro h; simp
    obtain ⟨k, Hk⟩ := Hg h
    by_cases H0 : (k.natAbs % n) = 0
    · apply (Nat.dvd_iff_mod_eq_zero _ _ ).mpr at H0
      obtain ⟨c, Hc⟩ := H0
      revert Hc
      cases' k with k k<;> simp at * <;> intro Hc
      · use c; ext; simp
        rw [<- pow_mul, <- Hc]
        exact Hk
      · use -c; ext; simp
        rw [<- pow_mul, <- Hc, <- Hk]
    · have E := Nat.mod_def k.natAbs n
      have Hr : g ^ (k.natAbs % n) ∈ H := by
        rw [E, pow_sub, pow_mul]; swap
        apply Nat.mul_div_le
        apply mul_mem
        · cases' k with k k<;> simp at *
          · rw [Hk]; simp
          · rw [<- inv_inv (g ^ (k + 1))]
            apply inv_mem
            rw [Hk]; simp
        · apply inv_mem
          apply Subgroup.pow_mem
          exact Hn
      have Hr := Hle _ ⟨Hr, H0⟩
      apply Nat.ne_zero_iff_zero_lt.mp at Hn0
      have H0 := (@Nat.mod_lt k.natAbs _ Hn0)
      apply Nat.lt_iff_le_not_le.mp at H0
      obtain ⟨_, F⟩ := H0
      cases (F Hr)