case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ ↑equivFunOnFintype (single i m) x = Pi.single i m x
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i✝ : ι
inst✝ : Fintype ι
i : ι
m : β i
⊢ ↑equivFunOnFintype (single i m) = Pi.single i m
ext x
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ ↑(single i m) x = if h : x = i then (_ : i = x) ▸ m else 0
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ ↑equivFunOnFintype (single i m) x = Pi.single i m x
dsimp [Pi.single, Function.update]
no goals
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ ↑(single i m) x = if h : x = i then (_ : i = x) ▸ m else 0
simp [Dfinsupp.single_eq_pi_single, @eq_comm _ i]