case h
α : Type u_3
β : Type u_1
γ : Type ?u.306308
ι : Type ?u.306311
M : Type u_2
M' : Type ?u.306317
N : Type ?u.306320
P : Type ?u.306323
G : Type ?u.306326
H : Type ?u.306329
R : Type ?u.306332
S : Type ?u.306335
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
a✝ : α
⊢ ↑(comapDomain f (v₁ + v₂) hv₁₂) a✝ = ↑(comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝
α : Type u_3
β : Type u_1
γ : Type ?u.306308
ι : Type ?u.306311
M : Type u_2
M' : Type ?u.306317
N : Type ?u.306320
P : Type ?u.306323
G : Type ?u.306326
H : Type ?u.306329
R : Type ?u.306332
S : Type ?u.306335
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
⊢ comapDomain f (v₁ + v₂) hv₁₂ = comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂
ext
no goals
case h
α : Type u_3
β : Type u_1
γ : Type ?u.306308
ι : Type ?u.306311
M : Type u_2
M' : Type ?u.306317
N : Type ?u.306320
P : Type ?u.306323
G : Type ?u.306326
H : Type ?u.306329
R : Type ?u.306332
S : Type ?u.306335
inst✝ : AddZeroClass M
f : α → β
v₁ v₂ : β →₀ M
hv₁ : Set.InjOn f (f ⁻¹' ↑v₁.support)
hv₂ : Set.InjOn f (f ⁻¹' ↑v₂.support)
hv₁₂ : Set.InjOn f (f ⁻¹' ↑(v₁ + v₂).support)
a✝ : α
⊢ ↑(comapDomain f (v₁ + v₂) hv₁₂) a✝ = ↑(comapDomain f v₁ hv₁ + comapDomain f v₂ hv₂) a✝
simp only [comapDomain_apply, coe_add, Pi.add_apply]