awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val : Fintype κ
⊢ HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
have this : HMul.hMul (α := Matrix κ ι R) (β := Matrix ι ι' R)
    ((toMatrix b₁ b₃ : (a : M →ₗ[R] N) → Matrix κ ι R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A) :
      Matrix κ ι R)
    (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
  (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
Tactic: have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val : Fintype κ
this :
  HMul.hMul (α := Matrix κ ι R) (β := Matrix ι ι' R)
      ((toMatrix b₁ b₃ : (a : M →ₗ[R] N) → Matrix κ ι R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A) :
        Matrix κ ι R)
      (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
⊢ HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
have intro : ∀
  (this :
    HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
      (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)),
  HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
Tactic: rwa [LinearMap.toMatrix_toLin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix (⇑(Pi.basisFun R ι) : (a : ι) → ι → R) * A =
    (of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i
have simp : Eq (α := Matrix ι ι R)
  ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
    Matrix ι ι R)
  ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
    Matrix ι ι R)
Tactic: simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ Eq (α := Matrix ι ι R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
    ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
      Matrix ι ι R)
have a : ∀ (i j : ι),
  Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
have a : Eq.{u_5 + 1} (α := R)
  ((((b.repr : (a : ι → R) → ι →₀ R)
            ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
              ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
          ι →₀ R) :
        (a : ι) → R)
      i :
    R)
  ((of : (a : ι → ι → R) → Matrix ι ι R)
      (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
    R)
Tactic: rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
a :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R)
              ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
                ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
have a₁ : Eq.{u_5 + 1} (α := R)
  ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ (Pi.basisFun R ι : (a : ι) → ι → R) j) : ι →₀ R) : (a : ι) → R) i : R)
  ((of : (a : ι → ι → R) → Matrix ι ι R)
      (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
    R)
Tactic: rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
a :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R)
              ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
                ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₁ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ (Pi.basisFun R ι : (a : ι) → ι → R) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
have a₂ : Eq.{u_5 + 1} (α := R)
  ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ Pi.single (M := fun (j : ι) ↦ R) j 1) : ι →₀ R) : (a : ι) → R) i : R)
  ((of : (a : ι → ι → R) → Matrix ι ι R)
      (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
    R)
Tactic: rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
a :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R)
              ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
                ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₁ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ (Pi.basisFun R ι : (a : ι) → ι → R) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₂ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ Pi.single (M := fun (j : ι) ↦ R) j 1) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
