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

case some
k : Type ?u.1962
l : Type u_2
m : Type u_1
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ some fi then 1 else 0) * M j_1 j) =
    Option.rec 0 (fun val => M val j) (some fi)
k : Type ?u.1962
l : Type u_2
m : Type u_1
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ ↑f i then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) (↑f i)
cases' h : f i with fi
no goals
case none
k : Type ?u.1962
l : Type u_2
m : Type u_1
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
h : ↑f i = none
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ none then 1 else 0) * M j_1 j) = Option.rec 0 (fun val => M val j) none
simp [h]
no goals
case some
k : Type ?u.1962
l : Type u_2
m : Type u_1
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : Semiring α
f : l ≃. m
M : Matrix m n α
i : l
j : n
fi : m
h : ↑f i = some fi
⊢ (Finset.sum Finset.univ fun j_1 => (if j_1 ∈ some fi then 1 else 0) * M j_1 j) =
    Option.rec 0 (fun val => M val j) (some fi)
rw [Finset.sum_eq_single fi] <;> simp (config := { contextual := true }) [h, eq_comm]