Module: Mathlib.Data.Matrix.Basis

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

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

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

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

Tactic:
<;>

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

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

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

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