-- 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
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) ⋯ :
                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) :
          (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)
have h : ∀ (z : G),
  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)
        (↑z : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) :
      M)
    ((f : (a : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) → M)
        (↑z : G ⧸ ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)).range.toAddSubgroup) :
      M)
Tactic: induction x using QuotientAddGroup.induction_on
Cleared hypotheses: x