case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = (toMatrix f ⬝ toMatrix g) i j
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
⊢ toMatrix (PEquiv.trans f g) = toMatrix f ⬝ toMatrix g
ext (i j)
case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = Option.casesOn (↑f i) 0 fun fi => toMatrix g fi j
case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = (toMatrix f ⬝ toMatrix g) i j
rw [mul_matrix_apply]
case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind (↑f i) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (↑f i)
case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ toMatrix (PEquiv.trans f g) i j = Option.casesOn (↑f i) 0 fun fi => toMatrix g fi j
dsimp [toMatrix, PEquiv.trans]
no goals
case a.h
k : Type ?u.18057
l : Type u_3
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : l ≃. m
g : m ≃. n
i : l
j : n
⊢ (if j ∈ Option.bind (↑f i) ↑g then 1 else 0) = Option.rec 0 (fun val => if j ∈ ↑g val then 1 else 0) (↑f i)
cases f i <;> simp