awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₄ : F.map δ ≫
    F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
        (F.map (minToRight i₀ j)) =
  F.map δ ≫ F.map β
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₅ : F.map δ ≫
    F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
        (F.map (minToRight i₀ j)) =
  F.map (δ ≫ β)
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
rw₅ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (δ ≫ β)
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₆ : F.map δ ≫
    F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
        (F.map (minToRight i₀ j)) =
  F.map (γ ≫ minToRight i₀ j)
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
rw₅ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (δ ≫ β)
rw₆ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (γ ≫ minToRight i₀ j)
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₇ : F.map δ ≫
    F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
        (F.map (minToRight i₀ j)) =
  F.map γ ≫ F.map (minToRight i₀ j)
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
rw₅ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (δ ≫ β)
rw₆ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (γ ≫ minToRight i₀ j)
rw₇ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₈ : F.map (δ ≫ α) ≫
    CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
      (F.map (minToRight i₀ j)) =
  F.map γ ≫ F.map (minToRight i₀ j)
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
rw :
  (h.isoMap α ⋯).hom ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).hom ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₁ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β
rw₂ :
  F.map α ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map β
rw₃ :
  (h.isoMap δ ⋯).hom ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    (h.isoMap δ ⋯).hom ≫ F.map β
rw₄ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map δ ≫ F.map β
rw₅ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (δ ≫ β)
rw₆ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map (γ ≫ minToRight i₀ j)
rw₇ :
  F.map δ ≫
      F.map α ≫
        CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
          (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
rw₈ :
  F.map (δ ≫ α) ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    F.map γ ≫ F.map (minToRight i₀ j)
⊢ CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
      (F.map (minToRight i₀ j)) =
    (h.isoMap α ⋯).inv ≫ F.map β
have rw₉ : F.map (γ ≫ minToLeft i₀ j) ≫
    CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
      (F.map (minToRight i₀ j)) =
  F.map γ ≫ F.map (minToRight i₀ j)
Tactic: rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc,
    ← cancel_epi (h.isoMap δ ⟨α⟩).hom, isoMap_hom,
    ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc,
    isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)
have rw : (h.isoMap (𝟙 i₀) sorry).inv ≫ F.map (𝟙 i₀) = 𝟙 (F.obj i₀)
Tactic: rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
rw : (h.isoMap (𝟙 i₀) ⋯).inv ≫ F.map (𝟙 i₀) = 𝟙 (F.obj i₀)
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)
have rw₁ : Eq.{v_2 + 1} (α := F.obj i₀ ⟶ F.obj i₀) (𝟙 (F.obj i₀)) (𝟙 (F.obj i₀))
Tactic: rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
⊢ map (obj (const J) (F.obj i₀)) φ ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have dsimp : 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
⊢ 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have rw : h.coneπApp j' = h.coneπApp j ≫ F.map φ
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have rw : h.coneπApp j' = ((h.isoMap α sorry).inv ≫ F.map β) ≫ F.map φ
Tactic: rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : h.coneπApp j' = ((h.isoMap α ⋯).inv ≫ F.map β) ≫ F.map φ
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have rw₁ : h.coneπApp j' = (h.isoMap α sorry).inv ≫ F.map β ≫ F.map φ
Tactic: rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : h.coneπApp j' = ((h.isoMap α ⋯).inv ≫ F.map β) ≫ F.map φ
rw₁ : h.coneπApp j' = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have rw₂ : (h.isoMap α sorry).inv ≫ F.map (β ≫ φ) = (h.isoMap α sorry).inv ≫ F.map β ≫ F.map φ
Tactic: rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : h.coneπApp j' = ((h.isoMap α ⋯).inv ≫ F.map β) ≫ F.map φ
rw₁ : h.coneπApp j' = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ
rw₂ : (h.isoMap α ⋯).inv ≫ F.map (β ≫ φ) = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ
have rw₃ : (h.isoMap α sorry).inv ≫ F.map β ≫ F.map φ = (h.isoMap α sorry).inv ≫ F.map β ≫ F.map φ
Tactic: rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
s : Cone F
j : J
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j
have dsimp : s.π.app i₀ ≫
    CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
      (F.map (minToRight i₀ j)) =
  s.π.app j
Tactic: dsimp [coneπApp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
s : Cone F
j : J
⊢ s.π.app i₀ ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    s.π.app j
have rw : CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (F.map (minToLeft i₀ j)) ≫
    CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
      (F.map (minToRight i₀ j)) =
  s.π.app j
Tactic: rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst_2 : IsCofiltered.{v_1, u_1} J
s : Cone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (F.map (minToLeft i₀ j)) ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    s.π.app j
⊢ s.π.app i₀ ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) ⋯))
        (F.map (minToRight i₀ j)) =
    s.π.app j
have rw₁ : Eq (α := s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
        (F.map (minToLeft i₀ j)) ≫
      CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (Iso.inv (h.isoMap (minToLeft i₀ j) sorry))
        (F.map (minToRight i₀ j)) :
    s.pt ⟶ F.obj j)
  (CategoryStruct.comp (Y := F.obj (IsCofiltered.min.{v_1, u_1} i₀ j)) (s.π.app (IsCofiltered.min.{v_1, u_1} i₀ j))
      (F.map (minToRight i₀ j)) :
    s.pt ⟶ F.obj j)
Tactic: rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]