awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : PartialOrder J
F : Functor.{w, v, w, u} J C
J' : Type w'
inst_2 : PartialOrder J'
e : J' ≃o J
inst_3 : F.IsWellOrderContinuous
⊢ (e.equivalence.functor ⋙ F).IsWellOrderContinuous

Tactic:
inferInstanceAs (e.toInitialSeg.monotone.functor ⋙ F).IsWellOrderContinuous

Premises used: _private.0.CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
⊢ Monotone f

Tactic:
have hf : Monotone f := fun _ _ h ↦ h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
rw : ∀ (j₂ : (↑(Set.Iio (↑m : J)) : Type w)), ∃ (j₁ : (↑(Set.Iio m) : Type w)), j₂ ≤ f j₁
⊢ hf.functor.Final

Tactic:
rw [Monotone.final_functor_iff]

Premises used: Monotone.final_functor_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj' : j' ∈ Set.Iio (↑m : J)
⊢ j' < (↑m : J)

Tactic:
push _ ∈ _ at hj'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
dsimp :
  ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)), Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤ f j₁

Tactic:
dsimp only [f]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
pos :
  ∀ (h : j' ≤ j),
    ∃ (j₁ : (↑(Set.Iio m) : Type w)),
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
        Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
neg :
  ∀ (h : j < j'),
    ∃ (j₁ : (↑(Set.Iio m) : Type w)),
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
        Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯

Tactic:
by_cases! h : j' ≤ j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯

Tactic:
⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩

Premises used: le_refl, Subtype.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
pos : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∈ Set.Iio m
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯

Tactic:
refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
pos : ∀ (h' : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∉ Set.Iio m), False
⊢ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∈ Set.Iio m

Tactic:
by_contra h'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯ ∉ Set.Iio m
⊢ m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯

Tactic:
simp only [Set.mem_Iio, not_lt] at h'

Premises used: Set.mem_Iio, not_lt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯
pos : IsMin m
⊢ False

Tactic:
apply hm.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯
k : J
hk : k ∈ Set.Ici j
hkm : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) k hk ≤ m
⊢ m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) k hk

Tactic:
h'.trans hk

Premises used: LE.le.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j' ≤ j
h' : m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) j ⋯
k : J
hk : k ∈ Set.Ici j
hkm : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) k hk ≤ m
⊢ m ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Ici j) k hk

Tactic:
exact h'.trans hk

Premises used: LE.le.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j < j'
⊢ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
j' : J
hj'_1 : j' ∈ Set.Iio (↑m : J)
hj' : j' < (↑m : J)
h : j < j'
⊢ ∃ (j₁ : (↑(Set.Iio m) : Type w)),
    Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) j' hj'_1 ≤
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) (↑j₁.1 : J) ⋯

Tactic:
exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
⊢ hf.functor.Final

Tactic:
have : hf.functor.Final := by
      rw [Monotone.final_functor_iff]
      rintro ⟨j', hj'⟩
      push _ ∈ _ at hj'
      dsimp only [f]
      by_cases! h : j' ≤ j
      · refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
        by_contra h'
        simp only [Set.mem_Iio, not_lt] at h'
        apply hm.1
        rintro ⟨k, hk⟩ hkm
        exact h'.trans hk
      · exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type w
inst_1 : PartialOrder J_1
J : Type w
inst_2 : LinearOrder J
F : Functor.{w, v, w, u} J C
inst_3 : F.IsWellOrderContinuous
j : J
m : { x : J // x ∈ Set.Ici j }
hm : Order.IsSuccLimit m
f : (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w) :=
  fun (x : (↑(Set.Iio m) : Type w)) ↦
    match (motive := (↑(Set.Iio m) : Type w) → (↑(Set.Iio (↑m : J)) : Type w)) x with
    | ⟨⟨a, ha⟩, ha'⟩ => Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio (↑m : J)) a ha'
hf : Monotone f
this : hf.functor.Final
⊢ IsColimit.{w, v, w, u} (J := (↑(Set.Iio m) : Type w)) (C := C) (F :=
    comp (D := { x : J // x ∈ Set.Ici j })
      (Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type w)) ↦ x1 < x2) (s :=
              fun (x1 x2 : { x : J // x ∈ Set.Ici j }) ↦ x1 < x2) (Set.principalSegIio m)) :
          (a : (↑(Set.Iio m) : Type w)) → { x : J // x ∈ Set.Ici j }))
        ⋯)
      (Monotone.functor ⋯ ⋙ F))
    (PrincipalSeg.cocone (Set.principalSegIio m) (Monotone.functor ⋯ ⋙ F))

Tactic:
exact (Functor.Final.isColimitWhiskerEquiv (F := hf.functor) _).2
      (F.isColimitOfIsWellOrderContinuous m.1 (Set.Ici.isSuccLimit_coe m hm))

Premises used: CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, Monotone.functor, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, Subtype.val, Set.Ici.isSuccLimit_coe, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
P : C
p : (b : β) → P ⟶ f b
⊢ (Fan.mk P p).proj = p

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fan.proj, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
P : C
p : (b : β) → f b ⟶ P
⊢ (Cofan.mk P p).inj = p

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofan.inj, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
e : β ≃ α
iso : (j : β) → g j ≅ f ((e : (a : β) → α) j)
have :
  ∀
    (α :
      Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
        ((Discrete.equivalence e).functor ⋙ Discrete.functor f)),
    HasCoproduct.{w, v, u} g
⊢ HasCoproduct.{w, v, u} g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α_1 : Type w₂
C : Type u
inst : Category.{v, u} C
f : α_1 → C
g : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
e : β ≃ α_1
iso : (j : β) → g j ≅ f ((e : (a : β) → α_1) j)
α :
  Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
    ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasCoproduct.{w, v, u} g

Tactic:
hasColimit_of_iso α

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α_1 : Type w₂
C : Type u
inst : Category.{v, u} C
f : α_1 → C
g : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
e : β ≃ α_1
iso : (j : β) → g j ≅ f ((e : (a : β) → α_1) j)
α :
  Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
    ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasCoproduct.{w, v, u} g

Tactic:
exact hasColimit_of_iso α

Premises used: CategoryTheory.Limits.hasColimit_of_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
inst_1 : HasProduct.{w₂, v, u} f
e : β ≃ α
iso : (j : β) → g j ≅ f ((e : (a : β) → α) j)
have :
  ∀
    (α :
      Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
        ((Discrete.equivalence e).functor ⋙ Discrete.functor f)),
    HasProduct.{w, v, u} g
⊢ HasProduct.{w, v, u} g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α_1 : Type w₂
C : Type u
inst : Category.{v, u} C
f : α_1 → C
g : β → C
inst_1 : HasProduct.{w₂, v, u} f
e : β ≃ α_1
iso : (j : β) → g j ≅ f ((e : (a : β) → α_1) j)
α :
  Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
    ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasProduct.{w, v, u} g

Tactic:
hasLimit_of_iso α.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α_1 : Type w₂
C : Type u
inst : Category.{v, u} C
f : α_1 → C
g : β → C
inst_1 : HasProduct.{w₂, v, u} f
e : β ≃ α_1
iso : (j : β) → g j ≅ f ((e : (a : β) → α_1) j)
α :
  Iso (C := Functor.{w, v, w, u} (Discrete β) C) (Discrete.functor g)
    ((Discrete.equivalence e).functor ⋙ Discrete.functor f)
⊢ HasProduct.{w, v, u} g

Tactic:
exact hasLimit_of_iso α.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
F : β → C
c : Fan.{w, v, u} F
hc : IsLimit c
A : C
f : (i : β) → A ⟶ F i
i : β
⊢ lift hc f ≫ c.proj i = f i

Tactic:
hc.fac (Fan.mk A f) ⟨i⟩

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.Fan.mk, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Fan.IsLimit.lift, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
X : β → C
c d : Fan.{w, v, u} X
hc : IsLimit c
i : β
⊢ hc.lift d ≫ c.proj i = d.proj i

Tactic:
hc.fac _ _

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u_1
F : I → C
c : Fan.{u_1, v, u} F
hc : IsLimit c
A : C
f g : A ⟶ c.pt
h : ∀ (i : I), f ≫ c.proj i = g ≫ c.proj i
⊢ f = g

Tactic:
hc.hom_ext (fun ⟨i⟩ => h i)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Limits.Fan.IsLimit.hom_ext.match_1, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
F : β → C
c : Cofan.{w, v, u} F
hc : IsColimit c
A : C
f : (i : β) → F i ⟶ A
i : β
⊢ c.inj i ≫ desc hc f = f i

Tactic:
hc.fac (Cofan.mk A f) ⟨i⟩

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
X : β → C
c d : Cofan.{w, v, u} X
hc : IsColimit c
i : β
⊢ c.inj i ≫ hc.desc d = d.inj i

Tactic:
hc.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u_1
F : I → C
c : Cofan.{u_1, v, u} F
hc : IsColimit c
A : C
f g : c.pt ⟶ A
h : ∀ (i : I), c.inj i ≫ f = c.inj i ≫ g
⊢ f = g

Tactic:
hc.hom_ext (fun ⟨i⟩ => h i)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Limits.Fan.IsLimit.hom_ext.match_1, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasProduct.{w, v, u} f
X : C
g₁ g₂ : X ⟶ piObj.{w, v, u} f
h : ∀ (b : β), g₁ ≫ π f b = g₂ ≫ π f b
⊢ g₁ = g₂

Tactic:
limit.hom_ext (fun ⟨j⟩ => h j)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Discrete.functor, CategoryTheory.Limits.limit.hom_ext, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Limits.Fan.IsLimit.hom_ext.match_1, Eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
f : β → C
inst_1 : HasCoproduct.{w, v, u} f
X : C
g₁ g₂ : sigmaObj.{w, v, u} f ⟶ X
h : ∀ (b : β), ι f b ≫ g₁ = ι f b ≫ g₂
⊢ g₁ = g₂

Tactic:
colimit.hom_ext (fun ⟨j⟩ => h j)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.CategoryStruct.comp, _private.0.CategoryTheory.Limits.Fan.IsLimit.hom_ext.match_1, Eq, CategoryTheory.Limits.colimit.hom_ext, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasProduct.{u_1, v, u} f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasProduct.{u_1, v, u} f
j j' : J
w : j = j'
⊢ Eq.{v + 1} (α := piObj.{u_1, v, u} f ⟶ f j') (π f j ≫ eqToHom ⋯) (π f j')

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasCoproduct.{u_1, v, u} f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasCoproduct.{u_1, v, u} f
j j' : J
w : j = j'
refl : Eq.{v + 1} (α := f j ⟶ sigmaObj.{u_1, v, u} f) (eqToHom ⋯ ≫ ι f j) (ι f j)
⊢ Eq.{v + 1} (α := f j ⟶ sigmaObj.{u_1, v, u} f) (eqToHom ⋯ ≫ ι f j') (ι f j)

Tactic:
cases w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
f : J → C
inst_1 : HasCoproduct.{u_1, v, u} f
j : J
⊢ Eq.{v + 1} (α := f j ⟶ sigmaObj.{u_1, v, u} f) (eqToHom ⋯ ≫ ι f j) (ι f j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
β : Type w
f : β → C
inst_1 : HasProduct.{w, v, u} f
P : C
p : (b : β) → P ⟶ f b
b : β
⊢ CategoryStruct.comp (Y := piObj.{w, v, u} f) (lift p) (π f b) = p b

Tactic:
simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Premises used: CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app