mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop

Tactic:
change c'.inj _ ≫ _ = _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.inj j ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((StructuredArrow.hom E).app X)

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
X : C
h : E.IsPointwiseLeftKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((StructuredArrow.hom E).app X)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
T : H
f g : (StructuredArrow.right E).obj Y ⟶ T
hfg :
  ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
    (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ f =
      (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ g
j : CostructuredArrow L Y
⊢ (E.coconeAt Y).ι.app j ≫ f = (E.coconeAt Y).ι.app j ≫ g

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
T : H
f g : (StructuredArrow.right E).obj Y ⟶ T
hfg :
  ∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
    (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ f =
      (StructuredArrow.hom E).app X ≫ (StructuredArrow.right E).map φ ≫ g
j : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app j.left ≫ (StructuredArrow.right E).map j.hom ≫ f =
    (StructuredArrow.hom E).app j.left ≫ (StructuredArrow.right E).map j.hom ≫ g
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
Z : H
φ : CostructuredArrow.proj L Y ⋙ F ⟶ (const (CostructuredArrow L Y)).obj Z
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ (IsColimit.homEquiv h).symm φ = φ.app g

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
Y : D
h : E.IsPointwiseLeftKanExtensionAt Y
Z : H
φ : CostructuredArrow.proj L Y ⋙ F ⟶ (const (CostructuredArrow L Y)).obj Z
g : CostructuredArrow L Y
⊢ (StructuredArrow.hom E).app g.left ≫ (StructuredArrow.right E).map g.hom ≫ (IsColimit.homEquiv h).symm φ = φ.app g
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (G.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right G).map φ

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (StructuredArrow.hom E).app X.left ≫
      (StructuredArrow.right E).map X.hom ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (StructuredArrow.hom G).app X.left ≫ (StructuredArrow.right G).map X.hom ≫ (StructuredArrow.right G).map φ
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
X : C
⊢ (StructuredArrow.hom E ≫
          ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).desc (G.coconeAt Y), naturality := ⋯ }).app
      X =
    (StructuredArrow.hom G).app X

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : L.LeftExtension F
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
X : C
⊢ (StructuredArrow.hom E).app X ≫ (h (L.obj X)).desc (G.coconeAt (L.obj X)) = (StructuredArrow.hom G).app X
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
X : C
h : E.IsPointwiseRightKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((CostructuredArrow.hom E).app X)

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
X : C
h : E.IsPointwiseRightKanExtensionAt (L.obj X)
inst✝¹ : L.Full
inst✝ : L.Faithful
⊢ IsIso ((CostructuredArrow.hom E).app X)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ (CostructuredArrow.left G).map φ ≫ (G.coneAt Y₂).π.app X =
    ((h Y₁).lift (G.coneAt Y₁) ≫ (CostructuredArrow.left E).map φ) ≫ (E.coneAt Y₂).π.app X

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : StructuredArrow Y₂ L
⊢ (CostructuredArrow.left G).map φ ≫ (CostructuredArrow.left G).map X.hom ≫ (CostructuredArrow.hom G).app X.right =
    (h Y₁).lift (G.coneAt Y₁) ≫
      (CostructuredArrow.left E).map φ ≫ (CostructuredArrow.left E).map X.hom ≫ (CostructuredArrow.hom E).app X.right
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
X : C
⊢ (((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
          CostructuredArrow.hom E).app
      X =
    (CostructuredArrow.hom G).app X

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
X : C
⊢ (h (L.obj X)).lift (G.coneAt (L.obj X)) ≫ (CostructuredArrow.hom E).app X = (CostructuredArrow.hom G).app X
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : CostructuredArrow L Y₁
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y₁ ⋙ F).map φ ≫
      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₂) =
    colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₁) ≫
      ((const (CostructuredArrow L Y₁)).obj (colimit (CostructuredArrow.proj L Y₂ ⋙ F))).map φ

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : CostructuredArrow L Y₁
φ : g₁ ⟶ g₂
⊢ F.map φ.left ≫ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₂) =
    colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₁)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : StructuredArrow Y₂ L
φ : g₁ ⟶ g₂
⊢ ((const (StructuredArrow Y₂ L)).obj (limit (StructuredArrow.proj Y₁ L ⋙ F))).map φ ≫
      limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₂) =
    limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₁) ≫ (StructuredArrow.proj Y₂ L ⋙ F).map φ

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : StructuredArrow Y₂ L
φ : g₁ ⟶ g₂
⊢ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₂) =
    limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g₁) ≫ F.map φ.right
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) (OverArrows.val p.snd)) = p.fst
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
⊢ A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map f ≫ g)).down

