case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.615890
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
i : ι
j : α i
⊢ ↑(↑(sigmaCurry (r • f)) i) j = ↑(↑(r • sigmaCurry f) i) j
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.615890
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
⊢ sigmaCurry (r • f) = r • sigmaCurry f
ext (i j)
no goals
case h.h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
κ : Type ?u.615890
α : ι → Type u_1
δ : (i : ι) → α i → Type v
inst✝² : Monoid γ
inst✝¹ : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)
r : γ
f : Π₀ (i : (i : ι) × α i), δ i.fst i.snd
i : ι
j : α i
⊢ ↑(↑(sigmaCurry (r • f)) i) j = ↑(↑(r • sigmaCurry f) i) j
rw [@smul_apply _ _ (fun i => Π₀ j, δ i j) _ _ _ _ (sigmaCurry _), smul_apply, sigmaCurry_apply,
  sigmaCurry_apply, smul_apply]