awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
n : Type u_4
inst_1 : Fintype m
M : Matrix m n R
⊢ Function.Injective (α := m → R) (β := n → R) (⇑M.vecMulLinear : (a : m → R) → n → R) ↔
    Function.Injective (α := m → R) (β := n → R) (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)
have a : Eq (α := (m → R) → n → R) (⇑M.vecMulLinear : (a : m → R) → n → R)
  (⇑(Fintype.linearCombination R M.row) : (a : m → R) → n → R)
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R A.row
have rw : Function.Injective (β := m → R) fun (v : m → R) ↦ v ᵥ* A
Tactic: rw [← Matrix.vecMul_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f g : (m → R) →ₗ[R] n → R
⊢ (fun (i : m) (j : n) ↦
      (f + g : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j) =
    HAdd.hAdd (α := Matrix m n R)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      fun (i : m) (j : n) ↦
      (g : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j
have a : ∀ (i : m) (j : n),
  (f + g : (a : m → R) → n → R)
      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
    HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      (fun (i : m) (j : n) ↦
        (g : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
c : Rᵐᵒᵖ
f : (m → R) →ₗ[R] n → R
⊢ (fun (i : m) (j : n) ↦
      (c • f : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j) =
    HSMul.hSMul (α := Rᵐᵒᵖ) (β := Matrix m n R) ((RingHom.id Rᵐᵒᵖ : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ) c : Rᵐᵒᵖ) fun (i : m) (j : n) ↦
      (f : (a : m → R) → n → R)
        (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j
have a : ∀ (i : m) (j : n),
  (c • f : (a : m → R) → n → R)
      (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j =
    HSMul.hSMul (α := Rᵐᵒᵖ) (β := Matrix m n R) ((RingHom.id Rᵐᵒᵖ : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ) c : Rᵐᵒᵖ)
      (fun (i : m) (j : n) ↦
        (f : (a : m → R) → n → R)
          (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f : (m → R) →ₗ[R] n → R
⊢ vecMulLinear
      ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
          ((f : (a : m → R) → n → R)
              (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
            R))
        f) =
    f
have apply : ∀ (i : m),
  Eq (α := n → R)
    ((vecMulLinear
            ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                ((f : (a : m → R) → n → R)
                    (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
                  R))
              f) :
          (a : m → R) → n → R)
        ((Pi.basisFun R m : (a : m) → m → R) i : m → R) :
      n → R)
    ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) i : m → R) : n → R)
Tactic: apply (Pi.basisFun R m).ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
f : (m → R) →ₗ[R] n → R
j : m
⊢ Eq (α := n → R)
    ((vecMulLinear
            ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                ((f : (a : m → R) → n → R)
                    (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
                  R))
              f) :
          (a : m → R) → n → R)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) :
      n → R)
    ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) : n → R)
have h : ∀ (i : n),
  Eq.{u_1 + 1} (α := R)
    ((vecMulLinear
            ((fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
                ((f : (a : m → R) → n → R)
                    (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
                  R))
              f) :
          (a : m → R) → n → R)
        ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i :
      R)
    ((f : (a : m → R) → n → R) ((Pi.basisFun R m : (a : m) → m → R) j : m → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
M : Matrix m n R
⊢ (fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
        ((f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
          R))
      M.vecMulLinear =
    M
have a : ∀ (i : m) (j : n),
  (fun (f : (m → R) →ₗ[R] n → R) (i : m) (j : n) ↦
        ((f : (a : m → R) → n → R)
            (((single R (fun (x : m) ↦ R) i : R →ₗ[R] (i : m) → R) : (a : R) → (i : m) → R) 1 : (i : m) → R) j :
          R))
      M.vecMulLinear i j =
    M i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
m : Type u_3
inst_1 : Fintype m
inst_2 : DecidableEq m
⊢ Eq (α := (m → R) →ₗ[R] m → R) ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1) LinearMap.id
have h : ∀ (i x : m),
  Eq.{u_1 + 1} (α := R)
    ((((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 ∘ₗ LinearMap.single R (fun (i : m) ↦ R) i :
            R →ₗ[R] m → R) :
          (a : R) → m → R)
        1 x :
      R)
    (((LinearMap.id ∘ₗ LinearMap.single R (fun (i : m) ↦ R) i : R →ₗ[R] m → R) : (a : R) → m → R) 1 x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
          x :
        m → R) =
    x
have rw : (((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R)
    x =
  x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw :
  (((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) :
        (a : n → R) → n → R)
      x =
    x
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
          x :
        m → R) =
    x
have rw₁ : ((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw :
  (((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) :
        (a : n → R) → n → R)
      x =
    x
rw₁ : ((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
          x :
        m → R) =
    x
have rw₂ : (LinearMap.id : (a : n → R) → n → R) x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw :
  (((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) :
        (a : n → R) → n → R)
      x =
    x
rw₁ : ((toLinearMapRight' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
rw₂ : (LinearMap.id : (a : n → R) → n → R) x = x
⊢ (((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
          x :
        m → R) =
    x
have rw₃ : x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
          x :
        n → R) =
    x
have rw : (((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) : (a : m → R) → m → R)
    x =
  x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw :
  (((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) :
        (a : m → R) → m → R)
      x =
    x
⊢ (((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
          x :
        n → R) =
    x
have rw₁ : ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw :
  (((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) :
        (a : m → R) → m → R)
      x =
    x
rw₁ : ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
⊢ (((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
          x :
        n → R) =
    x
have rw₂ : (LinearMap.id : (a : m → R) → m → R) x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : Semiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst_1 : Fintype m
inst_2 : DecidableEq m
inst_3 : Fintype n
inst_4 : DecidableEq n
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw :
  (((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) :
        (a : m → R) → m → R)
      x =
    x
rw₁ : ((toLinearMapRight' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
rw₂ : (LinearMap.id : (a : m → R) → m → R) x = x
⊢ (((toLinearMapRight' : (a : Matrix n m R) → (n → R) →ₗ[R] m → R) M' : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLinearMapRight' : (a : Matrix m n R) → (m → R) →ₗ[R] n → R) M : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
          x :
        n → R) =
    x
have rw₃ : x = x
Tactic: rw [← Matrix.toLinearMapRight'_mul_apply, hMM', Matrix.toLinearMapRight'_one, id_apply]
-- 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 : Fintype m
M : Matrix m n R
⊢ Eq (α := (m → R) →ₗ[R] n → R) Mᵀ.mulVecLin M.vecMulLinear
have h : ∀ (x : m → R) (x_1 : n),
  Eq.{u_1 + 1} (α := R) ((Mᵀ.mulVecLin : (a : m → R) → n → R) x x_1 : R)
    ((M.vecMulLinear : (a : m → R) → n → R) x x_1 : R)
Tactic: ext
-- 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 : Fintype n
M : Matrix m n R
⊢ Eq (α := (n → R) →ₗ[R] m → R) Mᵀ.vecMulLinear M.mulVecLin
have h : ∀ (x : n → R) (x_1 : m),
  Eq.{u_1 + 1} (α := R) ((Mᵀ.vecMulLinear : (a : n → R) → m → R) x x_1 : R)
    ((M.mulVecLin : (a : n → R) → m → R) x x_1 : 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 : Fintype n
inst_2 : DecidableEq n
⊢ Eq (α := (n → R) →ₗ[R] n → R) (mulVecLin 1) LinearMap.id
have h : ∀ (i x : n),
  Eq.{u_1 + 1} (α := R) ((mulVecLin 1 ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : (a : R) → n → R) 1 x : R)
    (((LinearMap.id ∘ₗ LinearMap.single R (fun (i : n) ↦ R) i : R →ₗ[R] n → R) : (a : R) → n → R) 1 x : R)
Tactic: ext
-- 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 : Fintype n
M : Matrix m n R
⊢ Eq (α := Submodule R (m → R)) (LinearMap.range M.mulVecLin) (span R (Set.range M.col))
have rw : Eq (α := Submodule R (m → R)) (LinearMap.range Mᵀ.vecMulLinear) (span R (Set.range M.col))
Tactic: rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]
-- 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 : Fintype n
M : Matrix m n R
rw : Eq (α := Submodule R (m → R)) (LinearMap.range Mᵀ.vecMulLinear) (span R (Set.range M.col))
⊢ Eq (α := Submodule R (m → R)) (LinearMap.range M.mulVecLin) (span R (Set.range M.col))
have rw₁ : Eq (α := Submodule R (m → R)) (span R (Set.range Mᵀ.row)) (span R (Set.range M.col))
Tactic: rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]
-- 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 : Fintype n
M : Matrix m n R
rw : Eq (α := Submodule R (m → R)) (LinearMap.range Mᵀ.vecMulLinear) (span R (Set.range M.col))
rw₁ : Eq (α := Submodule R (m → R)) (span R (Set.range Mᵀ.row)) (span R (Set.range M.col))
⊢ Eq (α := Submodule R (m → R)) (LinearMap.range M.mulVecLin) (span R (Set.range M.col))
have rw₂ : Eq (α := Submodule R (m → R)) (span R (Set.range M.col)) (span R (Set.range M.col))
Tactic: rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]
-- 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 : Fintype n
M : Matrix m n R
⊢ (Function.Injective (β := m → R) fun (x : n → R) ↦ M *ᵥ x) ↔ LinearIndependent R M.col
have simp_rw : (Function.Injective (β := m → R) fun (x : n → R) ↦ x ᵥ* Mᵀ) ↔ LinearIndependent R M.col
Tactic: simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]
-- 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 : Fintype n
M : Matrix m n R
simp_rw : (Function.Injective (β := m → R) fun (x : n → R) ↦ x ᵥ* Mᵀ) ↔ LinearIndependent R M.col
⊢ (Function.Injective (β := m → R) fun (x : n → R) ↦ M *ᵥ x) ↔ LinearIndependent R M.col
have simp_rw₁ : LinearIndependent R Mᵀ.row ↔ LinearIndependent R M.col
Tactic: simp_rw [← M.vecMul_transpose, vecMul_injective_iff, row_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
m : Type u_4
inst_1 : Fintype m
A : Matrix m m R
inst_2 : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R A.col
have rw : Function.Injective A.mulVec
Tactic: rw [← Matrix.mulVec_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f g : (n → R) →ₗ[R] m → R
⊢ ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
      (f + g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) =
    HAdd.hAdd (α := Matrix m n R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
have a : ∀ (i : m) (j : n),
  (of : (a : m → n → R) → Matrix m n R)
      (fun (i : m) (j : n) ↦ (f + g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
    HAdd.hAdd (α := Matrix m n R) (β := Matrix m n R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (g : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
c : R
f : (n → R) →ₗ[R] m → R
⊢ ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
      (c • f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) =
    HSMul.hSMul (α := R) (β := Matrix m n R) ((RingHom.id R : (a : R) → R) c : R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
have a : ∀ (i : m) (j : n),
  (of : (a : m → n → R) → Matrix m n R)
      (fun (i : m) (j : n) ↦ (c • f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i) i j =
    HSMul.hSMul (α := R) (β := Matrix m n R) ((RingHom.id R : (a : R) → R) c : R)
      ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
        (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i)
      i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] m → R
⊢ mulVecLin
      ((fun (f : (n → R) →ₗ[R] m → R) ↦
          ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
              (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
            Matrix m n R))
        f) =
    f
have apply : ∀ (i : n),
  Eq (α := m → R)
    ((mulVecLin
            ((fun (f : (n → R) →ₗ[R] m → R) ↦
                ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                    (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                  Matrix m n R))
              f) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) i : n → R) :
      m → R)
    ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) i : n → R) : m → R)
Tactic: apply (Pi.basisFun R n).ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
f : (n → R) →ₗ[R] m → R
j : n
⊢ Eq (α := m → R)
    ((mulVecLin
            ((fun (f : (n → R) →ₗ[R] m → R) ↦
                ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                    (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                  Matrix m n R))
              f) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) j : n → R) :
      m → R)
    ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) j : n → R) : m → R)
have h : ∀ (i : m),
  Eq.{u_1 + 1} (α := R)
    ((mulVecLin
            ((fun (f : (n → R) →ₗ[R] m → R) ↦
                ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
                    (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
                  Matrix m n R))
              f) :
          (a : n → R) → m → R)
        ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i :
      R)
    ((f : (a : n → R) → m → R) ((Pi.basisFun R n : (a : n) → n → R) j : n → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix m n R
⊢ (fun (f : (n → R) →ₗ[R] m → R) ↦
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
            (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
          Matrix m n R))
      M.mulVecLin =
    M
have a : ∀ (i : m) (j : n),
  (fun (f : (n → R) →ₗ[R] m → R) ↦
        ((of : (a : m → n → R) → Matrix m n R) fun (i : m) (j : n) ↦
            (f : (a : n → R) → m → R) (Pi.single (M := fun (a : n) ↦ R) j 1) i :
          Matrix m n R))
      M.mulVecLin i j =
    M i j
Tactic: ext i j
-- 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
⊢ 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)
  ((((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)
Tactic: rw [← toLin'_apply, toLin'_toMatrix']