case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142397
M : Type u_4
M' : Type ?u.142403
N : Type ?u.142406
P : Type ?u.142409
G : Type ?u.142412
H : Type ?u.142415
R : Type ?u.142418
S : Type ?u.142421
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ ↑(equivMapDomain (f.trans g) l) x = ↑(equivMapDomain g (equivMapDomain f l)) x
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142397
M : Type u_4
M' : Type ?u.142403
N : Type ?u.142406
P : Type ?u.142409
G : Type ?u.142412
H : Type ?u.142415
R : Type ?u.142418
S : Type ?u.142421
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)
ext x
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142397
M : Type u_4
M' : Type ?u.142403
N : Type ?u.142406
P : Type ?u.142409
G : Type ?u.142412
H : Type ?u.142415
R : Type ?u.142418
S : Type ?u.142421
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
x : γ
⊢ ↑(equivMapDomain (f.trans g) l) x = ↑(equivMapDomain g (equivMapDomain f l)) x
rfl