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

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
← map_comp e.inverse,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map
    (e.functor.map (e.unit.app (e.inverse.obj Y)) ≫
      e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

Tactic:
← map_comp e.inverse,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)) ≫ e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.counit.app Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
← map_comp e.inverse,

Goal state after:
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)) ≫ e.functor.map (e.inverse.map (e.counit.app Y)))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.obj X i = f'.obj X i

Tactic:
have := congr_obj h X

Goal state after:
case h_obj
I : Type w₀
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
A : Type u₃
inst✝ : Category.{v₃, u₃} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X
⊢ f.obj X i = f'.obj X i
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ W.map F f✝ ↔ (W.strictMap F).isoClosure f✝

Tactic:
refine ⟨fun ⟨_, _, f, hf, hf'⟩ ↦ ⟨_, _, _, ⟨hf⟩, hf'⟩, fun ⟨_, _, f, hf, hf'⟩ ↦ ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
W : MorphismProperty C
F : C ⥤ D
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
x✝ : (W.strictMap F).isoClosure f✝
w✝¹ w✝ : D
f : w✝¹ ⟶ w✝
hf : W.strictMap F f
hf' : Nonempty (Arrow.mk f ≅ Arrow.mk f✝)
⊢ W.map F f✝
Module: Mathlib.CategoryTheory.Types.Basic

Goal state before:
pp: case mp
X Y : Type u
f : X → Y
⊢ Mono (↾f) → Function.Injective f

pp: case mpr
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)

Tactic:
· intro H x x' h
    rw [← homOfElement_eq_iff] at h ⊢
    exact (cancel_mono (ofHom f)).mp h

Goal state after:
case mpr
X Y : Type u
f : X → Y
⊢ Function.Injective f → Mono (↾f)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ m = homOfCocone h s

Tactic:
rw [← homOfCocone_coconeOfHom h m]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ homOfCocone h (coconeOfHom h m) = homOfCocone h s
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation Cᵒᵖ (Type v₁) ⋙
            (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f

Tactic:
ext F g

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type v₁
g : ((yoneda.op ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((yoneda.op ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (yonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation Cᵒᵖ (Type v₁) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                  f).app
            F)).toFun
      g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ (uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
      (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
            (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
              uliftFunctor.{u₁, max v₁ w}).map
        f

Tactic:
ext F g

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type (max w v₁)
g : ((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((uliftYoneda.{w, v₁, u₁}.op ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (uliftYonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                      (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).map
                  f).app
            F)).toFun
      g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
⊢ (coyoneda.rightOp ⋙ coyoneda).map f ≫
      (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation C (Type v₁) ⋙
            (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
        f

Tactic:
ext F g

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type v₁) ⋙
                      (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                  f).app
            F)).toFun
      g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
⊢ (uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
      (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
      (evaluation C (Type (max v₁ w)) ⋙
            (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
              uliftFunctor.{u₁, max v₁ w}).map
        f

Tactic:
ext F g

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type (max v₁ w)) ⋙
                      (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).map
                  f).app
            F)).toFun
      g
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y

Tactic:
simp only [Functor.comp_map]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (lift F c) ≫ G.map (π F j✝) = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Tactic:
← G.map_comp,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (lift F c ≫ π F j✝) = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝

Tactic:
limit.post_π

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (pre F E) ≫ G.map (π (E ⋙ F) j✝) = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝

Tactic:
← G.map_comp,

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (pre F E ≫ π (E ⋙ F) j✝) = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (π F (E.obj j✝)) = post F G ≫ π (F ⋙ G) (E.obj j✝)

Tactic:
limit.post_π

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (π F (E.obj j✝)) = G.map (π F (E.obj j✝))
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (ι F j✝) ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
← G.map_comp,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (ι F j✝ ≫ desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι (E ⋙ F) j) ≫ G.map (pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G

Tactic:
← G.map_comp,

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι (E ⋙ F) j ≫ pre F E) = ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E ≫ post F G
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₁ = colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
ext1
  simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g = lift f fs w

Tactic:
apply
    (limit.isLimit (WidePullbackShape.wideCospan B objs arrows)).uniq
      (WidePullbackShape.mkCone f fs <| w)

Goal state after:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ ∀ (j : WidePullbackShape J),
    g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app j = (WidePullbackShape.mkCone f fs w).π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
j : J
⊢ ι arrows j ≫ desc f fs w = fs j

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_ι_app]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
⊢ head arrows ≫ desc f fs w = f

Tactic:
simp only [colimit.ι_desc, WidePushoutShape.mkCocone_ι_app]

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

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom ⋯

Tactic:
obtain rfl := Subsingleton.allEq b default
  symm
  simp [← Iso.comp_inv_eq]

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
⊢ x✝¹ = x✝

Tactic:
refine limit.hom_ext fun j => ?_
    simpa using h =≫ Pi.π _ j

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ s.ι.app none ≫ i.hom = t.ι.app none

Tactic:
← h₁,

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero
h₂ : F.map fst ≫ t.ι.app left = t.ι.app zero
⊢ (F.map fst ≫ s.ι.app left) ≫ i.hom = t.ι.app none
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
⊢ W₁.comp W₂ = ⊤

Tactic:
ext X Y f

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f ↔ ⊤ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }).hom ≫
      { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
                isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }.cone.π.app
        WalkingCospan.right =
    limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case e'_5.e'_6
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }).hom ≫
      { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
                isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }.cone.π.app
        WalkingCospan.right =
    limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right
e_3✝ : pullback i (f ≫ i) = limit (cospan (𝟙 Z ≫ i) (f ≫ i))
⊢ i = 𝟙 Z ≫ i

Tactic:
exact (Category.id_comp _).symm

Goal state after: