awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₃
hi₃' : i₃ < j
inl :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    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 ⋯)
inl₁ :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (objIso 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 ⋯
inl₂ :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (objIso c i₂ ⋯)) ≫
      Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
⊢ 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 ⋯))
have inl₃ : Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ hi₃').inv =
  Iso.hom (objIso c i₁ sorry) ≫
    (F.map (homOfLE hi) ≫ Iso.inv (objIso c i₂ sorry)) ≫
      Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
Tactic: rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₃
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < i₃ then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < i₃ then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < i₃ then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl : Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
  (if h₁ : i₁ < i₃ then
    (objIso c i₁ h₁).hom ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
  else eqToHom sorry)
  (CategoryStruct.comp (Y := obj c i₂)
    (if h₂ : i₂ < i₃ then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < i₃ then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry)
    (if h₂ : i₃ < i₃ then Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₂ < i₃ then
        (objIso c i₂ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i₃) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry))
Tactic: rw [dif_neg (by simp), dif_pos (hi₁₂.trans hi₂₃), dif_pos hi₂₃, dif_neg (by simp),
          dif_pos hi₂₃, eqToHom_refl, comp_id, assoc, assoc, Iso.inv_hom_id_assoc,
          Cocone.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃
have inl : map c i₁ i₂ sorry hi₃ = map c i₁ i₂ hi sorry ≫ 𝟙 (obj c i₂)
Tactic: rw [map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂)
⊢ map c i₁ i₂ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₂ hi' hi₃
have inl₁ : map c i₁ i₂ sorry hi₃ = map c i₁ i₂ hi sorry
Tactic: rw [map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
have inr : map c i₁ i₃ sorry hi₃ = 𝟙 (obj c i₁) ≫ map c i₁ i₃ hi' hi₃
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₁ hi ⋯ ≫ map c i₁ i₃ hi' hi₃
have inr₁ : map c i₁ i₃ sorry hi₃ = map c i₁ i₃ hi' hi₃
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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).map (homOfLE ⋯) =
    (ofCoconeObjIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv
have dsimp : (if h₂ : j < j then Iso.hom (ofCocone.objIso c i sorry) ≫ F.map (homOfLE sorry) ≫ (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 sorry) =
  (ofCocone.objIso c i hi).hom ≫
    c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
Tactic: dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ (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
have rw : (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 sorry) =
  (ofCocone.objIso c i hi).hom ≫
    c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
Tactic: rw [dif_neg (by simp), dif_pos hi, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (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
⊢ (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
have rw₁ : (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.obj c j) =
  (ofCocone.objIso c i hi).hom ≫
    c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
Tactic: rw [dif_neg (by simp), dif_pos hi, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (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
rw₁ :
  (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.obj c j) =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
⊢ (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
have rw₂ : (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.objIso c i hi).hom ≫
    c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
Tactic: rw [dif_neg (by simp), dif_pos hi, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ (ofCocone c).map (homOfLE hi) = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv
have dsimp : (if h₂ : i₂ < j then Iso.hom (ofCocone.objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (ofCocone.objIso c i₂ 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 ≫ eqToHom sorry
    else eqToHom sorry) =
  Iso.hom (ofCocone.objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
Tactic: dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ (if h₂ : i₂ < j then Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ 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 ≫ eqToHom ⋯
      else eqToHom ⋯) =
    Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
have rw : Iso.hom (ofCocone.objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (ofCocone.objIso c i₂ hi₂).inv =
  Iso.hom (ofCocone.objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
Tactic: rw [dif_pos hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
have rw : (Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
  Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi)
Tactic: rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
have rw₁ : Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ (F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
  Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi)
Tactic: rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₁ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      (F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
have rw₂ : Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv ≫ (ofCoconeObjIso c i₂ hi₂).hom =
  Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi)
Tactic: rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₁ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      (F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₂ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
have rw₃ : Iso.hom (ofCoconeObjIso c i₁ sorry) ≫
    F.map (homOfLE hi) ≫ 𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ hi₂)) =
  Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi)
Tactic: rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
rw :
  (Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₁ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      (F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₂ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₃ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      F.map (homOfLE hi) ≫ 𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ hi₂)) =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
have rw₄ : Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi) = Iso.hom (ofCoconeObjIso c i₁ sorry) ≫ F.map (homOfLE hi)
Tactic: rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
hc : IsColimit c
x : (↑(Set.Iio j) : Type u)
i : J
hi : i ∈ Set.Iio j
⊢ Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      ((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).pt)
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).symm.hom)
    (((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).ι.app
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
have dsimp : Eq (α :=
  F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
    (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))
  (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
  (Iso.inv (ofCoconeObjIso c i sorry) ≫ (ofCocone c).map (homOfLE sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
hc : IsColimit c
x : (↑(Set.Iio j) : Type u)
i : J
hi : i ∈ Set.Iio j
⊢ Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫ (ofCocone c).map (homOfLE ⋯))
have rw : Eq (α :=
  F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
    (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))
  (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
  (Iso.inv (ofCoconeObjIso c i sorry) ≫
    (ofCoconeObjIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
Tactic: rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
hc : IsColimit c
x : (↑(Set.Iio j) : Type u)
i : J
hi : i ∈ Set.Iio j
rw :
  Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫
      (ofCoconeObjIso c i hi).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
⊢ Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫ (ofCocone c).map (homOfLE ⋯))
have rw₁ : Eq (α :=
  F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
    (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))
  (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
  (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
Tactic: rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ arrowMap (ofCocone c) i j ⋯ ⋯ =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
have rw : Arrow.mk
    ((ofCoconeObjIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv) =
  Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
Tactic: rw [arrowMap, ofCocone_map_to_top _ _ hi]