mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPredOrder

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : IsMin i
⊢ cases 0 castSucc i = i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x✝² x✝¹ : ↑(Iic j)
x✝ : (fun j_1 ↦ ↑j_1) x✝² = (fun j_1 ↦ ↑j_1) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ {a b : ↑(Iic j)}, { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } a < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x : ↑(Iic j)
k : α
h : k < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ } x
⊢ k ∈ range ⇑{ toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
x✝² x✝¹ : ↑(Iio j)
x✝ : (fun j_1 ↦ ↑j_1) x✝² = (fun j_1 ↦ ↑j_1) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ {a b : ↑(Iio j)}, { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } a < { toFun := fun j_1 ↦ ↑j_1, inj' := ⋯ } b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j✝ j : α
⊢ ∀ (b : α), b ∈ range ⇑{ toFun := fun j_1 ↦ ↑j_1, inj' := ⋯, map_rel_iff' := ⋯ } ↔ b < j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
x✝² x✝¹ : ↑(Iic i)
x✝ : (fun k ↦ ⟨↑k, ⋯⟩) x✝² = (fun k ↦ ⟨↑k, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : ↑(Iic i)}, { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } a < { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
x✝² x✝¹ : ↑(Iio i)
x✝ : (fun k ↦ ⟨↑k, ⋯⟩) x✝² = (fun k ↦ ⟨↑k, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : ↑(Iio i)}, { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } a < { toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯ } b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.InitialSeg

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
i j : α
h : i ≤ j
⊢ ∀ (b : ↑(Iic j)), b ∈ range ⇑{ toFun := fun k ↦ ⟨↑k, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ } ↔ b < ⟨i, h⟩

Tactic:
by

Goal state after:
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
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ IsIso (f z)

Tactic:
by

Goal state after:
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
z : X ⟶ c.pt
inst✝ : IsFiltered J
⊢ Epi (f z)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: 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)
Z : Cᵒᵖ
g : unop Z ⟶ X j
h : (Sieve.ofArrows X c.inj).arrows (g ≫ c.inj j)
⊢ Sieve.ofArrows.h h ≫ c.inj (Sieve.ofArrows.i h) = g ≫ c.inj j

Tactic:
by

Goal state after:
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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
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
h : Epi f
⊢ ∃ j, IsIso (F.obj j).obj.hom

Tactic:
by

Goal state after:
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
⊢ ∃ j₀ y, z = y ≫ c.ι.app j₀

Tactic:
by

Goal state after:
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
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
inst✝¹ : IsCardinalFiltered J κ
hXκ : HasCardinalLT (Subobject X) κ
inst✝ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (Y.map φ)
c : Cocone Y
hc : IsColimit c
⊢ IsColimit ((coyoneda.obj (op X)).mapCocone c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: 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)
⊢ IsColimit (Cofan.mk (J.yoneda.obj c.pt) fun i ↦ J.yoneda.map (c.inj i))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
inst✝³ : J.Subcanonical
ι : Type u_1
inst✝² : CoproductsOfShapeDisjoint C ι
inst✝¹ : HasPullbacks C
inst✝ : HasStrictInitialObjects C
hcov : ∀ {X : ι → C} {c : Cofan X} (x : IsColimit c), Sieve.ofArrows X c.inj ∈ J c.pt
htriv : ∀ (Y : C) (a : IsInitial Y), ⊥ ∈ J Y
⊢ PreservesColimitsOfShape (Discrete ι) J.yoneda

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
Y : C
h : Presieve.IsSheaf J (CategoryTheory.uliftYoneda.{v', v, u}.obj Y)
⊢ Presieve.IsSheaf J (CategoryTheory.yoneda.obj Y)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v', u_1} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.IsContinuous J K
inst✝ : K.Subcanonical
⊢ J.Subcanonical

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : j ≤ b
this : ¬⟨b, hb'⟩ ⋖ m
⊢ ⟨b, hb'⟩ < m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
hb : b < ↑m
hb' : b < j
this : ↑m ≤ j
k : J
hk : k ∈ Ici j
a✝ : ⟨k, hk⟩ ≤ m
⊢ j ≤ ↑⟨k, hk⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Limit

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
m : ↑(Ici j)
hm : Order.IsSuccLimit m
b : J
⊢ ¬b ⋖ ↑m

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderBot J
x✝ : J ⥤ C
⊢ HasLimit x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : Preorder J
inst✝ : OrderTop J
x✝ : J ⥤ C
⊢ HasColimit x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasIterationOfShape J C
α : Type u_1
inst✝ : PartialOrder α
h : α <i J
hα : Order.IsSuccLimit h.top
⊢ HasColimitsOfShape α C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) (Arrow C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝³ : LinearOrder J
C : Type u
inst✝² : Category.{v, u} C
K : Type u'
inst✝¹ : Category.{v', u'} K
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) (K ⥤ C)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
F : J ⥤ C
G : C ⥤ D
inst✝¹ : F.IsWellOrderContinuous
inst✝ : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ IsColimit ((Set.principalSegIio j).cocone (F ⋙ G))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
⊢ HasColimitsOfShape α C

Tactic:
let s := f.toPrincipalSeg hf

Goal state after:
case neg
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
⊢ HasColimitsOfShape α C
Module: Mathlib.Order.Interval.Set.Final

Goal state before:
pp: J : Type u
inst✝ : LinearOrder J
j : J
⊢ ⋯.functor.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
G₁ : C ⥤ D
G₂ : D ⥤ E
inst✝¹ : PreservesWellOrderContinuousOfShape J G₁
inst✝ : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) (G₁ ⋙ G₂)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
inst✝³ : Category.{v'', u''} E
J : Type w
inst✝² : LinearOrder J
inst✝¹ : HasIterationOfShape J C
K : Type u_1
inst✝ : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) ((evaluation K C).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.leftFunc

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
i : J
hi : ¬IsMax i
a✝ : i = s.top → HasColimitsOfShape α C
hi₀ : Order.succ i = s.top
⊢ i < s.top

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder

Goal state before:
pp: C : Type u
D : Type u'
E : Type u''
inst✝⁴ : Category.{v, u} C
inst✝³ : Category.{v', u'} D
inst✝² : Category.{v'', u''} E
J : Type w
inst✝¹ : LinearOrder J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (↑(Set.Iio j)) Arrow.rightFunc

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ s.toRelEmbedding b < Order.succ (s.toRelEmbedding a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
hf : ¬Function.Surjective ⇑f
s : α <i J := f.toPrincipalSeg hf
a : α
hi : ¬IsMax (s.toRelEmbedding a)
a✝ : s.toRelEmbedding a = s.top → HasColimitsOfShape α C
hi₀ : Order.succ (s.toRelEmbedding a) = s.top
b : α
⊢ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : PartialOrder J
F : ℕ ⥤ C
m : ℕ
hm : Order.IsSuccLimit m
⊢ Nonempty (IsColimit ((Set.principalSegIio m).cocone F))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type w
inst✝² : PartialOrder J
F : J ⥤ C
J' : Type w'
inst✝¹ : PartialOrder J'
f : J' ≤i J
inst✝ : F.IsWellOrderContinuous
m' : J'
hm' : Order.IsSuccLimit m'
⊢ Order.IsSuccLimit ((Set.principalSegIio m').transInitial f).top

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : PartialOrder α
f : α ≤i J
inst✝ : Nonempty α
⊢ HasColimitsOfShape α C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : α ≤i J
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
j' : J
hj'✝ : j' ∈ Set.Iio ↑m
hj' : j' < ↑m
h : j < j'
⊢ ⟨j', hj'✝⟩ ≤ ⟨↑⟨⟨j', ⋯⟩, hj'⟩.1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : ↑(Set.Iio m) → ↑(Set.Iio ↑m) :=
  fun x ↦
    match x with
    | ⟨⟨a, ha⟩, ha'⟩ => ⟨a, ha'⟩
hf : Monotone f
⊢ hf.functor.Final

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J✝ : Type w
inst✝² : PartialOrder J✝
J : Type w
inst✝¹ : LinearOrder J
F : J ⥤ C
inst✝ : F.IsWellOrderContinuous
j : J
m : { x // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
⊢ IsColimit ((Set.principalSegIio m).cocone (⋯.functor ⋙ F))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Bot α
⊢ (equivShrink α) ((equivShrink α).symm ⊥) = (equivShrink α) ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ i ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = Order.succ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ i = ⟨Order.succ ↑i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝¹ : Small.{u, u_1} α
inst✝ : Preorder α
a b : α
⊢ (equivShrink α) a ≤ (equivShrink α) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Shrink

Goal state before:
pp: α : Type u_1
inst✝² : Small.{u, u_1} α
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : Shrink.{u, u_1} α
⊢ ⊥ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ i ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ ↑(Order.pred i) = Order.pred ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred ↑i ∈ Ici j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : PredOrder J
j : J
i : ↑(Ici j)
hi : ¬IsMin i
⊢ Order.pred i = ⟨Order.pred ↑i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{w, v, u} C
⊢ (monomorphisms C).IsStableUnderTransfiniteComposition

Tactic:
by

Goal state after:
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
F : C ⥤ D
inst✝¹ : PreservesWellOrderContinuousOfShape J F
inst✝ : PreservesColimitsOfShape J F
⊢ (F.mapIso c.isoBot).inv ≫ (Functor.whiskerRight c.incl F ≫ (Functor.constComp J Y F).hom).app ⊥ = F.map f

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ (Discrete.functor fun i ↦ A (c.π i)).obj { as := i } ⟶ (Discrete.functor fun i ↦ B (c.π i)).obj { as := i }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
x✝ : Discrete c.ι
i : c.ι
⊢ c.cofan₁.ι.app { as := i } ≫ c.m =
    c.cofan₁.ι.app { as := i } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun x ↦
                match x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f

Tactic:
by

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' : 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

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' : Type w'
inst✝³ : LinearOrder J'
inst✝² : OrderBot J'
inst✝¹ : SuccOrder J'
inst✝ : WellFoundedLT J'
e : J' ≃o J
j : J'
hj : ¬IsMax j
⊢ W ((h.ofOrderIso e).F.map (homOfLE ⋯))

Tactic:
by

Goal state after: