-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.represents_iff' {A : Matrix ι ι R} {f : Module.End R M} :
    A.Represents b f ↔ ∀ j, ∑ i : ι, A i j • b i = f (b j)

Proof state:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)

Tactic:
intro h i

Result:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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)

Proof state:
case mpr.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
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A ∘ₗ LinearMap.single R (fun i => R) i✝) 1 =
    ((PiToModule.fromEnd R b) f ∘ₗ LinearMap.single R (fun i => R) i✝) 1

Tactic:
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
  PiToModule.fromMatrix_apply_single_one]

Result:
case mpr.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
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
i✝ : ι
⊢ ∑ i : ι, A i i✝ • b i = f (b i✝)

Proof state:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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)

Tactic:
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this

Result:
no goals

Proof state:
case mpr.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
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
i✝ : ι
⊢ ∑ i : ι, A i i✝ • b i = f (b i✝)

Tactic:
apply h

Result:
no goals

Proof state:
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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

Tactic:
ext

Result:
case mpr.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
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A ∘ₗ LinearMap.single R (fun i => R) i✝) 1 =
    ((PiToModule.fromEnd R b) f ∘ₗ LinearMap.single R (fun i => R) i✝) 1

Proof state:
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)) → Represents b A f

Tactic:
intro h

Result:
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)

Tactic:
constructor

Result:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)) → Represents b A f

Proof state:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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)

Tactic:
have := LinearMap.congr_fun h (Pi.single i 1)

Result:
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
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)