awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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 (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
have 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))
Tactic: simp only [eval_det, map_zero, map_add, eval_add, Algebra.smul_def, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix = f.comp (evalRingHom 0)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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)
⊢ RingHom.comp (RingHom.mapMatrix (evalRingHom 0)) f.polyToMatrix = f.comp (evalRingHom 0)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MatrixPolynomialAlgebra (goal)
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
⊢ 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))))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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
⊢ 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)
have dsimp : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) = r • HSMul.hSMul (α := Matrix ι ι R) (single i i 1) x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (hypothesis)
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
⊢ HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) = r • HSMul.hSMul (α := Matrix ι ι R) (single i i 1) x
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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)
⊢ HSMul.hSMul (α := Matrix ι ι R) (single i i 1) (r • x) = r • HSMul.hSMul (α := Matrix ι ι R) (single i i 1) x
have 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)
Tactic: rw [← smul_assoc r, smul_eq_diagonal_mul, this.eq, mul_smul, ← smul_one_eq_diagonal]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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)
⊢ 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)
have 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)
Tactic: nth_rw 1 [← one_smul (Matrix ι ι R) x]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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)
⊢ 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)
have 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)
Tactic: rw [smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨y, rfl⟩ := mem_toModuleCatObj i |>.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : (↑M : Type u_1)
⊢ (r • m) • x = HSMul.hSMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) (m • x)
have rw : (r • m) • x = HMul.hMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) m • x
Tactic: rw [← mul_smul, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : (↑M : Type u_1)
rw : (r • m) • x = HMul.hMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) m • x
⊢ (r • m) • x = HSMul.hSMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) (m • x)
have rw₁ : (r • m) • x = ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x
Tactic: rw [← mul_smul, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : (↑M : Type u_1)
rw : (r • m) • x = HMul.hMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) m • x
rw₁ : (r • m) • x = ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x
⊢ (r • m) • x = HSMul.hSMul (α := Matrix ι ι R) ((Matrix.scalar ι : (a : R) → Matrix ι ι R) r : Matrix ι ι R) (m • x)
have rw₂ : ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x = ((Matrix.diagonal fun (x : ι) ↦ r) * m) • x
Tactic: rw [← mul_smul, Matrix.scalar_apply, Matrix.smul_eq_diagonal_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
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 R M
i : ι
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
⊢ (fun (x : M) ↦
        (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
            (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
          ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
      ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
        (Subtype.mk (p := fun (x : ι → M) ↦
          Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
    Subtype.mk (p := fun (x : ι → M) ↦
      Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx
have obtain : ∀ (y : ι → M) (hy : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y = x),
  (fun (x : M) ↦
        (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
            (Pi.single (M := fun (a : ι) ↦ M) i x) sorry :
          ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
      ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
        (Subtype.mk (p := fun (x : ι → M) ↦
          Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
    Subtype.mk (p := fun (x : ι → M) ↦
      Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx
Tactic: obtain ⟨y, hy⟩ := mem_toModuleCatObj i |>.1 hx
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (hypothesis)
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 R M
i : ι
x_1 : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))
x : ι → M
hx : Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x
y : ι → M
hy : HSMul.hSMul (α := Matrix ι ι R) (single i i 1) y = x
⊢ (fun (x : M) ↦
        (Subtype.mk (p := fun (x : ι → M) ↦
            Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x)
            (Pi.single (M := fun (a : ι) ↦ M) i x) ⋯ :
          ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))))
      ((fun (x : ↥(toModuleCatObj R (ι → M) i : Submodule R (ι → M))) ↦ (∑ i_1 : ι, (↑x : ι → M) i_1 : M))
        (Subtype.mk (p := fun (x : ι → M) ↦
          Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx)) =
    Subtype.mk (p := fun (x : ι → M) ↦
      Membership.mem (γ := Submodule R (ι → M)) (toModuleCatObj R (ι → M) i : Submodule R (ι → M)) x) x hx
have hy₁ : Pi.single (M := fun (j : ι) ↦ M) i (HSMul.hSMul.{u, u_1, u_1} (α := R) 1 (y i)) = x
Tactic: rw [single_smul] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x x_1 : (↑M : Type u_1)
⊢ (fun (i : ι) ↦
      Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
        Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
        (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) (x + x_1)) ⋯) =
    HAdd.hAdd (α := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
      (fun (i : ι) ↦
        Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x) ⋯)
      fun (i : ι) ↦
      Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
        Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
        (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x_1) ⋯
have h : ∀ (x_2 : ι),
  (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j x_2 1) (x + x_1)) sorry) :
      (↑M : Type u_1)) =
    (↑(HAdd.hAdd (α := ι → ↥(toModuleCatObj R (↑M : Type u_1) j)) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x) sorry)
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) x_1) sorry)
          x_2) :
      (↑M : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (hypothesis)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
⊢ (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) (x • m)) ⋯) :
      (↑M : Type u_1)) =
    (↑(HSMul.hSMul (α := Matrix ι ι R) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
          ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m) ⋯)
          i) :
      (↑M : Type u_1))
