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
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 G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
by

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'
r : ↑cR.pt
m₁ : ModuleColimit hcR hcM
m₂ : ModuleColimit hcR hcM'
⊢ ∃ U a x₁ x₂, (ιR cR) a = r ∧ ιM x₁ = m₁ ∧ ιM x₂ = m₂

Tactic:
by

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''
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ (r₁ * r₂) • m = r₁ • r₂ • m

Tactic:
by

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''
m : ModuleColimit hcR hcM
⊢ 1 • m = m

Tactic:
by

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
X : C
⊢ F.leftAdjointObjIsDefined X ↔ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
by

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
X : F.PartialLeftAdjointSource
Y Y' : D
f : F.partialLeftAdjointObj X ⟶ Y
g : Y ⟶ Y'
⊢ F.partialLeftAdjointHomEquiv (f ≫ g) = F.partialLeftAdjointHomEquiv f ≫ F.map g

Tactic:
by

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
X Y : F.PartialLeftAdjointSource
f : X ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) =
    f.hom ≫ F.partialLeftAdjointHomEquiv (𝟙 (F.partialLeftAdjointObj Y))

Tactic:
by

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
X X' : F.PartialLeftAdjointSource
Y : D
f : X ⟶ X'
g : F.partialLeftAdjointObj X' ⟶ Y
⊢ F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) = f.hom ≫ F.partialLeftAdjointHomEquiv g

Tactic:
by

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
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f = F.partialLeftAdjointHomEquiv.symm (g.hom ≫ f)

Tactic:
by

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''
r : ↑cR.pt
⊢ r • 0 = 0

Tactic:
by

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
X : F.PartialLeftAdjointSource
⊢ F.partialLeftAdjointMap (𝟙 X) = 𝟙 (F.partialLeftAdjointObj X)

Tactic:
by

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
X Y Z : F.PartialLeftAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.partialLeftAdjointMap (f ≫ g) = F.partialLeftAdjointMap f ≫ F.partialLeftAdjointMap g

Tactic:
by

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
h : F.leftAdjointObjIsDefined = ⊤
X : C
⊢ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
by

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''
r : ↑cR.pt
m₁ m₂ : ModuleColimit hcR hcM
⊢ r • (m₁ + m₂) = r • m₁ + r • m₂

Tactic:
by

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
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
X : C
Y Y' : D
g : Y ⟶ Y'
f : (F ⋙ coyoneda.obj (op X)).coreprX ⟶ Y
⊢ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv (f ≫ g) =
    (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv f ≫ F.map g

Tactic:
by

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
h : F.leftAdjointObjIsDefined = ⊤
⊢ F.IsRightAdjoint

Tactic:
by

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''
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ (r₁ + r₂) • m = r₁ • m + r₂ • m

Tactic:
by

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
⊢ F.IsRightAdjoint ↔ F.leftAdjointObjIsDefined = ⊤

Tactic:
by

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''
m : ModuleColimit hcR hcM
⊢ 0 • m = 0

Tactic:
by

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:
by

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
N : ModuleCat ↑cR.pt
α : ModuleColimit hcR hcM →+ ↑N
⊢ (∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)),
      (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) (r • m) =
        (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((homEquiv' hcR hcM) α).app U)) m) ↔
    ∀ (r : ↑cR.pt) (m : ModuleColimit hcR hcM), α (r • m) = r • α m

Tactic:
by

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:
by

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

Tactic:
by

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:
by

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:
by

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:
by

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:
by

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
Y : D
⊢ F.rightAdjointObjIsDefined Y ↔ (F.op ⋙ yoneda.obj Y).IsRepresentable

Tactic:
by

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
X Y : F.PartialRightAdjointSource
f : X ⟶ Y
⊢ F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) =
    F.partialRightAdjointHomEquiv (𝟙 (F.partialRightAdjointObj X)) ≫ f.hom

Tactic:
by

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
X : C
Y Y' : F.PartialRightAdjointSource
f : X ⟶ F.partialRightAdjointObj Y
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv (f ≫ F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g.hom

Tactic:
by

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
X : C
Y Y' : F.PartialRightAdjointSource
f : F.obj X ⟶ Y.obj
g : Y ⟶ Y'
⊢ F.partialRightAdjointHomEquiv.symm f ≫ F.partialRightAdjointMap g = F.partialRightAdjointHomEquiv.symm (f ≫ g.hom)

Tactic:
by

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
X : F.PartialRightAdjointSource
⊢ F.partialRightAdjointMap (𝟙 X) = 𝟙 (F.partialRightAdjointObj X)

Tactic:
by

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
X Y Z : F.PartialRightAdjointSource
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.partialRightAdjointMap (f ≫ g) = F.partialRightAdjointMap f ≫ F.partialRightAdjointMap g

Tactic:
by

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
h : F.rightAdjointObjIsDefined = ⊤
X : D
⊢ (F.op ⋙ yoneda.obj X).IsRepresentable

Tactic:
by

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
h : F.rightAdjointObjIsDefined = ⊤
⊢ F.IsLeftAdjoint

Tactic:
by

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
⊢ ∀ (m : ↑cR.pt) (x : ModuleColimit hcR hcM),
    ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) (m • x) =
      (RingHom.id ↑cR.pt) m • ((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)) x

Tactic:
by

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
⊢ F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤

Tactic:
by

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
⊢ (forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map
      ((fun ψ ↦
          ModuleCat.ofHom
            { toFun := ⇑((homEquiv' hcR hcM).symm ((toPresheaf R).map ψ)), map_add' := ⋯, map_smul' := ⋯ })
        ((fun φ ↦
            homMk ((homEquiv' hcR hcM) (AddCommGrpCat.Hom.hom ((forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ))) ⋯)
          φ)) =
    (forget₂ (ModuleCat ↑cR.pt) AddCommGrpCat).map φ

Tactic:
by

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
N : ModuleCat ↑cR.pt
β : M ⟶ (constFunctor cR).obj N
X : Cᵒᵖ
x : ↑(M.obj X)
⊢ (ConcreteCategory.hom ((homEquiv hcR hcM).symm β)) ((ConcreteCategory.hom (cM.ι.app X)) x) =
    (ConcreteCategory.hom (β.app X)) x

Tactic:
by

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' : 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:
by

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' : J
φ : j ⟶ j'
⊢ ((const J).obj Y).map φ ≫ F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j') =
    F.partialRightAdjointHomEquiv.symm (g ≫ c.π.app j) ≫ (R ⋙ F.partialRightAdjoint).map φ

Tactic:
by

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:
by

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:
by

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''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
r : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) (r • m) =
    (RingHom.id ↑cR.pt) r • (ConcreteCategory.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))) m

Tactic:
by

Goal state after: