awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : (Matrix n n R)[X]
r : R
hC :
  Eq (α := Matrix n n R →ₐ[R] Matrix n n R)
    (AlgHom.comp
      (AlgHom.comp (AlgHom.mapMatrix (aeval r))
        (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
      CAlgHom)
    (AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom)
hX :
  Eq (α := Matrix n n R)
    ((AlgHom.comp (AlgHom.mapMatrix (aeval r))
            (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]) :
          (a : (Matrix n n R)[X]) → Matrix n n R)
        X :
      Matrix n n R)
    (((eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯ :
            (Matrix n n R)[X] →ₐ[R] Matrix n n R) :
          (a : (Matrix n n R)[X]) → Matrix n n R)
        X :
      Matrix n n R)
⊢ Eq (α := (Matrix n n R)[X] →ₐ[R] Matrix n n R)
    (AlgHom.comp (AlgHom.mapMatrix (aeval r)) (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
    (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯)

Tactic:
ext : 1
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : (Matrix n n R)[X]
r : R
hC :
  ∀ (M : Matrix n n R),
    Eq (α := Matrix n n R)
      ((AlgHom.comp
              (AlgHom.comp (AlgHom.mapMatrix (aeval r))
                (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
              CAlgHom :
            (a : Matrix n n R) → Matrix n n R)
          M :
        Matrix n n R)
      (((AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom :
              Matrix n n R →ₐ[R] Matrix n n R) :
            (a : Matrix n n R) → Matrix n n R)
          M :
        Matrix n n R)
⊢ Eq (α := Matrix n n R →ₐ[R] Matrix n n R)
    (AlgHom.comp
      (AlgHom.comp (AlgHom.mapMatrix (aeval r))
        (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
      CAlgHom)
    (AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom)

Tactic:
ext M : 1
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M_1 : (Matrix n n R)[X]
r : R
M : Matrix n n R
⊢ Eq (α := Matrix n n R)
    ((AlgHom.comp
            (AlgHom.comp (AlgHom.mapMatrix (aeval r))
              (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]))
            CAlgHom :
          (a : Matrix n n R) → Matrix n n R)
        M :
      Matrix n n R)
    (((AlgHom.comp (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯) CAlgHom :
            Matrix n n R →ₐ[R] Matrix n n R) :
          (a : Matrix n n R) → Matrix n n R)
        M :
      Matrix n n R)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ Eq (α := Matrix n n R)
    ((AlgHom.comp (AlgHom.mapMatrix (aeval r))
            (↑(AlgEquiv.symm matPolyEquiv) : (Matrix n n R)[X] →ₐ[R] Matrix n n R[X]) :
          (a : (Matrix n n R)[X]) → Matrix n n R)
        X :
      Matrix n n R)
    (((eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n : (a : R) → Matrix n n R) r) ⋯ :
            (Matrix n n R)[X] →ₐ[R] Matrix n n R) :
          (a : (Matrix n n R)[X]) → Matrix n n R)
        X :
      Matrix n n R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix.{w, w, u_1} n n R[X]
r : R
⊢ eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M) =
    M.map (eval r)

Tactic:
simpa only [AlgEquiv.symm_apply_apply] using (matPolyEquiv_symm_map_eval (matPolyEquiv M) r).symm

Premises used: matPolyEquiv, AlgEquiv.symm_apply_apply, matPolyEquiv_symm_map_eval, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix.{w, w, u_1} n n R[X]
r : R
i j : n
rw : M.map (eval r) i j = eval r (M i j)
rw₁ rw₂ : eval r (M i j) = eval r (M i j)
⊢ eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M) i j =
    eval r (M i j)

Tactic:
rw [matPolyEquiv_eval_eq_map, map_apply]

Premises used: Matrix.map_apply, matPolyEquiv_eval_eq_map
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Matrix.{w, w, u_1} n n R[X]
i j : n
k : ℕ
contrapose :
  k ∉ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) → k ∉ (m i j).support
⊢ k ∈ (m i j).support → k ∈ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m)

Tactic:
contrapose
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Matrix.{w, w, u_1} n n R[X]
i j : n
k : ℕ
simp :
  Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0 →
    (m i j).coeff k = 0
⊢ k ∉ support (R := Matrix n n R) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) → k ∉ (m i j).support

Tactic:
simp only [notMem_support_iff]

Premises used: Polynomial.notMem_support_iff
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Matrix.{w, w, u_1} n n R[X]
i j : n
k : ℕ
hk : Eq (α := Matrix n n R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k) 0
rw : Eq.{u_1 + 1} (α := R) (coeff ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) m) k i j) 0
rw₁ : Eq.{u_1 + 1} (α := R) (0 i j) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (m i j).coeff k = 0

