awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
R₂ : Type u_7
M₂ : Type u_8
inst : CommRing R₂
inst_1 : AddCommGroup M₂
inst_2 : Module R₂ M₂
inst_3 : Fintype ι
inst_4 : DecidableEq ι
S : Type u_9
inst_5 : CommRing S
inst_6 : Nontrivial S
inst_7 : Algebra R₂ S
inst_8 : Module S M₂
inst_9 : IsScalarTower R₂ S M₂
inst_10 : IsDomain R₂
inst_11 : IsTorsionFree R₂ S
b : Basis ι S M₂
v : ι → ↥(span R₂ (Set.range.{u_8, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M₂)))
i j : ι
a :
  (toMatrix (restrictScalars R₂ b) v).map (⇑(algebraMap R₂ S) : (a : R₂) → S) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₁ :
  (algebraMap R₂ S : (a : R₂) → S) (toMatrix (restrictScalars R₂ b) v i j) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₂ :
  (algebraMap R₂ S : (a : R₂) → S)
      ((((repr (restrictScalars R₂ b) : (a : ↥(span R₂ (Set.range (⇑b : (a : ι) → M₂)))) → ι →₀ R₂) (v j) : ι →₀ R₂) :
            (a : ι) → R₂)
          i :
        R₂) =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
