awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 := ⋯ } }
⊢ ∃ (y : (hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).obj (op j)),
    ∀ (i : J) (hi : i < 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 i)))
          y =
        (↑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) i hi))

Tactic:
exact ⟨(hf.F.isColimitOfIsWellOrderContinuous j hj).desc c, fun k hk ↦
            by simpa using (hf.F.isColimitOfIsWellOrderContinuous j hj).fac c ⟨k, 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_1 : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f_1
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f_1
g : X ⟶ Z
d : (hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).WellOrderInductionData :=
  Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : (↑(hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).sections : Type (max w v)) :=
  d.sectionsMk (hf.toTransfiniteCompositionOfShape (W := P.isLocal).isoBot.hom ≫ g)
x x_1 : J
f : x ⟶ x_1
dsimp :
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map f ≫ (↑σ : (j : Jᵒᵖ) → hf.F.obj (unop j) ⟶ Z) (op x_1) =
    (↑σ : (j : Jᵒᵖ) → hf.F.obj (unop j) ⟶ Z) (op x) ≫ 𝟙 Z
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map f ≫
      (↑σ : (j : Jᵒᵖ) → (hf.F.op ⋙ yoneda.obj Z).obj j) (op x_1) =
    (↑σ : (j : Jᵒᵖ) → (hf.F.op ⋙ yoneda.obj Z).obj j) (op x) ≫ Functor.map (Functor.obj (Functor.const J) Z) f

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_1 : X ⟶ Y
h : P.isLocal.transfiniteCompositionsOfShape J f_1
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f_1
g : X ⟶ Z
d : (hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).WellOrderInductionData :=
  Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : (↑(hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).sections : Type (max w v)) :=
  d.sectionsMk (hf.toTransfiniteCompositionOfShape (W := P.isLocal).isoBot.hom ≫ g)
x x_1 : J
f : x ⟶ x_1
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.map f ≫ (↑σ : (j : Jᵒᵖ) → hf.F.obj (unop j) ⟶ Z) (op x_1) =
    (↑σ : (j : Jᵒᵖ) → hf.F.obj (unop j) ⟶ Z) (op x) ≫ 𝟙 Z

Tactic:
simpa only [Category.comp_id] using σ.2 f.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
d : (hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).WellOrderInductionData :=
  Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : (↑(hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).sections : Type (max w v)) :=
  d.sectionsMk (hf.toTransfiniteCompositionOfShape (W := P.isLocal).isoBot.hom ≫ g)
c : Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F :=
  { pt := Z, ι := { app := fun (j : J) ↦ (↑σ : (j : Jᵒᵖ) → (hf.F.op ⋙ yoneda.obj Z).obj j) (op j), naturality := ⋯ } }
⊢ (fun (g : Y ⟶ Z) ↦ f ≫ g) (hf.toTransfiniteCompositionOfShape (W := P.isLocal).isColimit.desc c) = g

Tactic:
simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot, CategoryTheory.TransfiniteCompositionOfShape.fac, Bot.bot, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, 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
g : X ⟶ Z
d : (hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).WellOrderInductionData :=
  Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : (↑(hf.toTransfiniteCompositionOfShape (W := P.isLocal).F.op ⋙ Functor.obj yoneda Z).sections : Type (max w v)) :=
  d.sectionsMk (hf.toTransfiniteCompositionOfShape (W := P.isLocal).isoBot.hom ≫ g)
c : Cocone hf.toTransfiniteCompositionOfShape (W := P.isLocal).F :=
  { pt := Z, ι := { app := fun (j : J) ↦ (↑σ : (j : Jᵒᵖ) → (hf.F.op ⋙ yoneda.obj Z).obj j) (op j), naturality := ⋯ } }
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
exact ⟨hf.isColimit.desc c, by
        simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
n : ℕ
Y : ComposableArrows.{v_2, u_2} D n
⊢ L.EssSurj

Tactic:
have := essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
Y : ComposableArrows.{v_2, u_2} D 0
zero : ∀ (Y : D), Functor.essImage (L.mapComposableArrows 0) (mk₀ Y)
⊢ Functor.essImage (L.mapComposableArrows 0) Y

Tactic:
obtain ⟨Y, rfl⟩ := mk₀_surjective Y

Premises used: CategoryTheory.ComposableArrows.mk₀_surjective, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
Y : D
⊢ Functor.essImage (L.mapComposableArrows 0) (mk₀ Y)

