awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
pos : ∀ (h : j = i1), x i j1 = ∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0
⊢ (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 neg : ∀ (h : ¬j = i1), Eq.{u + 1} (α := R) 0 (∑ x_1 : ι, if j = i1 ∧ x_1 = j1 then x i x_1 else 0)
Tactic: split_ifs with h
-- 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 : ι
v : ι → ↥(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) (β := (↑M : Type u_1)) (single j i 1)
          (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
        ⋯) =
    v
have h : ∀ (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) (β := (↑M : Type u_1)) (single j i 1)
            (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
          sorry) :
      (↑M : Type u_1)) =
    (↑(v i) : (↑M : Type u_1))
Tactic: ext i
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
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) (β := (↑M : Type u_1)) (single j i 1)
            (∑ i : ι, HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))))
          ⋯) :
      (↑M : Type u_1)) =
    (↑(v i) : (↑M : Type u_1))
have h : ∑ x : ι,
    HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single x j 1) (↑(v x) : (↑M : Type u_1))) =
  (↑(v i) : (↑M : Type u_1))
Tactic: simp only [Finset.smul_sum]
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
⊢ ∑ x : ι,
      HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
        (HSMul.hSMul (α := Matrix ι ι R) (single x j 1) (↑(v x) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))
have h : HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
    (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
  (↑(v i) : (↑M : Type u_1))
Tactic: rw [Finset.sum_eq_single i (fun b _ hb ↦ by
      simp [← mul_smul, single_mul_single_of_ne _ _ _ _ hb.symm]) (by simp)]
-- 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 : ι
v : ι → ↥(toModuleCatObj R (↑M : Type u_1) j)
i : ι
⊢ HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))
have h : ∀ (y : (↑M : Type u_1)) (hy : HSMul.hSMul (α := Matrix ι ι R) (single j j 1) y = (↑(v i) : (↑M : Type u_1))),
  HSMul.hSMul (α := Matrix ι ι R) (single j i 1)
      (HSMul.hSMul (α := Matrix ι ι R) (single i j 1) (↑(v i) : (↑M : Type u_1))) =
    (↑(v i) : (↑M : Type u_1))
