awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f * g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
have rw : (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ∘ₗ g) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
Tactic: rw [Module.End.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
rw :
  (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
⊢ (toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (f * g) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
      ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
have rw₁ : HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R) =
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) f : Matrix n n R)
    ((toMatrixAlgEquiv v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) g : Matrix n n R)
Tactic: rw [Module.End.mul_eq_comp, LinearMap.toMatrixAlgEquiv_comp v₁ f g]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ Eq (α := Matrix n n R)
    ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) : Matrix n n R)
    (Matrix.diagonal fun (x_1 : n) ↦ x : Matrix n n R)
have a : ∀ (i j : n),
  Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a : Eq.{u_1 + 1} (α := R)
  ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
          n →₀ R) :
        (a : n) → R)
      i :
    R)
  (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₁ : Eq.{u_1 + 1} (α := R)
  ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
    R)
  (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₂ : Eq.{u_1 + 1} (α := R)
  ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
  (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₃ : Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
  (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₃ :
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₄ : Eq.{u_1 + 1} (α := R) ((Finsupp.single j x : (a : n) → R) i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₃ :
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₄ : Eq.{u_1 + 1} (α := R) ((Finsupp.single j x : (a : n) → R) i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₅ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (j : n) ↦ R) j x i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₃ :
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₄ : Eq.{u_1 + 1} (α := R) ((Finsupp.single j x : (a : n) → R) i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₅ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (j : n) ↦ R) j x i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₆ : Pi.single (M := fun (j : n) ↦ R) j x i = if i = j then x else 0
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
v₁ : Basis n R M₁
x : R
i j : n
a :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) ((DistribSMul.toLinearMap R M₁ x : (a : M₁) → M₁) ((v₁ : (a : n) → M₁) j : M₁)) :
            n →₀ R) :
          (a : n) → R)
        i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((((v₁.repr : (a : M₁) → n →₀ R) (HSMul.hSMul (β := M₁) x ((v₁ : (a : n) → M₁) j : M₁)) : n →₀ R) : (a : n) → R) i :
      R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (β := n →₀ R) x ((v₁.repr : (a : M₁) → n →₀ R) ((v₁ : (a : n) → M₁) j) : n →₀ R) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₃ :
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (β := n →₀ R) x (Finsupp.single j 1) : (a : n) → R) i : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₄ : Eq.{u_1 + 1} (α := R) ((Finsupp.single j x : (a : n) → R) i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₅ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (j : n) ↦ R) j x i : R) (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
a₆ : Pi.single (M := fun (j : n) ↦ R) j x i = if i = j then x else 0
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) (DistribSMul.toLinearMap R M₁ x) i j : R)
    (Matrix.diagonal (fun (x_1 : n) ↦ x) i j : R)
have a₇ : (if i = j then x else 0) = if i = j then x else 0
Tactic: rw [LinearMap.toMatrix_apply, DistribSMul.toLinearMap_apply, map_smul,
    Basis.repr_self, Finsupp.smul_single_one, Finsupp.single_eq_pi_single, Matrix.diagonal_apply,
    Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
⊢ Eq (α := Matrix (n ⊕ m) (n ⊕ m) R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
    (fromBlocks ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
have a : ∀ (i j : n),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inl i) (Sum.inl j) :
      R)
    (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
      R)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
a :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inl j) :
        R)
      (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0
          0 ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
        R)
⊢ Eq (α := Matrix (n ⊕ m) (n ⊕ m) R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
    (fromBlocks ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
have a₁ : ∀ (i : n) (j : m),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inl i) (Sum.inr j) :
      R)
    (fromBlocks (l := n) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inr j) :
      R)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
a :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inl j) :
        R)
      (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0
          0 ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
        R)
a₁ :
  ∀ (i : n) (j : m),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inr j) :
        R)
      (fromBlocks (l := n) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
          ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inr j) :
        R)
⊢ Eq (α := Matrix (n ⊕ m) (n ⊕ m) R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
    (fromBlocks ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
have a₂ : ∀ (i : m) (j : n),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inr i) (Sum.inl j) :
      R)
    (fromBlocks (m := m) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inl j) :
      R)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype n
inst_2 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₁
inst_6 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_7 : Fintype m
inst_8 : DecidableEq m
inst_9 : DecidableEq (n ⊕ m)
φ₁ : End R M₁
φ₂ : End R M₂
a :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inl j) :
        R)
      (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (m := m) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0
          0 ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inl j) :
        R)
a₁ :
  ∀ (i : n) (j : m),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inl i) (Sum.inr j) :
        R)
      (fromBlocks (l := n) (o := m) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
          ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inl i) (Sum.inr j) :
        R)
a₂ :
  ∀ (i : m) (j : n),
    Eq.{u_1 + 1} (α := R)
      ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
          (Sum.inr i) (Sum.inl j) :
        R)
      (fromBlocks (m := m) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
          ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inl j) :
        R)
⊢ Eq (α := Matrix (n ⊕ m) (n ⊕ m) R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
    (fromBlocks ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) :
      Matrix (n ⊕ m) (n ⊕ m) R)
have a₃ : ∀ (i j : m),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix (v₁.prod v₂) (v₁.prod v₂) : (a : M₁ × M₂ →ₗ[R] M₁ × M₂) → Matrix (n ⊕ m) (n ⊕ m) R) (prodMap φ₁ φ₂)
        (Sum.inr i) (Sum.inr j) :
      R)
    (fromBlocks.{u_4, u_3, u_4, u_3, u_1} (l := n) (n := n) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) φ₁) 0 0
        ((toMatrix v₂ v₂ : (a : M₂ →ₗ[R] M₂) → Matrix m m R) φ₂) (Sum.inr i) (Sum.inr j) :
      R)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 1) : Matrix m m R)
    (1 : Matrix m m R)
have rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 1) 1
Tactic: rw [map_one, LinearMap.toMatrix_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
rw : Eq (α := Matrix m m R) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) 1) 1
⊢ Eq (α := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) 1) : Matrix m m R)
    (1 : Matrix m m R)
have rw₁ : Eq (α := Matrix m m R) 1 1
Tactic: rw [map_one, LinearMap.toMatrix_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
m : Type u_3
inst_3 : Fintype m
inst_4 : DecidableEq m
b : Basis m R S
x y : S
⊢ (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) (x * y)) =
    HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
have rw : (toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R)
    (HMul.hMul (α := End R S) (β := End R S) ((lmul R S : (a : S) → End R S) x : End R S)
      ((lmul R S : (a : S) → End R S) y : End R S)) =
  HMul.hMul (α := Matrix m m R) (β := Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) x) : Matrix m m R)
    ((toMatrix b b : (a : S →ₗ[R] S) → Matrix m m R) ((lmul R S : (a : S) → End R S) y) : Matrix m m R)
Tactic: rw [map_mul, LinearMap.toMatrix_mul]