mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.ι.app j.1)).app (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) =
    c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
rw [initial_iff_of_isCofiltered]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ x✝.as = (F.obj (Classical.choice ⋯)).as

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝ : Discrete PUnit.{u_1 + 1}
⊢ (F.obj (Classical.choice ⋯)).as = x✝.as

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
X✝ Y✝ : J
x✝ : X✝ ⟶ Y✝
⊢ (Functor.diag J ⋙ externalProduct F₁ F₂).map x✝ ≫ (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj Y✝)).hom =
    (Iso.refl ((Functor.diag J ⋙ externalProduct F₁ F₂).obj X✝)).hom ≫ (F₁ ⊗ F₂).map x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones (curry.obj G)
Q : (j : J) → IsLimit (D.obj j)
c : Cone G
x✝¹ j' : J
x✝ : x✝¹ ⟶ j'
⊢ ∀ (j : K),
    (((const J).obj c.pt).map x✝ ≫
          (Q j').lift { pt := c.pt, π := { app := fun k ↦ c.π.app (j', k), naturality := ⋯ } }) ≫
        (D.obj j').π.app j =
      ((Q x✝¹).lift { pt := c.pt, π := { app := fun k ↦ c.π.app (x✝¹, k), naturality := ⋯ } } ≫ D.conePoints.map x✝) ≫
        (D.obj j').π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f = (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones (curry.obj G)
Q : (j : J) → IsColimit (D.obj j)
c : Cocone G
j x✝¹ : J
x✝ : j ⟶ x✝¹
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        D.coconePoints.map x✝ ≫ (Q x✝¹).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (x✝¹, k), naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫
        (Q j).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j, k), naturality := ⋯ } } ≫ ((const J).obj c.pt).map x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
c₃ : Cone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsLimit c₃
j : J₁ × J₂
⊢ (G.map (c₁.π.app j.1)).app c₂.pt ≫ (G.obj (K₁.obj j.1)).map (c₂.π.app j.2) =
    (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom ≫ c₃.π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
n : s.π.app j' = s.π.app j ≫ (D.map fj).hom
⊢ (s.π.app j ≫ (D.map fj).hom) ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
k : K
⊢ (P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } } ≫
        (coneOfConeUncurry Q c).π.app j) ≫
      (D.obj j).π.app k =
    s.π.app j ≫ (D.obj j).π.app k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
j : J
k : K
⊢ m ≫ c.π.app (j, k) = (m ≫ (coneOfConeUncurry Q c).π.app j) ≫ (D.obj j).π.app k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ ((D.map fj).hom ≫ s.ι.app j') ≫ 𝟙 s.pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
⊢ (D.obj j).ι.app k ≫
      (coconeOfCoconeUncurry Q c).ι.app j ≫
        P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    (D.obj j).ι.app k ≫ s.ι.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
⊢ c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ m

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (Cone.forget (F ⋙ lim)).map
        ((limit.isLimit (F ⋙ lim)).liftConeMorphism
          (coneOfConeUncurry (fun j ↦ limit.isLimit (F.obj j)) (limit.cone (uncurry.obj F)))) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (uncurry.obj F) (j, k)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (F.obj j) k ≫
      colimit.ι (F ⋙ colim) j ≫
        (Cocone.forget (F ⋙ colim)).map
          ((colimit.isColimit (F ⋙ colim)).descCoconeMorphism
            (coconeOfCoconeUncurry (fun j ↦ colimit.isColimit (F.obj j)) (colimit.cocone (uncurry.obj F)))) =
    colimit.ι (uncurry.obj F) (j, k)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ (colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom) ≫
      (colimitUncurryIsoColimitCompColim F).inv =
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j) ≫ (colimitUncurryIsoColimitCompColim F).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) =
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom) ≫ (colimitIsoColimitCurryCompColim G).inv =
    (colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j) ≫ (colimitIsoColimitCurryCompColim G).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ ((colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫
          colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k ≫
            (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).inv) ≫
        (HasColimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
      (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) ≫ colimit.ι (Prod.swap K J ⋙ G) (k, j)) ≫
      (colimitIsoColimitCurryCompColim (Prod.swap K J ⋙ G)).hom =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
φ : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM) ⟶ N
⊢ ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM),
    (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ)) (r • m) =
      r • (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ)) m

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
⊢ ∀ (x y : ModuleColimit hcR hcM),
    ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) (x + y) =
      ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) x + ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
