awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this_1 : IsIso (F.map π)
this : IsIso (F.map (φ ≫ π))
⊢ IsIso (F.map φ)

Tactic:
IsIso.of_isIso_fac_right (F.map_comp φ π).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.Functor.map_comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this_1 : IsIso (F.map π)
this : IsIso (F.map (φ ≫ π))
⊢ IsIso (F.map φ)

Tactic:
exact IsIso.of_isIso_fac_right (F.map_comp φ π).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.Functor.map_comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
j : J
f : j ⟶ i₀
⊢ F.IsEventuallyConstantTo j

Tactic:
fun _ φ ↦ h.isIso_map φ f

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_map
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
hφ : Nonempty.{v_1 + 1} (j ⟶ i₀)
⊢ F.map φ ≫ (h.isoMap φ hφ).inv = 𝟙 (F.obj i)

Tactic:
(h.isoMap φ hφ).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
hφ : Nonempty.{v_1 + 1} (j ⟶ i₀)
⊢ (h.isoMap φ hφ).inv ≫ F.map φ = 𝟙 (F.obj j)

Tactic:
(h.isoMap φ hφ).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
obtain :
  ∀ (s : J) (γ : s ⟶ IsCofiltered.min.{v_1, u_1} i₀ j) (δ : s ⟶ j') (h₁ : γ ≫ minToRight i₀ j = δ ≫ β)
    (h₂ : γ ≫ minToLeft i₀ j = δ ≫ α), h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsCofiltered.bowtie
    (IsCofiltered.minToRight i₀ j) β (IsCofiltered.minToLeft i₀ j) α

Premises used: CategoryTheory.IsCofiltered.bowtie, CategoryTheory.IsCofiltered.minToRight, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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 = δ ≫ α
dsimp :
  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 β
⊢ h.coneπApp j = (h.isoMap α ⋯).inv ≫ F.map β

Tactic:
dsimp [coneπApp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀)
rw₁ rw₂ : Eq.{v_2 + 1} (α := F.obj i₀ ⟶ F.obj i₀) (𝟙 (F.obj i₀)) (𝟙 (F.obj i₀))
⊢ h.coneπApp i₀ = 𝟙 (F.obj i₀)

Tactic:
rw [h.coneπApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_inv_hom_id]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_inv_hom_id, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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'
dsimp : 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ
⊢ map (obj (const J) (F.obj i₀)) φ ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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'
rw : h.coneπApp j' = h.coneπApp j ≫ F.map φ
⊢ 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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 φ
rw₃ rw₄ : (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
rw [h.coneπApp_eq j _ α β, assoc, h.coneπApp_eq j' _ α (β ≫ φ), map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
dsimp :
  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
⊢ s.π.app i₀ ≫ h.cone.π.app j = s.π.app j

Tactic:
dsimp [coneπApp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
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) ⋯))
          (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)
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) ⋯))
            (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)
rw₃ 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 (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)
⊢ 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

