case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)

case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)) → Represents b A f
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
constructor
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
intro h i
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ↑(↑(PiToModule.fromMatrix R b) A) (Pi.single i 1) = ↑(↑(PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
have := LinearMap.congr_fun h (Pi.single i 1)
no goals
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ↑(↑(PiToModule.fromMatrix R b) A) (Pi.single i 1) = ↑(↑(PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
⊢ Represents b A f
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)) → Represents b A f
intro h
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ↑(LinearMap.comp (↑(PiToModule.fromMatrix R b) A) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) f) (LinearMap.single i)) 1
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
⊢ Represents b A f
refine LinearMap.pi_ext' (fun i => LinearMap.ext_ring ?_)
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ↑(LinearMap.comp (↑(PiToModule.fromMatrix R b) A) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) f) (LinearMap.single i)) 1
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
  PiToModule.fromMatrix_apply_single_one]
no goals
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_3
inst✝³ : AddCommGroup M
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
apply h