case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142684
M : Type u_4
M' : Type ?u.142690
N : Type ?u.142693
P : Type ?u.142696
G : Type ?u.142699
H : Type ?u.142702
R : Type ?u.142705
S : Type ?u.142708
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ ↑(equivMapDomain (f.trans g) x) a✝ = ↑((equivMapDomain g ∘ equivMapDomain f) x) a✝
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142684
M : Type u_4
M' : Type ?u.142690
N : Type ?u.142693
P : Type ?u.142696
G : Type ?u.142699
H : Type ?u.142702
R : Type ?u.142705
S : Type ?u.142708
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
⊢ equivMapDomain (f.trans g) = equivMapDomain g ∘ equivMapDomain f
ext x
no goals
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type ?u.142684
M : Type u_4
M' : Type ?u.142690
N : Type ?u.142693
P : Type ?u.142696
G : Type ?u.142699
H : Type ?u.142702
R : Type ?u.142705
S : Type ?u.142708
inst✝ : Zero M
f : α ≃ β
g : β ≃ γ
x : α →₀ M
a✝ : γ
⊢ ↑(equivMapDomain (f.trans g) x) a✝ = ↑((equivMapDomain g ∘ equivMapDomain f) x) a✝
rfl