awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
φ :
  Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      M ⟶
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      N
hφ :
  ∀ (r : R),
    φ ≫ (N.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj N)) r =
      (M.smul : (a : R) → End ((forget₂ (ModuleCat R) AddCommGrpCat).obj M)) r ≫ φ
⊢ CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      (homMk φ hφ) =
    φ

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
change :
  IsIso (X :=
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
      (Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        A))
    (CategoryTheory.Functor.map
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
      (CategoryTheory.Functor.map
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        f))
⊢ IsIso (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)

Tactic:
change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))

Premises used: CategoryTheory.IsIso, CategoryTheory.Functor.map, CategoryTheory.forget₂, AddCommGrpCat, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
      (Functor.obj
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        A))
    (CategoryTheory.Functor.map
      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
      (CategoryTheory.Functor.map
        (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
          (CD := AddCommGrpCat.carrier))
        f))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)

Tactic:
have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommGrpCat).map f))
      infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u
inst : Ring R
X₁ X₂ : Type v
M N A B : ModuleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier))
      f)
this :
  IsIso (X :=
    Functor.obj
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (ModuleCat.{v, u} R) (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
        carrier))
      f)
⊢ IsIso f

Tactic:
apply isIso_of_reflects_iso _ (forget _)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u_1
inst : CommRing R
M N P : ModuleCat.{u, u_1} R
f : (↑M : Type u) →ₗ[R] (↑N : Type u) →ₗ[R] (↑P : Type u)
⊢ hom₂ (ofHom₂ f) = f

Tactic:
rfl

Premises used: ModuleCat.Hom.hom₂, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u_1
inst : CommRing R
M N P : ModuleCat.{u, u_1} R
f : M ⟶ of R (N ⟶ P)
⊢ ofHom₂ (Hom.hom₂ f) = f

Tactic:
rfl

Premises used: ModuleCat.ofHom₂, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u_1
inst : Ring R
G : ModuleCat.{u, u_1} R
H : Type u
inst_1 : AddCommGroup H
inst_2 : Module R H
f : (↑G : Type u) →ₗ[R] H
⊢ f ∘ₗ Hom.hom (𝟙 G) = f

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Basic
Goal:
R : Type u_1
inst : Ring R
G : Type u
inst_1 : AddCommGroup G
inst_2 : Module R G
H : ModuleCat.{u, u_1} R
f : G →ₗ[R] (↑H : Type u)
⊢ Hom.hom (𝟙 H) ∘ₗ f = f

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
⊢ HasBinaryBiproducts (ModuleCat.{v, u} R)

Tactic:
HasBinaryBiproducts.of_hasBinaryProducts

Premises used: CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
⊢ HasFiniteBiproducts (ModuleCat.{v, u} R)

Tactic:
HasFiniteBiproducts.of_hasFiniteProducts

Premises used: CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj (pair M N) { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (CategoryTheory.Functor.map
        (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { down := { down := ⋯ } })
      (Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v)))) x ⟶
          Functor.obj (pair M N) x)
        { as := WalkingPair.left : Discrete WalkingPair } fun (j : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              { as := x : Discrete WalkingPair } ⟶
            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))))
    ((Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v)))) x ⟶
          Functor.obj (pair M N) x)
        { as := WalkingPair.left : Discrete WalkingPair } fun (j : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              { as := x : Discrete WalkingPair } ⟶
            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))) ≫
      CategoryTheory.Functor.map (pair M N)
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := WalkingPair.left : Discrete WalkingPair }.as =
                  { as := WalkingPair.left : Discrete WalkingPair }.as) } :
          ULift.{0, 0}
            (PLift
              ({ as := WalkingPair.left : Discrete WalkingPair }.as =
                { as := WalkingPair.left : Discrete WalkingPair }.as)) })

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (CategoryTheory.Functor.map
        (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
        { down := { down := ⋯ } })
      (Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v)))) x ⟶
          Functor.obj (pair M N) x)
        { as := WalkingPair.right : Discrete WalkingPair } fun (j : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              { as := x : Discrete WalkingPair } ⟶
            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))))
    ((Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
        Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v)))) x ⟶
          Functor.obj (pair M N) x)
        { as := WalkingPair.right : Discrete WalkingPair } fun (j : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              { as := x : Discrete WalkingPair } ⟶
            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))) ≫
      CategoryTheory.Functor.map (pair M N)
        {
          down :=
            { down := ⋯ :
              PLift
                ({ as := WalkingPair.right : Discrete WalkingPair }.as =
                  { as := WalkingPair.right : Discrete WalkingPair }.as) } :
          ULift.{0, 0}
            (PLift
              ({ as := WalkingPair.right : Discrete WalkingPair }.as =
                { as := WalkingPair.right : Discrete WalkingPair }.as)) })

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R ((↑M : Type v) × (↑N : Type v)),
        π :=
          {
            app := fun (j : Discrete WalkingPair) ↦
              Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                    x ⟶
                  Functor.obj (pair M N) x)
                j fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj
                      (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      { as := x : Discrete WalkingPair } ⟶
                    Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                  j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
            naturality := ⋯ :
            NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              (pair M N) } :
        Cone (pair M N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R ((↑M : Type v) × (↑N : Type v)),
                π :=
                  {
                    app := fun (j : Discrete WalkingPair) ↦
                      Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                        Functor.obj
                            (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                            x ⟶
                          Functor.obj (pair M N) x)
                        j fun (j : WalkingPair) ↦
                        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                          Functor.obj
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (of R ((↑M : Type v) × (↑N : Type v))))
                              { as := x : Discrete WalkingPair } ⟶
                            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                          (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                    naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      (pair M N) } :
                Cone (pair M N) }.π.app
          j =
      s.π.app j
