-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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 : ℤ))))
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) ⋯ :
                  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)
          (↑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)
⊢ 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)

Tactic:
induction x using QuotientAddGroup.induction_on