Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
⊢ toFun s (Classical.choose (_ : ↑f a ∈ Set.range ↑f)) = toFun s a
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
⊢ toFun (embDomain s f) (↑f a) = toFun s a
rw [embDomain_apply, dif_pos (Set.mem_range_self a)]
no goals
Γ : Type u_1
R : Type u_2
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_4
β : Type u_3
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
⊢ toFun s (Classical.choose (_ : ↑f a ∈ Set.range ↑f)) = toFun s a
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))