awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
i : ι'
j : κ'
i' : ι
j' : κ
⊢ Eq.{u_1 + 1} (α := R)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            (M ⊗[R] N →ₗ[R] M' ⊗[R] N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] M' ⊗[R] N') → Matrix (ι' × κ') (ι × κ) R)
        (map f g) (i, j) (i', j') :
      R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) f)
        ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) g) (i, j) (i', j') :
      R)
have a : HSMul.hSMul (α := R) (β := R)
    ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
      R)
    ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
      R) =
  HMul.hMul (α := R) (β := R)
    ((((bM'.repr : (a : M') → ι' →₀ R) ((f : (a : M) → M') ((bM : (a : ι) → M) i' : M)) : ι' →₀ R) : (a : ι') → R) i :
      R)
    ((((bN'.repr : (a : N') → κ' →₀ R) ((g : (a : N) → N') ((bN : (a : κ) → N) j' : N)) : κ' →₀ R) : (a : κ') → R) j :
      R)
Tactic: simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply,
    TensorProduct.map_tmul, Basis.tensorProduct_repr_tmul_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
have rw : Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
  (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
        (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
      (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
      ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
Tactic: rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
rw :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
have rw₁ : Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
  (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
        (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
      (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
      ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
Tactic: rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
rw :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₁ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
have rw₂ : Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
  (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2)
    ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A))
    ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
Tactic: rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
rw :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₁ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₂ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2)
      ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A))
      ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
have rw₃ : Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
  (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A
    ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
Tactic: rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : Finite ι'
inst_5 : Finite κ'
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup M'
inst_10 : AddCommGroup N'
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R M'
inst_14 : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
rw :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((LinearEquiv.symm (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₁ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (((toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') :
          (TensorProduct R M N →ₗ[R] TensorProduct R M' N') ≃ₗ[R] Matrix (ι' × κ') (ι × κ) R) :
        (a : TensorProduct R M N →ₗ[R] TensorProduct R M' N') → Matrix (ι' × κ') (ι × κ) R)
      (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₂ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2)
      ((toMatrix bM bM' : (a : M →ₗ[R] M') → Matrix ι' ι R) ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A))
      ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
rw₃ :
  Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A
      ((toMatrix bN bN' : (a : N →ₗ[R] N') → Matrix κ' κ R) ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B)))
⊢ Eq (α := TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (((toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') :
            Matrix (ι' × κ') (ι × κ) R ≃ₗ[R] TensorProduct R M N →ₗ[R] TensorProduct R M' N') :
          (a : Matrix (ι' × κ') (ι × κ) R) → TensorProduct R M N →ₗ[R] TensorProduct R M' N')
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
    (TensorProduct.map ((toLin bM bM' : (a : Matrix ι' ι R) → M →ₗ[R] M') A)
        ((toLin bN bN' : (a : Matrix κ' κ R) → N →ₗ[R] N') B) :
      TensorProduct R M N →ₗ[R] TensorProduct R M' N')
have rw₄ : Eq (α := Matrix (ι' × κ') (ι × κ) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
  (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B)
Tactic: rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
    toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
inst_3 : Fintype κ
inst_4 : CommRing R
inst_5 : AddCommGroup M
inst_6 : AddCommGroup N
inst_7 : Module R M
inst_8 : Module R N
bM : Basis ι R M
bN : Basis κ R N
⊢ Eq (α := Matrix (κ × ι) (ι × κ) R)
    (((toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) :
            (M ⊗[R] N →ₗ[R] N ⊗[R] M) ≃ₗ[R] Matrix (κ × ι) (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] N ⊗[R] M) → Matrix (κ × ι) (ι × κ) R)
        (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) :
      Matrix (κ × ι) (ι × κ) R)
    (submatrix 1 Prod.swap _root_.id : Matrix (κ × ι) (ι × κ) R)
have a : ∀ (i : κ) (j i' : ι) (j' : κ),
  Eq.{u_1 + 1} (α := R)
    (((toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) :
            (M ⊗[R] N →ₗ[R] N ⊗[R] M) ≃ₗ[R] Matrix (κ × ι) (ι × κ) R) :
          (a : M ⊗[R] N →ₗ[R] N ⊗[R] M) → Matrix (κ × ι) (ι × κ) R)
        (↑(TensorProduct.comm R M N) : M ⊗[R] N →ₗ[R] N ⊗[R] M) (i, j) (i', j') :
      R)
    (submatrix 1 Prod.swap _root_.id (i, j) (i', j') : R)
Tactic: ext ⟨i, j⟩ ⟨i', j'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Matrix (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
ι : Type u_7
κ : Type u_8
τ : Type u_9
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : DecidableEq τ
inst_3 : Fintype ι
inst_4 : Fintype κ
inst_5 : Fintype τ
inst_6 : CommRing R
inst_7 : AddCommGroup M
inst_8 : AddCommGroup N
inst_9 : AddCommGroup P
inst_10 : Module R M
inst_11 : Module R N
inst_12 : Module R P
bM : Basis ι R M
bN : Basis κ R N
bP : Basis τ R P
⊢ Eq (α := Matrix (ι × κ × τ) ((ι × κ) × τ) R)
    (((toMatrix (Basis.tensorProduct (bM.tensorProduct bN) bP) (bM.tensorProduct (bN.tensorProduct bP)) :
            (M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) ≃ₗ[R] Matrix (ι × κ × τ) ((ι × κ) × τ) R) :
          (a : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) → Matrix (ι × κ × τ) ((ι × κ) × τ) R)
        (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
      Matrix (ι × κ × τ) ((ι × κ) × τ) R)
    (submatrix (n := ι × κ × τ) 1 _root_.id (⇑(Equiv.prodAssoc ι κ τ) : (a : (ι × κ) × τ) → ι × κ × τ) :
      Matrix (ι × κ × τ) ((ι × κ) × τ) R)
have a : ∀ (i : ι) (j : κ) (k k' : τ) (i' : ι) (j' : κ),
  Eq.{u_1 + 1} (α := R)
    (((toMatrix (Basis.tensorProduct (bM.tensorProduct bN) bP) (bM.tensorProduct (bN.tensorProduct bP)) :
            (M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) ≃ₗ[R] Matrix (ι × κ × τ) ((ι × κ) × τ) R) :
          (a : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) → Matrix (ι × κ × τ) ((ι × κ) × τ) R)
        (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) (i, j, k) ((i', j'), k') :
      R)
    (submatrix (n := ι × κ × τ) 1 _root_.id (⇑(Equiv.prodAssoc ι κ τ) : (a : (ι × κ) × τ) → ι × κ × τ) (i, j, k)
        ((i', j'), k') :
      R)
Tactic: ext ⟨i, j, k⟩ ⟨⟨i', j'⟩, k'⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
⊢ Eq (α := A ⊗[R] B →ₐ[S] A ⊗[R] B)
    ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
        (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
          (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯ :
            TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ)
          ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
              (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯) :
            (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)) :
      A ⊗[R] B →ₐ[S] A ⊗[R] B)
    ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
        (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ) :
      A ⊗[R] B →ₐ[S] A ⊗[R] B)
have ha : ∀ (x : A),
  Eq (α := A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
              (AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
                (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) sorry sorry :
                  TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ)
                ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                    (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) sorry sorry) :
                  (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)))
            includeLeft :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)
    ((AlgHom.comp (B := A ⊗[R] B)
            ((Equiv.symm AlgHom.op : (a : (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) → A ⊗[R] B →ₐ[S] A ⊗[R] B)
              (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))
            includeLeft :
          (a : A) → A ⊗[R] B)
        x :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
e₁ : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] A ⊗[R] B) ≪≫ₗ
    (opLinearEquiv S : A ⊗[R] B ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ)
e₂ : A ⊗[R] B ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ :=
  (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R) :
      A ⊗[R] B ≃ₗ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) ≪≫ₗ
    (opLinearEquiv S : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₗ[S] (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)ᵐᵒᵖ)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (AlgHom.comp (B := (A ⊗[R] B)ᵐᵒᵖ)
        ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
          (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) ⋯ ⋯))
        (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) ⋯ ⋯) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (AlgHom.id S (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
have ha : ∀ (x : Aᵐᵒᵖ),
  Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    ((AlgHom.comp (B := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
            (AlgHom.comp (B := (A ⊗[R] B)ᵐᵒᵖ)
                ((AlgHom.opComm : (a : A ⊗[R] B →ₐ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ →ₐ[S] Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
                  (algHomOfLinearMapTensorProduct (↑e₂ : A ⊗[R] B →ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) sorry sorry))
                (algHomOfLinearMapTensorProduct (↑e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ →ₗ[S] (A ⊗[R] B)ᵐᵒᵖ) sorry sorry) :
              TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
            (includeLeft : Aᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (((AlgHom.comp (AlgHom.id S (TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)) includeLeft :
            Aᵐᵒᵖ →ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : Aᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        x :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
Tactic: ext