k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (↑(PEquiv.symm f) j)
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M ⬝ toMatrix f) i j = Option.casesOn (↑(PEquiv.symm f) j) 0 fun fj => M i fj
dsimp [toMatrix, Matrix.mul_apply]
case none
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : ↑(PEquiv.symm f) j = none
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none

case some
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (some fj)
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (↑(PEquiv.symm f) j)
cases' h : f.symm j with fj
no goals
case none
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : ↑(PEquiv.symm f) j = none
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none
simp [h, ← f.eq_some_iff]
case some
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (M i fj * if j ∈ ↑f fj then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)

case some.h₀
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fj → (M i b * if j ∈ ↑f b then 1 else 0) = 0

case some.h₁
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ¬fj ∈ Finset.univ → (M i fj * if j ∈ ↑f fj then 1 else 0) = 0
case some
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (Finset.sum Finset.univ fun j_1 => M i j_1 * if j ∈ ↑f j_1 then 1 else 0) =
    Option.rec 0 (fun val => M i val) (some fj)
rw [Finset.sum_eq_single fj]
no goals
case some
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ (M i fj * if j ∈ ↑f fj then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)
simp [h, ← f.eq_some_iff]
case some.h₀
k : Type ?u.10982
l : Type u_3
m : Type u_1
n✝ : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : ↑(PEquiv.symm f) j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ ↑f b then 1 else 0) = 0
case some.h₀
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ∀ (b : m), b ∈ Finset.univ → b ≠ fj → (M i b * if j ∈ ↑f b then 1 else 0) = 0
rintro b - n
no goals
case some.h₀
k : Type ?u.10982
l : Type u_3
m : Type u_1
n✝ : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : ↑(PEquiv.symm f) j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ ↑f b then 1 else 0) = 0
simp [h, ← f.eq_some_iff, n.symm]
no goals
case some.h₁
k : Type ?u.10982
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : ↑(PEquiv.symm f) j = some fj
⊢ ¬fj ∈ Finset.univ → (M i fj * if j ∈ ↑f fj then 1 else 0) = 0
simp