-- 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
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) ⋯ :
                  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)
⊢ (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

Tactic:
ext x