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
s t : CostructuredArrow yoneda A
p : OverArrows s.hom t.hom
⊢ yoneda.map p.val ≫ s.hom = t.hom

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
G : D ⥤ H
β : G ⟶ F'
⊢ L.whiskerLeft ((fun β ↦ F'.liftOfIsRightKanExtension α G β) ((fun β ↦ L.whiskerLeft β ≫ α) β)) ≫ α =
    L.whiskerLeft β ≫ α

Tactic:
simp

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
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 ≫
      (((whiskeringLeft C D H).obj L).map φ.left ≫ CostructuredArrow.hom E').app G.right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α

Tactic:
intro
    refine isRightKanExtension_of_iso e.symm α' α ?_
    rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]

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
E E' : L.RightExtension F
e : E ≅ E'
h : E.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)) h) =
    h

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝¹ : F'.IsRightKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : L ⋙ G' ⟶ G
inst✝ : G'.IsRightKanExtension β
⊢ L.whiskerLeft (G'.liftOfIsRightKanExtension β F' (α ≫ i.hom) ≫ F'.liftOfIsRightKanExtension α G' (β ≫ i.inv)) ≫ α =
    L.whiskerLeft (𝟙 F') ≫ α

Tactic:
simp

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
E E' : L.RightExtension F
e : E ≅ E'
h : E'.IsPointwiseRightKanExtension
⊢ (fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y))
      ((fun h Y ↦ (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)) h) =
    h

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝¹ : F'.IsRightKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : L ⋙ G' ⟶ G
inst✝ : G'.IsRightKanExtension β
⊢ L.whiskerLeft (F'.liftOfIsRightKanExtension α G' (β ≫ i.inv) ≫ G'.liftOfIsRightKanExtension β F' (α ≫ i.hom)) ≫ β =
    L.whiskerLeft (𝟙 G') ≫ β

Tactic:
simp

Goal state after:
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
F : C ⥤ H
⊢ 𝟙 (L ⋙ L.ran.obj F) ≫ L.ranCounit.app F = L.ranCounit.app F

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₁ (η ≫ μ) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₁ μ ∘ map₁ η) x✝²).fst.app x✝¹)).toFun x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (H.map (eqToHom ⋯))) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Tactic:
simp

Goal state after:
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
G : D ⥤ H
⊢ L.whiskerLeft ((L.ranAdjunction H).unit.app G) ≫ L.ranCounit.app (L ⋙ G) = 𝟙 (L ⋙ G)

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
G : D ⥤ H
β : F' ⟶ G
⊢ α ≫ L.whiskerLeft ((fun β ↦ F'.descOfIsLeftKanExtension α G β) ((fun β ↦ α ≫ L.whiskerLeft β) β)) =
    α ≫ L.whiskerLeft β

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (𝟙 X) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((id x✝²).fst.app x✝¹)).toFun x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ α ≫ L.whiskerLeft (F'.descOfIsLeftKanExtension α G' (i.hom ≫ β) ≫ G'.descOfIsLeftKanExtension β F' (i.inv ≫ α)) =
    α ≫ L.whiskerLeft (𝟙 F')

Tactic:
simp

Goal state after:
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'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝¹ : F'.IsLeftKanExtension α
G : C ⥤ H
i : F ≅ G
G' : D ⥤ H
β : G ⟶ L ⋙ G'
inst✝ : G'.IsLeftKanExtension β
⊢ β ≫ L.whiskerLeft (G'.descOfIsLeftKanExtension β F' (i.inv ≫ α) ≫ F'.descOfIsLeftKanExtension α G' (i.hom ≫ β)) =
    β ≫ L.whiskerLeft (𝟙 G')

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝² : YonedaCollection F Z
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (f ≫ g) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₂ F f ∘ map₂ F g) x✝²).fst.app x✝¹)).toFun x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ G f (map₁ η p)).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((map₁ η (map₂ F f p)).fst.app x✝¹)).toFun x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯))) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
x✝ : (yonedaCollectionPresheaf A F).obj X✝
⊢ (ConcreteCategory.hom ((yonedaCollectionPresheaf A F).map f✝ ≫ ↾YonedaCollection.map₁ η)).toFun x✝ =
    (ConcreteCategory.hom (↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f✝)).toFun x✝

Tactic:
simp

Goal state after:
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
x : F.obj (op X)
⊢ (ConcreteCategory.hom
        (η.app
          (op (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).left)))
      x =
    yonedaEquiv (unop (op (CostructuredArrow.mk (yonedaEquiv.symm ((ConcreteCategory.hom (η.app (op X))) x))))).hom

Tactic:
simp

Goal state after:
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
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ YonedaCollection.fst (counitForward F s x).val = s.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ YonedaCollection.fst (counitForward G (unop s) ((ConcreteCategory.hom (η.app s)) x)).val =
    YonedaCollection.fst ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val) =
    YonedaCollection.snd (counitForward G (unop s) ((ConcreteCategory.hom (η.app s)) x)).val

Tactic:
simp

Goal state after:
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 t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ yoneda.map f.unop.left ≫ (unop t).hom = (unop s).hom

Tactic:
simp

Goal state after:
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ YonedaCollection.fst (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val =
    YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val

Tactic:
simp

Goal state after:
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op.unop = (f ≫ eqToHom ⋯).unop

Tactic:
simp

Goal state after:
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (unop t).hom)
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ YonedaCollection.fst (counitForward F (unop t) x).val = t.1.hom

Tactic:
simp

Goal state after:
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
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ YonedaCollection.fst ((counitForward F s ∘ counitBackward F s) p).val = YonedaCollection.fst (id p).val

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
⊢ ∀ [inst : Mono f], ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
hf

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
⊢ ∀ [inst : Mono f], ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
hf

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Subobject X ≃o (Subobject (op X))ᵒᵈ

Tactic:
by
  refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_
  · change (cokernelOrderHom X).comp (kernelOrderHom X) = _
    refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
    intro A f hf
    dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
      cokernelOrderHom_coe, OrderHom.id_coe, id]
    refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
    · exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op
    · exact (cokernel.desc _ _ (kernel.condition f.unop)).op
    · rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
      simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
        comp_epiDesc, Category.comp_id]
    · simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
        cokernel.π_desc, Category.comp_id]
    · exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])
  · change (kernelOrderHom X).comp (cokernelOrderHom X) = _
    refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
    intro A f hf
    dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
      kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op]
    refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
    · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
    · exact kernel.lift _ _ (cokernel.condition f)
    · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
        Category.id_comp]
    · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
    · simp only [monoLift_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case e'_3.e'_2
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 (yoneda.obj X)
Z : Cᵒᵖ
f : (yoneda.obj X).obj Z
⊢ f = (hom ((yoneda.obj X).map (Quiver.Hom.op f))) (𝟙 X)

Tactic:
simp

Goal state after:
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 Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
⊢ ∀ [inst : Mono f] [inst_1 : Mono g] (i : P ≅ Q),
    i.hom ≫ g = f → Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)

Tactic:
hf

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 Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
⊢ ∀ [inst : Mono g] (i : P ≅ Q), i.hom ≫ g = f → Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)
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
⊢ ∀ [inst : Mono f] {q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))}
    (hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f

Tactic:
hf

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),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f
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
⊢ Hom.right ((isoMk (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)) ⋯).hom ≫ f) =
    Hom.right (homMk (projectSubobject (Subobject.mk f)).arrow hq)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
⊢ (∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h) → IsIso f

Tactic:
hf

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
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 Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
⊢ ∀ [inst : Mono f] [inst_1 : Mono g],
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g

Tactic:
hf

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 Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
⊢ ∀ [inst : Mono g],
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
          (Subobject.mk f) ≤
        { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯,
            right_inv := ⋯ }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_2
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 Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectSubobject P, ⋯⟩, invFun := fun P ↦ liftSubobject ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
⊢ homMk (Subobject.ofMkLEMk (Hom.right (MonoOver.mk f).arrow) (Hom.right (MonoOver.mk g).arrow) h) ⋯ ≫ g = f

Tactic:
simp

Goal state after: