case a.h
k : Type ?u.7888
l : Type ?u.7891
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ toMatrix (PEquiv.symm f) i✝ x✝ = (toMatrix f)ᵀ i✝ x✝
k : Type ?u.7888
l : Type ?u.7891
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ toMatrix (PEquiv.symm f) = (toMatrix f)ᵀ
ext
case a.h
k : Type ?u.7888
l : Type ?u.7891
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ (if i✝ ∈ ↑f x✝ then 1 else 0) = ↑of (fun x y => if x ∈ ↑f y then 1 else 0) i✝ x✝
case a.h
k : Type ?u.7888
l : Type ?u.7891
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ toMatrix (PEquiv.symm f) i✝ x✝ = (toMatrix f)ᵀ i✝ x✝
simp only [transpose, mem_iff_mem f, toMatrix_apply]
no goals
case a.h
k : Type ?u.7888
l : Type ?u.7891
m : Type u_1
n : Type u_2
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
i✝ : n
x✝ : m
⊢ (if i✝ ∈ ↑f x✝ then 1 else 0) = ↑of (fun x y => if x ∈ ↑f y then 1 else 0) i✝ x✝
congr