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
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)
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)
⊢ 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 ∘ₗ 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
k : Type u_2
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 m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R) x :
        n → R) =
    x
have rw : (((toLin' : (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.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw : (((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) (M * M') : (m → R) →ₗ[R] m → R) : (a : m → R) → m → R) x = x
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R) x :
        n → R) =
    x
have rw₁ : ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
Tactic: rw [← Matrix.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw : (((toLin' : (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₁ : ((toLin' : (a : Matrix m m R) → (m → R) →ₗ[R] m → R) 1 : (a : m → R) → m → R) x = x
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLin' : (a : Matrix n m 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.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : m → R
rw : (((toLin' : (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₁ : ((toLin' : (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
⊢ (((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R)
      ((((toLin' : (a : Matrix n m 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.toLin'_mul_apply, hMM', Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) =
    x
have rw : (((toLin' : (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.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw : (((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (M' * M) : (n → R) →ₗ[R] n → R) : (a : n → R) → n → R) x = x
⊢ (((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLin' : (a : Matrix m n R) → (n → R) →ₗ[R] m → R) M : (n → R) →ₗ[R] m → R) : (a : n → R) → m → R) x :
        m → R) =
    x
have rw₁ : ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
Tactic: rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw : (((toLin' : (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₁ : ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) 1 : (a : n → R) → n → R) x = x
⊢ (((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLin' : (a : Matrix m n 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.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]
-- 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
inst_3 : Fintype m
inst_4 : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
rw : (((toLin' : (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₁ : ((toLin' : (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
⊢ (((toLin' : (a : Matrix n m R) → (m → R) →ₗ[R] n → R) M' : (m → R) →ₗ[R] n → R) : (a : m → R) → n → R)
      ((((toLin' : (a : Matrix m n 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.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f
have rw : (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) (((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f
Tactic: rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
rw : (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) (((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f
⊢ (toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f) = f
have rw₁ : f = f
Tactic: rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
⊢ (toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M
have rw : ((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M
Tactic: rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
rw : ((toLin v₁ v₂).symm : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M
⊢ (toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M) = M
have rw₁ : M = M
Tactic: rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_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₁
⊢ Eq (α := Matrix n n R) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → 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 v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) id i j : R) (1 i j : R)
Tactic: ext i j
-- 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₁
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id
have rw : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
  ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
    M₁ →ₗ[R] M₁)
  (LinearMap.id : M₁ →ₗ[R] M₁)
Tactic: rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]
-- 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₁
rw :
  Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁)
    ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁)
        ((toMatrix v₁ v₁ : (a : M₁ →ₗ[R] M₁) → Matrix n n R) LinearMap.id) :
      M₁ →ₗ[R] M₁)
    (LinearMap.id : M₁ →ₗ[R] M₁)
⊢ Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) ((toLin v₁ v₁ : (a : Matrix n n R) → M₁ →ₗ[R] M₁) 1) LinearMap.id
have rw₁ : Eq.{u_5 + 1} (α := M₁ →ₗ[R] M₁) LinearMap.id LinearMap.id
Tactic: rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_8 : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix v₁.reindexRange v₂.reindexRange :
          (a : M₁ →ₗ[R] M₂) →
            Matrix (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₂) ↦
          Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
          ((v₂ : (a : m) → M₂) k) ⋯)
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) i) ⋯) :
      R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f k i : R)
have simp_rw : Eq.{u_1 + 1} (α := R)
  ((((v₂.reindexRange.repr : (a : M₂) → (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) →₀ R)
            ((f : (a : M₁) → M₂)
              ((v₁.reindexRange : (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → M₁)
                  (Subtype.mk (p := fun (x : M₁) ↦
                      Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
                      ((v₁ : (a : n) → M₁) i) sorry :
                    { x : M₁ //
                      Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
                M₁)) :
          Finsupp.{u_6, u_1} (↑(Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) : Type u_6) R) :
        (a : (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6)) → R)
      (Subtype.mk (p := fun (x : M₂) ↦
          Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
          ((v₂ : (a : m) → M₂) k) sorry :
        { x : M₂ // Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x }) :
    R)
  ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) : m →₀ R) : (a : m) → R) k : R)
Tactic: simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst_8 : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
simp_rw :
  Eq.{u_1 + 1} (α := R)
    ((((v₂.reindexRange.repr : (a : M₂) → (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) →₀ R)
              ((f : (a : M₁) → M₂)
                ((v₁.reindexRange : (a : (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5)) → M₁)
                    (Subtype.mk (p := fun (x : M₁) ↦
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
                        ((v₁ : (a : n) → M₁) i) ⋯ :
                      { x : M₁ //
                        Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x }) :
                  M₁)) :
            Finsupp.{u_6, u_1} (↑(Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) : Type u_6) R) :
          (a : (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6)) → R)
        (Subtype.mk (p := fun (x : M₂) ↦
            Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
            ((v₂ : (a : m) → M₂) k) ⋯ :
          { x : M₂ // Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x }) :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) : m →₀ R) : (a : m) → R) k : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((toMatrix v₁.reindexRange v₂.reindexRange :
          (a : M₁ →ₗ[R] M₂) →
            Matrix (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) (↑(Set.range (⇑v₁ : (a : n) → M₁)) : Type u_5) R)
        f
        (Subtype.mk (p := fun (x : M₂) ↦
          Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
          ((v₂ : (a : m) → M₂) k) ⋯)
        (Subtype.mk (p := fun (x : M₁) ↦
          Membership.mem (γ := Set M₁) (Set.range.{u_5, u_4 + 1} (ι := n) (⇑v₁ : (a : n) → M₁)) x)
          ((v₁ : (a : n) → M₁) i) ⋯) :
      R)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f k i : R)
have simp_rw₁ : Eq.{u_1 + 1} (α := R)
  ((((v₂.reindexRange.repr : (a : M₂) → (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6) →₀ R)
            ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) :
          Finsupp.{u_6, u_1} (↑(Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) : Type u_6) R) :
        (a : (↑(Set.range (⇑v₂ : (a : m) → M₂)) : Type u_6)) → R)
      (Subtype.mk (p := fun (x : M₂) ↦
          Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x)
          ((v₂ : (a : m) → M₂) k) sorry :
        { x : M₂ // Membership.mem (γ := Set M₂) (Set.range.{u_6, u_3 + 1} (ι := m) (⇑v₂ : (a : m) → M₂)) x }) :
    R)
  ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) ((v₁ : (a : n) → M₁) i : M₁)) : m →₀ R) : (a : m) → R) k : R)
Tactic: simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
⊢ Eq (α := m → R)
    (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
      (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R))
    (⇑((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R)
have h : ∀ (i : m),
  Eq.{u_1 + 1} (α := R)
    (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
        (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
Tactic: ext i
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ Eq.{u_1 + 1} (α := R)
    (mulVec.{u_1, u_3, u_4} (n := n) ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) f)
        (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
have h : Eq.{u_1 + 1} (α := R)
  ((((v₂.repr : (a : M₂) → m →₀ R)
            ((f : (a : M₁) → M₂)
              ((v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) :
                M₁)) :
          m →₀ R) :
        (a : m) → R)
      i :
    R)
  ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
Tactic: rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
    LinearEquiv.arrowCongr_apply, v₂.equivFun_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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ Eq.{u_1 + 1} (α := R)
    ((((v₂.repr : (a : M₂) → m →₀ R)
              ((f : (a : M₁) → M₂)
                ((v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) :
                  M₁)) :
            m →₀ R) :
          (a : m) → R)
        i :
      R)
    ((((v₂.repr : (a : M₂) → m →₀ R) ((f : (a : M₁) → M₂) x) : m →₀ R) : (a : m) → R) i : R)
have h : (v₁.equivFun.symm : (a : n → R) → M₁) (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) = x
Tactic: congr
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
x : M₁
⊢ (⇑((v₂.repr : (a : M₂) → m →₀ R)
            ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x) :
          m →₀ R) :
      (a : m) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
have rw : mulVec.{u_1, u_3, u_4} (n := n)
    ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M))
    (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) =
  M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
Tactic: rw [← toMatrix_mulVec_repr v₁, toMatrix_toLin]
-- 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 : Finite m
inst_3 : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₁
inst_7 : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
x : M₁
rw :
  mulVec.{u_1, u_3, u_4} (n := n)
      ((toMatrix v₁ v₂ : (a : M₁ →ₗ[R] M₂) → Matrix m n R) ((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M))
      (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
⊢ (⇑((v₂.repr : (a : M₂) → m →₀ R)
            ((((toLin v₁ v₂ : (a : Matrix m n R) → M₁ →ₗ[R] M₂) M : M₁ →ₗ[R] M₂) : (a : M₁) → M₂) x) :
          m →₀ R) :
      (a : m) → R) =
    M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
have rw₁ : M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R) =
  M *ᵥ (⇑((v₁.repr : (a : M₁) → n →₀ R) x : n →₀ R) : (a : n) → R)
Tactic: rw [← toMatrix_mulVec_repr v₁, toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
R : Type u_1
inst : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype l
inst_6 : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ Eq (α := Matrix l l R)
    ((toMatrix b' b : (a : M₂ →ₗ[R] M₁) → Matrix l l R) (↑(b'.equiv b (Equiv.refl l)) : M₂ →ₗ[R] M₁) : Matrix l l R)
    (1 : Matrix l l R)
have a : ∀ (i j : l),
  Eq.{u_1 + 1} (α := R)
    ((toMatrix b' b : (a : M₂ →ₗ[R] M₁) → Matrix l l R) (↑(b'.equiv b (Equiv.refl l)) : M₂ →ₗ[R] M₁) i j : R)
    (1 i j : R)
Tactic: ext i j