case h
α : Type ?u.241739
β : Type ?u.241742
M✝ : Type ?u.241745
N : Type ?u.241748
P : Type ?u.241751
G : Type ?u.241754
H : Type ?u.241757
F : Type ?u.241760
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
x✝ : M
⊢ ↑(comp φ ψ⁻¹) x✝ = ↑(comp φ ψ)⁻¹ x✝
α : Type ?u.241739
β : Type ?u.241742
M✝ : Type ?u.241745
N : Type ?u.241748
P : Type ?u.241751
G : Type ?u.241754
H : Type ?u.241757
F : Type ?u.241760
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
⊢ comp φ ψ⁻¹ = (comp φ ψ)⁻¹
ext
no goals
case h
α : Type ?u.241739
β : Type ?u.241742
M✝ : Type ?u.241745
N : Type ?u.241748
P : Type ?u.241751
G : Type ?u.241754
H : Type ?u.241757
F : Type ?u.241760
inst✝⁵ : Group G
inst✝⁴ : CommGroup H
inst✝³ : MulOneClass M✝
M : Type u_1
A : Type u_2
B : Type u_3
inst✝² : MulOneClass M
inst✝¹ : CommGroup A
inst✝ : CommGroup B
φ : A →* B
ψ : M →* A
x✝ : M
⊢ ↑(comp φ ψ⁻¹) x✝ = ↑(comp φ ψ)⁻¹ x✝
simp only [Function.comp_apply, inv_apply, map_inv, coe_comp]