awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this :
  Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
        (Pi.single (M := fun (a : ι) ↦ R) i 1) :
      M)
mp :
  ∀
    (this :
      Eq.{u_2 + 1} (α := M)
        ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) : (a : ι → R) → M)
            (Pi.single (M := fun (a : ι) ↦ R) i 1) :
          M)
        ((f : (a : M) → M) (b i) : M)),
    Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
mp₁ mp₂ mp₃ mp₄ :
  ∀ (this : Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)),
    Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
⊢ Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)

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

Premises used: PiToModule.fromMatrix_apply_single_one, PiToModule.fromEnd_apply_single_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
mpr :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := M)
      ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A ∘ₗ
                LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
      ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
⊢ Represents b A f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
i : ι
mpr : Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)

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

Premises used: LinearMap.comp_apply, PiToModule.fromMatrix_apply_single_one, PiToModule.fromEnd_apply_single_one, LinearMap.coe_single
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), Eq (α := M) (∑ i : ι, A i j • b i : M) ((f : (a : M) → M) (b j) : M)
i : ι
⊢ Eq (α := M) (∑ i_1 : ι, A i_1 i • b i_1 : M) ((f : (a : M) → M) (b i) : M)

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
rw :
  Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
              (Fintype.linearCombination R b) :
            ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
          (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
        (HMul.hMul (α := Module.End R (ι → R)) (β := Module.End R (ι → R))
          ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R))
          ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R))) :
      (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f * f') : (ι → R) →ₗ[R] M)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
                (Fintype.linearCombination R b) ∘ₗ
              AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix') :
            Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M) :
          (a : Matrix ι ι R) → (ι → R) →ₗ[R] M)
        (A * A') :
      (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f * f') : (ι → R) →ₗ[R] M)

Tactic:
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_mul]

Premises used: LinearMap.comp_apply, map_mul, AlgEquiv.toLinearMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
h₁ :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := M)
      ((((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
                        (Fintype.linearCombination R b) :
                      ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
                    (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
                  (HMul.hMul (α := Module.End R (ι → R)) (β := Module.End R (ι → R))
                    ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A :
                      Module.End R (ι → R))
                    ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' :
                      Module.End R (ι → R))) ∘ₗ
                LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
      ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f * f') ∘ₗ
                LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
              (Fintype.linearCombination R b) :
            ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
          (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
        (HMul.hMul (α := Module.End R (ι → R)) (β := Module.End R (ι → R))
          ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R))
          ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R))) :
      (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f * f') : (ι → R) →ₗ[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i : ι
h₁ :
  Eq (α := M)
    ((Fintype.linearCombination R b : (a : ι → R) → M)
        ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R)) :
              (a : (i : ι) → R) → (i : ι) → R)
            ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R)) :
                  (a : (i : ι) → R) → (i : ι) → R)
                (Pi.single (M := fun (i : ι) ↦ R) i 1) :
              (i : ι) → R) :
          (i : ι) → R) :
      M)
    ((f : (a : M) → M)
        ((f' : (a : M) → M)
            ((Fintype.linearCombination R b : (a : (i : ι) → R) → M) (Pi.single (M := fun (i : ι) ↦ R) i 1) : M) :
          M) :
      M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
                      (Fintype.linearCombination R b) :
                    ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
                  (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
                (HMul.hMul (α := Module.End R (ι → R)) (β := Module.End R (ι → R))
                  ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R))
                  ((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' :
                    Module.End R (ι → R))) ∘ₗ
              LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f * f') ∘ₗ
              LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)

Tactic:
dsimp [PiToModule.fromEnd]

Premises used: PiToModule.fromEnd
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i : ι
h₁ :
  Eq.{u_2 + 1} (α := M)
    ((Fintype.linearCombination R b : (a : ι → R) → M)
        ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R)) :
              (a : (i : ι) → R) → (i : ι) → R)
            ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R)) :
                  (a : (i : ι) → R) → (i : ι) → R)
                (Pi.single (M := fun (i : ι) ↦ R) i 1) :
              (i : ι) → R) :
          (i : ι) → R) :
      M)
    ((Fintype.linearCombination R b : (a : ι → R) → M) (A *ᵥ A' *ᵥ Pi.single (M := fun (i : ι) ↦ R) i 1) : M)
⊢ Eq (α := M)
    ((Fintype.linearCombination R b : (a : ι → R) → M)
        ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R)) :
              (a : (i : ι) → R) → (i : ι) → R)
            ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R)) :
                  (a : (i : ι) → R) → (i : ι) → R)
                (Pi.single (M := fun (i : ι) ↦ R) i 1) :
              (i : ι) → R) :
          (i : ι) → R) :
      M)
    ((f : (a : M) → M)
        ((f' : (a : M) → M)
            ((Fintype.linearCombination R b : (a : (i : ι) → R) → M) (Pi.single (M := fun (i : ι) ↦ R) i 1) : M) :
          M) :
      M)

Tactic:
rw [← h'.congr_fun, ← h.congr_fun]

Premises used: Matrix.Represents.congr_fun
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i : ι
⊢ Eq.{u_2 + 1} (α := M)
    ((Fintype.linearCombination R b : (a : ι → R) → M)
        ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A : Module.End R (ι → R)) :
              (a : (i : ι) → R) → (i : ι) → R)
            ((((AlgEquiv.symm algEquivMatrix' : (a : Matrix ι ι R) → Module.End R (ι → R)) A' : Module.End R (ι → R)) :
                  (a : (i : ι) → R) → (i : ι) → R)
                (Pi.single (M := fun (i : ι) ↦ R) i 1) :
              (i : ι) → R) :
          (i : ι) → R) :
      M)
    ((Fintype.linearCombination R b : (a : ι → R) → M) (A *ᵥ A' *ᵥ Pi.single (M := fun (i : ι) ↦ R) i 1) : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
rw :
  Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
            (Fintype.linearCombination R b) :
          ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
        (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
      1)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 1)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
              (Fintype.linearCombination R b) ∘ₗ
            AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix') :
          Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M) :
        (a : Matrix ι ι R) → (ι → R) →ₗ[R] M)
      1)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 1)

