mathlib-initiative/mathlib-tactics huggingface dataset:
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
p p' : J × K
f : p ⟶ p'
⊢ (uncurry.obj F).map f ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ ((const (J × K)).obj s.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)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.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)
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
⊢ (F.map (fj, fk).1).app (j, k).2 ≫
      (F.obj (j', k').1).map (fj, fk).2 ≫ (D.obj (j', k').1).ι.app (j', k').2 ≫ s.ι.app (j', k').1 =
    (D.obj (j, k).1).ι.app (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt

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)
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
⊢ (F.map fj).app k ≫ (F.obj j').map fk ≫ (D.obj j').ι.app k' ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.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)
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 =
    { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, 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 : 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 ≫ s.ι.app j
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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : limit.π ((curry.obj G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂) = limit.π ((curry.obj G).obj x.1) y.2
⊢ 𝟙 (limit (curry.obj G ⋙ lim)) ≫
      (limit.π (curry.obj G ⋙ lim) x.1 ≫ (curry.obj G ⋙ lim).map f₁) ≫ limit.π ((curry.obj G).obj y.1) y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ limit.π ((curry.obj G).obj x.1) x.2) ≫ G.map (f₁, 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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
Q : DiagramOfCones (curry.obj G) := DiagramOfCones.mkOfHasLimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : limit.π ((curry.obj G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂) = limit.π ((curry.obj G).obj x.1) y.2
⊢ 𝟙 (limit (curry.obj G ⋙ lim)) ≫
      (limit.π (curry.obj G ⋙ lim) x.1 ≫ limMap ((curry.obj G).map f₁)) ≫ limit.π ((curry.obj G).obj y.1) y.2 =
    (limit.π (curry.obj G ⋙ lim) x.1 ≫ limit.π ((curry.obj G).obj x.1) x.2) ≫ G.map (f₁, f₂)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (freeObj F).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ModuleCat.freeDesc (↾fun x ↦ ModuleCat.freeMk ((ConcreteCategory.hom (F.map f)) x)) ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (ModuleCat.freeDesc (φ.app Y)) =
    ModuleCat.freeDesc (φ.app X) ≫ G.map f
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ((fun φ ↦ freeObjDesc φ)
          ((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab)) ψ)).app
      X =
    ψ.app X

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ModuleCat.freeDesc ((↾fun x ↦ ModuleCat.freeMk x) ≫ ↾⇑(ConcreteCategory.hom (((toPresheaf R).map ψ).app X))) = ψ.app X
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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ ((curry.obj G).map (f₁, f₂).1).app x.2 ≫
      ((curry.obj G).obj y.1).map (f₁, f₂).2 ≫
        colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ (curry.obj G ⋙ colim).map f₁ ≫ colimit.ι (curry.obj G ⋙ colim) y.1

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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
Q : DiagramOfCocones (curry.obj G) := DiagramOfCocones.mkOfHasColimits (curry.obj G)
x y : J × K
x✝ : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this : G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 = colimit.ι ((curry.obj G).obj y.1) x.2
⊢ G.map (Prod.mkHom f₁ (𝟙 x.2)) ≫
      G.map (Prod.mkHom (𝟙 y.1) f₂) ≫ colimit.ι ((curry.obj G).obj y.1) y.2 ≫ colimit.ι (curry.obj G ⋙ colim) y.1 =
    colimit.ι ((curry.obj G).obj x.1) x.2 ≫ colimMap ((curry.obj G).map f₁) ≫ colimit.ι (curry.obj G ⋙ colim) y.1
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 : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = ((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))) x✝

Tactic:
dsimp

Goal state after:
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 : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)
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 : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (R.map f ≫ cR.ι.app Y)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)

Tactic:
dsimp

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' : J
φ : j ⟶ j'
⊢ (R ⋙ F.leftAdjointObjIsDefined.ι).map φ ≫ F.partialLeftAdjointHomEquiv (c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f) ≫ ((const J).obj (F.1 Y)).map φ

Tactic:
dsimp

Goal state after:
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' : J
φ : j ⟶ j'
⊢ (R.map φ).hom ≫ F.partialLeftAdjointHomEquiv (c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f) ≫ 𝟙 (F.1 Y)
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' : J
φ : j ⟶ j'
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap (R.map φ) ≫ c'.ι.app j' ≫ f) =
    F.partialLeftAdjointHomEquiv ((R ⋙ F.partialLeftAdjoint).map φ ≫ c'.ι.app j' ≫ f)

Tactic:
dsimp

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 Y' : D
g : Y ⟶ Y'
f : c'.pt ⟶ Y
j : J
⊢ c.ι.app j ≫
      {
          toFun := fun f ↦
            hc.desc
              { pt := F.1 Y', ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.desc
              { pt := Y', ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (f ≫ g) =
    c.ι.app j ≫
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op c.pt)).map g))
        ({
            toFun := fun f ↦
              hc.desc
                { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.desc
                { pt := Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f)

Tactic:
dsimp

Goal state after:
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 Y' : D
g : Y ⟶ Y'
f : c'.pt ⟶ Y
j : J
⊢ c.ι.app j ≫
      hc.desc
        { pt := F.1 Y', ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f ≫ g), naturality := ⋯ } } =
    c.ι.app j ≫
      hc.desc { pt := F.1 Y, ι := { app := fun j ↦ F.partialLeftAdjointHomEquiv (c'.ι.app j ≫ f), naturality := ⋯ } } ≫
        F.map g
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' : J
φ : j ⟶ j'
⊢ ((const J).obj (F.1 Y)).map φ ≫ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j') =
    F.partialRightAdjointHomEquiv (f ≫ c'.π.app j) ≫ (R ⋙ F.rightAdjointObjIsDefined.ι).map φ

Tactic:
dsimp

Goal state after:
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' : J
φ : j ⟶ j'
⊢ 𝟙 (F.1 Y) ≫ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j') =
    F.partialRightAdjointHomEquiv (f ≫ c'.π.app j) ≫ (R.map φ).hom
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' : J
φ : j ⟶ j'
⊢ F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ) =
    F.partialRightAdjointHomEquiv ((f ≫ c'.π.app j) ≫ F.partialRightAdjointMap (R.map φ))

Tactic:
dsimp

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 Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ {
          toFun := fun f ↦
            hc.lift
              { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
          invFun := fun g ↦
            hc'.lift
              { pt := Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
          left_inv := ⋯, right_inv := ⋯ }
        (g ≫ f) ≫
      c.π.app j =
    (ConcreteCategory.hom ((F.op ⋙ yoneda.obj c.pt).map g.op))
        ({
            toFun := fun f ↦
              hc.lift
                { pt := F.1 Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } },
            invFun := fun g ↦
              hc'.lift
                { pt := Y',
                  π := { app := fun j ↦ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j), naturality := ⋯ } },
            left_inv := ⋯, right_inv := ⋯ }
          f) ≫
      c.π.app j

Tactic:
dsimp

Goal state after:
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 Y' : C
g : Y ⟶ Y'
f : Y' ⟶ c'.pt
j : J
⊢ hc.lift
        { pt := F.1 Y, π := { app := fun j ↦ F.partialRightAdjointHomEquiv ((g ≫ f) ≫ c'.π.app j), naturality := ⋯ } } ≫
      c.π.app j =
    (F.map g ≫
        hc.lift
          { pt := F.1 Y', π := { app := fun j ↦ F.partialRightAdjointHomEquiv (f ≫ c'.π.app j), naturality := ⋯ } }) ≫
      c.π.app j
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) (f ≫ g)) =
    freeYonedaEquiv
      ((ConcreteCategory.hom ((pushforward φ ⋙ coyoneda.obj (op ((free S).obj (yoneda.obj X)))).map g))
        ((freeYonedaEquiv.trans freeYonedaEquiv.symm) f))

Tactic:
dsimp

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (yoneda.obj (F.obj X)) ⟶ M
⊢ freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) (f ≫ g)) =
    freeYonedaEquiv ((freeYonedaEquiv.trans freeYonedaEquiv.symm) f ≫ (pushforward φ).map g)
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 Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) (a • m₁) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
dsimp

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 Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) (a • m₁) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
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 Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (a • m₂) =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
dsimp

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 Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (a • m₂) =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ModuleCat.Hom.hom
        ((tensorObj M₁ M₃).map φ ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).map
            (f.app Y ⊗ₘ g.app Y)))
      (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] m₃) =
    (ModuleCat.Hom.hom ((f.app X ⊗ₘ g.app X) ≫ (tensorObj M₂ M₄).map φ))
      (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] m₃)

Tactic:
dsimp

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)
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : ↑(M₁.obj X)
m₃ : ↑(M₃.obj X)
⊢ (ConcreteCategory.hom (f.app Y ⊗ₘ g.app Y)) ((ModuleCat.Hom.hom ((tensorObj M₁ M₃).map φ)) (m₁ ⊗ₜ[↑(R.obj X)] m₃)) =
    (ModuleCat.Hom.hom ((tensorObj M₂ M₄).map φ)) ((ModuleCat.Hom.hom (f.app X ⊗ₘ g.app X)) (m₁ ⊗ₜ[↑(R.obj X)] m₃))
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
a✝ : S ∈ ⊤ X
⊢ S ∈ (discrete C) X