Tactic: obtain ⟨y, hy⟩ := by simpa [-SetLike.coe_mem] using (v i).2
-- 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 ι
i : ι
X Y : ModuleCat (Matrix ι ι R)
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) X ⟶ Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y)
    (CategoryTheory.Functor.map (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) f ≫
      Iso.hom
        ((fun (X : ModuleCat (Matrix ι ι R)) ↦
            ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
              Iso (C := ModuleCat (Matrix ι ι R))
                (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
          Y))
    (Iso.hom
        ((fun (X : ModuleCat (Matrix ι ι R)) ↦
            ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
              Iso (C := ModuleCat (Matrix ι ι R))
                (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (ModuleCat (Matrix ι ι R))) f)
have hf : ∀ (x : (↑(Functor.obj (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) X) : Type (max v u_1))),
  Eq (α := (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (CategoryTheory.Functor.map (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι) f ≫
              Iso.hom
                ((fun (X : ModuleCat (Matrix ι ι R)) ↦
                    ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
                      Iso (C := ModuleCat (Matrix ι ι R))
                        (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                        (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
                  Y)) :
          (a : (↑((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat (Matrix ι ι R))).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (Iso.hom
                ((fun (X : ModuleCat (Matrix ι ι R)) ↦
                    ((toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso :
                      Iso (C := ModuleCat (Matrix ι ι R))
                        (ModuleCat.of (Matrix ι ι R) (ι → ↥(toModuleCatObj R (↑X : Type (max v u_1)) i)))
                        (ModuleCat.of (Matrix ι ι R) (↑X : Type (max v u_1)))))
                  X) ≫
              CategoryTheory.Functor.map (𝟭 (ModuleCat (Matrix ι ι R))) f) :
          (a : (↑((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat (Matrix ι ι R))).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat (Matrix ι ι R))) Y) : Type (max v u_1)))
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 ι
i : ι
X : ModuleCat R
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat (Matrix ι ι R)) (Functor.obj (toMatrixModCat R ι) X)
      (Functor.obj (toMatrixModCat R ι) X))
    (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
      NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X))
    (𝟙 (Functor.obj (toMatrixModCat R ι) X))
have hf : Eq (α :=
  LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1))
    (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
  (Hom.hom
    (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
      NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X)))
  (Hom.hom (𝟙 (Functor.obj (toMatrixModCat R ι) X)))
Tactic: ext1
-- 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 ι
i : ι
X : ModuleCat R
⊢ Eq (α :=
    LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1))
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (Hom.hom
      (CategoryTheory.Functor.map (toMatrixModCat R ι) (NatTrans.app (Iso.hom (Iso.symm (unitIso.{u, v, u_1} R i))) X) ≫
        NatTrans.app (Iso.hom (counitIso.{u, v, u_1} R i)) (Functor.obj (toMatrixModCat R ι) X)))
    (Hom.hom (𝟙 (Functor.obj (toMatrixModCat R ι) X)))
have hf : (↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
      (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
        (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
    LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) =
  LinearMap.id
Tactic: suffices (toModuleCatFromModuleCatLinearEquiv R ((ModuleCat.toMatrixModCat R ι).obj X)
      i).symm.toLinearMap ∘ₗ LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom
      ((unitIso R i).inv.app X)) = LinearMap.id by simpa using this
-- 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 ι
i : ι
X : ModuleCat R
⊢ (↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
        (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
          (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
      LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) =
    LinearMap.id
have hf : ∀ (x : ι → (↑(Functor.obj (𝟭 (ModuleCat R)) X) : Type (max v u_1))),
  Eq (α := (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    (((↑(LinearEquiv.symm (toModuleCatFromModuleCatLinearEquiv R (Functor.obj (toMatrixModCat R ι) X) i)) :
              (ι → ↥(toModuleCatObj R (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)) i)) →ₗ[Matrix ι ι R]
                (↑((toMatrixModCat R ι).obj X) : Type (max v u_1))) ∘ₗ
            LinearMap.mapMatrixModule ι (Hom.hom (NatTrans.app (Iso.inv (unitIso.{u, v, u_1} R i)) X)) :
          (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
            (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
        x :
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
    ((LinearMap.id :
          (a : ι → (↑((𝟭 (ModuleCat R)).obj X) : Type (max v u_1))) →
            (↑((toMatrixModCat R ι).obj X) : Type (max v u_1)))
        x :
      (↑(Functor.obj (toMatrixModCat R ι) X) : Type (max v u_1)))
Tactic: ext 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 ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
⊢ CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f) =
    HSMul.hSMul (β :=
      Quiver.Hom (V := ModuleCat (Matrix ι ι R)) (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
        (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
      r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)
have hf : ∀ (v : ι → (↑X : Type (max u v))),
  Eq (α := (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom
            (HSMul.hSMul (β :=
              Quiver.Hom (V := ModuleCat (Matrix ι ι R))
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
              r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
Tactic: ext (v : ι → 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 ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
⊢ Eq (α := (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) (r • f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
    ((ModuleCat.Hom.hom
            (HSMul.hSMul (β :=
              Quiver.Hom (V := ModuleCat (Matrix ι ι R))
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) X)
                (Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y))
              r (CategoryTheory.Functor.map (Equivalence.functor (ModuleCat.matrixEquivalence R i)) f)) :
          (a : (↑((ModuleCat.matrixEquivalence R i).functor.obj X) : Type (max u v))) →
            (↑((ModuleCat.matrixEquivalence R i).functor.obj Y) : Type (max u v)))
        v :
      (↑(Functor.obj (Equivalence.functor (ModuleCat.matrixEquivalence R i)) Y) : Type (max u v)))
have hf : (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
    v =
  HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
    ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
        v :
      ι → (↑Y : Type (max u v)))
Tactic: simp only [ModuleCat.matrixEquivalence_functor, ModuleCat.toMatrixModCat_obj_carrier,
      ModuleCat.toMatrixModCat_map, ModuleCat.hom_smul, ModuleCat.hom_ofHom, LinearMap.smul_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 ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
⊢ (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
have hf : ∀ (i_1 : ι),
  (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v i_1 =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i_1
Tactic: ext i
-- 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 ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i_1 : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
i : ι
⊢ (LinearMap.mapMatrixModule ι (r • ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
      v i =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i
have hf : HSMul.hSMul (β := (↑Y : Type (max u v))) r
    ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
  HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
    ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
        v :
      ι → (↑Y : Type (max u v)))
    i
Tactic: simp only [LinearMap.mapMatrixModule_apply, LinearMap.compLeft_apply, Function.comp_apply,
      LinearMap.smul_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 ι
R₀ : Type u_1
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
i_1 : ι
X Y : ModuleCat R
f : X ⟶ Y
r : R₀
v : ι → (↑X : Type (max u v))
i : ι
⊢ HSMul.hSMul (β := (↑Y : Type (max u v))) r
      ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
    HSMul.hSMul (β := ι → (↑Y : Type (max u v))) r
      ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
          v :
        ι → (↑Y : Type (max u v)))
      i
have hf : HSMul.hSMul (β := (↑Y : Type (max u v))) r
    ((ModuleCat.Hom.hom f : (a : (↑X : Type (max u v))) → (↑Y : Type (max u v))) (v i) : (↑Y : Type (max u v))) =
  HSMul.hSMul (α := Matrix ι ι R) (β := ι → (↑Y : Type (max u v)))
    ((algebraMap R₀ (Matrix ι ι R) : (a : R₀) → Matrix ι ι R) r : Matrix ι ι R)
    ((LinearMap.mapMatrixModule ι (ModuleCat.Hom.hom f) : (a : ι → (↑X : Type (max u v))) → ι → (↑Y : Type (max u v)))
        v :
      ι → (↑Y : Type (max u v)))
    i
Tactic: change _ = ((algebraMap R₀ (Matrix ι ι R) r) • ((ModuleCat.Hom.hom f).mapMatrixModule ι v)) i
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
⊢ FiniteMultiplicity a b
have by_contra : ∀ (nh : ¬FiniteMultiplicity a b), False
Tactic: by_contra nh
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
nh : ¬FiniteMultiplicity a b
⊢ False
have nh₁ : Eq (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: rw [← emultiplicity_eq_top, h] at nh
Cleared hypotheses: nh
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = (↑n : ℕ∞)
⊢ multiplicity a b = n
have simp : WithTop.untopD 1 (↑n : ℕ∞) = n
Tactic: simp [multiplicity, h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
⊢ emultiplicity a b = (↑(multiplicity a b) : ℕ∞)
have top : ∀ (hm : emultiplicity a b = ⊤), Eq (α := ℕ∞) ⊤ (↑(multiplicity a b) : ℕ∞)
Tactic: cases hm : emultiplicity a b
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
top : ∀ (hm : emultiplicity a b = ⊤), Eq (α := ℕ∞) ⊤ (↑(multiplicity a b) : ℕ∞)
⊢ emultiplicity a b = (↑(multiplicity a b) : ℕ∞)
have coe : ∀ (a_1 : ℕ) (hm : emultiplicity a b = (↑a_1 : ℕ∞)), Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑(multiplicity a b) : ℕ∞)
Tactic: cases hm : emultiplicity a b
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
h : FiniteMultiplicity a b
a_1 : ℕ
hm : emultiplicity a b = (↑a_1 : ℕ∞)
⊢ Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑(multiplicity a b) : ℕ∞)
have coe : Eq (α := ℕ∞) (↑a_1 : ℕ∞) (↑a_1 : ℕ∞)
Tactic: rw [multiplicity_eq_of_emultiplicity_eq_some hm]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
⊢ emultiplicity a b = (↑n : ℕ∞) ↔ multiplicity a b = n
have mp : emultiplicity a b = (↑n : ℕ∞) → multiplicity a b = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
n : ℕ
h : n ≠ 1
mp : emultiplicity a b = (↑n : ℕ∞) → multiplicity a b = n
⊢ emultiplicity a b = (↑n : ℕ∞) ↔ multiplicity a b = n
have mpr : multiplicity a b = n → emultiplicity a b = (↑n : ℕ∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
⊢ (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
have pos : ∀ (hf : FiniteMultiplicity a b), (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
Tactic: by_cases hf : FiniteMultiplicity a b
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
pos : ∀ (hf : FiniteMultiplicity a b), (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
⊢ (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
have neg : ∀ (hf : ¬FiniteMultiplicity a b), (↑(multiplicity a b) : ℕ∞) ≤ emultiplicity a b
Tactic: by_cases hf : FiniteMultiplicity a b
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
a b : α
c d : β
h : emultiplicity a b = emultiplicity c d
⊢ WithTop.untopD 1 (emultiplicity a b) = WithTop.untopD 1 (emultiplicity c d)
have rw : WithTop.untopD 1 (emultiplicity c d) = WithTop.untopD 1 (emultiplicity c d)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b ≤ n
⊢ emultiplicity a b ≤ (↑n : ℕ∞)
have rw : LE.le (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)
Tactic: rw [emultiplicity_eq_multiplicity hfin]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : (↑n : ℕ∞) ≤ emultiplicity a b
⊢ n ≤ multiplicity a b
have h₁ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
Tactic: rw [emultiplicity_eq_multiplicity hfin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
⊢ n ≤ multiplicity a b
have assumption_mod_cast : ∀ (h : n ≤ multiplicity a b), n ≤ multiplicity a b
Tactic: assumption_mod_cast
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : multiplicity a b < n
⊢ emultiplicity a b < (↑n : ℕ∞)
have rw : LT.lt (α := ℕ∞) (↑(multiplicity a b) : ℕ∞) (↑n : ℕ∞)
Tactic: rw [emultiplicity_eq_multiplicity hfin]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : (↑n : ℕ∞) < emultiplicity a b
⊢ n < multiplicity a b
have h₁ : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
Tactic: rw [emultiplicity_eq_multiplicity hfin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : Monoid α
a b : α
hfin : FiniteMultiplicity a b
n : ℕ
h : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑(multiplicity a b) : ℕ∞)
⊢ n < multiplicity a b
have assumption_mod_cast : ∀ (h : n < multiplicity a b), n < multiplicity a b
Tactic: assumption_mod_cast
Cleared hypotheses: h