mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYoneda.{w, v, u}.map (↑(unop f)).unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop Y✝).snd)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop X✝).snd)).hom

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYoneda.{w, v, u}.map (↑(unop f)).unop ≫ uliftYonedaEquiv.symm (unop Y✝).snd = uliftYonedaEquiv.symm (unop X✝).snd
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map f.left.op)) (F.elementsMk (op Y✝.left) (uliftYonedaEquiv Y✝.hom)).snd =
    (F.elementsMk (op X✝.left) (uliftYonedaEquiv X✝.hom)).snd

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map f.left.op)) (uliftYonedaEquiv Y✝.hom) = uliftYonedaEquiv X✝.hom
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
x : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom
        (F.map
          (Iso.refl
              (F.elementsMk
                  (op
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).left)
                  (uliftYonedaEquiv
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).hom)).fst).hom))
      (F.elementsMk
          (op
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).left)
          (uliftYonedaEquiv
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).hom)).snd =
    (unop x).snd

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
x : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (F.map (𝟙 (unop x).1))) (uliftYonedaEquiv (uliftYonedaEquiv.symm (unop x).snd)) = (unop x).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (fiberwiseColimit G).map f ≫ colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ ((const C).obj c.pt).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (colimMap (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F x✝) G).hom) ≫
        colimit.pre (Grothendieck.ι F x✝ ⋙ G) (F.map f).toFunctor) ≫
      colimit.desc (Grothendieck.ι F x✝ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝) c) =
    colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c✝ : Cocone G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
⊢ (coconeFiberwiseColimitOfCocone c✝).ι.app c ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c✝ : Cocone G
hc : IsColimit c✝
s : Cocone (fiberwiseColimit G)
c : C
⊢ colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    s.ι.app c
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom =
    (Cat.Hom.isoMk (mapComp (f✝ ≫ g✝).toFunctor h✝.toFunctor)).hom ≫
      Bicategory.whiskerRight (Cat.Hom.isoMk (mapComp f✝.toFunctor g✝.toFunctor)).hom (prelaxfunctor.map h✝) ≫
        (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫
          Bicategory.whiskerLeft (prelaxfunctor.map f✝) (Cat.Hom.isoMk (mapComp g✝.toFunctor h✝.toFunctor)).inv ≫
            (Cat.Hom.isoMk (mapComp f✝.toFunctor (g✝ ≫ h✝).toFunctor)).inv

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ c✝ d✝ : Cat
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
⊢ NatTrans.toCatHom₂ (map₂ (f✝.toFunctor.associator g✝.toFunctor h✝.toFunctor).hom) =
    NatTrans.toCatHom₂ (mapComp (f✝.toFunctor ⋙ g✝.toFunctor) h✝.toFunctor).hom ≫
      Bicategory.whiskerRight (NatTrans.toCatHom₂ (mapComp f✝.toFunctor g✝.toFunctor).hom) (map h✝.toFunctor).toCatHom ≫
        (Bicategory.associator (map f✝.toFunctor).toCatHom (map g✝.toFunctor).toCatHom
              (map h✝.toFunctor).toCatHom).hom ≫
          Bicategory.whiskerLeft (map f✝.toFunctor).toCatHom
              (NatTrans.toCatHom₂ (mapComp g✝.toFunctor h✝.toFunctor).inv) ≫
            NatTrans.toCatHom₂ (mapComp f✝.toFunctor (g✝.toFunctor ⋙ h✝.toFunctor)).inv
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F G : C ⥤ Cat
H : C ⥤ Cat
α : F ⟶ G
X✝ Y✝ : Grothendieck (F ⋙ Cat.asSmallFunctor)
f : X✝ ⟶ Y✝
⊢ (map (whiskerRight α Cat.asSmallFunctor)).map f ≫ (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj Y✝)).hom =
    (Iso.refl ((map (whiskerRight α Cat.asSmallFunctor)).obj X✝)).hom ≫
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).map f

Tactic:
by
      fapply Grothendieck.ext
      · simp [compAsSmallFunctorEquivalenceInverse]
      · simp only [compAsSmallFunctorEquivalence_functor, compAsSmallFunctorEquivalence_inverse,
        comp_obj, compAsSmallFunctorEquivalenceInverse_obj_base, map_obj_base,
        compAsSmallFunctorEquivalenceFunctor_obj_base, Cat.asSmallFunctor_obj, Cat.of_α,
        Iso.refl_hom, Functor.comp_map, comp_base, id_base,
        compAsSmallFunctorEquivalenceInverse_map_base, map_map_base,
        compAsSmallFunctorEquivalenceFunctor_map_base, Cat.asSmallFunctor_map, toCatHom_toFunctor,
        map_obj_fiber, whiskerRight_app, AsSmall.down_obj, AsSmall.up_obj_down,
        compAsSmallFunctorEquivalenceInverse_obj_fiber,
        compAsSmallFunctorEquivalenceFunctor_obj_fiber, comp_fiber, map_map_fiber, AsSmall.down_map,
        down_comp, eqToHom_down, AsSmall.up_map_down, map_comp, eqToHom_map, id_fiber,
        Category.assoc, eqToHom_trans_assoc, compAsSmallFunctorEquivalenceInverse_map_fiber,
        compAsSmallFunctorEquivalenceFunctor_map_fiber, eqToHom_comp_iff, comp_eqToHom_iff]
        simp only [conj_eqToHom_iff_heq']
        rw [G.map_id]
        simp

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ (𝟭 (Grothendieck (G ⋙ typeToCat))).map { base := base, fiber := { down := { down := f } } } ≫
      (casesOn { base := base✝, fiber := { as := as✝ } } fun base fiber ↦
          Discrete.casesOn fiber fun as ↦
            Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom =
    (casesOn { base := base✝¹, fiber := { as := as✝¹ } } fun base fiber ↦
          Discrete.casesOn fiber fun as ↦
            Iso.refl ((𝟭 (Grothendieck (G ⋙ typeToCat))).obj { base := base, fiber := { as := as } })).hom ≫
      (grothendieckTypeToCatFunctor G ⋙ grothendieckTypeToCatInverse G).map
        { base := base, fiber := { down := { down := f } } }

Tactic:
dsimp at *

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
base✝¹ : C
as✝¹ : G.obj base✝¹
base✝ : C
as✝ : G.obj base✝
base : { base := base✝¹, fiber := { as := as✝¹ } }.base ⟶ { base := base✝, fiber := { as := as✝ } }.base
f :
  (((G ⋙ typeToCat).map base).toFunctor.obj { base := base✝¹, fiber := { as := as✝¹ } }.fiber).as =
    { base := base✝, fiber := { as := as✝ } }.fiber.as
⊢ { base := base, fiber := { down := { down := f } } } ≫ 𝟙 { base := base✝, fiber := { as := as✝ } } =
    𝟙 { base := base✝¹, fiber := { as := as✝¹ } } ≫
      (grothendieckTypeToCatInverse G).map
        ((grothendieckTypeToCatFunctor G).map { base := base, fiber := { down := { down := f } } })
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : ⟨fst✝¹, snd✝¹⟩.fst ⟶ ⟨fst✝, snd✝⟩.fst
e : (ConcreteCategory.hom (G.map f)) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ (grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).map ⟨f, e⟩ ≫
      (Sigma.casesOn (motive := fun t ↦
          ⟨fst✝, snd✝⟩ = t →
            ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst✝, snd✝⟩ ≅
              (𝟭 G.Elements).obj ⟨fst✝, snd✝⟩))
          ⟨fst✝, snd✝⟩
          (fun fst snd h ↦
            ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
          ⋯).hom =
    (Sigma.casesOn (motive := fun t ↦
          ⟨fst✝¹, snd✝¹⟩ = t →
            ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst✝¹, snd✝¹⟩ ≅
              (𝟭 G.Elements).obj ⟨fst✝¹, snd✝¹⟩))
          ⟨fst✝¹, snd✝¹⟩
          (fun fst snd h ↦
            ⋯ ▸ Iso.refl ((grothendieckTypeToCatInverse G ⋙ grothendieckTypeToCatFunctor G).obj ⟨fst, snd⟩))
          ⋯).hom ≫
      (𝟭 G.Elements).map ⟨f, e⟩

Tactic:
dsimp at *

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
fst✝¹ : C
snd✝¹ : G.obj fst✝¹
fst✝ : C
snd✝ : G.obj fst✝
f : ⟨fst✝¹, snd✝¹⟩.fst ⟶ ⟨fst✝, snd✝⟩.fst
e : (ConcreteCategory.hom (G.map f)) ⟨fst✝¹, snd✝¹⟩.snd = ⟨fst✝, snd✝⟩.snd
⊢ (grothendieckTypeToCatFunctor G).map ((grothendieckTypeToCatInverse G).map ⟨f, e⟩) ≫
      𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst✝, snd✝⟩)) =
    𝟙 ((grothendieckTypeToCatFunctor G).obj ((grothendieckTypeToCatInverse G).obj ⟨fst✝¹, snd✝¹⟩)) ≫ ⟨f, e⟩
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) =
    (G.map (homToLift F X) ≫ c.ι.app (lift F X)) ≫ ((const D).obj c.pt).map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = (G.map (homToLift F X) ≫ c.ι.app (lift F X)) ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
d : ↑(F.obj c)
⊢ { base := 𝟙 { base := c, fiber := d }.base, fiber := eqToHom ⋯ ≫ 𝟙 d } = 𝟙 { base := c, fiber := d }

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
d : ↑(F.obj c)
⊢ { base := 𝟙 c, fiber := eqToHom ⋯ ≫ 𝟙 d } = 𝟙 { base := c, fiber := d }
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ { base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f ≫ g }.fiber =
    ({ base := 𝟙 { base := c, fiber := X✝ }.base, fiber := eqToHom ⋯ ≫ f } ≫
        { base := 𝟙 { base := c, fiber := Y✝ }.base, fiber := eqToHom ⋯ ≫ g }).fiber

Tactic:
simp only [comp_base, ← Category.assoc, eqToHom_trans, comp_fiber, Functor.map_comp,
      eqToHom_map]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eqToHom ⋯ ≫ f) ≫ g = ((eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) ≫ eqToHom ⋯) ≫ g
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₂ ≫ c.ι.app X₂ →
        G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map k₁ ≫ c.ι.app X₁

pp: case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app ?X₀

pp: case X₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ C

pp: case k₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ X ⟶ F.obj ?X₀

Tactic:
· intro Z₁ Z₂ k₁ k₂ g a z
              rw [← a, Functor.map_comp, Category.assoc, ← Functor.comp_map, c.w] at z
              rw [z]

Goal state after:
case z
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ G.map f ≫ G.map (homToLift F Y) ≫ c.ι.app (lift F Y) = G.map ?k₀ ≫ c.ι.app ?X₀

case X₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ C

case k₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ X ⟶ F.obj ?X₀
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ ((𝟭 (C ⥤ D)).obj (incl ⋙ F)).map f ≫ F.map (starTerminal.from (of y)) =
    F.map (starTerminal.from (of x)) ≫ ((Functor.const C).obj (F.obj star)).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (incl.map f) ≫ F.map (starTerminal.from (of y)) = F.map (starTerminal.from (of x)) ≫ 𝟙 (F.obj star)
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
j : J
⊢ s.π.app (Classical.arbitrary J) ≫ (constCone J X).π.app j = s.π.app j

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cone ((Functor.const J).obj X)
j : J
⊢ s.π.app (Classical.arbitrary J) ≫ 𝟙 X = s.π.app j
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j : J
⊢ (constCocone J X).ι.app j ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
dsimp

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
X : C
inst✝ : IsConnected J
s : Cocone ((Functor.const J).obj X)
j : J
⊢ 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j
Module: Mathlib.CategoryTheory.EffectiveEpi.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
B : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
inst✝¹ : HasCoproduct X
inst✝ : IsIso (Sigma.desc π)
W✝ : C
e : (a : α) → X a ⟶ W✝
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂
a : α
this : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom
⊢ Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom ≫ (asIso (Sigma.desc π)).inv ≫ Sigma.desc e = e a

Tactic:
simp only [asIso_hom, asIso_inv, IsIso.hom_inv_id_assoc, colimit.ι_desc,
      Cofan.mk_ι_app]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ ((const D).obj c.pt).map f ≫ c.π.app (lift F Y) ≫ G.map (homToLift F Y) =
    (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ 𝟙 c.pt ≫ c.π.app (lift F Y) ≫ G.map (homToLift F Y) = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (extendCone.obj c).π.app Y = c.π.app X ≫ G.map f

Tactic:
apply induction (k₀ := f) (z := rfl) F fun Z g =>
    c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ → c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f → c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ → c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f → c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ ((Functor.const C).obj (F.obj star)).map f ≫ F.map (starInitial.to (of y)) =
    F.map (starInitial.to (of x)) ≫ ((𝟭 (C ⥤ D)).obj (incl ⋙ F)).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ 𝟙 (F.obj star) ≫ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x)) ≫ F.map (incl.map f)
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ 𝟙 (F.obj star) ≫ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x)) ≫ F.map (incl.map f)

Tactic:
rw [Category.id_comp, ← F.map_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x) ≫ incl.map f)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case hy
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := ⋯
RXm : Type (max w₁ 0) := ⋯
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := ⋯
g' : Fin n → RXn := ⋯
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := ⋯
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
hx✝ : aeval_h.toRingHom x₁ + y₁ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : aeval_h.toRingHom x₁ + y₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
hy✝ : aeval_h.toRingHom x₂ + y₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₂ : aeval_h.toRingHom x₂ + y₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ y₁ * aeval_h.toRingHom x₂ + (aeval_h.toRingHom x₁ + y₁) * y₂ ∈ (Ideal.span s').toAddSubmonoid

Tactic:
· exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
s : Cofork (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m✝ : (Cofork.ofπ f ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ f ⋯).π ≫ m✝ = s.π
⊢ m✝ = g

Tactic:
rwa [← cancel_epi f, hg]

Goal state after: