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
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] m → R
v : n → R
rw :
  Eq (α := m → R)
    ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) :
            (n → R) →ₗ[R] m → R) :
          (a : n → R) → m → R)
        v :
      m → R)
    ((f : (a : n → R) → m → R) v : m → R)
⊢ Eq (α := m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f *ᵥ v) ((f : (a : n → R) → m → R) v)
have rw₁ : Eq (α := m → R) ((f : (a : n → R) → m → R) v : m → R) ((f : (a : n → R) → m → R) v : m → R)
Tactic: rw [← toLin'_apply, toLin'_toMatrix']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Eq (α := Matrix n n R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id : Matrix n n R) (1 : Matrix n n R)
have a : ∀ (i j : n), Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 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_5
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)
have a : Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (if i = j then 1 else 0 : R)
Tactic: rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_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_5
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (if i = j then 1 else 0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)
have a₁ : Eq.{u_1 + 1} (α := R) ((id : (a : n → R) → n → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i : R)
  (if i = j then 1 else 0 : R)
Tactic: rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_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_5
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (if i = j then 1 else 0 : R)
a₁ :
  Eq.{u_1 + 1} (α := R) ((id : (a : n → R) → n → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i : R)
    (if i = j then 1 else 0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)
have a₂ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : n) ↦ R) j 1 i : R) (if i = j then 1 else 0 : R)
Tactic: rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_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_5
inst_1 : DecidableEq n
inst_2 : Fintype n
i j : n
a :
  Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (if i = j then 1 else 0 : R)
a₁ :
  Eq.{u_1 + 1} (α := R) ((id : (a : n → R) → n → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i : R)
    (if i = j then 1 else 0 : R)
a₂ : Eq.{u_1 + 1} (α := R) (Pi.single (M := fun (a : n) ↦ R) j 1 i : R) (if i = j then 1 else 0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) id i j : R) (1 i j : R)
have a₃ : Eq.{u_1 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
have succ : (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
  HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
    ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
Tactic: rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
succ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
have succ₁ : (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
  HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
    (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
    ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
Tactic: rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
succ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
succ₁ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
have succ₂ : (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) ∘ₗ
    (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
  HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
    (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
    ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
Tactic: rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
succ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
succ₁ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₂ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
have succ₃ : HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
    (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
  HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
    (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
    ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
Tactic: rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n_1 : Type u_5
inst_1 : DecidableEq n_1
inst_2 : Fintype n_1
M : Matrix n_1 n_1 R
n : ℕ
ih :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n
succ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
succ₁ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n * M) =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₂ :
  (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ n) ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
succ₃ :
  HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
      (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M =
    HMul.hMul (β := (n_1 → R) →ₗ[R] n_1 → R)
      (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
        ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R)
⊢ (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) (M ^ (n + 1)) =
    HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) (n + 1)
have succ₄ : Eq (α := (n_1 → R) →ₗ[R] n_1 → R)
  (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
    (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M)
  (HPow.hPow (α := (n_1 → R) →ₗ[R] n_1 → R)
      ((toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M : (n_1 → R) →ₗ[R] n_1 → R) n ∘ₗ
    (toLin' : (a : Matrix n_1 n_1 R) → (n_1 → R) →ₗ[R] n_1 → R) M)
Tactic: rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
⊢ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ k) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) k
have zero : (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (HPow.hPow (β := ℕ) M 0) =
  HPow.hPow (α := (n → R) →ₗ[R] n → R) (β := ℕ)
    ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) 0
Tactic: induction k with
  | zero => simp [End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
k : ℕ
zero :
  (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (HPow.hPow (β := ℕ) M 0) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) (β := ℕ)
      ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) 0
⊢ (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ k) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R) k
have succ : ∀ (n_1 : ℕ)
  (ih :
    (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ n_1) =
      HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R)
        n_1),
  (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M ^ (n_1 + 1)) =
    HPow.hPow (α := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) M : (n → R) →ₗ[R] n → R)
      (n_1 + 1)
Tactic: induction k with
  | zero => simp [End.one_eq_id]
  | succ n ih => rw [pow_succ, pow_succ, toLin'_mul, ih, Module.End.mul_eq_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
⊢ Eq (α := l → R)
    ((((toLin' : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (M * N) : (n → R) →ₗ[R] l → R) : (a : n → R) → l → R) x :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
have rw : Eq (α := l → R)
  (((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M ∘ₗ (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N :
        (a : n → R) → l → R)
      x :
    l → R)
  ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) :
    l → R)
Tactic: rw [Matrix.toLin'_mul, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
rw :
  Eq (α := l → R)
    (((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M ∘ₗ (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N :
          (a : n → R) → l → R)
        x :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
⊢ Eq (α := l → R)
    ((((toLin' : (a : Matrix l n R) → (n → R) →ₗ[R] l → R) (M * N) : (n → R) →ₗ[R] l → R) : (a : n → R) → l → R) x :
      l → R)
    ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
        ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
          m → R) :
      l → R)
have rw₁ : Eq (α := l → R)
  ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) :
    l → R)
  ((((toLin' : (a : Matrix l m R) → (m → R) →ₗ[R] l → R) M : (m → R) →ₗ[R] l → R) : (a : m → R) → l → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) N : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) :
    l → R)
Tactic: rw [Matrix.toLin'_mul, LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this :
  f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
⊢ (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
have rw : (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R)
    ((toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))) =
  HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
    ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
    ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
Tactic: rw [this, LinearMap.toMatrix'_toLin']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this :
  f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
rw :
  (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R)
      ((toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
        (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
          ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
          ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
⊢ (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
have rw₁ : HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
    ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
    ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R) =
  HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
    ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
    ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
Tactic: rw [this, LinearMap.toMatrix'_toLin']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ (toMatrix' : (a : (l → R) →ₗ[R] m → R) → Matrix m l R) (f ∘ₗ g) =
    HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R)
have suffices : f ∘ₗ g =
  (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
    (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
      ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
      ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
Tactic: suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
    rw [this, LinearMap.toMatrix'_toLin']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
have rw : f ∘ₗ g =
  (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) ∘ₗ
    (toLin' : (a : Matrix n l R) → (l → R) →ₗ[R] n → R) ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g)
Tactic: rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : Fintype l
inst_4 : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
rw :
  f ∘ₗ g =
    (toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f) ∘ₗ
      (toLin' : (a : Matrix n l R) → (l → R) →ₗ[R] n → R) ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g)
⊢ f ∘ₗ g =
    (toLin' : (a : Matrix m l R) → (l → R) →ₗ[R] m → R)
      (HMul.hMul (α := Matrix m n R) (β := Matrix n l R)
        ((toMatrix' : (a : (n → R) →ₗ[R] m → R) → Matrix m n R) f : Matrix m n R)
        ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g : Matrix n l R))
have rw₁ : f ∘ₗ g =
  f ∘ₗ (toLin' : (a : Matrix n l R) → (l → R) →ₗ[R] n → R) ((toMatrix' : (a : (l → R) →ₗ[R] n → R) → Matrix n l R) g)
Tactic: rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']