Tactic:
rw [← matPolyEquiv_coeff_apply, hk, zero_apply]

Premises used: Matrix.zero_apply, matPolyEquiv_coeff_apply
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
M : Matrix.{w, w, u_3} n n R[X]
r : R
rw :
  Eq.{u_3 + 1} (α := R)
    (det.{u_3, w} (n := n)
      ((RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r) : (a : Matrix n n R[X]) → Matrix n n R) M))
    (det.{u_3, w} (n := n)
      (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M)))
⊢ eval r M.det =
    det.{u_3, w} (n := n)
      (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M))

Tactic:
rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]

Premises used: Polynomial.eval, RingHom.map_det, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
M : Matrix.{w, w, u_3} n n R[X]
r : R
⊢ Eq.{u_3 + 1} (α := R)
    (det.{u_3, w} (n := n)
      ((RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r) : (a : Matrix n n R[X]) → Matrix n n R) M))
    (det.{u_3, w} (n := n)
      (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M)))

Tactic:
congr_arg det <| ext fun _ _ ↦ matPolyEquiv_eval _ _ _ _ |>.symm

Premises used: congr_arg, matPolyEquiv_eval, Eq.symm, Matrix.ext, Matrix.det
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
M : Matrix.{w, w, u_3} n n R[X]
r : R
⊢ Eq.{u_3 + 1} (α := R)
    (det.{u_3, w} (n := n)
      ((RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r) : (a : Matrix n n R[X]) → Matrix n n R) M))
    (det.{u_3, w} (n := n)
      (eval ((scalar n : (a : R) → Matrix n n R) r) ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) M)))

Tactic:
exact congr_arg det <| ext fun _ _ ↦ matPolyEquiv_eval _ _ _ _ |>.symm

Premises used: congr_arg, matPolyEquiv_eval, Eq.symm, Matrix.ext, Matrix.det
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
A : Matrix.{w, w, u_3} n n R[X]
M : Matrix n n R
simp :
  (eval 0 ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) A) +
        eval 0
          (HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X])
            ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
                ((algebraMap R[X] (Matrix.{w, w, u_3} n n R[X]) : (a : R[X]) → Matrix n n R[X]) X) :
              (Matrix n n R)[X])
            ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (M.map (⇑C : (a : R) → R[X])) :
              (Matrix n n R)[X]))).det =
    det.{u_3, w} (n := n) (eval 0 ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) A))
⊢ eval 0 (A + HSMul.hSMul (α := R[X]) (β := Matrix.{w, w, u_3} n n R[X]) X (M.map (⇑C : (a : R) → R[X]))).det =
    eval 0 A.det

Tactic:
simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, map_mul]

Premises used: map_zero, map_add, map_mul, eval_det, Polynomial.eval_add, Algebra.smul_def
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
n : Type w
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_3
inst_2 : CommRing R
A : Matrix.{w, w, u_3} n n R[X]
M : Matrix n n R
⊢ (eval 0 ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) A) +
        eval 0
          (HMul.hMul (α := (Matrix n n R)[X]) (β := (Matrix n n R)[X])
            ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
                ((algebraMap R[X] (Matrix.{w, w, u_3} n n R[X]) : (a : R[X]) → Matrix n n R[X]) X) :
              (Matrix n n R)[X])
            ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) (M.map (⇑C : (a : R) → R[X])) :
              (Matrix n n R)[X]))).det =
    det.{u_3, w} (n := n) (eval 0 ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X]) A))

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, matPolyEquiv_smul_one, map_X, X_mul, eval_mul_X,
    mul_zero, add_zero]

Premises used: Polynomial.map_X, MulZeroClass.mul_zero, Algebra.algebraMap_eq_smul_one, Polynomial.X_mul, Polynomial.eval_mul_X, add_zero, matPolyEquiv_smul_one
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommSemiring S
f : S →+* Matrix n n R
h₁ :
  ∀ (x : S) (i j : n),
    Eq.{u_1 + 1} (α := R)
      (((RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix).comp C : (a : S) → Matrix n n R) x i j : R)
      (((f.comp (evalRingHom 0)).comp C : (a : S) → Matrix n n R) x i j : R)
h₂ :
  ∀ (i j : n),
    Eq.{u_1 + 1} (α := R)
      ((RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix : (a : S[X]) → Matrix n n R) X i j : R)
      ((f.comp (evalRingHom 0) : (a : S[X]) → Matrix n n R) X i j : R)
⊢ RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix = f.comp (evalRingHom 0)

