case h
α : Type u_1
β : Type u_2
γ : Type ?u.304416
ι : Type ?u.304419
M : Type u_3
M' : Type ?u.304425
N : Type ?u.304428
P : Type ?u.304431
G : Type ?u.304434
H : Type ?u.304437
R : Type ?u.304440
S : Type ?u.304443
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑0.support)) (_ : Set.InjOn f (f ⁻¹' ↑∅))
a✝ : α
⊢ ↑(comapDomain f 0 hif) a✝ = ↑0 a✝
α : Type u_1
β : Type u_2
γ : Type ?u.304416
ι : Type ?u.304419
M : Type u_3
M' : Type ?u.304425
N : Type ?u.304428
P : Type ?u.304431
G : Type ?u.304434
H : Type ?u.304437
R : Type ?u.304440
S : Type ?u.304443
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑0.support)) (_ : Set.InjOn f (f ⁻¹' ↑∅))
⊢ comapDomain f 0 hif = 0
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.304416
ι : Type ?u.304419
M : Type u_3
M' : Type ?u.304425
N : Type ?u.304428
P : Type ?u.304431
G : Type ?u.304434
H : Type ?u.304437
R : Type ?u.304440
S : Type ?u.304443
inst✝ : Zero M
f : α → β
hif : optParam (Set.InjOn f (f ⁻¹' ↑0.support)) (_ : Set.InjOn f (f ⁻¹' ↑∅))
a✝ : α
⊢ ↑(comapDomain f 0 hif) a✝ = ↑0 a✝
rfl