Inferring `Normal` instance for quotient

Stream: mathlib4

[Johannes Choo]

I'm trying to restate the second isomorphism theorem for groups without having to assume that the subgroup N below is normal in G, since the weaker condition H ≤ N.normalizersuffices. In order to state the respective quotients, instances of (N.subgroupOf H).Normal and (N.subgroupOf (H ⊔ N)).Normal need to be in context or synthesizable. I have portioned out what I have into an MWE. I want to be able to remove the optional arguments hNinf and hNsup, perhaps with making inf_subgroupOf_normal_of_le_normalizer and subgroupOf_sup_normal_of_le_normalizer into instances. But doing it naively (theorem ... -> instance ...) doesn't work. If sensible and possible, what needs to be done?

import Mathlib

open Subgroup

theorem inf_subgroupOf_normal_of_le_normalizer [Group G] {H N : Subgroup G}
    (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal := by sorry

theorem subgroupOf_sup_normal_of_le_normalizer [Group G] {H N : Subgroup G}
    (hLE : H ≤ N.normalizer) : (N.subgroupOf (H ⊔ N)).Normal := by sorry

noncomputable def quotientInfEquivProdNormalizerQuotient [Group G] (H N : Subgroup G)
    (hLE : H ≤ N.normalizer)
    (hNinf : (N.subgroupOf H).Normal := inf_subgroupOf_normal_of_le_normalizer hLE)
    (hNsup : (N.subgroupOf (H ⊔ N)).Normal := subgroupOf_sup_normal_of_le_normalizer hLE) :
    _ ⧸ N.subgroupOf H ≃* _ ⧸ N.subgroupOf (H ⊔ N) := by sorry

[Thomas Browning]

You aren't going to be able to avoid the theorems, I think, since typeclass inference can't infer the assumption hLE.

[Johannes Choo]

Got it, thanks!