-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots (goal)
Goal:
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst : CommMonoid M
inst_1 : CommMonoid N
inst_2 : DivisionCommMonoid G
k l : ℕ
inst_3 : CommRing R
ζ : Rˣ
h_1 h : IsPrimitiveRoot ζ k
left :
  Function.Injective.{1, u_4 + 1} (α := ZMod k) (β := Additive ↥(Subgroup.zpowers ζ))
    (⇑((AddMonoidHom.liftOfRightInverse (Int.castAddHom (ZMod k)) ZMod.cast ⋯ :
              (a : { g : ℤ →+ Additive ↥(Subgroup.zpowers ζ) // (Int.castAddHom (ZMod k)).ker ≤ g.ker }) →
                ZMod k →+ Additive ↥(Subgroup.zpowers ζ))
            (Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
              AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
              {
                toFun := fun (i : ℤ) ↦
                  (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                    (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                      ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯),
                map_zero' := ⋯, map_add' := ⋯ }
              ⋯) :
          ZMod k →+ Additive ↥(Subgroup.zpowers ζ)) :
      (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ))
⊢ Function.Bijective.{1, u_4 + 1} (α := ZMod k) (β := Additive ↥(Subgroup.zpowers ζ))
    (⇑((AddMonoidHom.liftOfRightInverse (Int.castAddHom (ZMod k)) ZMod.cast ⋯ :
              (a : { g : ℤ →+ Additive ↥(Subgroup.zpowers ζ) // (Int.castAddHom (ZMod k)).ker ≤ g.ker }) →
                ZMod k →+ Additive ↥(Subgroup.zpowers ζ))
            (Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
              AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
              {
                toFun := fun (i : ℤ) ↦
                  (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                    (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                      ((fun (x : ℤ) ↦ ζ ^ x) i) ⋯),
                map_zero' := ⋯, map_add' := ⋯ }
              ⋯) :
          ZMod k →+ Additive ↥(Subgroup.zpowers ζ)) :
      (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ))
have right : Function.Surjective.{1, u_4 + 1} (α := ZMod k) (β := Additive ↥(Subgroup.zpowers ζ))
  (⇑((AddMonoidHom.liftOfRightInverse (Int.castAddHom (ZMod k)) ZMod.cast sorry :
            (a : { g : ℤ →+ Additive ↥(Subgroup.zpowers ζ) // (Int.castAddHom (ZMod k)).ker ≤ g.ker }) →
              ZMod k →+ Additive ↥(Subgroup.zpowers ζ))
          (Subtype.mk (p := fun (g : ℤ →+ Additive ↥(Subgroup.zpowers ζ)) ↦
            AddMonoidHom.ker (M := ZMod k) (Int.castAddHom (ZMod k)) ≤ g.ker)
            {
              toFun := fun (i : ℤ) ↦
                (Additive.ofMul : (a : ↥(Subgroup.zpowers ζ)) → Additive ↥(Subgroup.zpowers ζ))
                  (Subtype.mk (p := fun (x : Rˣ) ↦ Membership.mem (γ := Subgroup Rˣ) (Subgroup.zpowers ζ) x)
                    ((fun (x : ℤ) ↦ ζ ^ x) i) sorry),
              map_zero' := sorry, map_add' := sorry }
            sorry) :
        ZMod k →+ Additive ↥(Subgroup.zpowers ζ)) :
    (a : ZMod k) → Additive ↥(Subgroup.zpowers ζ))
Tactic: constructor