Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

pp: case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

pp: case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

pp: case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

Tactic:
<;>

Goal state after:
case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case pos
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b

case neg
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
k : n
d : α
a : l
b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ ∑ j_1,
      of (fun i' j' ↦ if i = i' ∧ j = j' then c else 0) a j_1 *
        of (fun i' j' ↦ if j = i' ∧ k = j' then d else 0) j_1 b =
    of (fun i' j' ↦ if i = i' ∧ k = j' then c * d else 0) a b