-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
⊢ (fun (φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }) ↦
        (QuotientAddGroup.lift
            (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
              (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))
            (↑φ : G →+ M) ⋯ :
          AddMonoidHom.{u_1, u_3}
            (HasQuotient.Quotient G (B := AddSubgroup G)
              (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                  ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))))
            M))
      ((fun (f : AddMonoidHom.{u_1, u_3} (ModN G n) M) ↦
          (Subtype.mk (p := fun (φ : G →+ M) ↦ ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0)
              (f.comp
                (QuotientAddGroup.mk'
                  (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                      ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))))
              ⋯ :
            { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }))
        f) =
    f
have h : ∀
  (x :
    HasQuotient.Quotient G (B := AddSubgroup G)
      (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
        (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
          ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))),
  Eq.{u_3 + 1} (α := M)
    (((fun (φ : { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }) ↦
              (QuotientAddGroup.lift
                  (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                      ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))
                  (↑φ : G →+ M) sorry :
                AddMonoidHom.{u_1, u_3}
                  (HasQuotient.Quotient G (B := AddSubgroup G)
                    (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                      (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                        ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))))
                  M))
            ((fun (f : AddMonoidHom.{u_1, u_3} (ModN G n) M) ↦
                (Subtype.mk (p := fun (φ : G →+ M) ↦ ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0)
                    (f.comp
                      (QuotientAddGroup.mk'
                        (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                          (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                            ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))))
                    sorry :
                  { φ : G →+ M // ∀ (g : G), HSMul.hSMul (β := M) n ((φ : (a : G) → M) g : M) = 0 }))
              f) :
          (a : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) → M)
        x :
      M)
    ((f : (a : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) → M) x : M)
Tactic: ext x