mathlib-initiative/mathlib-tactics huggingface dataset:
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
p q : YonedaCollection F X
h : p.fst = q.fst
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) q.snd = p.snd
⊢ p = q

Tactic:
rcases p with ⟨p, p'⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
q : YonedaCollection F X
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = q.fst
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) q.snd = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = q
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
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (E'.coneAt Y).π.app G = (E.coneAt Y).π.app G

Tactic:
dsimp

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
Y : D
E E' : L.RightExtension F
φ : E ⟶ E'
G : StructuredArrow Y L
⊢ φ.left.app Y ≫ (CostructuredArrow.left E').map G.hom ≫ (CostructuredArrow.hom E').app G.right =
    (CostructuredArrow.left E).map G.hom ≫ (CostructuredArrow.hom E).app G.right
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
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ ((L.ran ⋙ lim).map f ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom) ≫ limit.π Y✝ i =
    (((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ lim.map f) ≫ limit.π Y✝ i

Tactic:
dsimp

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
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ (limMap (L.ran.map f) ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom) ≫ limit.π Y✝ i =
    (((L.ran.obj X✝).limitIsoOfIsRightKanExtension (L.ranCounit.app X✝)).hom ≫ limMap f) ≫ limit.π Y✝ i
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 : D
j : CostructuredArrow L Y
⊢ colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))

Tactic:
dsimp

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 : D
j : CostructuredArrow L Y
⊢ colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y ⋙ F) ((CostructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L Y ⋙ F))
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₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }

Tactic:
dsimp

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₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }
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
X : D
j : CostructuredArrow L X
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt).hom =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j

Tactic:
dsimp

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
X : D
j : CostructuredArrow L X
⊢ colimit.ι (CostructuredArrow.proj L X ⋙ F) j ≫ 𝟙 (colimit (CostructuredArrow.proj L X ⋙ F)) =
    colimit.ι (CostructuredArrow.proj L (L.obj j.left) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj j.left))) ≫
      colimit.desc (CostructuredArrow.proj L (L.obj j.left) ⋙ F)
        { pt := colimit (CostructuredArrow.proj L X ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L X ⋙ F) ((CostructuredArrow.map j.hom).obj g),
              naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : Cᵒᵖ
p : YonedaCollection (restrictedYonedaObj η) (unop X)
⊢ (ConcreteCategory.hom (η.app X)) (unitForward η (unop X) p) = p.yonedaEquivFst

Tactic:
by
  simpa [unitForward] using! p.snd.app_val

Goal state after:
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 : D
j : StructuredArrow Y L
⊢ limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j

Tactic:
dsimp

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 : D
j : StructuredArrow Y L
⊢ limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j
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₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
        { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j =
    (limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₂ L ⋙ F) ((StructuredArrow.map f').obj g),
                naturality := ⋯ } }) ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j

Tactic:
dsimp

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₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
        { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j =
    (limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₁ L ⋙ F) ((StructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj Y₂ L ⋙ F) ((StructuredArrow.map f').obj g),
                naturality := ⋯ } }) ≫
      limit.π (StructuredArrow.proj Y₃ L ⋙ F) j
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
X : D
j : StructuredArrow X L
⊢ (limit.cone (StructuredArrow.proj X L ⋙ F)).π.app j =
    (Iso.refl (limit.cone (StructuredArrow.proj X L ⋙ F)).pt).hom ≫
      ((RightExtension.mk (L.pointwiseRightKanExtension F) (L.pointwiseRightKanExtensionCounit F)).coneAt X).π.app j

Tactic:
dsimp

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
X : D
j : StructuredArrow X L
⊢ limit.π (StructuredArrow.proj X L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj X L ⋙ F)) ≫
      limit.lift (StructuredArrow.proj (L.obj j.right) L ⋙ F)
          { pt := limit (StructuredArrow.proj X L ⋙ F),
            π :=
              { app := fun g ↦ limit.π (StructuredArrow.proj X L ⋙ F) ((StructuredArrow.map j.hom).obj g),
                naturality := ⋯ } } ≫
        limit.π (StructuredArrow.proj (L.obj j.right) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj j.right)))
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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
⊢ a = default

Tactic:
dsimp

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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
⊢ a = StructuredArrow.homMk (hb.desc u) ⋯
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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right a))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫
              ((whiskeringLeft D D' H).obj L').map
                (StructuredArrow.Hom.right (StructuredArrow.homMk (hb.desc u) ⋯)))).app
      t

Tactic:
dsimp

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
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
a : (precomp₂ L' α).obj b ⟶ y
t : C
⊢ α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (StructuredArrow.Hom.right a).app (L'.obj (L.obj t)) =
    α.app t ≫ (StructuredArrow.hom b).app (L.obj t) ≫ (hb.desc u).app (L'.obj (L.obj t))
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm x)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ uliftYonedaEquiv.symm x = uliftYonedaEquiv.symm ((hom (P.map g)) x)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

Tactic:
simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
        cokernel.π_desc, Category.comp_id]

Goal state after:
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
φ : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x)) ⟶ CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ (hom (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) })).toFun x =
    (hom
          ((↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
            ((restrictedULiftYoneda A).obj E).map g)).toFun
      x

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
φ : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x)) ⟶ CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x))) } =
    { down := A.map g.unop ≫ f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm 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 : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A).map f ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down =
    (uliftYonedaEquiv (y.hom ≫ g)).down ≫
      ((Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ A.map f.left ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down = (uliftYonedaEquiv (y.hom ≫ g)).down ≫ 𝟙 E
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  (uliftYoneda.{max w v₂, v₁, u₁}.obj
        (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).obj
    Y
⊢ (hom
          ((uliftYoneda.{max w v₂, v₁, u₁}.map
                  (Iso.refl
                      (CostructuredArrow.mk
                          (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).hom ≫
                X.hom).app
            Y)).toFun
      x =
    (hom
          ((CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).hom.app
            Y)).toFun
      x

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  (uliftYoneda.{max w v₂, v₁, u₁}.obj
        (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).obj
    Y
⊢ (hom (X.hom.app Y)) { down := x.down ≫ 𝟙 X.left } =
    (hom (P.map x.down.op)) ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left })
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ (functorToRepresentables P).map f ≫ uliftYonedaEquiv.symm (unop x₂).snd =
    uliftYonedaEquiv.symm (unop x₁).snd ≫ ((Functor.const P.Elementsᵒᵖ).obj P).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop ≫ uliftYonedaEquiv.symm (unop x₂).snd =
    uliftYonedaEquiv.symm (unop x₁).snd ≫ 𝟙 P