ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      1 =
    ↑(PiToModule.fromEnd R b) 1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Represents b 1 1
delta Matrix.Represents PiToModule.fromMatrix
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1 = ↑(PiToModule.fromEnd R b) 1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      1 =
    ↑(PiToModule.fromEnd R b) 1
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_one]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
i✝ : ι
⊢ ↑(LinearMap.comp (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1) (LinearMap.single i✝)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) 1) (LinearMap.single i✝)) 1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1 = ↑(PiToModule.fromEnd R b) 1
ext
no goals
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
i✝ : ι
⊢ ↑(LinearMap.comp (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1) (LinearMap.single i✝)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) 1) (LinearMap.single i✝)) 1
rfl