mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₂.ι.app j ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom ≫ (S.map colim).g =
    c₂.ι.app j ≫ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
j : J
⊢ c₂.ι.app j ≫ (hc₂.coconePointUniqueUpToIso (colimit.isColimit S.X₂)).hom ≫ colimMap S.g =
    c₂.ι.app j ≫ g ≫ (hc₃.coconePointUniqueUpToIso (colimit.isColimit S.X₃)).hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f✝ : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f✝ = (F.obj j).obj.hom
this : Mono f✝
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ (F ⋙ MonoOver.forget X ⋙ Over.forget X).map f ≫ Subobject.ofMkLEMk (F.obj j').obj.hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯ ≫ ((Functor.const J).obj A✝).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X ⋙ Over.forget X)
hc : IsColimit c
f✝ : c.pt ⟶ X
hf : ∀ (j : J), c.ι.app j ≫ f✝ = (F.obj j).obj.hom
this : Mono f✝
A✝ : C
g : A✝ ⟶ X
inst✝ : Mono g
H : ∀ (i : J), Subobject.mk (F.obj i).obj.hom ≤ Subobject.mk g
j j' : J
f : j ⟶ j'
⊢ Over.Hom.left (F.map f).hom ≫ Subobject.ofMkLEMk (F.obj j').obj.hom g ⋯ =
    Subobject.ofMkLEMk (F.obj j).obj.hom g ⋯ ≫ 𝟙 A✝
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ ((Functor.const (Under j₀)).obj X).map f ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ (Under.forget j₀ ⋙ Y).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
t₁ t₂ : Under j₀
f : t₁ ⟶ t₂
⊢ 𝟙 X ≫ y ≫ Y.map t₂.hom = (y ≫ Y.map t₁.hom) ≫ Y.map (Under.Hom.right f)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ ((colimit.cocone ((F ⋙ MonoOver.forget X) ⋙ Over.forget X)).ι.app j ≫ (Subobject.isoOfMkEqMk f c.pt.hom this).hom) ≫
      c.pt.hom =
    ((Over.forget X).mapCocone c).ι.app j ≫ c.pt.hom

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
F : J ⥤ MonoOver X
inst✝¹ : IsFiltered J
c : Cocone (F ⋙ MonoOver.forget X)
inst✝ : Mono c.pt.hom
h : Subobject.mk c.pt.hom = ⨆ j, Subobject.mk (F.obj j).obj.hom
f : colimit (F ⋙ MonoOver.forget X ⋙ Over.forget X) ⟶ X :=
  colimit.desc (F ⋙ MonoOver.forget X ⋙ Over.forget X)
    { pt := X, ι := { app := fun j ↦ (F.obj j).obj.hom, naturality := ⋯ } }
this✝ : Mono f
this : Subobject.mk f = Subobject.mk c.pt.hom
j : J
⊢ (colimit.ι ((F ⋙ MonoOver.forget X) ⋙ Over.forget X) j ≫ Subobject.ofMkLEMk f c.pt.hom ⋯) ≫ c.pt.hom =
    Over.Hom.left (c.ι.app j) ≫ c.pt.hom
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ (Iso.refl (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).left).hom ≫ (Arrow.mk (f z)).hom =
    (Arrow.mk (colim.map (pullback.snd c.ι ((Functor.const J).map z)))).hom ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ 𝟙 (colimit (pullback c.ι ((Functor.const J).map z))) ≫ f z =
    colimMap (pullback.snd c.ι ((Functor.const J).map z)) ≫
      ((colimit.isColimit ((Functor.const J).obj X)).coconePointUniqueUpToIso (isColimitConstCocone J X)).hom
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
⊢ ((Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫
        {
          hom :=
            ⋯.extend
              {
                app := fun Y ↦
                  ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
                naturality := ⋯ } }).hom =
    (s.inj j).hom

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
j : ι
u : (j : ι) → CategoryTheory.yoneda.obj (X j) ⟶ (Sieve.ofArrows X c.inj).functor :=
  fun j ↦ (Sieve.ofArrows X c.inj).toFunctor (c.inj j) ⋯
this : ∀ (j : ι), u j ≫ (Sieve.ofArrows X c.inj).functorInclusion = CategoryTheory.yoneda.map (c.inj j)
⊢ CategoryTheory.yoneda.map (c.inj j) ≫
      ⋯.extend
        { app := fun Y ↦ ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
          naturality := ⋯ } =
    (s.inj j).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f✝ : α <i β
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : β ⥤ C
i j : α
f : i ⟶ j
⊢ (⋯.functor ⋙ F).map f ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ ((Functor.const α).obj (F.obj f✝.top)).map f

Tactic:
dsimp

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f✝ : α <i β
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : β ⥤ C
i j : α
f : i ⟶ j
⊢ F.map (⋯.functor.map f) ≫ F.map (homOfLE ⋯) = F.map (homOfLE ⋯) ≫ 𝟙 (F.obj f✝.top)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ z = (inv ((F z).obj j).obj.hom ≫ (pullback.fst c.ι ((Functor.const J).map z)).app j) ≫ c.ι.app j

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝² : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
inst✝¹ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
z : X ⟶ c.pt
this✝¹ : IsFiltered J
this✝ : ∀ (j₀ : J) [inst : HasColimitsOfShape (Under j₀) C] [colim.PreservesMonomorphisms], Mono (c.ι.app j₀)
this : Mono c.ι
j : J
h✝ : IsIso ((F z).obj j).obj.hom
⊢ z =
    (inv ((pullback.snd c.ι ((Functor.const J).map z)).app j) ≫ (pullback.fst c.ι ((Functor.const J).map z)).app j) ≫
      c.ι.app j
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m.hom =
    {
        hom :=
          ⋯.extend
            {
              app := fun Y ↦
                ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
              naturality := ⋯ } }.hom

Tactic:
dsimp

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : J.Subcanonical
ι : Type u_1
X : ι → C
c : Cofan X
H : Sieve.ofArrows X c.inj ∈ J c.pt
inst✝ : ∀ (i : ι), Mono (c.inj i)
hempty : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
hdisj : ∀ {i j : ι}, i ≠ j → ∀ {Y : C} (a : Y ⟶ X i) (b : Y ⟶ X j), a ≫ c.inj i = b ≫ c.inj j → Nonempty (IsInitial Y)
heq :
  ∀ (s : Cofan fun i ↦ J.yoneda.obj (X i)) {Y : C} {i j : ι} (a : Y ⟶ X i) (b : Y ⟶ X j),
    a ≫ c.inj i = b ≫ c.inj j →
      (ConcreteCategory.hom ((s.inj i).hom.app (op Y))) a = (ConcreteCategory.hom ((s.inj j).hom.app (op Y))) b
s : Cofan fun i ↦ J.yoneda.obj (X i)
m : (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).pt ⟶ s.pt
hm : ∀ (j : ι), (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i)).inj j ≫ m = s.inj j
⊢ m.hom =
    ⋯.extend
      { app := fun Y ↦ ↾fun g ↦ (ConcreteCategory.hom ((s.inj (Sieve.ofArrows.i ⋯)).hom.app Y)) (Sieve.ofArrows.h ⋯),
        naturality := ⋯ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
X Y : C
f : X ⟶ Y
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
φ : i ⟶ i'
⊢ (⋯.functor ⋙ c.F).map φ ≫ c.F.map (homOfLE ⋯) =
    c.F.map (homOfLE ⋯) ≫ ((Functor.const ↑(Set.Iic j)).obj (c.F.obj j)).map φ

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
X Y : C
f : X ⟶ Y
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
c : TransfiniteCompositionOfShape J f
j : J
i i' : ↑(Set.Iic j)
φ : i ⟶ i'
⊢ c.F.map (⋯.functor.map φ) ≫ c.F.map (homOfLE ⋯) = c.F.map (homOfLE ⋯) ≫ 𝟙 (c.F.obj j)
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
D : Type u'
inst✝¹² : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝¹¹ : LinearOrder J
inst✝¹⁰ : SuccOrder J
inst✝⁹ : OrderBot J
inst✝⁸ : WellFoundedLT J
J'✝ : Type w'
inst✝⁷ : LinearOrder J'✝
inst✝⁶ : SuccOrder J'✝
inst✝⁵ : OrderBot J'✝
inst✝⁴ : WellFoundedLT J'✝
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : OrderBot J'
inst✝¹ : SuccOrder J'
inst✝ : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
⊢ ¬IsMax (e j)

Tactic:
by simpa only [e.isMax_apply]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
⊢ ¬IsMax ↑i

Tactic:
rw [not_isMax_iff] at hi ⊢
      obtain ⟨i', hi'⟩ := hi
      exact ⟨j, lt_of_lt_of_le hi' i'.2⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk ((colimit.cocone (restrictionLT iter.F hij)).ι.app ⟨k, hk⟩ ≫ (eqToIso ⋯).hom) =
    Arrow.mk ((coconeOfLE iter.F hij).ι.app ⟨k, hk⟩)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape (↑(Set.Iio i)) C := hasColimitsOfShape_of_isSuccLimit C i hi
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (colimit.ι (restrictionLT iter.F hij) ⟨k, hk⟩ ≫ eqToHom ⋯) = Arrow.mk (iter.F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor
  · exact (le_transfiniteCompositions P).trans
  · intro h
    exact (transfiniteCompositions_monotone.{w} h).trans Q.transfiniteCompositions_le

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
⊢ functorObjTop f πX ≫ πX = functorObjLeft f πX ≫ π'FunctorObj f πX

Tactic:
ext; simp [π'FunctorObj]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
⊢ Small.{t, max v w} (attachCellsιFunctorObj f πX).ι

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : LocallySmall.{t, v, u} C
inst✝ : Small.{t, w} I
⊢ Small.{t, max v w} (FunctorObjIndex f πX)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
k j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k ≤ j₁
h₂ : k ≤ j₂
h : j₁ ≤ j₂
⊢ (iter₂.trunc h).F.obj ⟨k, h₁⟩ = iter₂.F.obj ⟨k, h₂⟩

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).symm.hom =
    ((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).ι.app ⟨i, hi⟩

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
hc : IsColimit c
x✝ : ↑(Set.Iio j)
i : J
hi : i ∈ Set.Iio j
⊢ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv = (ofCoconeObjIso c i ⋯).inv ≫ (ofCocone c).map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ (restrictionLT iter.F hij').mapArrow.obj (Arrow.mk f) =
    (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))) hij).mapArrow.obj (Arrow.mk f)

Tactic:
dsimp

Goal state after:
case e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : ⟨k₁, h₁⟩ ⟶ ⟨k₂, h₂⟩
⊢ Arrow.mk (iter.F.map (homOfLE ⋯)) = Arrow.mk ((extendToSucc hj iter.F (Φ.toSucc (iter.F.obj ⟨j, ⋯⟩))).map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ ((Functor.const J).obj Φ.X₀).map f ≫ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    ((Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯)) ≫ (Φ.iterationFunctor J).map f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
Φ : SuccStruct C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ 𝟙 Φ.X₀ ≫ (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯) =
    ((Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE ⋯)) ≫ (Φ.iterationFunctor J).map f
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
⊢ (restrictionLT (iter i hij).F ⋯).mapArrow.obj (Arrow.mk f) =
    (restrictionLT (functor hj iter) hij✝).mapArrow.obj (Arrow.mk f)

Tactic:
dsimp

Goal state after:
case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
⊢ Arrow.mk ((iter i hij).F.map (homOfLE ⋯)) = Arrow.mk ((functor hj iter).map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
g : Arrow C
⊢ Arrow.Hom.right (Arrow.homMk (functorMap f (𝟙 g)) (Arrow.Hom.right (𝟙 g)) ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (πFunctorObj f g.hom)))

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ Arrow.Hom.left (Arrow.homMk (functorMap f (τ ≫ τ')) (Arrow.Hom.right (τ ≫ τ')) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk (functorMap f τ) (Arrow.Hom.right τ) ⋯ ≫ Arrow.homMk (functorMap f τ') (Arrow.Hom.right τ') ⋯)

Tactic:
dsimp

Goal state after:
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝² : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
inst✝¹ : HasPushouts C
inst✝ : ∀ {X S : C} (πX : X ⟶ S), HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
π₁ π₂ π₃ : Arrow C
τ : π₁ ⟶ π₂
τ' : π₂ ⟶ π₃
⊢ functorMap f (τ ≫ τ') = functorMap f τ ≫ functorMap f τ'