Tactic:
have := (g.naturality_apply f.op) (ULift.up (𝟙 Y))

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
this :
  (hom (g.app (op X))) ((hom ((uliftYoneda.{max w v₂, v₁, u₁}.obj Y).map f.op)) { down := 𝟙 Y }) =
    (hom (((restrictedULiftYoneda A).obj E).map f.op)) ((hom (g.app (op Y))) { down := 𝟙 Y })
⊢ A.map f ≫ (uliftYonedaEquiv g).down = (uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map f ≫ g)).down
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
y : StructuredArrow F₀ ((whiskeringLeft C C H).obj (𝟭 C))
m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ y
x : C
⊢ (StructuredArrow.Hom.right m).app x =
    (StructuredArrow.Hom.right (StructuredArrow.homMk (α.inv ≫ y.hom ≫ y.right.leftUnitor.hom) ⋯)).app x

Tactic:
simpa using

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
y : StructuredArrow F₀ ((whiskeringLeft C C H).obj (𝟭 C))
m : (LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom) ⟶ y
x : C
⊢ (StructuredArrow.Hom.right m).app x = α.inv.app x ≫ y.hom.app x
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow ((whiskeringLeft C C H).obj (𝟭 C)) F₀
m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)
x : C
⊢ m.left.app x = (CostructuredArrow.homMk (y.left.leftUnitor.inv ≫ y.hom ≫ α.inv) ⋯).left.app x

Tactic:
simpa using

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ≌ D
F₀ : C ⥤ H
F₁ : D ⥤ H
α : L.functor ⋙ F₁ ≅ F₀
y : CostructuredArrow ((whiskeringLeft C C H).obj (𝟭 C)) F₀
m : y ⟶ (RightExtension.postcomp₁ L.functor L.functor.leftUnitor.hom F₀).obj (RightExtension.mk F₁ α.hom)
x : C
⊢ m.left.app x = y.hom.app x ≫ α.inv.app x
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
Z : Cᵒᵖ
f : (yoneda.obj X).obj Z
⊢ (hom
          ((StructuredArrow.hom
                  (Functor.LeftExtension.mk (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)) (uliftYonedaMap F X)) ≫
                ((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).map
                  (uliftYonedaEquiv.symm (uliftYonedaEquiv (StructuredArrow.hom Y)))).app
            Z)).toFun
      { down := f } =
    (hom ((StructuredArrow.hom Y).app Z)).toFun { down := f }

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (uliftYoneda.{max w v₂, v₁, u₁}.obj X)
Z : Cᵒᵖ
f : (yoneda.obj X).obj Z
⊢ (hom ((StructuredArrow.right Y).map (F.map f).op)) ((hom ((StructuredArrow.hom Y).app (op X))) { down := 𝟙 X }) =
    (hom ((StructuredArrow.hom Y).app Z)) { down := f }
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsSeparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsSeparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op Y
⊢ f ≫ h.unop = g ≫ h.unop
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : P G
h : unop X ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : P G
h : unop X ⟶ G
⊢ h.op ≫ f = h.op ≫ g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCoseparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : P.op G
h : op X ⟶ G
⊢ (f.op ≫ h).unop = (g.op ≫ h).unop

Tactic:
simpa using

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.op.IsCoseparating
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : P.op G
h : op X ⟶ G
⊢ h.unop ≫ f = h.unop ≫ g
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : G ⟶ unop Y
⊢ (h ≫ f.unop).op = (h ≫ g.unop).op

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : G ⟶ unop Y
⊢ f ≫ h.op = g ≫ h.op
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ uliftYonedaEquiv (uliftYoneda.{max v₂ w, v₁, u₁}.map (↑f).unop ≫ uliftYonedaEquiv.symm x.snd) =
    uliftYonedaEquiv (uliftYonedaEquiv.symm y.snd)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ (hom (P.map ↑f)) x.snd = y.snd
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso (Hom.right f)).hom) ≫ T.map (Hom.right f) = P.hom ≫ T.map (Hom.right f)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ q ≫ T.map (Subobject.mk (Hom.right f)).arrow = A.hom