awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
neg :
  Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) h))
    (if h₁ : Order.succ j ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE ⋯) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))
    else
      if h₂ : i₁ ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ h₂)) ≫
          F.map (homOfLE h₂) ≫
            τ ≫
              Iso.inv (objSuccIso hj F X) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)))
      (if h₁ : Order.succ j ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ ⋯)) ≫
          F.map (homOfLE h₂₃) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))
      else
        if h₂ : i₂ ≤ j then
          Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)) ≫
            F.map (homOfLE h₂) ≫
              τ ≫
                Iso.inv (objSuccIso hj F X) ≫
                  𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
        else eqToHom ⋯))
⊢ map hj F τ i₁ (Order.succ j) ⋯ h =
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂))) ≫
      map hj F τ i₂ (Order.succ j) h₂₃ h

Tactic:
dsimp [map]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc.map
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ : J
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
neg :
  map hj F τ i₁ (Order.succ j) ⋯ h =
    map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫
      𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
neg₁ neg₂ : map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h

Tactic:
rw [map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_id
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ j
⊢ Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) =
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hi)

Tactic:
extendToSucc.obj_eq F X ⟨i, hi⟩

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj, dite, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq, Subtype.mk
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ Functor.obj (extendToSucc hj F τ) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯) = X

Tactic:
extendToSucc.obj_succ_eq hj F X

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_succ_eq, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj, dite
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
dsimp :
  Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
        (extendToSucc.map hj F τ i₁ i₂ ⋯ ⋯)
        (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
⊢ Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫ Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) =
    Iso.hom (extendToSuccObjIso hj F τ i₁ ⋯) ≫ F.map (homOfLE hi)

Tactic:
dsimp [extendToSucc, extendToSuccObjIso]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso, CategoryTheory.SmallObject.SuccStruct.extendToSucc
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ : J
h₁ : i₁ ∈ Set.Iic j
i₂ : J
h₂ : i₂ ∈ Set.Iic j
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂
⊢ (restrictionLE (j := Order.succ j) (extendToSucc hj F τ) ⋯).map f ≫
      Iso.hom
        ((fun (i : (↑(Set.Iic j) : Type u)) ↦
            (extendToSuccObjIso hj F τ (↑i : J) ⋯ :
              Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
                  (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (↑i : J) ⋯) ≅
                F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (↑i : J) ⋯)))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)) =
    Iso.hom
        ((fun (i : (↑(Set.Iic j) : Type u)) ↦
            (extendToSuccObjIso hj F τ (↑i : J) ⋯ :
              Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
                  (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (↑i : J) ⋯) ≅
                F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (↑i : J) ⋯)))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ h₁)) ≫
      F.map f

Tactic:
apply extendToSuccObjIso_hom_naturality

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
rw :
  Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
      Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
rw₁ :
  Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
      𝟙
        (Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
rw₂ rw₃ :
  Eq (α :=
    Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
    (Functor.map (extendToSucc hj F τ) (homOfLE hi)) (Functor.map (extendToSucc hj F τ) (homOfLE hi))
⊢ Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Iso.hom (extendToSuccObjIso hj F τ i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)

Tactic:
rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ j ≤ j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ Eq (α :=
    Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
      Functor.obj (extendToSucc hj F τ) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (Functor.map (extendToSucc hj F τ) (homOfLE ⋯))
    (Iso.hom (extendToSuccObjIso hj F τ j ⋯) ≫ τ ≫ Iso.inv (extendToSuccObjSuccIso hj F τ))

Tactic:
extendToSucc.map_self_succ _ _ _

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ, Order.succ, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj, dite, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ arrowMap (j := Order.succ j) (extendToSucc hj F τ) i₁ i₂ hi ⋯ = arrowMap F i₁ i₂ hi hi₂

Tactic:
simp [arrowMap, extendToSucc_map hj F τ i₁ i₂ hi hi₂,
    extendToSuccObjIso, extendToSucc.objIso]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ arrowSucc (j := Order.succ j) (extendToSucc hj F τ) j ⋯ = Arrow.mk τ

Tactic:
simp [arrowSucc, arrowMap, extendToSucc_map_le_succ, extendToSuccObjIso,
    extendToSucc.objIso, extendToSuccObjSuccIso, extendToSucc.objSuccIso]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso, CategoryTheory.SmallObject.SuccStruct.arrowSucc, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.SmallObject.SuccStruct.extendToSucc.objIso, CategoryTheory.SmallObject.SuccStruct.extendToSucc.objSuccIso
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
⊢ ¬j < j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
⊢ j ≤ i₂

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : i₁ < j
subst :
  ∀ {F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C} (c : Cocone F) (hi₂ : i₂ ≤ i₂) (h₂ : ¬i₂ < i₂)
    (h₁ : i₁ < i₂), obj c i₂ = obj c i₂
⊢ obj c j = obj c i₂

Tactic:
subst h₂'
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
i₁ i₂ : J
hi : i₁ ≤ i₂
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C
c : Cocone F
hi₂ : i₂ ≤ i₂
h₂ : ¬i₂ < i₂
h₁ : i₁ < i₂
⊢ obj c i₂ = obj c i₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : ¬i₁ < j
⊢ j ≤ i₁

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : ¬i₁ < j
h₁' : i₁ = j
subst :
  ∀ (hi : i₂ ≤ i₂) {F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C} (c : Cocone F) (hi₂ : i₂ ≤ i₂)
    (h₂ h₁ : ¬i₂ < i₂), obj c i₂ = obj c i₂
⊢ obj c i₁ = obj c i₂

Tactic:
subst h₁' h₂'
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
i₂ : J
hi : i₂ ≤ i₂
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C
c : Cocone F
hi₂ : i₂ ≤ i₂
h₂ h₁ : ¬i₂ < i₂
⊢ obj c i₂ = obj c i₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i ≤ j
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i ≤ j
dsimp :
  Eq.{v_1 + 1} (α := obj c i ⟶ obj c i)
    (if h₂ : i < j then
      Iso.hom (objIso c i ⋯) ≫ F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i ⋯)) ≫ (objIso c i h₂).inv
    else
      if h₁ : i < j then
        (objIso c i h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else 𝟙 (obj c i))
    (𝟙 (obj c i))
⊢ map c i i ⋯ hi = 𝟙 (obj c i)

Tactic:
dsimp [map]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.map
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i ≤ j
⊢ Eq.{v_1 + 1} (α := obj c i ⟶ obj c i)
    (if h₂ : i < j then
      Iso.hom (objIso c i ⋯) ≫ F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i ⋯)) ≫ (objIso c i h₂).inv
    else
      if h₁ : i < j then
        (objIso c i h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else 𝟙 (obj c i))
    (𝟙 (obj c i))

Tactic:
grind
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
inl : ∀ (hi₁₂ : i₁ < i₂), map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
inr : ∀ (hi : i₁ ≤ i₁) (hi' : i₁ ≤ i₃), map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
obtain hi₁₂ | rfl := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
inl : ∀ (hi₂₃ : i₂ < i₃), map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
inl₁ : ∀ (hi' : i₂ ≤ i₂) (hi₃ : i₂ ≤ j), map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
obtain hi₂₃ | rfl := hi'.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
inl :
  Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃

Tactic:
dsimp [map]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.map
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₃) : Type u) C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ ¬i₃ < i₃

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₁₂ : i₁ < i₂
hi' : i₂ ≤ i₂
hi₃ : i₂ ≤ j
inl : map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ 𝟙 (obj c i₂)
inl₁ inl₂ : map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃

Tactic:
rw [map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.SmallObject.SuccStruct.ofCocone.map_id
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₃ : J
hi₃ : i₃ ≤ j
hi : i₁ ≤ i₁
hi' : i₁ ≤ i₃
inr : map c i₁ i₃ ⋯ hi₃ = 𝟙 (obj c i₁) ≫ map c i₁ i₃ hi' hi₃
inr₁ inr₂ : map c i₁ i₃ ⋯ hi₃ = map c i₁ i₃ hi' hi₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃

Tactic:
rw [map_id, id_comp]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
⊢ (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)

Tactic:
dif_pos hi

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.obj, dif_pos, dite
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
⊢ j ∈ Set.Iic j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
⊢ ¬(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) : J) < j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
dsimp :
  (if h₂ : j < j then Iso.hom (ofCocone.objIso c i ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c j h₂).inv
    else
      if h₁ : i < j then
        (ofCocone.objIso c i h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫
            (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j)
      else eqToHom ⋯) =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
⊢ (ofCocone c).map (homOfLE ⋯) =
    (ofCoconeObjIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv

Tactic:
dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.map, CategoryTheory.SmallObject.SuccStruct.ofCocone, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsoPt, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
⊢ ¬j < j

Tactic:
simp