case a.mk.h.mk
R : Type ?u.5462
α : Type u_1
α' : Type ?u.5468
β : Type u_2
β' : Type ?u.5474
γ : Type u_3
γ' : Type ?u.5480
l : Type ?u.5483
m : Type u_4
n : Type u_5
p : Type ?u.5492
q : Type ?u.5495
r : Type ?u.5498
l' : Type ?u.5501
m' : Type ?u.5504
n' : Type ?u.5507
p' : Type ?u.5510
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.fst) (b mn.snd)) (i₁, i₂) (j₁, j₂)
R : Type ?u.5462
α : Type u_1
α' : Type ?u.5468
β : Type u_2
β' : Type ?u.5474
γ : Type u_3
γ' : Type ?u.5480
l : Type ?u.5483
m : Type u_4
n : Type u_5
p : Type ?u.5492
q : Type ?u.5495
r : Type ?u.5498
l' : Type ?u.5501
m' : Type ?u.5504
n' : Type ?u.5507
p' : Type ?u.5510
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn => f (a mn.fst) (b mn.snd)
ext (⟨i₁, i₂⟩⟨j₁, j₂⟩)
no goals
case a.mk.h.mk
R : Type ?u.5462
α : Type u_1
α' : Type ?u.5468
β : Type u_2
β' : Type ?u.5474
γ : Type u_3
γ' : Type ?u.5480
l : Type ?u.5483
m : Type u_4
n : Type u_5
p : Type ?u.5492
q : Type ?u.5495
r : Type ?u.5498
l' : Type ?u.5501
m' : Type ?u.5504
n' : Type ?u.5507
p' : Type ?u.5510
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
i₁ : m
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f (diagonal a) (diagonal b) (i₁, i₂) (j₁, j₂) =
    diagonal (fun mn => f (a mn.fst) (b mn.snd)) (i₁, i₂) (j₁, j₂)
simp [diagonal, apply_ite f, ite_and, ite_apply, apply_ite (f (a i₁)), hf₁, hf₂]