α : Type ?u.89699
M : Type ?u.89702
G : Type u_1
G₀ : Type ?u.89708
R : Type ?u.89711
K : Type ?u.89714
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹⁻¹ = g⁻¹ * ↑h * g
α : Type ?u.89699
M : Type ?u.89702
G : Type u_1
G₀ : Type ?u.89708
R : Type ?u.89711
K : Type ?u.89714
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑(↑(MulEquiv.symm (↑MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g
change _ * _⁻¹⁻¹ = _
α : Type ?u.89699
M : Type ?u.89702
G : Type u_1
G₀ : Type ?u.89708
R : Type ?u.89711
K : Type ?u.89714
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * ↑(MulEquiv.toMonoidHom toConjAct) g = g⁻¹ * ↑h * g
α : Type ?u.89699
M : Type ?u.89702
G : Type u_1
G₀ : Type ?u.89708
R : Type ?u.89711
K : Type ?u.89714
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹⁻¹ = g⁻¹ * ↑h * g
rw [inv_inv]
no goals
α : Type ?u.89699
M : Type ?u.89702
G : Type u_1
G₀ : Type ?u.89708
R : Type ?u.89711
K : Type ?u.89714
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
g : G
h : { x // x ∈ H }
⊢ ↑ofConjAct (↑(MulEquiv.toMonoidHom toConjAct) g)⁻¹ * ↑h * ↑(MulEquiv.toMonoidHom toConjAct) g = g⁻¹ * ↑h * g
rfl