mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (((Functor.const J).obj (limitPresheafOfModules F)).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limit.π (F ⋙ evaluation R Y) j) =
    limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (limMap (F.whiskerLeft (restriction R f)) ≫
        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limit.π (F ⋙ evaluation R Y) j) =
    limit.π (F ⋙ evaluation R X) j ≫ (F.obj j).map f
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫ m.app X = ((evaluation R X).mapCocone s).ι.app j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (colimit (F ⋙ evaluation R X))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ (colimit (F ⋙ evaluation R X))).inv
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (λ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (ConcreteCategory.hom
        ((extendScalars f).map (λ_ M).inv ≫
          (AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M).symm.toModuleIso.inv ≫
            (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv ▷ (extendScalars f).obj M))
      (1 ⊗ₜ[R] m)

Tactic:
dsimp

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (λ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (Hom.hom (↟↑(AlgebraTensorModule.rid R S S) ▷ (extendScalars f).obj M))
      ((Hom.hom (↟↑(AlgebraTensorModule.distribBaseChange R S ↑(𝟙_ (ModuleCat R)) ↑M))) (1 ⊗ₜ[R] (1 ⊗ₜ[R] m)))
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (ρ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (ConcreteCategory.hom
        ((extendScalars f).map (ρ_ M).inv ≫
          (AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))).symm.toModuleIso.inv ≫
            (extendScalars f).obj M ◁ (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv))
      (1 ⊗ₜ[R] m)

Tactic:
dsimp

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom (ρ_ ((extendScalars f).obj M)).inv) (1 ⊗ₜ[R] m) =
    (Hom.hom ((extendScalars f).obj M ◁ ↟↑(AlgebraTensorModule.rid R S S)))
      ((Hom.hom (↟↑(AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))))) (1 ⊗ₜ[R] (m ⊗ₜ[R] 1)))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app ((F.obj j).obj X) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j) =
    (ModuleCat.restrictScalarsId'App (RingCat.Hom.hom (R.map (𝟙 X))) ⋯ ((F.obj j).obj X)).inv ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))).map (colimit.ι (F ⋙ evaluation R X) j)

Tactic:
dsimp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (colimMap (F.whiskerLeft (restriction R f)) ≫
          (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (f ≫ g))) ⋯).inv.app
            (colimit (F ⋙ evaluation R Z))

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (f ≫ g))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (colimMap (F.whiskerLeft (restriction R f)) ≫
          (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv) ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (colimMap (F.whiskerLeft (restriction R g)) ≫
              (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)).inv) ≫
          (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))).inv
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom
        (δ (extendScalars f) ((restrictScalars f).obj M₁) ((restrictScalars f).obj M₂) ≫
          ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂)))
      (1 ⊗ₜ[R] (m₁ ⊗ₜ[R] m₂)) =
    m₁ ⊗ₜ[S] m₂

Tactic:
dsimp

Goal state after:
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (Hom.hom ((extendRestrictScalarsAdj f).counit.app M₁ ⊗ₘ (extendRestrictScalarsAdj f).counit.app M₂))
      ((Hom.hom (δ (extendScalars f) ((restrictScalars f).obj M₁) ((restrictScalars f).obj M₂)))
        (1 ⊗ₜ[R] (m₁ ⊗ₜ[R] m₂))) =
    m₁ ⊗ₜ[S] m₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫ (((Functor.const J).obj (colimitPresheafOfModules F)).obj j).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
j : J
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (colimit.ι (F ⋙ evaluation R Y) j) =
    colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R f)) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)).inv
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (tensorObj F F').map f ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (tensorObj G G').map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom).app X =
    ((α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom).app X

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X) (G.obj X) (H.obj X)).hom ▷ K.obj X ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ F.obj X ◁ (α_ (G.obj X) (H.obj X) (K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ ((F ⊗ G) ⋙ H).map f ≫ (prodComparisonIso H (F.obj Y) (G.obj Y)).hom =
    (prodComparisonIso H (F.obj X) (G.obj X)).hom ≫ (F ⋙ H ⊗ G ⋙ H).map f

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y) =
    CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))
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
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ ((uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map (f₁, f₂) ≫
      match (k₁, k₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) =
    (match (j₁, j₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫ (G.obj (((const J₁).obj c₁.pt).obj j₁)).map (c₂.ι.app j₂)) ≫
      ((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map (f₁, f₂)

Tactic:
dsimp

Goal state after:
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
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ ((G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)) ≫
      (G.map (c₁.ι.app k₁)).app (K₂.obj k₂) ≫ (G.obj c₁.pt).map (c₂.ι.app k₂) =
    ((G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)) ≫ 𝟙 ((G.obj c₁.pt).obj c₂.pt)
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
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cone K₁
c₂ : Cone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ (((const (J₁ × J₂)).obj ((G.obj c₁.pt).obj c₂.pt)).map (f₁, f₂) ≫
      match (k₁, k₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) =
    (match (j₁, j₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).map (f₁, f₂)

Tactic:
dsimp

Goal state after:
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
G : C₁ ⥤ C₂ ⥤ C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
c₁ : Cone K₁
c₂ : Cone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ 𝟙 ((G.obj c₁.pt).obj c₂.pt) ≫ (G.map (c₁.π.app k₁)).app c₂.pt ≫ (G.obj (K₁.obj k₁)).map (c₂.π.app k₂) =
    ((G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)
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✝ : IsFilteredOrEmpty C
X : C × C
⊢ IsFiltered (StructuredArrow X (Functor.diag C))

Tactic:
have : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) := by
    rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
    infer_instance
  apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : InitiallySmall C
D : Type w
w✝¹ : SmallCategory D
w✝ : IsFiltered D
F : D ⥤ Cᵒᵖ
h✝ : F.Final
⊢ ∃ D x, ∃ (_ : IsCofiltered D), ∃ F, F.Initial

Tactic:
exact ⟨Dᵒᵖ, inferInstance, inferInstance, F.leftOp, inferInstance⟩

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
T : C ⥤ D
inst✝ : T.Initial
Y : D
⊢ (proj T Y).Initial

Tactic:
refine ⟨fun X => ?_⟩
  rw [isConnected_iff_of_equivalence (ofCostructuredArrowProjEquivalence T Y X)]
  exact (initial_comp (Over.forget X) T).out _

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 ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ ((const K).obj c.pt).map f

Tactic:
dsimp

Goal state after:
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 ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ 𝟙 c.pt
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' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        D.coconePoints.map f ≫ (Q j').desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j', 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 f

Tactic:
dsimp

Goal state after:
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' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j', k), naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫ (Q j).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j, k), naturality := ⋯ } } ≫ 𝟙 c.pt
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
p p' : J × K
f : p ⟶ p'
⊢ ((const (J × K)).obj s.pt).map f ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (uncurry.obj F).map f

Tactic:
dsimp

Goal state after:
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
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
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
⊢ s.π.app (j', k').1 ≫ (D.obj (j', k').1).π.app (j', k').2 =
    s.π.app (j, k).1 ≫
      (D.obj (j, k).1).π.app (j, k).2 ≫ (F.map (fj, fk).1).app (j, k).2 ≫ (F.obj (j', k').1).map (fj, fk).2

Tactic:
dsimp

Goal state after:
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
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.map fj).app k ≫ (F.obj j').map fk
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) =
    { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } }.π.app (j, k)

Tactic:
dsimp

Goal state after:
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) = s.π.app j ≫ (D.obj j).π.app k