awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
X Y : C
f : X ⟶ Y
this : G.map (F.map f) ≫ adj.counit.app Y = adj.counit.app X ≫ f
⊢ IsIso (G.map (F.map f)) ↔ IsIso (F.map f)

Tactic:
exact ⟨fun _ ↦ isIso_of_fully_faithful G (F.map f), fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
h :
  ∀ ⦃P₁ P₂ : C⦄ (f : P₁ ⟶ P₂),
    isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔
      MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f
⊢ (isColocal fun (x : C) ↦ x ∈ Set.range G.obj) = MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F

Tactic:
ext P₁ P₂ f
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
P₁ P₂ : C
f : P₁ ⟶ P₂
h : IsIso (F.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f
⊢ isColocal (fun (x : C) ↦ x ∈ Set.range G.obj) f ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f

Tactic:
rw [isColocal_iff_isIso_map adj]

Premises used: CategoryTheory.ObjectProperty.isColocal_iff_isIso_map
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
P₁ P₂ : C
f : P₁ ⟶ P₂
⊢ IsIso (F.map f) ↔ MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
rw : F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F)
⊢ F.IsLocalization (isColocal fun (x : C) ↦ x ∈ Set.range G.obj)

Tactic:
rw [isColocal_eq_inverseImage_isomorphisms adj]

Premises used: CategoryTheory.ObjectProperty.isColocal_eq_inverseImage_isomorphisms
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
⊢ F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F)

Tactic:
adj.isLocalization'

Premises used: CategoryTheory.Adjunction.isLocalization'
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : G ⊣ F
inst_2 : G.Full
inst_3 : G.Faithful
⊢ F.IsLocalization (MorphismProperty.inverseImage (MorphismProperty.isomorphisms D) F)

Tactic:
exact adj.isLocalization'

Premises used: CategoryTheory.Adjunction.isLocalization'
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
rw rw₁ : P.isLocal ≤ P.isLocal
⊢ P ≤ P.isLocal.isLocal

Tactic:
rw [← le_isLocal_iff]

Premises used: CategoryTheory.ObjectProperty.le_isLocal_iff
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
rw rw₁ : W.isLocal ≤ W.isLocal
⊢ W ≤ W.isLocal.isLocal

Tactic:
rw [ObjectProperty.le_isLocal_iff]

Premises used: CategoryTheory.ObjectProperty.le_isLocal_iff
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
rw rw₁ : P.isColocal ≤ P.isColocal
⊢ P ≤ P.isColocal.isColocal

Tactic:
rw [← le_isColocal_iff]

Premises used: CategoryTheory.ObjectProperty.le_isColocal_iff
-- Module: Mathlib.CategoryTheory.Localization.Bousfield
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
rw rw₁ : W.isColocal ≤ W.isColocal
⊢ W ≤ W.isColocal.isColocal

Tactic:
rw [ObjectProperty.le_isColocal_iff]

Premises used: CategoryTheory.ObjectProperty.le_isColocal_iff
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
⟨fun g₁ g₂ h ↦ hf.isColimit.hom_ext (fun j ↦ ?_), fun g ↦ ?_⟩

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, And.intro, Function.Bijective, CategoryTheory.TransfiniteCompositionOfShape.isColimit
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
refine_1 :
  ∀ (g₁ g₂ : Y ⟶ Z) (h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)) (j : J),
    { pt := Y, ι := hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl :
                Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F }.ι.app
          j ≫
        g₁ =
      { pt := Y, ι := hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl :
                Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F }.ι.app
          j ≫
        g₂
refine_2 : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
refine ⟨fun g₁ g₂ h ↦ hf.isColimit.hom_ext (fun j ↦ ?_), fun g ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
j : J
refine_1 :
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
⊢ { pt := Y, ι := hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl :
              Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F }.ι.app
        j ≫
      g₁ =
    { pt := Y, ι := hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl :
              Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F }.ι.app
        j ≫
      g₂

Tactic:
dsimp at h ⊢
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : IsMin j
refine_1 :
  ∀ (hj : IsMin.{w} (α := J) ⊥),
    Eq (α := hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj ⊥ ⟶ Z)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app ⊥ ≫ g₁)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app ⊥ ≫ g₂)
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂

Tactic:
obtain rfl := hj.eq_bot

Premises used: IsMin.eq_bot, rfl
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
hj : IsMin.{w} (α := J) ⊥
⊢ Eq (α := hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj ⊥ ⟶ Z)
    (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app ⊥ ≫ g₁)
    (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app ⊥ ≫ g₂)

Tactic:
simpa [← cancel_epi hf.isoBot.inv]

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : ¬IsMax j
hj' :
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
⊢ Eq.{v + 1} (α := hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj j ⟶ Z)
    ((fun (g : hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj (Order.succ j) ⟶ Z) ↦
        hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map (homOfLE ⋯) ≫ g)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₁))
    ((fun (g : hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj (Order.succ j) ⟶ Z) ↦
        hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map (homOfLE ⋯) ≫ g)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₂))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : ¬IsMax j
hj' :
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
⊢ Eq (α := hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj (Order.succ j) ⟶ Z)
    (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₁)
    (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₂)

Tactic:
exact (hf.map_mem j hj _ hZ).1 (by simpa)

Premises used: And.left, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₁ =
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₂
x : (↑(Set.Iio j) : Type w)
k : J
hk : k ∈ Set.Iio j
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ⟶
      Z)
    (NatTrans.app
        (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) hf.toTransfiniteCompositionOfShape (W := P.isLocal).F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ≫
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁)
    (NatTrans.app
        (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) hf.toTransfiniteCompositionOfShape (W := P.isLocal).F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk) ≫
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂)

Tactic:
simpa using hj' _ hk
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
hj : Order.IsSuccLimit j
hj' :
  ∀ b < j,
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₁ =
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₂
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂

Tactic:
exact (hf.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
          (fun ⟨k, hk⟩ ↦ by simpa using hj' _ hk)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.TransfiniteCompositionOfShape.F, CategoryTheory.Limits.Cocone.ι, _private.0.CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionOfShapeIsLocal.match_2, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.CategoryStruct.comp, Set.principalSegIio, Eq, PrincipalSeg.cocone, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h_1 : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g₁ g₂ : Y ⟶ Z
h : f ≫ g₁ = f ≫ g₂
j : J
refine_1 :
  ∀ (j : J) (hj : IsMin j),
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
refine_1₁ :
  ∀ (j : J) (hj : ¬IsMax j)
    (hj' :
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
        hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂),
    Eq (α := hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.obj (Order.succ j) ⟶ Z)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₁)
      (hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app (Order.succ j) ≫ g₂)
refine_1₂ :
  ∀ (j : J) (hj : Order.IsSuccLimit j)
    (hj' :
      ∀ b < j,
        hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₁ =
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app b ≫ g₂),
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
      hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂

Tactic:
induction j using SuccOrder.limitRecOn with
      | isMin j hj =>
        obtain rfl := hj.eq_bot
        simpa [← cancel_epi hf.isoBot.inv]
      | succ j hj hj' => exact (hf.map_mem j hj _ hZ).1 (by simpa)
      | isSuccLimit j hj hj' =>
        exact (hf.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
          (fun ⟨k, hk⟩ ↦ by simpa using hj' _ hk)

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g_1 : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z)) :
    Type (max w v))
x x_1 : (↑(Set.Iio j) : Type w)
g : x ⟶ x_1
dsimp :
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → hf.F.obj (↑(unop j_1) : J) ⟶ Z) (op x_1) =
    (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → hf.F.obj (↑(unop j_1) : J) ⟶ Z) (op x) ≫ 𝟙 Z
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F)
        x ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) Z) x_1)
    (Functor.map
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F)
        g ≫
      (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).obj j_1) (op x_1))
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).obj j_1) (op x) ≫
      Functor.map (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) Z) g)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g_1 : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z)) :
    Type (max w v))
x x_1 : (↑(Set.Iio j) : Type w)
g : x ⟶ x_1
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → hf.F.obj (↑(unop j_1) : J) ⟶ Z) (op x_1) =
    (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → hf.F.obj (↑(unop j_1) : J) ⟶ Z) (op x) ≫ 𝟙 Z

Tactic:
simpa only [Category.comp_id] using s.2 g.op

Premises used: Quiver.Hom.op, CategoryTheory.Category.comp_id, Subtype.property
-- Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z)) :
    Type (max w v))
c : Cocone (J := (↑(Set.Iio j) : Type w))
  (Monotone.functor (f :=
      (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
            x1 < x2) (Set.principalSegIio j)) :
        (a : (↑(Set.Iio j) : Type w)) → J))
      ⋯ ⋙
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).F) :=
  { pt := Z,
    ι :=
      {
        app := fun (k : (↑(Set.Iio j) : Type w)) ↦
          (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).obj j_1) (op k),
        naturality := ⋯ } }
k : J
hk : k < j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).map (homOfLE ⋯).op) :
        (a : (fun (X : Type v) ↦ X) ((hf.F.op ⋙ yoneda.obj Z).obj (op j))) →
          (fun (X : Type v) ↦ X) ((hf.F.op ⋙ yoneda.obj Z).obj (op k)))
      ((hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.isColimitOfIsWellOrderContinuous j hj).desc c) =
    (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ hf.F.op ⋙ yoneda.obj Z).obj j_1)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) k hk))

Tactic:
simpa using (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, hk⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.isColimitOfIsWellOrderContinuous, CategoryTheory.TransfiniteCompositionOfShape.F, Subtype.mk, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape