Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_1
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
⊢ ∀ (a : (j : C) × (R ⋙ forget RingCat).obj j) (b₁ b₂ : (j : C) × (M ⋙ forget Ab).obj j),
    (M ⋙ forget Ab).ColimitTypeRel b₁ b₂ →
      (M ⋙ forget Ab).ιColimitType (IsFiltered.max a.fst b₁.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a.fst b₁.fst))) a.snd •
            (ConcreteCategory.hom (M.map (rightToMax a.fst b₁.fst))) b₁.snd) =
        (M ⋙ forget Ab).ιColimitType (IsFiltered.max a.fst b₂.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a.fst b₂.fst))) a.snd •
            (ConcreteCategory.hom (M.map (rightToMax a.fst b₂.fst))) b₂.snd)

pp: case refine_2
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
⊢ ∀ (a₁ a₂ : (j : C) × (R ⋙ forget RingCat).obj j) (b : (j : C) × (M ⋙ forget Ab).obj j),
    (R ⋙ forget RingCat).ColimitTypeRel a₁ a₂ →
      (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₁.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₁.fst b.fst))) a₁.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₁.fst b.fst))) b.snd) =
        (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₂.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₂.fst b.fst))) a₂.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₂.fst b.fst))) b.snd)

Tactic:
· rintro ⟨U, a⟩ ⟨V₁, b₁⟩ ⟨V₂, b₂⟩ ⟨f : V₁ ⟶ V₂, rfl : b₂ = M.map _ b₁⟩
    obtain ⟨s, α, β, h₁, h₂⟩ :=
      bowtie (leftToMax U V₁) (leftToMax U V₂)
        (rightToMax U V₁) (f ≫ rightToMax U V₂)
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
    simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]

Goal state after:
case refine_2
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 : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
⊢ ∀ (a₁ a₂ : (j : C) × (R ⋙ forget RingCat).obj j) (b : (j : C) × (M ⋙ forget Ab).obj j),
    (R ⋙ forget RingCat).ColimitTypeRel a₁ a₂ →
      (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₁.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₁.fst b.fst))) a₁.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₁.fst b.fst))) b.snd) =
        (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₂.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₂.fst b.fst))) a₂.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₂.fst b.fst))) b.snd)