Tactic:
ext
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommSemiring S
f : S →+* Matrix n n R
x : S
i j : n
⊢ Eq.{u_1 + 1} (α := R)
    (((RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix).comp C : (a : S) → Matrix n n R) x i j : R)
    (((f.comp (evalRingHom 0)).comp C : (a : S) → Matrix n n R) x i j : R)

Tactic:
simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

Premises used: apply_ite, RingHom.polyToMatrix, AlgEquiv.symm_toRingEquiv, Matrix.diagonal
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
S : Type u_3
inst_3 : CommSemiring S
f : S →+* Matrix n n R
i j : n
⊢ Eq.{u_1 + 1} (α := R)
    ((RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix : (a : S[X]) → Matrix n n R) X i j : R)
    ((f.comp (evalRingHom 0) : (a : S[X]) → Matrix n n R) X i j : R)

Tactic:
simp [RingHom.polyToMatrix, -AlgEquiv.symm_toRingEquiv, diagonal, apply_ite]

Premises used: apply_ite, RingHom.polyToMatrix, AlgEquiv.symm_toRingEquiv, Matrix.diagonal
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type u_4
inst_3 : Fintype m
inst_4 : DecidableEq m
a :
  ∀ (x : Matrix m m (Matrix.{w, w, u_1} n n R[X])) (i j : m × n),
    Eq.{u_1 + 1} (α := R)
      ((RingHom.comp (RingHom.mapMatrix (evalRingHom 0))
              (↑(compRingEquiv m n R[X]) : Matrix m m (Matrix n n R[X]) →+* Matrix (m × n) (m × n) R[X]) :
            (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R)
          x i j :
        R)
      ((RingHom.comp (RingEquiv.toRingHom (compRingEquiv m n R))
              (RingHom.mapMatrix (RingHom.mapMatrix (evalRingHom 0))) :
            (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R)
          x i j :
        R)
⊢ Eq (α := Matrix m m (Matrix.{w, w, u_1} n n R[X]) →+* Matrix (m × n) (m × n) R)
    (RingHom.comp (RingHom.mapMatrix (evalRingHom 0))
      (↑(compRingEquiv m n R[X]) : Matrix m m (Matrix n n R[X]) →+* Matrix (m × n) (m × n) R[X]))
    (RingHom.comp (RingEquiv.toRingHom (compRingEquiv m n R)) (RingHom.mapMatrix (RingHom.mapMatrix (evalRingHom 0))))

Tactic:
ext
-- Module: Mathlib.RingTheory.MatrixPolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type u_4
inst_3 : Fintype m
inst_4 : DecidableEq m
x : Matrix m m (Matrix.{w, w, u_1} n n R[X])
i j : m × n
⊢ Eq.{u_1 + 1} (α := R)
    ((RingHom.comp (RingHom.mapMatrix (evalRingHom 0))
            (↑(compRingEquiv m n R[X]) : Matrix m m (Matrix n n R[X]) →+* Matrix (m × n) (m × n) R[X]) :
          (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R)
        x i j :
      R)
    ((RingHom.comp (RingEquiv.toRingHom (compRingEquiv m n R)) (RingHom.mapMatrix (RingHom.mapMatrix (evalRingHom 0))) :
          (a : Matrix m m (Matrix n n R[X])) → Matrix (m × n) (m × n) R)
        x i j :
      R)

Tactic:
simp
-- Module: Mathlib.RingTheory.Morita.Basic
Goal:
R : Type u₀
inst : CommSemiring R
A : Type u₁
inst_1 : Ring A
inst_2 : Algebra R A
B : Type u₂
inst_3 : Ring B
inst_4 : Algebra R B
e : MoritaEquivalence R A B
⊢ e.eqv.functor.Additive

Tactic:
e.eqv.functor.additive_of_preserves_binary_products

Premises used: MoritaEquivalence.eqv, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.additive_of_preserves_binary_products
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
dsimp : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) = r • HSMul.hSMul (α := Matrix ι ι R) (single i i 1) x
⊢ ZeroHom.toFun (↑(DistribSMul.toAddMonoidHom (M := Matrix ι ι R) M (single i i 1)) : ZeroHom M M) (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (ZeroHom.toFun (↑(DistribSMul.toAddMonoidHom (M := Matrix ι ι R) M (single i i 1)) : ZeroHom M M) x)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
a :
  ∀ (i_1 j : ι),
    HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1) i_1 j =
      HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R) (single i i 1) (diagonal fun (x : ι) ↦ r) i_1 j
⊢ Commute (S := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1)

Tactic:
ext
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
i_1 j : ι
⊢ HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1) i_1 j =
    HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R) (single i i 1) (diagonal fun (x : ι) ↦ r) i_1 j

