case h
α : Type u_1
β : Type u_2
γ : Type ?u.144676
ι : Type ?u.144679
M : Type u_3
M' : Type ?u.144685
N : Type ?u.144688
P : Type ?u.144691
G : Type ?u.144694
H : Type ?u.144697
R : Type ?u.144700
S : Type ?u.144703
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ ↑(equivMapDomain f 0) a✝ = ↑0 a✝
α : Type u_1
β : Type u_2
γ : Type ?u.144676
ι : Type ?u.144679
M : Type u_3
M' : Type ?u.144685
N : Type ?u.144688
P : Type ?u.144691
G : Type ?u.144694
H : Type ?u.144697
R : Type ?u.144700
S : Type ?u.144703
inst✝ : Zero M
f : α ≃ β
⊢ equivMapDomain f 0 = 0
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.144676
ι : Type ?u.144679
M : Type u_3
M' : Type ?u.144685
N : Type ?u.144688
P : Type ?u.144691
G : Type ?u.144694
H : Type ?u.144697
R : Type ?u.144700
S : Type ?u.144703
inst✝ : Zero M
f : α ≃ β
a✝ : β
⊢ ↑(equivMapDomain f 0) a✝ = ↑0 a✝
simp only [equivMapDomain_apply, coe_zero, Pi.zero_apply]