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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
⊢ filter p (single i x) = if p i then single i x else 0
ext j
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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else ↑0 j
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else ↑0 j
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
dsimp at this
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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
⊢ (if p j then ↑(single i x) j else 0) = if p i then ↑(single i x) j 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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
⊢ ↑(filter p (single i x)) j = ↑(if p i then single i x else 0) j
rw [filter_apply, this]
case h.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
this : ↑(if p i then single i x else 0) i = if p i then ↑(single i x) i else 0
⊢ (if p i then ↑(single i x) i else 0) = if p i then ↑(single i x) i else 0

case h.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
hij : i ≠ j
⊢ (if p j then ↑(single i x) j else 0) = if p i then ↑(single i x) j 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✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
⊢ (if p j then ↑(single i x) j else 0) = if p i then ↑(single i x) j else 0
obtain rfl | hij := Decidable.eq_or_ne i j
no goals
case h.inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
this : ↑(if p i then single i x else 0) i = if p i then ↑(single i x) i else 0
⊢ (if p i then ↑(single i x) i else 0) = if p i then ↑(single i x) i else 0
rfl
no goals
case h.inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
s : Finset ι
x✝ : (i : ↑↑s) → β ↑i
i✝ : ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
j : ι
this : ↑(if p i then single i x else 0) j = if p i then ↑(single i x) j else 0
hij : i ≠ j
⊢ (if p j then ↑(single i x) j else 0) = if p i then ↑(single i x) j else 0
rw [single_eq_of_ne hij, ite_self, ite_self]