have this₁ : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
Tactic: haveI := MatrixModCat.isScalarTower_toModuleCat R M
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
⊢ (↑(Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
          Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
          (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) (x • m)) ⋯) :
      (↑M : Type u_1)) =
    (↑(HSMul.hSMul (α := Matrix ι ι R) (β := ι → ↥(toModuleCatObj R (↑M : Type u_1) j))
          ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : (↑M : Type u_1)) ↦
              Membership.mem (γ := Submodule R (↑M : Type u_1)) (toModuleCatObj R (↑M : Type u_1) j) x)
              (HSMul.hSMul (α := Matrix ι ι R) (single j i 1) m) ⋯)
          i) :
      (↑M : Type u_1))
have simp : (single j i 1 * x) • m =
  HSMul.hSMul (α := Matrix ι ι R) (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) m
Tactic: simp only [← mul_smul, RingHom.id_apply, Module.smul_apply,
      AddSubmonoidClass.coe_finsetSum, SetLike.val_smul, ← smul_assoc, ← Finset.sum_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
⊢ (single j i 1 * x) • m =
    HSMul.hSMul (α := Matrix ι ι R) (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) m
have e_a : single j i 1 * x = ∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
⊢ single j i 1 * x = ∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)
have e_a : ∀ (i1 j1 : ι),
  HMul.hMul (α := Matrix ι ι R) (single j i 1) x i1 j1 =
    (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) i1 j1
Tactic: ext i1 j1
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
⊢ HMul.hMul (α := Matrix ι ι R) (single j i 1) x i1 j1 =
    (∑ i_1 : ι, HSMul.hSMul (β := Matrix ι ι R) (x i i_1) (single j i_1 1)) i1 j1
have e_a : Eq.{u + 1} (α := R) (∑ j_1 : ι, single j i 1 i1 j_1 * x j_1 j1) (∑ c : ι, single j c (x i c) i1 j1)
Tactic: simp only [mul_apply, smul_single, smul_eq_mul, mul_one, sum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
⊢ Eq.{u + 1} (α := R) (∑ j_1 : ι, single j i 1 i1 j_1 * x j_1 j1) (∑ c : ι, single j c (x i c) i1 j1)
have e_a : single j i 1 i1 i * x i j1 = ∑ c : ι, single j c (x i c) i1 j1
Tactic: rw [Finset.sum_eq_single_of_mem (a := i) (by simp) (fun b _ hb ↦ by simp [single, Ne.symm hb])]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
⊢ single j i 1 i1 i * x i j1 = ∑ c : ι, single j c (x i c) i1 j1
have e_a : (if j = i1 then x i j1 else 0) = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
Tactic: simp only [single_apply, and_true, ite_mul, one_mul, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : (↑M : Type u_1)
i : ι
this_1 : Module.{u, u_1} R (↑M : Type u_1) := Module.compHom (R := Matrix ι ι R) (↑M : Type u_1) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) (↑M : Type u_1)
i1 j1 : ι
⊢ (if j = i1 then x i j1 else 0) = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
have pos : ∀ (h : j = i1), x i j1 = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
Tactic: split_ifs with h