f : c'.pt ⟶ Y
j : J
⊢ c'.ι.app j ≫
      (fun g ↦
          hc'.desc
            { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } })
        ((fun f ↦
            hc.desc
              { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } })
          f) =
    c'.ι.app j ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j : J
⊢ c.ι.app j ≫
      (fun f ↦
          hc.desc
            { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } })
        ((fun g ↦
            hc'.desc
              { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } })
          g) =
    c.ι.app j ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
f : Y ⟶ c'.pt
j : J
⊢ (fun g ↦
          hc'.lift
            { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } })
        ((fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } })
          f) ≫
      c'.π.app j =
    f ≫ c'.π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialRightAdjointSource
c : Cone (R ⋙ F.rightAdjointObjIsDefined.ι)
hc : IsLimit c
c' : Cone (R ⋙ F.partialRightAdjoint)
hc' : IsLimit c'
Y : C
g : (F.op ⋙ yoneda.obj c.pt).obj (op Y)
j : J
⊢ (fun f ↦
          hc.lift
            { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } })
        ((fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } })
          g) ≫
      c.π.app j =
    g ≫ c.π.app j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ (map hcR hcM hcM (𝟙 M)) (ιM m) = LinearMap.id (ιM m)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C₁
inst✝ : Category.{v_3, u_3} C₂
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₀₂ : C₀ ⥤ C₂
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₂₀ : C₂ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂) ((conjugateIsoEquiv adj₀₂ (adj₀₁.comp adj₁₂)).symm e₀₁₂.symm).inv = e₀₁₂.hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ (map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f) (ιM m) = (map hcR hcM hcM'' (f ≫ g)) (ιM m)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
x : ↑(M.obj (F.op.obj X))
⊢ (ConcreteCategory.hom (M.map (𝟙 (F.op.obj X)))) x =
    (ModuleCat.Hom.hom
        ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
          (ModuleCat.of ↑((F.op ⋙ R).obj X) ↑(M.obj (F.op.obj X)))))
      x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' x✝² x✝¹ : Subfunctor F
x✝ : C
⊢ x✝¹.obj x✝ ⊆ { obj := fun U ↦ x✝².obj U ⊔ x✝¹.obj U, map := ⋯ }.obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : ↑(M.obj (F.op.obj X✝))
⊢ (ConcreteCategory.hom (M.map (F.op.map f ≫ F.op.map g))) x =
    (ModuleCat.Hom.hom
        (M.map (F.op.map f) ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((F.op ⋙ R).map f))).map (M.map (F.op.map g)) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((F.op ⋙ R).map f)) (RingCat.Hom.hom ((F.op ⋙ R).map g))
                    (RingCat.Hom.hom ((F.op ⋙ R).map (f ≫ g))) ⋯).inv.app
              (ModuleCat.of ↑((F.op ⋙ R).obj Z✝) ↑(M.obj (F.op.obj Z✝)))))
      x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊤ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
⊢ ∀ {U V : C} (i : U ⟶ V), ⊥ ⊆ ⇑(hom (F.map i)) ⁻¹' ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map (𝟙 X))) m₁ ⊗ₜ[↑(R.obj X)] (ConcreteCategory.hom (M₂.map (𝟙 X))) m₂ =
    m₁ ⊗ₜ[↑(R.obj X)] m₂

Tactic:
simp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₁.obj X)).inv)
        m₁ ⊗ₜ[↑(R.obj X)]
      (ConcreteCategory.hom (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₂.obj X)).inv) m₂ =
    m₁ ⊗ₜ[↑(R.obj X)] m₂