awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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'
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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'
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
    ((((((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)
have 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)
Tactic: dsimp [PiToModule.fromEnd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 (α := 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)
have 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)
Tactic: rw [← h'.congr_fun, ← h.congr_fun]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ι
⊢ 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)
have 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)
Tactic: rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ι
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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')
Tactic: rw [map_add, map_add, h, h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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')
⊢ 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)
have 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)
Tactic: rw [map_add, map_add, h, h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_add, h, h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_add, h, h']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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 ι
⊢ 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)
have rw : Eq (α := (ι → R) →ₗ[R] M) 0 ((PiToModule.fromEnd R b : (a : Module.End R M) → (ι → R) →ₗ[R] M) 0)
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have rw₁ : Eq (α := (ι → R) →ₗ[R] M) 0 0
Tactic: rw [map_zero, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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
⊢ 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)
have 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)
Tactic: rw [map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_smul, map_smul, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap (goal)
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) (γ := Submodule R M) (LinearMap.range (Ideal.finsuppTotal ι M I b))
      ((f : (a : M) → M) x : M)
have rw : ∀ (x : M), Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : M) → M) x : M)
Tactic: rw [Ideal.range_finsuppTotal, hb]