case h
N : Type ?u.177654
G : Type ?u.177657
H : Type ?u.177660
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ↑(MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝¹))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝¹))) (MonoidHom.comp F inl)) x✝
N : Type ?u.177654
G : Type ?u.177657
H : Type ?u.177660
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝ : G
⊢ MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝)) =
    MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝))) (MonoidHom.comp F inl)
ext
no goals
case h
N : Type ?u.177654
G : Type ?u.177657
H : Type ?u.177660
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ↑(MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝¹))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝¹))) (MonoidHom.comp F inl)) x✝
simp [inl_aut]
N : Type u_2
G : Type u_1
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G),
    ↑F x =
      ↑(lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
            (_ :
              ∀ (x : G),
                MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
                  MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x)))
                    (MonoidHom.comp F inl)))
        x
N : Type u_2
G : Type u_1
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ F =
    lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x))) (MonoidHom.comp F inl))
rw [FunLike.ext_iff]
no goals
N : Type u_2
G : Type u_1
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G),
    ↑F x =
      ↑(lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
            (_ :
              ∀ (x : G),
                MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
                  MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x)))
                    (MonoidHom.comp F inl)))
        x
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul,
  inl_left_mul_inr_right, forall_const]