Tactic:
simp [Matrix.single]

Premises used: Matrix.single
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
⊢ Commute (S := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1)

Tactic:
have : Commute (diagonal fun x : ι ↦ r) (single i i 1) := by
          ext; simp [Matrix.single]
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (S := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1)
rw :
  HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) =
    HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (HSMul.hSMul (β := Matrix ι ι R) r 1 • x)
⊢ HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) = r • HSMul.hSMul (α := Matrix ι ι R) (single i i 1) x

Tactic:
rw [← smul_assoc r, smul_eq_diagonal_mul, this.eq, mul_smul, ← smul_one_eq_diagonal]

Premises used: smul_assoc, Matrix.smul_one_eq_diagonal, Commute.eq, Matrix.smul_eq_diagonal_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (S := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1)
nth_rw :
  HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • HSMul.hSMul (α := Matrix ι ι R) 1 x) =
    HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (HSMul.hSMul (β := Matrix ι ι R) r 1 • x)
⊢ HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) =
    HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (HSMul.hSMul (β := Matrix ι ι R) r 1 • x)

Tactic:
nth_rw 1 [← one_smul (Matrix ι ι R) x]

Premises used: Matrix, one_smul
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
this : Commute (S := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) (single i i 1)
rw rw₁ :
  HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • HSMul.hSMul (α := Matrix ι ι R) 1 x) =
    HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • HSMul.hSMul (α := Matrix ι ι R) 1 x)
⊢ HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • HSMul.hSMul (α := Matrix ι ι R) 1 x) =
    HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (HSMul.hSMul (β := Matrix ι ι R) r 1 • x)

Tactic:
rw [smul_assoc]

Premises used: smul_assoc
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
i : ι
x : M
⊢ Membership.mem (γ := Submodule R M) (toModuleCatObj R M i) x ↔
    ∃ (y : M), HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
N : Type u_2
inst_7 : AddCommGroup N
inst_8 : Module (Matrix ι ι R) N
i : ι
inst_9 : Module R N
inst_10 : IsScalarTower R (Matrix ι ι R) N
f : LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) M N
x : M
hx : Membership.mem (γ := Submodule R M) (toModuleCatObj R M i) x
obtain :
  ∀ (y : M)
    (hx :
      Membership.mem (γ := Submodule R M) (toModuleCatObj R M i) (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y)),
    Membership.mem (α := N) (γ := Submodule R N) (toModuleCatObj R N i)
      (((↑R :
                {S : Type (max u v)} →
                  {M : Type u_1} →
                    {M₂ : Type u_2} →
                      [inst : Semiring R] →
                        [inst_11 : Semiring S] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module R M] →
                                [inst_15 : Module R M₂] →
                                  [inst_16 : Module S M] →
                                    [inst_17 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              f :
            (a : M) → N)
          (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y) :
        N)
⊢ Membership.mem (α := N) (γ := Submodule R N) (toModuleCatObj R N i)
    (((↑R :
              {S : Type (max u v)} →
                {M : Type u_1} →
                  {M₂ : Type u_2} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → N)
        x :
      N)

Tactic:
obtain ⟨y, rfl⟩ := mem_toModuleCatObj i |>.1 hx

Premises used: MatrixModCat.mem_toModuleCatObj, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : Type u_1
inst_3 : AddCommGroup M
inst_4 : Module (Matrix ι ι R) M
inst_5 : Module R M
inst_6 : IsScalarTower R (Matrix ι ι R) M
N : Type u_2
inst_7 : AddCommGroup N
inst_8 : Module (Matrix ι ι R) N
i : ι
inst_9 : Module R N
inst_10 : IsScalarTower R (Matrix ι ι R) N
f : LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) M N
y : M
hx : Membership.mem (γ := Submodule R M) (toModuleCatObj R M i) (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y)
⊢ Membership.mem (α := N) (γ := Submodule R N) (toModuleCatObj R N i)
    (((↑R :
              {S : Type (max u v)} →
                {M : Type u_1} →
                  {M₂ : Type u_2} →
                    [inst : Semiring R] →
                      [inst_11 : Semiring S] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module R M] →
                              [inst_15 : Module R M₂] →
                                [inst_16 : Module S M] →
                                  [inst_17 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f :
          (a : M) → N)
        (HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y) :
      N)

Tactic:
⟨f y, map_smul _ _ _ |>.symm⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, Eq.symm, DFunLike.coe, map_smul