case h
α : Type u_1
β : Type ?u.141801
γ : Type ?u.141804
ι : Type ?u.141807
M : Type u_2
M' : Type ?u.141813
N : Type ?u.141816
P : Type ?u.141819
G : Type ?u.141822
H : Type ?u.141825
R : Type ?u.141828
S : Type ?u.141831
inst✝ : Zero M
l : α →₀ M
x : α
⊢ ↑(equivMapDomain (Equiv.refl α) l) x = ↑l x
α : Type u_1
β : Type ?u.141801
γ : Type ?u.141804
ι : Type ?u.141807
M : Type u_2
M' : Type ?u.141813
N : Type ?u.141816
P : Type ?u.141819
G : Type ?u.141822
H : Type ?u.141825
R : Type ?u.141828
S : Type ?u.141831
inst✝ : Zero M
l : α →₀ M
⊢ equivMapDomain (Equiv.refl α) l = l
ext x
no goals
case h
α : Type u_1
β : Type ?u.141801
γ : Type ?u.141804
ι : Type ?u.141807
M : Type u_2
M' : Type ?u.141813
N : Type ?u.141816
P : Type ?u.141819
G : Type ?u.141822
H : Type ?u.141825
R : Type ?u.141828
S : Type ?u.141831
inst✝ : Zero M
l : α →₀ M
x : α
⊢ ↑(equivMapDomain (Equiv.refl α) l) x = ↑l x
rfl