awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
    A.charpoly
have rw : Eq (α := R[X])
  (HMul.hMul (β := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      (HMul.hMul (α := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
        Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q : Matrix ι' (ChooseBasisIndex R M) R)
        ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R))
      ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R)).charpoly
  A.charpoly
Tactic: rw [charpoly_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Eq (α := R[X]) (P * A * Q).charpoly A.charpoly
have A₁ : Eq (α := R[X])
  (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
    ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
  (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
      (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
        ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
        ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
      ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q : Matrix ι' (ChooseBasisIndex R M) R)).charpoly
Tactic: calc
    (P * A * Q).charpoly = (φ (P * A * Q)).charpoly := (charpoly_reindex ..).symm
    _ = (φ₁ P * φ₂ A * φ₃ Q).charpoly := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
    _ = A.charpoly := by rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
A₁ :
  Eq (α := R[X])
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
⊢ Eq (α := R[X]) (P * A * Q).charpoly A.charpoly
have A₂ : Eq (α := R[X])
  (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
      (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
        ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
        ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
      ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q : Matrix ι' (ChooseBasisIndex R M) R)).charpoly
  A.charpoly
Tactic: calc
    (P * A * Q).charpoly = (φ (P * A * Q)).charpoly := (charpoly_reindex ..).symm
    _ = (φ₁ P * φ₂ A * φ₃ Q).charpoly := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
    _ = A.charpoly := by rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂)) R (M₁ × M₂) := b₁.prod b₂
⊢ (f₁.prodMap f₂).charpoly (M := M₁ × M₂) = f₁.charpoly * f₂.charpoly
have rw : (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
  Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) *
    f₂.charpoly
Tactic: rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂)) R (M₁ × M₂) := b₁.prod b₂
rw :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) *
      f₂.charpoly
⊢ (f₁.prodMap f₂).charpoly (M := M₁ × M₂) = f₁.charpoly * f₂.charpoly
have rw₁ : (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
  HMul.hMul (α := R[X])
    (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
    (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
Tactic: rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂)) R (M₁ × M₂) := b₁.prod b₂
rw :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) *
      f₂.charpoly
rw₁ :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
⊢ (f₁.prodMap f₂).charpoly (M := M₁ × M₂) = f₁.charpoly * f₂.charpoly
have rw₂ : Matrix.charpoly (n := Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂))
    ((toMatrix b b :
        (a : M₁ × M₂ →ₗ[R] M₁ × M₂) →
          Matrix (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R)
      (f₁.prodMap f₂)) =
  HMul.hMul (α := R[X])
    (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
    (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
Tactic: rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
f₁ : M₁ →ₗ[R] M₁
f₂ : M₂ →ₗ[R] M₂
b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂
b : Basis (Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂)) R (M₁ × M₂) := b₁.prod b₂
rw :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) *
      f₂.charpoly
rw₁ :
  (f₁.prodMap f₂).charpoly (M := M₁ × M₂) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
rw₂ :
  Matrix.charpoly (n := Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂))
      ((toMatrix b b :
          (a : M₁ × M₂ →ₗ[R] M₁ × M₂) →
            Matrix (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R)
        (f₁.prodMap f₂)) =
    HMul.hMul (α := R[X])
      (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
        ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
      (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
        ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
⊢ (f₁.prodMap f₂).charpoly (M := M₁ × M₂) = f₁.charpoly * f₂.charpoly
have rw₃ : Matrix.charpoly (n := Sum.{u_3, u_4} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₂))
    (fromBlocks ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁) 0 0
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂)) =
  HMul.hMul (α := R[X])
    (Matrix.charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) f₁))
    (Matrix.charpoly.{u_1, u_4} (n := ChooseBasisIndex R M₂)
      ((toMatrix b₂ b₂ : (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₂) (ChooseBasisIndex R M₂) R) f₂))
Tactic: rw [← charpoly_toMatrix f₁ b₁, ← charpoly_toMatrix f₂ b₂, ← charpoly_toMatrix (f₁.prodMap f₂) b,
    toMatrix_prodMap b₁ b₂ f₁ f₂, Matrix.charpoly_fromBlocks_zero₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ LinearMap.charpoly.{u_1, u_4} (M := M₂) ((e.conj : (a : End R M₁) → End R M₂) φ) = LinearMap.charpoly φ
have rw : Eq.{u_1 + 1} (α := R[X])
  (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
        (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
      ((e.conj : (a : End R M₁) → End R M₂) φ)))
  (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ))
Tactic: rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ Eq.{u_1 + 1} (α := R[X])
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ)))
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ))
have e_M : Eq (α := Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
  ((LinearMap.toMatrix (b.map e) (b.map e) :
        (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
      ((e.conj : (a : End R M₁) → End R M₂) φ) :
    Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
  ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ :
    Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
⊢ Eq (α := Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ) :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
have e_M : ∀ (i j : ChooseBasisIndex R M₁),
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ) i j :
      R)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ i j : R)
Tactic: ext i j : 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ Eq (α := R[X]) (LinearMap.charpoly (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A)) A.charpoly
have rw : Eq (α := R[X])
  (LinearMap.charpoly (M := n → R)
    ((toLin (Pi.basisFun R n) (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A))
  A.charpoly
Tactic: rw [← Matrix.toLin_eq_toLin', charpoly_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
Goal:
R : Type u_1
inst : CommRing R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
rw :
  Eq (α := R[X])
    (LinearMap.charpoly (M := n → R)
      ((toLin (Pi.basisFun R n) (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A))
    A.charpoly
⊢ Eq (α := R[X]) (LinearMap.charpoly (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A)) A.charpoly
have rw₁ : Eq (α := R[X]) A.charpoly A.charpoly
Tactic: rw [← Matrix.toLin_eq_toLin', charpoly_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
v : V
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) (1 ⊗ₜ[R] v)) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((Q : (a : V) → R) v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
have rw : Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : V) → R) v : R) (HMul.hMul (α := A) 1 1)) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((Q : (a : V) → R) v) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
Tactic: rw [QuadraticForm.baseChange_tmul, one_mul, ← Algebra.algebraMap_eq_smul_one,
      ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange (goal)
Goal:
R : Type u_1
A : Type u_2
V : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup V
inst_3 : Algebra R A
inst_4 : Module R V
inst_5 : Invertible (α := R) 2
Q : QuadraticForm R V
v : V
rw :
  Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : V) → R) v : R) (HMul.hMul (α := A) 1 1)) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((Q : (a : V) → R) v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
⊢ Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((QuadraticForm.baseChange A Q : (a : A ⊗[R] V) → A) (1 ⊗ₜ[R] v)) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
    ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
          (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
        ((Q : (a : V) → R) v) :
      CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
have rw₁ : Eq (α := CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap A (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : A) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := A) ((Q : (a : V) → R) v : R) 1) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
  ((algebraMap R (CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q)) :
        (a : R) → CliffordAlgebra (QuadraticForm.baseChange A Q))
      ((Q : (a : V) → R) v) :
    CliffordAlgebra (R := A) (M := A ⊗[R] V) (QuadraticForm.baseChange A Q))
Tactic: rw [QuadraticForm.baseChange_tmul, one_mul, ← Algebra.algebraMap_eq_smul_one,
      ← IsScalarTower.algebraMap_apply]