Tactic:
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_one]

Premises used: LinearMap.comp_apply, map_one, AlgEquiv.toLinearMap_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
h :
  ∀ (i : ι),
    Eq.{u_2 + 1} (α := M)
      ((((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
                        (Fintype.linearCombination R b) :
                      ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
                    (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
                  1 ∘ₗ
                LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
      ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 1 ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
            (Fintype.linearCombination R b) :
          ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
        (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
      1)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
i : ι
⊢ Eq.{u_2 + 1} (α := M)
    ((((((LinearMap.llcomp R (ι → R) (ι → R) M : (a : (ι → R) →ₗ[R] M) → ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M)
                      (Fintype.linearCombination R b) :
                    ((ι → R) →ₗ[R] ι → R) →ₗ[R] (ι → R) →ₗ[R] M) :
                  (a : (ι → R) →ₗ[R] ι → R) → (ι → R) →ₗ[R] M)
                1 ∘ₗ
              LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 1 ∘ₗ LinearMap.single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h :
  Eq (α := (ι → R) →ₗ[R] M) ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
h' :
  Eq (α := (ι → R) →ₗ[R] M) ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A' : (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f' : (ι → R) →ₗ[R] M)
rw :
  HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M)
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A' : (ι → R) →ₗ[R] M) =
    (PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f + f')
rw₁ :
  HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M)
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A' : (ι → R) →ₗ[R] M) =
    HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f' : (ι → R) →ₗ[R] M)
rw₂ :
  HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A' : (ι → R) →ₗ[R] M) =
    HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f' : (ι → R) →ₗ[R] M)
rw₃ rw₄ :
  HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f' : (ι → R) →ₗ[R] M) =
    HAdd.hAdd (α := (ι → R) →ₗ[R] M) (β := (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f' : (ι → R) →ₗ[R] M)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) (A + A') : (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (f + f') : (ι → R) →ₗ[R] M)

Tactic:
rw [map_add, map_add, h, h']

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
rw : Eq (α := (ι → R) →ₗ[R] M) 0 ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 0)
rw₁ rw₂ : Eq (α := (ι → R) →ₗ[R] M) 0 0
⊢ Eq (α := (ι → R) →ₗ[R] M) ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) 0)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 0)

Tactic:
rw [map_zero, map_zero]

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h :
  Eq (α := (ι → R) →ₗ[R] M) ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
r : R
rw :
  HSMul.hSMul (β := (ι → R) →ₗ[R] M) r
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) =
    (PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (r • f)
rw₁ :
  HSMul.hSMul (β := (ι → R) →ₗ[R] M) r
      ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) A : (ι → R) →ₗ[R] M) =
    HSMul.hSMul (β := (ι → R) →ₗ[R] M) r
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
rw₂ rw₃ :
  HSMul.hSMul (β := (ι → R) →ₗ[R] M) r
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) =
    HSMul.hSMul (β := (ι → R) →ₗ[R] M) r
      ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M)
⊢ Eq (α := (ι → R) →ₗ[R] M)
    ((PiToModule.fromMatrix R b : (a : Matrix ι ι R) → (ι → R) →ₗ[R] M) (r • A) : (ι → R) →ₗ[R] M)
    ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) (r • f) : (ι → R) →ₗ[R] M)

