mathlib-initiative/mathlib-tactics huggingface dataset:
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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } = 𝟙 (fiberwiseColimit G)

Tactic:
ext

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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ }.app x✝ =
    (𝟙 (fiberwiseColimit G)).app x✝
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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ } =
    { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
      { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }

Tactic:
ext

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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
x✝ : C
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ }.app x✝ =
    ({ app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
          { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }).app
      x✝
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
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ comp X✝.id f = f

Tactic:
ext

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ (comp X✝.id f).base = f.base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X✝ Y✝ : Grothendieck F
f : X✝.Hom Y✝
⊢ eqToHom ⋯ ≫ (comp X✝.id f).fiber = f.fiber
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✝
⊢ (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

Tactic:
ext

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✝
j✝ : ↑(F.obj x✝¹)
⊢ colimit.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      (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.ι (Grothendieck.ι F x✝¹ ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F x✝¹ ⋙ G) (Cocone.whisker (Grothendieck.ι F x✝¹) c) ≫ 𝟙 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
X Y : Grothendieck F
f : X.Hom Y
⊢ comp f Y.id = f

Tactic:
ext

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ (comp f Y.id).base = f.base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber
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
⊢ 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

Tactic:
ext

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
j✝ : ↑(F.obj c)
⊢ colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫
      colimit.desc (Grothendieck.ι F c ⋙ G) (Cocone.whisker (Grothendieck.ι F c) c✝) ≫
        hc.desc
          { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι } =
    colimit.ι (Grothendieck.ι F c ⋙ G) j✝ ≫ s.ι.app c
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
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
ext

Goal state after:
case w_base
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ (comp (comp f g) h).base = (comp f (comp g h)).base

case w_fiber
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
W✝ X✝ Y✝ Z✝ : Grothendieck F
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ eqToHom ⋯ ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber
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
E : Cat
F : ↑E ⥤ Cat
⊢ Over.homMk (map (𝟙 F)).toCatHom ⋯ = 𝟙 (Over.mk (forget F).toCatHom)

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F✝ : C ⥤ Cat
E : Cat
F : ↑E ⥤ Cat
⊢ (Over.Hom.left (Over.homMk (map (𝟙 F)).toCatHom ⋯)).toFunctor =
    (Over.Hom.left (𝟙 (Over.mk (forget F).toCatHom))).toFunctor
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
x : WithTerminal C ⥤ D
⊢ mkCommaMorphism
      (NatIso.ofComponents
          (fun X ↦
            match X with
            | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
            | star => Iso.refl (x.obj star))
          ⋯).hom =
    𝟙 (mkCommaObject x)

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).left.app
      x✝ =
    (𝟙 (mkCommaObject x)).left.app x✝

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithTerminal C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).right =
    (𝟙 (mkCommaObject x)).right
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Type u_1
x✝¹ x✝ : WithTerminal (Discrete J)
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
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
inst✝¹ : HasColimitsOfShape D E
inst✝ : HasColimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ colimMap (F.whiskerLeft f) ≫ colimit.pre Y✝ F = colimit.pre X✝ F ≫ colimMap f

Tactic:
ext

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
inst✝¹ : HasColimitsOfShape D E
inst✝ : HasColimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
j✝ : C
⊢ colimit.ι (F ⋙ X✝) j✝ ≫ colimMap (F.whiskerLeft f) ≫ colimit.pre Y✝ F =
    colimit.ι (F ⋙ X✝) j✝ ≫ colimit.pre X✝ F ≫ colimMap f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := ⋯
AX : Type (max w₂ 0) := ⋯
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ⋯
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : f p = 0
this :
  (MvPolynomial.map (algebraMap R A)) p + q ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
x : RX
hx : x ∈ ↑s
⊢ (MvPolynomial.map (algebraMap R A)) x ∈ ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s

Tactic:
exact Set.mem_image_of_mem _ hx

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

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) := ⋯
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) := ⋯
⊢ (I d).toEquiv y₁ = (I d).toEquiv y₂

Tactic:
ext

Goal state after:
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
x : WithInitial C ⥤ D
⊢ mkCommaMorphism
      (NatIso.ofComponents
          (fun X ↦
            match X with
            | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
            | star => Iso.refl (x.obj star))
          ⋯).hom =
    𝟙 (mkCommaObject x)

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
⊢ (mkCommaMorphism
        (NatIso.ofComponents
            (fun X ↦
              match X with
              | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
              | star => Iso.refl (x.obj star))
            ⋯).hom).left =
    (𝟙 (mkCommaObject x)).left

case h₂
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
x : WithInitial C ⥤ D
x✝ : C
⊢ (mkCommaMorphism
            (NatIso.ofComponents
                (fun X ↦
                  match X with
                  | of x_1 => (Iso.refl (incl ⋙ x)).app x_1
                  | star => Iso.refl (x.obj star))
                ⋯).hom).right.app
      x✝ =
    (𝟙 (mkCommaObject x)).right.app x✝
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
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
⊢ limMap f ≫ limit.pre Y✝ F = limit.pre X✝ F ≫ limMap (F.whiskerLeft f)

Tactic:
ext

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
inst✝¹ : HasLimitsOfShape D E
inst✝ : HasLimitsOfShape C E
X✝ Y✝ : D ⥤ E
f : X✝ ⟶ Y✝
j✝ : C
⊢ (limMap f ≫ limit.pre Y✝ F) ≫ limit.π (F ⋙ Y✝) j✝ = (limit.pre X✝ F ≫ limMap (F.whiskerLeft f)) ≫ limit.π (F ⋙ Y✝) j✝
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : aeval_h.toRingHom x✝ + y ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : f' x✝ = 0
x : RXm
hx : x ∈ ↑s
⊢ aeval_h x ∈ ⇑aeval_h '' ↑s

Tactic:
exact Set.mem_image_of_mem _ hx

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
P Q : IsKernelPair f a b
⊢ P = Q

Tactic:
constructor

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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
⊢ (pre F G).Final

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
⊢ ∀ (d : Grothendieck F), IsConnected (StructuredArrow d (pre F G))
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
⊢ IsColimit (Cofork.ofπ f ⋯)

Tactic:
refine Cofork.IsColimit.mk _
    (fun s => Cofork.IsColimit.desc r.isColimit s.π
      (by rw [← ht, assoc, s.condition, reassoc_of% kt]))
    (fun s => ?_) (fun s m w => ?_)

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
⊢ (Cofork.ofπ f ⋯).π ≫ Cofork.IsColimit.desc r.isColimit s.π ⋯ = s.π

case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
m : (Cofork.ofπ f ⋯).pt ⟶ s.pt
w : (Cofork.ofπ f ⋯).π ≫ m = s.π
⊢ m = Cofork.IsColimit.desc r.isColimit s.π ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
          ⋯).fst =
    s.fst

Tactic:
ext

Goal state after:
case refine_3.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.fst f g =
    s.fst ≫ pullback.fst f g

case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).fst) ≫
      pullback.snd f g =
    s.fst ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
      (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯) (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯)
          ⋯).snd =
    s.snd

Tactic:
ext

Goal state after:
case refine_4.h₀
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).snd) ≫
      pullback.fst f g =
    s.snd ≫ pullback.fst f g

case h₁
C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
s : PullbackCone (pullback.fst f g) (pullback.fst f g)
⊢ (pullback.lift (s.fst ≫ pullback.fst f g) (h.lift (s.fst ≫ pullback.snd f g) (s.snd ≫ pullback.snd f g) ⋯) ⋯ ≫
        (PullbackCone.mk (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₁ (𝟙 Z) ⋯ ⋯)
            (pullback.map f (a₁ ≫ g) f g (𝟙 X) a₂ (𝟙 Z) ⋯ ⋯) ⋯).snd) ≫
      pullback.snd f g =
    s.snd ≫ pullback.snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : IsRegularEpiCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
⊢ StrongEpi f

Tactic:
have := isRegularEpi_of_regularEpi <| regularEpiOfEpi f
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ Mono f

Tactic:
constructor

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
⊢ ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₁ =
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
      i₂

Tactic:
ext

Goal state after:
case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      fst f i =
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      fst f i

case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₁) ≫
      snd f i =
    ((snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
          snd (i₁ ≫ snd f i) (i₂ ≫ snd f i)) ≫
        i₂) ≫
      snd f i
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f =
    map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
      map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯

Tactic:
ext

Goal state after:
case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ fst f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst f f

case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd f f