Tactic:
apply Set.mem_univ

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
I : S.shape.R
⊢ P.map (S.shape.fst I).f.op ≫ (S.index P).fst I = P.map (S.shape.snd I).f.op ≫ (S.index P).snd I

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
I : S.shape.R
⊢ P.map I.fst.f.op ≫ P.map I.r.g₁.op = P.map I.snd.f.op ≫ P.map I.r.g₂.op
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ R.diagram.map F ≫ x g₂.obj.hom ⋯ = x g₁.obj.hom ⋯ ≫ ((Functor.const R.category).obj W).map F

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X : C
J J₂ : GrothendieckTopology C
R : Presieve X
W : C
x : FamilyOfElements (yoneda.obj W) R
hx : x.Compatible
g₁ g₂ : R.category
F : g₁ ⟶ g₂
⊢ Over.Hom.left F.hom ≫ x g₂.obj.hom ⋯ = x g₁.obj.hom ⋯ ≫ 𝟙 W
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
⊢ ∀ {Y Z : C} {f : Y ⟶ X}, S.arrows f ∨ R.arrows f → ∀ (g : Z ⟶ Y), S.arrows (g ≫ f) ∨ R.arrows (g ≫ f)

Tactic:
rintro _ _ _ (h | h) g

Goal state after:
case inl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : S.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)

case inr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R✝ S R : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ X
h : R.arrows f✝
g : Z✝ ⟶ Y✝
⊢ S.arrows (g ≫ f✝) ∨ R.arrows (g ≫ f✝)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : D
T : Presieve X
x : FamilyOfElements (F.op ⋙ P) T
Y : C
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F T f
⊢ P.obj (op Y)

Tactic:
obtain ⟨Z, g, h, h₁, _⟩ := getFunctorPushforwardStructure h

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : D
T : Presieve X
x : FamilyOfElements (F.op ⋙ P) T
Y : C
f : Y ⟶ F.obj X
h✝ : Presieve.functorPushforward F T f
Z : D
g : Z ⟶ X
h : Y ⟶ F.obj Z
h₁ : T g
fac✝ : f = h ≫ F.map g
⊢ P.obj (op Y)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
by
  rintro Z _ ⟨g, rfl, hg⟩
  exact ⟨_, g, f, h, hg, rfl⟩

Goal state after: