case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.605040
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
i : ι
j : α i
⊢ ↑(↑(sigmaCurry (f + g)) i) j = ↑(↑(sigmaCurry f + sigmaCurry g) i) j
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.605040
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
⊢ sigmaCurry (f + g) = sigmaCurry f + sigmaCurry g
ext (i j)
no goals
case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.605040
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
i : ι
j : α i
⊢ ↑(↑(sigmaCurry (f + g)) i) j = ↑(↑(sigmaCurry f + sigmaCurry g) i) j
rw [@add_apply _ (fun i => Π₀ j, δ i j) _ (sigmaCurry _), add_apply, sigmaCurry_apply,
  sigmaCurry_apply, sigmaCurry_apply, add_apply]