Tactic:
rw [map_smul, map_smul, h]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
r : R
⊢ Represents.{u_1, u_2, u_3} (R := R) b ((Algebra.algebraMap R (Matrix ι ι R) : (a : R) → Matrix ι ι R) r)
    ((Algebra.algebraMap R (Module.End R M) : (a : R) → Module.End R M) r)

Tactic:
simpa only [Algebra.algebraMap_eq_smul_one] using Matrix.Represents.one.smul r

Premises used: Matrix.Represents.smul, Algebra.algebraMap_eq_smul_one, Matrix.Represents.one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
A : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A f'
⊢ f = f'

Tactic:
PiToModule.fromEnd_injective R b hb (h.symm.trans h')

Premises used: PiToModule.fromEnd_injective, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
A : ↥(isRepresentation R b)
⊢ Represents b (↑A : Matrix ι ι R) ((toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) A)

Tactic:
A.2.choose_spec

Premises used: Exists.choose_spec, Classical.choose, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
A : ↥(isRepresentation R b)
f : Module.End R M
h : Represents b (↑A : Matrix ι ι R) f
⊢ (toEnd R b hb : (a : ↥(isRepresentation R b)) → Module.End R M) A = f

Tactic:
A.2.choose_spec.eq hb h

Premises used: Exists.choose_spec, Classical.choose, Matrix.Represents.eq, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
rw : ∀ (x : M), Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : M) → M) x : M)
⊢ ∀ (x : M),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Ideal.finsuppTotal ι M I b))
      ((f : (a : M) → M) x : M)

Tactic:
rw [Ideal.range_finsuppTotal, hb]

Premises used: Ideal.range_finsuppTotal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Goal:
ι : Type u_1
inst : Fintype ι
M : Type u_2
inst_1 : AddCommGroup M
R : Type u_3
inst_2 : CommRing R
inst_3 : Module R M
b : ι → M
inst_4 : DecidableEq ι
hb : Eq (α := Submodule R M) (Submodule.span R (Set.range b)) ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ ∀ (x : M), Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : M) → M) x : M)

Tactic:
fun x => hI (LinearMap.mem_range_self f x)

Premises used: LinearMap.mem_range_self