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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
this : R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g)
⊢ iC.map
      ((Trans.trans
          (Trans.trans
            (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
              (adj.homEquiv (iC.obj X) (iD.obj Y)))
            ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
          hiC.homEquiv.symm)
        (f ≫ g)) =
    iC.map
      ((Trans.trans
            (Trans.trans
              (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
                (adj.homEquiv (iC.obj X) (iD.obj Y')))
              ((Iso.refl (iC.obj X)).homCongr (comm2.app Y')))
            hiC.homEquiv.symm)
          f ≫
        R.map g)

Tactic:
by
          simp [Trans.trans, this]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : MonoOver Y
this : Mono ((forget Y).obj g).hom
⊢ Mono ((Over.pullback f).obj ((forget Y).obj g)).hom

Tactic:
apply pullback.snd_of_mono

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelSubobjectMap (𝟙 (Arrow.mk f)) = 𝟙 (underlying.obj (kernelSubobject f))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
inst✝³ : HasZeroMorphisms C
f : X ⟶ Y
inst✝² : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝¹ : HasKernel f'
X'' Y'' : C
f'' : X'' ⟶ Y''
inst✝ : HasKernel f''
sq : Arrow.mk f ⟶ Arrow.mk f'
sq' : Arrow.mk f' ⟶ Arrow.mk f''
⊢ kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernel.map f f' sq.left sq.right ⋯ ≫ (kernelSubobjectIso f').inv = (kernelSubobjectIso f).inv ≫ kernelSubobjectMap sq

Tactic:
cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
F : C ⥤ D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.PreservesHomology
X Y : C
f : X ⟶ Y
hf : Epi f
⊢ Epi (F.map f)

Tactic:
let S := ShortComplex.mk f (0 : Y ⟶ Y) comp_zero
    exact ((S.map F).exact_iff_epi (by simp [S])).1
      (((S.exact_iff_epi rfl).2 hf).map F)

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ ⊥.arrow = 0

Tactic:
bot_arrow_eq_zero

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
⊢ ∀ (s : PullbackCone f.arrow g.arrow), (f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE f ⋯ = s.fst

Tactic:
cat_disch

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

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ (sInf s).arrow = f.arrow

Tactic:
· dsimp [sInf]
    rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : Subobject (underlying.obj Y)
⊢ (underlyingIso (Z.arrow ≫ Y.arrow)).hom ≫ Z.arrow = (↑((fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩) Z)).ofLE Y ⋯

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h : ⟨mk (W.arrow ≫ Y.arrow), ⋯⟩ ≤ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩
⊢ ((underlyingIso (W.arrow ≫ Y.arrow)).inv ≫
        (mk (W.arrow ≫ Y.arrow)).ofLE (mk (Z.arrow ≫ Y.arrow)) ⋯ ≫ (underlyingIso (Z.arrow ≫ Y.arrow)).hom) ≫
      Z.arrow =
    W.arrow

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
F : C ⥤ H
Y : D
⊢ ∀ {L L' : C ⥤ D} (e : L ≅ L'), L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y

Tactic:
suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y],
      HasPointwiseRightKanExtensionAt L' F Y from
    fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
F : C ⥤ H
Y : D
⊢ ∀ ⦃L L' : C ⥤ D⦄ (x : L ≅ L') [L.HasPointwiseRightKanExtensionAt F Y], L'.HasPointwiseRightKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).obj s).map f ≫
        (OverArrows.costructuredArrowIso s (unop Y)).hom =
      (OverArrows.costructuredArrowIso s (unop X)).hom ≫ (yoneda.obj s).map f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : CostructuredArrow yoneda A} (f : X ⟶ Y),
    (CostructuredArrow.toOver yoneda A ⋙ restrictedYoneda A).map f ≫
        (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso Y (unop x)) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ OverArrows.costructuredArrowIso X (unop x)) ⋯).hom ≫ yoneda.map f

Tactic:
cat_disch

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 Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ (ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g f).op)) ((ConcreteCategory.hom (F.map (eqToHom ⋯))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp g' f).op)) x)

Tactic:
cat_disch

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.ran.obj F).IsRightKanExtension (L.ranCounit.app F)

Tactic:
dsimp [ran, ranCounit]
  infer_instance

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
⊢ Function.RightInverse (fun β ↦ F'.liftOfIsRightKanExtension α G β) fun β ↦ L.whiskerLeft β ≫ α

Tactic:
cat_disch

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
⊢ map₁ (𝟙 F) = id

Tactic:
cat_disch

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
⊢ Function.RightInverse (fun β ↦ F'.descOfIsLeftKanExtension α G β) fun β ↦ α ≫ L.whiskerLeft β

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {Y Z : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (g : Y ⟶ Z),
    (yonedaCollectionFunctor A).map g ≫ yonedaCollectionPresheafToA Z = yonedaCollectionPresheafToA Y

Tactic:
cat_disch

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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ yonedaCollectionPresheafMap₁ η ≫ yonedaCollectionPresheafToA G = yonedaCollectionPresheafToA F

Tactic:
cat_disch

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 ⋯
this :
  (ConcreteCategory.hom
        (F.map (CostructuredArrow.mkPrecomp (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op))
      ((ConcreteCategory.hom (F.map (eqToHom ⋯))) x) =
    (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      ((ConcreteCategory.hom (F.map (CostructuredArrow.mkPrecomp t.1.hom f.unop.left).op)) x)
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val

Tactic:
cat_disch

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
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    F.map f ≫ (counitAuxAux F (unop Y)).hom =
      (counitAuxAux F (unop X)).hom ≫ (restrictedYonedaObj (yonedaCollectionPresheafToA F)).map f

Tactic:
cat_disch

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
A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (f : X ⟶ Y),
    (𝟭 ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v)).map f ≫ (counitAux Y).hom =
      (counitAux X).hom ≫ (costructuredArrowPresheafToOver A ⋙ restrictedYoneda A).map f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
T : Over A
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((toOver yoneda A).op ⋙ yoneda.obj T).map f ≫
        ((overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
            (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop Y)).homCongr
                (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))).toIso).hom =
      ((overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
            (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X)).homCongr
                (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj T))).toIso).hom ≫
        (yoneda.op ⋙ yoneda.obj ((overEquivPresheafCostructuredArrow A).functor.obj T)).map f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A✝ A : Cᵒᵖ ⥤ Type v
⊢ ∀ {X Y : (CostructuredArrow yoneda A)ᵒᵖ} (f : X ⟶ Y),
    ((toOver yoneda A).op ⋙ coyoneda).map f ≫
        (NatIso.ofComponents
            (fun Y_1 ↦
              (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
                (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop Y)).homCongr
                    (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y_1))).toIso)
            ⋯).hom =
      (NatIso.ofComponents
            (fun Y ↦
              (overEquivPresheafCostructuredArrow A).fullyFaithfulFunctor.homEquiv.toIso ≪≫
                (((toOverCompOverEquivPresheafCostructuredArrow A).app (unop X)).homCongr
                    (Iso.refl ((overEquivPresheafCostructuredArrow A).functor.obj Y))).toIso)
            ⋯).hom ≫
        (yoneda.op ⋙
              coyoneda ⋙
                (Functor.whiskeringLeft (Over A) ((CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v) (Type (max u v))).obj
                  (overEquivPresheafCostructuredArrow A).functor).map
          f

Tactic:
cat_disch

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 α
c : Cocone F
hc : IsColimit c
s : Cocone F'
⊢ α ≫
      L.whiskerLeft
        (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
          (const D).map (hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι })) =
    α ≫ L.whiskerLeft s.ι

Tactic:
cat_disch

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 ⥤ ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E
this : (hom (g.app (op X))) { down := f ≫ 𝟙 Y } = { down := A.map f ≫ ((hom (g.app (op Y))) { down := 𝟙 Y }).down }
⊢ A.map f ≫ ((hom (g.app (op Y))) { down := 𝟙 Y }).down = ((hom (g.app (op X))) { down := 𝟙 X ≫ f }).down

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
⊢ PreservesColimit H lim

Tactic:
have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimit H lim
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 α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ L.whiskerLeft
        ((const D).map (hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α }) ≫
          F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π) ≫
      α =
    L.whiskerLeft s.π ≫ α

Tactic:
cat_disch

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
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) ?_

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
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ ((proj S T).mapIso i).hom ≫ Hom.right g = Hom.right f
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily J
⊢ (match X✝, X✝, Hom.id X✝ ≫ Hom.id X✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match X✝, X✝, Hom.id X✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
cat_disch

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

Goal state before:
pp: case id.line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, Hom.id zero ≫ line a✝ with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, zero, Hom.id zero with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
cat_disch

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

Goal state before:
pp: case line.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
a✝ : J
⊢ (match zero, one, line a✝ ≫ Hom.id one with
    | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
    | .(zero), .(one), line j => f j) =
    (match zero, one, line a✝ with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j) ≫
      match one, one, Hom.id one with
      | x, .(x), Hom.id .(x) => 𝟙 (WalkingParallelFamily.casesOn x X Y)
      | .(zero), .(one), line j => f j

Tactic:
cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

Tactic:
cat_disch

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

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
cat_disch

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
X✝ : WalkingParallelFamily J
⊢ F.map (Hom.id X✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
a✝ : J
⊢ F.map (line a✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)

Tactic:
cat_disch

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (Hom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (Hom.id X✝)

Tactic:
cat_disch

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

Goal state before:
pp: case line.false
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := false }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := false })

Tactic:
cat_disch

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

Goal state before:
pp: case line.true
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := true }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := true })

Tactic:
cat_disch

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

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.left ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.left

Tactic:
cat_disch

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

Goal state before:
pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.right ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.right

Tactic:
cat_disch

Goal state after: