-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic (goal)
Goal:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst : Group α
inst_1 : Group G
inst_2 : Group G'
M : Type u_4
inst_3 : Monoid M
inst_4 : IsCyclic G
inst_5 : MulDistribMulAction M G
n_1 : ℕ
hn : Nat.card G = n_1
m n : M
g : G
hg : orderOf g = Nat.card G
rw :
  Eq (α := ZMod n_1)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1)
    (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
          Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) :
      ZMod n_1)
rw₁ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑n_1 : ℤ)]
rw₂ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(Nat.card G) : ℤ)]
rw₃ :
  Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ ≡
    Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
      Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯ [ZMOD
    (↑(orderOf g) : ℤ)]
rw₄ :
  g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ =
    g ^
      (Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯ *
        Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯)
rw₅ :
  g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯ =
    (g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) ^
      Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯
⊢ (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1) =
    HMul.hMul (α := ZMod n_1)
      (↑(Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G m : (a : G) → G) g = g ^ m_1) ⋯) : ZMod n_1)
      (↑(Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) ⋯) : ZMod n_1)
have rw₆ : g ^ Exists.choose (p := fun (m_1 : ℤ) ↦ ∀ (g : G), (toMonoidHom G (m * n) : (a : G) → G) g = g ^ m_1) sorry =
  (toMonoidHom G m : (a : G) → G)
    (g ^ Exists.choose (p := fun (m : ℤ) ↦ ∀ (g : G), (toMonoidHom G n : (a : G) → G) g = g ^ m) sorry)
Tactic: rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]