Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r s✝ : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
U₁ : C
a₁ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₁
U₂ : C
a₂ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₂
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
s : C
α : IsFiltered.max (IsFiltered.max U₁ U₂) V ⟶ s
β : IsFiltered.max U₁ (IsFiltered.max U₂ V) ⟶ s
h₁ : (leftToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α = leftToMax U₁ (IsFiltered.max U₂ V) ≫ β
h₂ :
  (rightToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α =
    (leftToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
h₃ : rightToMax (IsFiltered.max U₁ U₂) V ≫ α = (rightToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
⊢ (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U₁, a₁⟩ *
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel
          ⟨U₂, a₂⟩) •
      Quot.mk (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
        ⟨V, b⟩ =
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel ⟨U₁, a₁⟩ •
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel
          ⟨U₂, a₂⟩ •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
          ⟨V, b⟩

Tactic:
refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_

Goal state after:
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r s✝ : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
U₁ : C
a₁ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₁
U₂ : C
a₂ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₂
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
s : C
α : IsFiltered.max (IsFiltered.max U₁ U₂) V ⟶ s
β : IsFiltered.max U₁ (IsFiltered.max U₂ V) ⟶ s
h₁ : (leftToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α = leftToMax U₁ (IsFiltered.max U₂ V) ≫ β
h₂ :
  (rightToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α =
    (leftToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
h₃ : rightToMax (IsFiltered.max U₁ U₂) V ≫ α = (rightToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ((ConcreteCategory.hom
            (R.map
              (leftToMax
                ⟨⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                        (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₁, a₁⟩.snd *
                          (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₂, a₂⟩.snd⟩.fst,
                    ⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                        (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₁, a₁⟩.snd *
                          (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₂, a₂⟩.snd⟩.snd⟩.fst
                ⟨V, b⟩.fst)))
          ⟨⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                  (ConcreteCategory.hom
                        (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                          (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                      ⟨U₁, a₁⟩.snd *
                    (ConcreteCategory.hom
                        (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                          (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                      ⟨U₂, a₂⟩.snd⟩.fst,
              ⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                  (ConcreteCategory.hom
                        (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                          (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                      ⟨U₁, a₁⟩.snd *
                    (ConcreteCategory.hom
                        (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                          (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                      ⟨U₂, a₂⟩.snd⟩.snd⟩.snd •
        (ConcreteCategory.hom
            (M.map
              (rightToMax
                ⟨⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                        (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₁, a₁⟩.snd *
                          (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₂, a₂⟩.snd⟩.fst,
                    ⟨IsFiltered.max ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst,
                        (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (leftToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₁, a₁⟩.snd *
                          (ConcreteCategory.hom
                              (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat).map
                                (rightToMax ⟨U₁, a₁⟩.fst ⟨U₂, a₂⟩.fst)))
                            ⟨U₂, a₂⟩.snd⟩.snd⟩.fst
                ⟨V, b⟩.fst)))
          ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom
            (R.map
              (leftToMax ⟨U₁, a₁⟩.fst
                ⟨IsFiltered.max ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst,
                    (ConcreteCategory.hom (R.map (leftToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨U₂, a₂⟩.snd •
                      (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd⟩.fst)))
          ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom
            (M.map
              (rightToMax ⟨U₁, a₁⟩.fst
                ⟨IsFiltered.max ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst,
                    (ConcreteCategory.hom (R.map (leftToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨U₂, a₂⟩.snd •
                      (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd⟩.fst)))
          ⟨IsFiltered.max ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst,
              (ConcreteCategory.hom (R.map (leftToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨U₂, a₂⟩.snd •
                (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, a₂⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd⟩.snd)