have a₃ : Eq.{u_5 + 1} (α := R) ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
  ((of : (a : ι → ι → R) → Matrix ι ι R)
      (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
    R)
Tactic: rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
i j : ι
a :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R)
              ((((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) : (a : ι → R) → ι → R)
                ((Pi.basisFun R ι : (a : ι) → ι → R) j : ι → R)) :
            ι →₀ R) :
          (a : ι) → R)
        i :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₁ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ (Pi.basisFun R ι : (a : ι) → ι → R) j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₂ :
  Eq.{u_5 + 1} (α := R)
    ((((b.repr : (a : ι → R) → ι →₀ R) (A *ᵥ Pi.single (M := fun (j : ι) ↦ R) j 1) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
a₃ :
  Eq.{u_5 + 1} (α := R) ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
⊢ Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
have a₄ : Eq.{u_5 + 1} (α := R) ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
  ((((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i : R)
Tactic: rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
⊢ b.toMatrix (⇑(Pi.basisFun R ι) : (a : ι) → ι → R) * A =
    (of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i
have simp : Eq (α := Matrix ι ι R)
  ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
    Matrix ι ι R)
  ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
    Matrix ι ι R)
Tactic: classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
inst : CommSemiring R
inst_1 : Fintype ι
b : Basis ι R (ι → R)
A : Matrix ι ι R
simp :
  Eq (α := Matrix ι ι R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) :
      Matrix ι ι R)
    ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i :
      Matrix ι ι R)
⊢ b.toMatrix (⇑(Pi.basisFun R ι) : (a : ι) → ι → R) * A =
    (of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
      (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i
have a : ∀ (i j : ι),
  Eq.{u_5 + 1} (α := R)
    ((toMatrix (Pi.basisFun R ι) b : (a : (ι → R) →ₗ[R] ι → R) → Matrix ι ι R)
        ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A) i j :
      R)
    ((of : (a : ι → ι → R) → Matrix ι ι R)
        (fun (i j : ι) ↦ (((b.repr : (a : ι → R) → ι →₀ R) (A.col j) : ι →₀ R) : (a : ι) → R) i) i j :
      R)
Tactic: classical
  simp only [basis_toMatrix_mul _ _ (Pi.basisFun R ι), Matrix.toLin_eq_toLin']
  ext i j
  rw [LinearMap.toMatrix_apply, Matrix.toLin'_apply, Pi.basisFun_apply,
    Matrix.mulVec_single_one, Matrix.of_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι'
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v =
    (reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))
have a : ∀ (i j : ι'),
  (b.reindex e).toMatrix v i j =
    (reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : Finite ι'
m : M
⊢ mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
have intro : ∀ (val : Fintype ι'),
  mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
Tactic: cases nonempty_fintype ι'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : Finite ι'
m : M
⊢ mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
have intro : ∀ (val : Fintype ι'),
  mulVec.{u_5, u_2, u_1} (n := ι) (b'.toMatrix (⇑b : (a : ι) → M))
      (⇑((b.repr : (a : M) → ι →₀ R) m : ι →₀ R) : (a : ι) → R) =
    (⇑((b'.repr : (a : M) → ι' →₀ R) m : ι' →₀ R) : (a : ι') → R)
Tactic: classical
  cases nonempty_fintype ι'
  simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
have haveI : ∀ (this : DecidableEq ι),
  HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this : DecidableEq ι
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
have haveI : ∀ (this : DecidableEq ι'),
  HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
Tactic: haveI := Classical.decEq ι'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this_1 : DecidableEq ι
this : DecidableEq ι'
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
have haveI : ∀ (this : DecidableEq ι''),
  HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
Tactic: haveI := Classical.decEq ι''
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
ι'' : Type u_10
inst_3 : Fintype ι'
b'' : ι'' → M
this_1 : DecidableEq ι
this_2 : DecidableEq ι'
this : DecidableEq ι''
⊢ HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') = b.toMatrix b''
have a : ∀ (i : ι) (j : ι''),
  HMul.hMul (α := Matrix ι ι' R) (b.toMatrix (⇑b' : (a : ι') → M)) (b'.toMatrix b'') i j = b.toMatrix b'' i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : DecidableEq ι
inst_4 : Fintype ι'
⊢ HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' ι R) (b.toMatrix (⇑b' : (a : ι') → M))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    1
have rw : Eq (α := Matrix ι ι R) (b.toMatrix (⇑b : (a : ι) → M)) 1
Tactic: rw [toMatrix_mul_toMatrix, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : DecidableEq ι
inst_4 : Fintype ι'
rw : Eq (α := Matrix ι ι R) (b.toMatrix (⇑b : (a : ι) → M)) 1
⊢ HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' ι R) (b.toMatrix (⇑b' : (a : ι') → M))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    1
have rw₁ : Eq (α := Matrix ι ι R) 1 1
Tactic: rw [toMatrix_mul_toMatrix, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm : (a : ι') → ι) _root_.id
have a : ∀ (i j : ι'), (b.reindex e).toMatrix v i j = (b.toMatrix v).submatrix (⇑e.symm : (a : ι') → ι) _root_.id i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
⊢ (b.map f).toMatrix v = b.toMatrix ((⇑f.symm : (a : N) → M) ∘ v)
have a : ∀ (i j : ι), (b.map f).toMatrix v i j = b.toMatrix ((⇑f.symm : (a : N) → M) ∘ v) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B₂ : BilinForm R₁ (n → R₁)
⊢ toBilin'Aux
      ((BilinForm.toMatrixAux fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
have rw : toBilin'Aux
    (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
            Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
        (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
      B₂) =
  B₂
Tactic: rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.BilinearForm (goal)
Goal:
R₁ : Type u_1
inst : CommSemiring R₁
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
B₂ : BilinForm R₁ (n → R₁)
rw :
  toBilin'Aux
      (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
              Pi.single (M := fun (j : n) ↦ R₁) j 1 :
            (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
⊢ toBilin'Aux
      ((BilinForm.toMatrixAux fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
        B₂) =
    B₂
have rw₁ : toLinearMap₂'Aux (RingHom.id R₁) (RingHom.id R₁)
    (((toMatrix₂Aux R₁ (fun (j : n) ↦ Pi.single (M := fun (j : n) ↦ R₁) j 1) fun (j : n) ↦
            Pi.single (M := fun (j : n) ↦ R₁) j 1 :
          (((j : n) → R₁) →ₗ[R₁] ((j : n) → R₁) →ₗ[R₁] R₁) →ₗ[R₁] Matrix n n R₁) :
        (a : BilinForm R₁ ((j : n) → R₁)) → Matrix n n R₁)
      B₂) =
  B₂
Tactic: rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, toLinearMap₂'Aux_toMatrix₂Aux]