simp_rw :
  m =
    ↟(LinearMap.prod (Hom.hom (m ≫ ↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))))
        (Hom.hom (m ≫ ↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))))
⊢ m = ↟(LinearMap.prod (Hom.hom (s.π.app { as := WalkingPair.left })) (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
simp_rw [← w ⟨WalkingPair.left⟩, ← w ⟨WalkingPair.right⟩]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
s : Cone (pair M N)
m :
  s.pt ⟶
    { pt := of R ((↑M : Type v) × (↑N : Type v)),
        π :=
          {
            app := fun (j : Discrete WalkingPair) ↦
              Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                    x ⟶
                  Functor.obj (pair M N) x)
                j fun (j : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj
                      (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      { as := x : Discrete WalkingPair } ⟶
                    Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                  j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))) (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
            naturality := ⋯ :
            NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
              (pair M N) } :
        Cone (pair M N) }.pt
w :
  ∀ (j : Discrete WalkingPair),
    m ≫
        { pt := of R ((↑M : Type v) × (↑N : Type v)),
                π :=
                  {
                    app := fun (j : Discrete WalkingPair) ↦
                      Discrete.casesOn (motive := fun (x : Discrete WalkingPair) ↦
                        Functor.obj
                            (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                            x ⟶
                          Functor.obj (pair M N) x)
                        j fun (j : WalkingPair) ↦
                        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                          Functor.obj
                              (Functor.obj (Functor.const (Discrete WalkingPair))
                                (of R ((↑M : Type v) × (↑N : Type v))))
                              { as := x : Discrete WalkingPair } ⟶
                            Functor.obj (pair M N) { as := x : Discrete WalkingPair })
                          j (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))
                          (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))),
                    naturality := ⋯ :
                    NatTrans (Functor.obj (Functor.const (Discrete WalkingPair)) (of R ((↑M : Type v) × (↑N : Type v))))
                      (pair M N) } :
                Cone (pair M N) }.π.app
          j =
      s.π.app j
⊢ m =
    ↟(LinearMap.prod (Hom.hom (m ≫ ↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))))
        (Hom.hom (m ≫ ↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (M.binaryProductLimitCone N).cone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj (pair M N) { as := WalkingPair.left : Discrete WalkingPair })
    ((M.binaryProductLimitCone N).cone.π.app { as := WalkingPair.left })
    (↟(LinearMap.fst R (↑M : Type v) (↑N : Type v)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (M.binaryProductLimitCone N).cone.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj (pair M N) { as := WalkingPair.right : Discrete WalkingPair })
    ((M.binaryProductLimitCone N).cone.π.app { as := WalkingPair.right })
    (↟(LinearMap.snd R (↑M : Type v) (↑N : Type v)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ (M.biprodIsoProd N).inv ≫ biprod.fst = ↟(LinearMap.fst R (↑M : Type v) (↑N : Type v))

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.left)

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.Algebra.Category.ModuleCat.Biproducts
Goal:
R : Type u
inst : Ring R
M N : ModuleCat.{v, u} R
⊢ (M.biprodIsoProd N).inv ≫ biprod.snd = ↟(LinearMap.snd R (↑M : Type v) (↑N : Type v))

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ _ (Discrete.mk WalkingPair.right)

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp