no goals
N : Type u_1
G : Type u_2
H : Type ?u.123220
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N ⋊[φ] G
⊢ x✝ ∈ MonoidHom.range inl → x✝ ∈ MonoidHom.ker rightHom
simp (config := { contextual := true }) [MonoidHom.mem_ker, eq_comm]
no goals
N : Type u_1
G : Type u_2
H : Type ?u.123220
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ ↑inl x.left = x
ext <;> simp_all [MonoidHom.mem_ker]