a₃ :
  (((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i = b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
⊢ (RingHom.mapMatrix (algebraMap R₂ S) : (a : Matrix ι ι R₂) → Matrix ι ι S) (toMatrix (restrictScalars R₂ b) v) i j =
    b.toMatrix (fun (i : ι) ↦ (↑(v i) : M₂)) i j
have a₄ : Eq.{u_9 + 1} (α := S) ((((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i : S)
  ((((b.repr : (a : M₂) → ι →₀ S) (↑(v j) : M₂) : ι →₀ S) : (a : ι) → S) i : S)
Tactic: rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply,
    Basis.restrictScalars_repr_apply, Basis.toMatrix_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst_3 : Fintype ι
inst_4 : DecidableEq ι
inst_5 : Finite ι'
⊢ Eq (α := Matrix ι' ι R) ((toMatrix b b' : (a : M →ₗ[R] M) → Matrix ι' ι R) id : Matrix ι' ι R)
    (b'.toMatrix (⇑b : (a : ι) → M) : Matrix ι' ι R)
have a : ∀ (i : ι') (j : ι), (toMatrix b b' : (a : M →ₗ[R] M) → Matrix ι' ι R) id i j = b'.toMatrix (⇑b : (a : ι) → M) i j
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have haveI : ∀ (this : DecidableEq κ'),
  Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
Tactic: haveI := Classical.decEq κ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have rw : (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
    (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
      ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
  f
Tactic: rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
rw :
  (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
    f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have rw₁ : (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ
    (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) =
  f
Tactic: rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
rw :
  (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
    f
rw₁ :
  (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ
      (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) =
    f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have rw₂ : (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ f = f
Tactic: rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
rw :
  (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
    f
rw₁ :
  (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ
      (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) =
    f
rw₂ : (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ f = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have rw₃ : LinearMap.id ∘ₗ f = f
Tactic: rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype κ'
inst_8 : DecidableEq ι'
this : DecidableEq κ'
rw :
  (toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) =
    f
rw₁ :
  (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ
      (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) =
    f
rw₂ : (toLin c' c : (a : Matrix κ κ' R) → N →ₗ[R] N) (c.toMatrix (⇑c' : (a : κ') → N)) ∘ₗ f = f
rw₃ : LinearMap.id ∘ₗ f = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R)) :
      M →ₗ[R] N)
    ((toLin b' c : (a : Matrix κ ι' R) → M →ₗ[R] N) ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f) : M →ₗ[R] N)
have rw₄ : f = f
Tactic: rw [toLin_toMatrix, toLin_mul b' c' c, toLin_toMatrix, c.toLin_toMatrix, LinearMap.id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Fintype κ
inst_7 : Finite ι
inst_8 : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
⊢ HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
have this : HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' κ R) (b₁.toMatrix (⇑b₂ : (a : ι') → M))
    ((toMatrix b₃ b₂ : (a : N →ₗ[R] M) → Matrix ι' κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A) :
      Matrix ι' κ R) =
  (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
Tactic: have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Fintype κ
inst_7 : Finite ι
inst_8 : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this :
  HMul.hMul (α := Matrix ι ι' R) (β := Matrix ι' κ R) (b₁.toMatrix (⇑b₂ : (a : ι') → M))
      ((toMatrix b₃ b₂ : (a : N →ₗ[R] M) → Matrix ι' κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A) :
        Matrix ι' κ R) =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
⊢ HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
have rwa : ∀
  (this :
    HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
      (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)),
  HMul.hMul (α := Matrix ι ι' R) (b₁.toMatrix (⇑b₂ : (a : ι') → M)) A =
    (toMatrix b₃ b₁ : (a : N →ₗ[R] M) → Matrix ι κ R) ((toLin b₃ b₂ : (a : Matrix ι' κ R) → N →ₗ[R] M) A)
Tactic: rwa [LinearMap.toMatrix_toLin] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)
have rw : (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
    (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
      ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
  f
Tactic: rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
rw :
  (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
    f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)
have rw₁ : (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) ∘ₗ
    (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) =
  f
Tactic: rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
rw :
  (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
    f
rw₁ :
  (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) ∘ₗ
      (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) =
    f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)
have rw₂ : f ∘ₗ (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) = f
Tactic: rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
rw :
  (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
    f
rw₁ :
  (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) ∘ₗ
      (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) =
    f
rw₂ : f ∘ₗ (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)
have rw₃ : f ∘ₗ LinearMap.id = f
Tactic: rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Fintype ι
inst_7 : Finite κ'
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
rw :
  (toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
      (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) =
    f
rw₁ :
  (toLin b' c' : (a : Matrix κ' ι' R) → M →ₗ[R] N) ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f) ∘ₗ
      (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) =
    f
rw₂ : f ∘ₗ (toLin b b' : (a : Matrix ι' ι R) → M →ₗ[R] M) (b'.toMatrix (⇑b : (a : ι) → M)) = f
rw₃ : f ∘ₗ LinearMap.id = f
⊢ Eq (α := M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N)
        (HMul.hMul (α := Matrix κ' ι' R) (β := Matrix ι' ι R)
          ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R) (b'.toMatrix (⇑b : (a : ι) → M))) :
      M →ₗ[R] N)
    ((toLin b c' : (a : Matrix κ' ι R) → M →ₗ[R] N) ((toMatrix b c' : (a : M →ₗ[R] N) → Matrix κ' ι R) f) : M →ₗ[R] N)
have rw₄ : f = f
Tactic: rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, LinearMap.comp_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : Fintype κ'
inst_9 : DecidableEq ι
inst_10 : DecidableEq ι'
⊢ HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
have intro : ∀ (val : Fintype κ),
  HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
Tactic: cases nonempty_fintype κ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : Fintype κ'
inst_9 : DecidableEq ι
inst_10 : DecidableEq ι'
val : Fintype κ
⊢ HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
have intro : HMul.hMul (α := Matrix κ ι' R) (β := Matrix ι' ι R)
    ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f : Matrix κ ι' R) (b'.toMatrix (⇑b : (a : ι) → M)) =
  (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
Tactic: rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : Fintype κ'
inst_9 : DecidableEq ι
inst_10 : DecidableEq ι'
val : Fintype κ
intro :
  HMul.hMul (α := Matrix κ ι' R) (β := Matrix ι' ι R)
      ((toMatrix b' c : (a : M →ₗ[R] N) → Matrix κ ι' R) f : Matrix κ ι' R) (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
⊢ HMul.hMul (β := Matrix ι' ι R)
      (HMul.hMul (α := Matrix κ κ' R) (β := Matrix κ' ι' R) (c.toMatrix (⇑c' : (a : κ') → N))
        ((toMatrix b' c' : (a : M →ₗ[R] N) → Matrix κ' ι' R) f : Matrix κ' ι' R))
      (b'.toMatrix (⇑b : (a : ι) → M)) =
    (toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f
have intro₁ : Eq (α := Matrix κ ι R) ((toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f : Matrix κ ι R)
  ((toMatrix b c : (a : M →ₗ[R] N) → Matrix κ ι R) f : Matrix κ ι R)
Tactic: rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_9
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι'
inst_6 : Finite κ
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
⊢ HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
have intro : ∀ (val : Fintype κ),
  HMul.hMul (β := Matrix ι ι' R) A (b₁.toMatrix (⇑b₂ : (a : ι') → M)) =
    (toMatrix b₂ b₃ : (a : M →ₗ[R] N) → Matrix κ ι' R) ((toLin b₁ b₃ : (a : Matrix κ ι R) → M →ₗ[R] N) A)
Tactic: cases nonempty_fintype κ