-- Mathlib/Data/Matrix/PEquiv.lean
theorem mul_toMatrix_apply [Fintype m] [Semiring α] [DecidableEq n] (M : Matrix l m α) (f : m ≃. n)
    (i j) : (M * f.toMatrix :) i j = Option.casesOn (f.symm j) 0 (M i)

Proof state:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)

Tactic:
rw [Finset.sum_eq_single fj]

Result:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm 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₀
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ ∀ b ∈ Finset.univ, b ≠ fj → (M i b * if j ∈ f b then 1 else 0) = 0

case some.h₁
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ fj ∉ Finset.univ → (M i fj * if j ∈ f fj then 1 else 0) = 0

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) (f.symm j)

Tactic:
rcases h : f.symm j with - | fj

Result:
case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : f.symm j = none
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none

case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)

Proof state:
case some.h₁
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ fj ∉ Finset.univ → (M i fj * if j ∈ f fj then 1 else 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
case none
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
h : f.symm j = none
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) none

Tactic:
simp [h, ← f.eq_some_iff]

Result:
no goals

Proof state:
case some.h₀
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ ∀ b ∈ Finset.univ, b ≠ fj → (M i b * if j ∈ f b then 1 else 0) = 0

Tactic:
rintro b - n

Result:
case some.h₀
l : Type u_2
m : Type u_3
n✝ : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : f.symm j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ f b then 1 else 0) = 0

Proof state:
case some.h₀
l : Type u_2
m : Type u_3
n✝ : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n✝
M : Matrix l m α
f : m ≃. n✝
i : l
j : n✝
fj : m
h : f.symm j = some fj
b : m
n : b ≠ fj
⊢ (M i b * if j ∈ f b then 1 else 0) = 0

Tactic:
simp [h, ← f.eq_some_iff, n.symm]

Result:
no goals

Proof state:
case some
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
fj : m
h : f.symm j = some fj
⊢ (M i fj * if j ∈ f fj then 1 else 0) = Option.rec 0 (fun val => M i val) (some fj)

Tactic:
simp [h, ← f.eq_some_iff]

Result:
no goals

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 (M i)

Tactic:
dsimp [Matrix.mul_apply, toMatrix_apply]

Result:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Semiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (∑ j_1 : m, M i j_1 * if j ∈ f j_1 then 1 else 0) = Option.rec 0 (fun val => M i val) (f.symm j)