Tactic:
rw [← s.w (IsCofiltered.minToLeft i₀ j), ← s.w (IsCofiltered.minToRight i₀ j), assoc,
      isoMap_hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsCofiltered.minToRight, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc, CategoryTheory.IsCofiltered.minToLeft
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
m : s.pt ⟶ h.cone.pt
hm : ∀ (j : J), m ≫ h.cone.π.app j = s.π.app j
⊢ m = s.π.app i₀

Tactic:
simp only [← hm i₀, cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.cone_π_app, CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
⊢ HasLimit F

Tactic:
⟨_, h.isLimitCone⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Functor.IsEventuallyConstantTo.isLimitCone
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
hc : IsLimit c
simp : IsIso (Y := F.obj i₀) (Iso.hom (hc.conePointUniqueUpToIso h.isLimitCone) : c.pt ⟶ F.obj i₀)
⊢ IsIso (c.π.app i₀)

Tactic:
simp only [← IsLimit.conePointUniqueUpToIso_hom_comp hc h.isLimitCone i₀,
    cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.cone_π_app, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.IsEventuallyConstantTo.cone_pt, CategoryTheory.Functor.IsEventuallyConstantTo.isLimitCone
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
hc : IsLimit c
⊢ IsIso (Y := F.obj i₀) (Iso.hom (hc.conePointUniqueUpToIso h.isLimitCone) : c.pt ⟶ F.obj i₀)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
hc : IsLimit c
j : J
π : j ⟶ i₀
⊢ IsIso (c.π.app j)

Tactic:
(h.precomp π).isIso_π_of_isLimit hc

Premises used: CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit, CategoryTheory.Functor.IsEventuallyConstantTo.precomp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
refine : ∀ (j : J), h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j
⊢ h.cone ≅ c

Tactic:
refine Cone.ext (asIso (c.π.app i₀)).symm (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
dsimp : h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
⊢ h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
c : Cone F
inst_3 : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min.{v_1, u_1} i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
rw : c.π.app i₀ ≫ h.coneπApp j = c.π.app j
rw₁ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app j
rw₂ : (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β
rw₃ : (c.π.app i ≫ F.map α) ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
rw₄ : c.π.app i ≫ F.map α ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
rw₅ rw₆ : c.π.app i ≫ F.map β = c.π.app i ≫ F.map β
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j

Tactic:
rw [IsIso.eq_inv_comp, ← c.w α, ← c.w β, h.coneπApp_eq j _ α β, assoc, isoMap_hom_inv_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eq, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
⊢ IsIso (F.map ι)

Tactic:
have := h ι
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this : IsIso (F.map ι)
⊢ IsIso (F.map (ι ≫ φ))

Tactic:
have := h (ι ≫ φ)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this_1 : IsIso (F.map ι)
this : IsIso (F.map (ι ≫ φ))
⊢ IsIso (F.map φ)

Tactic:
IsIso.of_isIso_fac_left (F.map_comp ι φ).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_left, CategoryTheory.Functor.map_comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
ι : i₀ ⟶ i
this_1 : IsIso (F.map ι)
this : IsIso (F.map (ι ≫ φ))
⊢ IsIso (F.map φ)

Tactic:
exact IsIso.of_isIso_fac_left (F.map_comp ι φ).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_left, CategoryTheory.Functor.map_comp, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
j : J
f : i₀ ⟶ j
⊢ F.IsEventuallyConstantFrom j

Tactic:
fun _ φ ↦ h.isIso_map φ f

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom, CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_map
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
hφ : Nonempty.{v_1 + 1} (i₀ ⟶ i)
⊢ F.map φ ≫ (h.isoMap φ hφ).inv = 𝟙 (F.obj i)

Tactic:
(h.isoMap φ hφ).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀
i j : J
φ : i ⟶ j
hφ : Nonempty.{v_1 + 1} (i₀ ⟶ i)
⊢ (h.isoMap φ hφ).inv ≫ F.map φ = 𝟙 (F.obj j)

Tactic:
(h.isoMap φ hφ).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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'
obtain :
  ∀ (s : J) (γ : IsFiltered.max.{v_1, u_1} i₀ j ⟶ s) (δ : j' ⟶ s) (h₁ : leftToMax i₀ j ≫ γ = β ≫ δ)
    (h₂ : rightToMax i₀ j ≫ γ = α ≫ δ), h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
    (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.bowtie, CategoryTheory.IsFiltered.leftToMax
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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 ≫ γ = α ≫ δ
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) ⋯)) =
    F.map α ≫ (h.isoMap β ⋯).inv
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
dsimp [coconeιApp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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₀)
rw₁ rw₂ : Eq.{v_2 + 1} (α := F.obj i₀ ⟶ F.obj i₀) (𝟙 (F.obj i₀)) (𝟙 (F.obj i₀))
⊢ h.coconeιApp i₀ = 𝟙 (F.obj i₀)

Tactic:
rw [h.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_hom_inv_id]

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap_hom_inv_id, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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'
dsimp : F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ map (obj (const J) (F.obj i₀)) φ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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'
rw : F.map φ ≫ h.coconeιApp j' = h.coconeιApp j
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
rw₃ 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

Tactic:
rw [h.coconeιApp_eq j' _ β α, h.coconeιApp_eq j _ (φ ≫ β) α, map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp_eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
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
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) ⋯)) ≫
      s.ι.app i₀ =
    s.ι.app j
⊢ h.cocone.ι.app j ≫ s.ι.app i₀ = s.ι.app j

Tactic:
dsimp [coconeιApp]

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp