-- Mathlib/Data/Matrix/Kronecker.lean
theorem kroneckerMap_stdBasisMatrix_stdBasisMatrix
    [Zero α] [Zero β] [Zero γ] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p]
    (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p)
    (f : α → β → γ) (hf₁ : ∀ b, f 0 b = 0) (hf₂ : ∀ a, f a 0 = 0) (a : α) (b : β) :
    kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) =
      stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b)

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')

Tactic:
dsimp [stdBasisMatrix]

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
    if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
⊢ kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) = stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b)

Tactic:
ext ⟨i₁', i₂'⟩ ⟨j₁', j₂'⟩

Result:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ kroneckerMap f (stdBasisMatrix i₁ j₁ a) (stdBasisMatrix i₂ j₂ b) (i₁', i₂') (j₁', j₂') =
    stdBasisMatrix (i₁, i₂) (j₁, j₂) (f a b) (i₁', i₂') (j₁', j₂')

Proof state:
case a.mk.mk
α : Type u_2
β : Type u_4
γ : Type u_6
l : Type u_8
m : Type u_9
n : Type u_10
p : Type u_11
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
i₁' : l
i₂' : n
j₁' : m
j₂' : p
⊢ f (if i₁ = i₁' ∧ j₁ = j₁' then a else 0) (if i₂ = i₂' ∧ j₂ = j₂' then b else 0) =
    if (i₁, i₂) = (i₁', i₂') ∧ (j₁, j₂) = (j₁', j₂') then f a b else 0

Tactic:
aesop

Result:
no goals