Fintype.zpowers_card_eq_orderOf.lean

import Mathlib.tactic

example [Group G] [Fintype G] (g : G) :
  Fintype.card (Subgroup.zpowers g) = orderOf g
:= by
   have : orderOf g = Fintype.card (Fin (orderOf g)) := by simp
   rw [this]
   apply Fintype.card_congr
   refine {
    toFun := λ ⟨x, Hx⟩ => by
      apply Subgroup.mem_zpowers_iff.mp at Hx
      let k := Hx.choose
      use (k % Int.ofNat (orderOf g)).toNat
      have E := orderOf_pos g
      have E' : 0 < Int.ofNat (orderOf g) := by aesop
      have : orderOf g = (Int.ofNat (orderOf g)).toNat := by simp
      nth_rw 2 [this]
      apply (Int.toNat_lt_toNat E').mpr
      apply Int.emod_lt_of_pos; simp
      exact E
    invFun := λ ⟨k, Hk⟩ => by
      use g^k
      apply Subgroup.mem_zpowers_iff.mpr; use k; simp
    left_inv := λ ⟨x, Hx⟩ => by
      apply Subgroup.mem_zpowers_iff.mp at Hx
      let k := Hx.choose
      have Hk : g ^ k = x := Hx.choose_spec
      conv => arg 1; arg 1; simp; arg 1; arg 1; arg 1; change k
      simp
      rw [<- Hk]
      have : g ^ ((k % ↑(orderOf g)).toNat ) = g ^ (↑(k % ↑(orderOf g)).toNat : ℤ) := by simp
      rw [this]
      suffices : ↑(k % ↑(orderOf g)).toNat = (k % ↑(orderOf g))
      rw [this]
      apply zpow_mod_orderOf
      apply Int.toNat_of_nonneg
      apply Int.emod_nonneg; simp; intro F
      have := orderOf_pos g
      rw [F] at this; contradiction
    right_inv := λ ⟨k, Hk⟩ => by
      have Hgk : g ^ k ∈ Subgroup.zpowers g := by
        apply Subgroup.mem_zpowers_iff.mpr; use k; simp
      let k' := Hgk.choose
      conv => arg 1; arg 1; simp; change ⟨g ^ k, Hgk⟩
      simp
      conv => arg 1; arg 1; arg 1; change k'
      have H : g ^ k' = g ^ k:= Hgk.choose_spec; simp at H
      have : g ^ k = g ^ (↑k : ℤ) := by simp
      rw [this] at H
      have : g ^ (k' - ↑k) = 1 := by
        rw [zpow_sub, H]; simp
      apply zpow_eq_one_iff_modEq.mp at this
      unfold Int.ModEq at this; simp at this
      obtain ⟨c, Hc⟩ := this
      have : k' = ↑(orderOf g) * c + ↑k := by omega
      rw [this]
      suffices : (↑(orderOf g) * c + ↑k) % ↑(orderOf g) = ↑k % ↑(orderOf g)
      rw [this]
      rw [Int.emod_eq_of_lt]
      simp; simp; simp; assumption

      rw [Int.emod_def, Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left, Int.mul_add]
      ring_nf
      rw [Int.emod_def]; ring_nf
      simp; intro F
      have := orderOf_pos g; rw [F] at this; contradiction
      simp
   }