Tactic:
⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩

Premises used: CategoryTheory.ComposableArrows.isoMk₀, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro, CategoryTheory.ComposableArrows.mk₀
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
Y : D
⊢ Functor.essImage (L.mapComposableArrows 0) (mk₀ Y)

Tactic:
exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D (n + 1)
succ :
  ∀ (Y : ComposableArrows.{v_2, u_2} D n) (Z : D) (f : Z ⟶ Y.left),
    Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) Y

Tactic:
obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y

Premises used: CategoryTheory.ComposableArrows.precomp_surjective, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
succ :
  ∀ (Y' : ComposableArrows.{v_1, u_1} C n) (e : (L.mapComposableArrows n).obj Y' ≅ Y),
    Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)

Tactic:
obtain ⟨Y', ⟨e⟩⟩ := hn Y
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows.{v_1, u_1} C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
succ :
  ∀ (f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0))
    (hf' : Iso.hom (L.objObjPreimageIso Z) ≫ f ≫ Iso.inv (e.app 0) = f'.map (W := W) L ⋯),
    Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)

Tactic:
obtain ⟨f', hf'⟩ := exists_rightFraction L W
        ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)

Premises used: CategoryTheory.Localization.exists_rightFraction, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.app, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows.{v_1, u_1} C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : Iso.hom (L.objObjPreimageIso Z) ≫ f ≫ Iso.inv (e.app 0) = f'.map (W := W) L ⋯
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)

Tactic:
⟨Y'.precomp f'.f,
        ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩

Premises used: CategoryTheory.MorphismProperty.RightFraction.f, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.ComposableArrows.isoMkSucc, CategoryTheory.Localization.isoOfHom, CategoryTheory.ComposableArrows.precomp, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.MorphismProperty.RightFraction.hs
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows.{v_1, u_1} C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : Iso.hom (L.objObjPreimageIso Z) ≫ f ≫ Iso.inv (e.app 0) = f'.map (W := W) L ⋯
succ :
  Eq (α :=
    (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶
      (Y.precomp f).δ₀.obj' 0 ⋯)
    ((Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).map' 0 1 homMk₁._proof_4 ⋯ ≫
        app' e.hom 0 ⋯ :
      (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶
        (Y.precomp f).δ₀.obj' 0 ⋯)
    ((isoOfHom L W (f'.s (W := W)) ⋯ ≪≫ L.objObjPreimageIso Z).hom ≫ (Y.precomp f).map' 0 1 homMk₁._proof_4 ⋯ :
      (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj' 0 ⋯ ⟶ (Y.precomp f).obj ⟨1, ⋯⟩)
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)

Tactic:
refine ⟨Y'.precomp f'.f,
        ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows.{v_1, u_1} C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : Iso.hom (L.objObjPreimageIso Z) ≫ f ≫ Iso.inv (e.app 0) = f'.map (W := W) L ⋯
succ : L.map (f'.f (W := W)) ≫ e.hom.app 0 = (L.map (f'.s (W := W)) ≫ Iso.hom (L.objObjPreimageIso Z)) ≫ f
⊢ Eq (α :=
    (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶
      (Y.precomp f).δ₀.obj' 0 ⋯)
    ((Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).map' 0 1 homMk₁._proof_4 ⋯ ≫
        app' e.hom 0 ⋯ :
      (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, ⋯⟩ : Fin (n + 1 + 1)) ⟶
        (Y.precomp f).δ₀.obj' 0 ⋯)
    ((isoOfHom L W (f'.s (W := W)) ⋯ ≪≫ L.objObjPreimageIso Z).hom ≫ (Y.precomp f).map' 0 1 homMk₁._proof_4 ⋯ :
      (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj' 0 ⋯ ⟶ (Y.precomp f).obj ⟨1, ⋯⟩)

Tactic:
dsimp at hf' ⊢
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows.{v_2, u_2} D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows.{v_1, u_1} C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : Iso.hom (L.objObjPreimageIso Z) ≫ f ≫ e.inv.app 0 = f'.map (W := W) L ⋯
⊢ L.map (f'.f (W := W)) ≫ e.hom.app 0 = (L.map (f'.s (W := W)) ≫ Iso.hom (L.objObjPreimageIso Z)) ≫ f

Tactic:
simp [← cancel_mono (e.inv.app 0), hf']

Premises used: CategoryTheory.cancel_mono, OfNat.ofNat, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasRightCalculusOfFractions
n : ℕ
Y : ComposableArrows.{v_2, u_2} D n
this : L.EssSurj
zero : ∀ (Y : ComposableArrows.{v_2, u_2} D 0), Functor.essImage (L.mapComposableArrows 0) Y
succ :
  ∀ (n : ℕ) (hn : ∀ (Y : ComposableArrows.{v_2, u_2} D n), (L.mapComposableArrows n).essImage Y)
    (Y : ComposableArrows.{v_2, u_2} D (n + 1)), Functor.essImage (L.mapComposableArrows (n + 1)) Y
⊢ (L.mapComposableArrows n).essImage Y

Tactic:
induction n with
    | zero =>
      obtain ⟨Y, rfl⟩ := mk₀_surjective Y
      exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩
    | succ n hn =>
      obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y
      obtain ⟨Y', ⟨e⟩⟩ := hn Y
      obtain ⟨f', hf'⟩ := exists_rightFraction L W
        ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)
      refine ⟨Y'.precomp f'.f,
        ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
      dsimp at hf' ⊢
      simp [← cancel_mono (e.inv.app 0), hf']

Premises used: CategoryTheory.ComposableArrows.mk₀_surjective, CategoryTheory.ComposableArrows.precomp_surjective, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
n : ℕ
⊢ (L.op.mapComposableArrows n).EssSurj

Tactic:
have := essSurj_mapComposableArrows_of_hasRightCalculusOfFractions L.op W.op n
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
n : ℕ
this : (L.op.mapComposableArrows n).EssSurj
⊢ (L.mapComposableArrows n ⋙ Functor.rightOp (Equivalence.functor (opEquivalence D n))).EssSurj

Tactic:
have := Functor.essSurj_of_iso (L.mapComposableArrowsOpIso n).symm
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
n : ℕ
this_1 : (L.op.mapComposableArrows n).EssSurj
this : (L.mapComposableArrows n ⋙ Functor.rightOp (Equivalence.functor (opEquivalence D n))).EssSurj
⊢ (L.mapComposableArrows n).EssSurj

Tactic:
Functor.essSurj_of_comp_fully_faithful _ (opEquivalence D n).functor.rightOp

Premises used: CategoryTheory.Functor.essSurj_of_comp_fully_faithful, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.rightOp, CategoryTheory.ComposableArrows.opEquivalence
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
n : ℕ
this_1 : (L.op.mapComposableArrows n).EssSurj
this : (L.mapComposableArrows n ⋙ Functor.rightOp (Equivalence.functor (opEquivalence D n))).EssSurj
⊢ (L.mapComposableArrows n).EssSurj

Tactic:
exact Functor.essSurj_of_comp_fully_faithful _ (opEquivalence D n).functor.rightOp

Premises used: CategoryTheory.Functor.essSurj_of_comp_fully_faithful, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.rightOp, CategoryTheory.ComposableArrows.opEquivalence
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X Y : C
z : W.LeftFraction₂ X Y
⊢ IsIso (L.map (z.s (W := W)))

Tactic:
Localization.inverts L W _ z.hs

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.hs, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X Y : C
z : W.LeftFraction₃ X Y
⊢ IsIso (L.map (z.s (W := W)))

Tactic:
Localization.inverts L W _ z.hs

Premises used: CategoryTheory.MorphismProperty.LeftFraction₃.hs, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X Y : C
z : W.RightFraction₂ X Y
⊢ IsIso (L.map (z.s (W := W)))

Tactic:
Localization.inverts L W _ z.hs

Premises used: CategoryTheory.MorphismProperty.RightFraction₂.hs, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel (W := W) z₁ z₂
obtain :
  ∀ (Z : C) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
    (hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂),
    z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂ →
      ∀ (ht : W (z₁.s (W := W) ≫ t₁)), LeftFractionRel (W := W) (z₁.fst (W := W)) (z₂.fst (W := W))
⊢ LeftFractionRel (W := W) (z₁.fst (W := W)) (z₂.fst (W := W))

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, _, ht⟩ := h
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
w : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) (z₁.fst (W := W)) (z₂.fst (W := W))

Tactic:
⟨Z, t₁, t₂, hst, hft, ht⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
w : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) (z₁.fst (W := W)) (z₂.fst (W := W))

Tactic:
exact ⟨Z, t₁, t₂, hst, hft, ht⟩