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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
have rw₆ : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫ F.map β) ≫
    (h.isoMap δ sorry).hom =
  F.map α ≫ (h.isoMap δ sorry).hom
Tactic: rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
rw₆ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      (h.isoMap δ ⋯).hom =
    F.map α ≫ (h.isoMap δ ⋯).hom
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
have rw₇ : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫ F.map β) ≫
    F.map δ =
  F.map α ≫ F.map δ
Tactic: rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
rw₆ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      (h.isoMap δ ⋯).hom =
    F.map α ≫ (h.isoMap δ ⋯).hom
rw₇ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      F.map δ =
    F.map α ≫ F.map δ
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
have rw₈ : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
    ((Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫ F.map β) ≫ F.map δ) =
  F.map α ≫ F.map δ
Tactic: rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
rw₆ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      (h.isoMap δ ⋯).hom =
    F.map α ≫ (h.isoMap δ ⋯).hom
rw₇ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      F.map δ =
    F.map α ≫ F.map δ
rw₈ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      ((Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫ F.map δ) =
    F.map α ≫ F.map δ
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
have rw₉ : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
    (Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫ F.map β ≫ F.map δ) =
  F.map α ≫ F.map δ
Tactic: rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      (h.isoMap β ⋯).hom =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₁ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    (F.map α ≫ (h.isoMap β ⋯).inv) ≫ (h.isoMap β ⋯).hom
rw₂ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ (h.isoMap β ⋯).hom) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ (h.isoMap β ⋯).hom
rw₃ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ (h.isoMap β ⋯).inv ≫ F.map β
rw₄ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α ≫ 𝟙 (F.obj j')
rw₅ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) =
    F.map α
rw₆ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      (h.isoMap δ ⋯).hom =
    F.map α ≫ (h.isoMap δ ⋯).hom
rw₇ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫
      F.map δ =
    F.map α ≫ F.map δ
rw₈ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      ((Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β) ≫ F.map δ) =
    F.map α ≫ F.map δ
rw₉ :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯) ≫ F.map β ≫ F.map δ) =
    F.map α ≫ F.map δ
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
have rw₁₀ : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
    (Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫ F.map β ≫ F.map δ) =
  F.map (α ≫ δ)
Tactic: rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
    comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
    ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
⊢ h.coconeιApp i₀ = 𝟙 (F.obj i₀)
have rw : F.map (𝟙 i₀) ≫ (h.isoMap (𝟙 i₀) sorry).inv = 𝟙 (F.obj i₀)
Tactic: rw [h.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_hom_inv_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
rw : F.map (𝟙 i₀) ≫ (h.isoMap (𝟙 i₀) ⋯).inv = 𝟙 (F.obj i₀)
⊢ h.coconeι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.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_hom_inv_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ map (obj (const J) (F.obj i₀)) φ
have dsimp : F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)
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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)
have rw : F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
Tactic: rw [comp_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max.{v_1, u_1} i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
have rw : F.map φ ≫ F.map β ≫ (h.isoMap α sorry).inv = h.coconeιApp j
Tactic: rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, 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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max.{v_1, u_1} i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
rw : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = h.coconeιApp j
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
have rw₁ : F.map φ ≫ F.map β ≫ (h.isoMap α sorry).inv = F.map (φ ≫ β) ≫ (h.isoMap α sorry).inv
Tactic: rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, 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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max.{v_1, u_1} i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
rw : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = h.coconeιApp j
rw₁ : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map (φ ≫ β) ≫ (h.isoMap α ⋯).inv
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
have rw₂ : F.map φ ≫ F.map β ≫ (h.isoMap α sorry).inv = (F.map φ ≫ F.map β) ≫ (h.isoMap α sorry).inv
Tactic: rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, 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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
j j' : J
φ : j ⟶ j'
i : J := IsFiltered.max.{v_1, u_1} i₀ j'
α : i₀ ⟶ i := leftToMax i₀ j'
β : j' ⟶ i := rightToMax i₀ j'
rw : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = h.coconeιApp j
rw₁ : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = F.map (φ ≫ β) ≫ (h.isoMap α ⋯).inv
rw₂ : F.map φ ≫ F.map β ≫ (h.isoMap α ⋯).inv = (F.map φ ≫ F.map β) ≫ (h.isoMap α ⋯).inv
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
have rw₃ : F.map φ ≫ F.map β ≫ (h.isoMap α sorry).inv = F.map φ ≫ F.map β ≫ (h.isoMap α sorry).inv
Tactic: rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, 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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
j : J
⊢ h.cocone.ι.app j ≫ s.ι.app i₀ = s.ι.app j
have dsimp : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) sorry)) ≫
    s.ι.app i₀ =
  s.ι.app j
Tactic: dsimp [coconeι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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
j : J
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    s.ι.app j
have rw : CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) sorry)) ≫
    s.ι.app i₀ =
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
    (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))
Tactic: rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    s.ι.app j
have rw₁ : Eq (α := F.obj j ⟶ s.pt)
  (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) sorry)) ≫
      CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (leftToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
    F.obj j ⟶ s.pt)
  (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
    F.obj j ⟶ s.pt)
Tactic: rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_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.IsEventuallyConstantFrom i₀
inst_2 : IsFiltered.{v_1, u_1} J
s : Cocone F
j : J
rw :
  CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))
rw₁ :
  Eq (α := F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
          (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
        CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (leftToMax i₀ j))
          (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
    (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
      F.obj j ⟶ s.pt)
⊢ CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
        (Iso.inv (h.isoMap (leftToMax i₀ j) ⋯)) ≫
      s.ι.app i₀ =
    s.ι.app j
have rw₂ : Eq (α := F.obj j ⟶ s.pt)
  (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (Iso.inv (h.isoMap (leftToMax i₀ j) sorry) ≫
        CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (leftToMax i₀ j))
          (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j))) :
    F.obj j ⟶ s.pt)
  (CategoryStruct.comp (Y := F.obj (IsFiltered.max.{v_1, u_1} i₀ j)) (F.map (rightToMax i₀ j))
      (s.ι.app (IsFiltered.max.{v_1, u_1} i₀ j)) :
    F.obj j ⟶ s.pt)
Tactic: rw [← s.w (IsFiltered.rightToMax i₀ j), ← s.w (IsFiltered.leftToMax i₀ j), assoc,
      isoMap_inv_hom_id_assoc]