awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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
have 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₂
Tactic: refine ⟨fun g₁ g₂ h ↦ hf.isColimit.hom_ext (fun j ↦ ?_), fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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₂
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have refine_2 : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
Tactic: refine ⟨fun g₁ g₂ h ↦ hf.isColimit.hom_ext (fun j ↦ ?_), fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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
⊢ { 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₂
have refine_1 : hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
  hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
Tactic: dsimp at h ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
have 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₂)
Tactic: obtain rfl := hj.eq_bot
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
have 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₂
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)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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₂
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
have 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₂)
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)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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₂)
⊢ hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₁ =
    hf.toTransfiniteCompositionOfShape (W := P.isLocal).incl.app j ≫ g₂
have 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₂
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)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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
⊢ 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)
have 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))
          sorry)
        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: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition (goal)
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.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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (hypothesis)
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.mapComposableArrows n).essImage Y
have this : L.EssSurj
Tactic: have := essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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
⊢ Functor.essImage (L.mapComposableArrows 0) Y
have zero : ∀ (Y : D), Functor.essImage (L.mapComposableArrows 0) (mk₀ Y)
Tactic: obtain ⟨Y, rfl⟩ := mk₀_surjective Y
Cleared hypotheses: Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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)
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) Y
have succ : ∀ (Y : ComposableArrows.{v_2, u_2} D n) (Z : D) (f : Z ⟶ Y.left),
  Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
Tactic: obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y
Cleared hypotheses: Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
have 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)
Tactic: obtain ⟨Y', ⟨e⟩⟩ := hn Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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
⊢ Functor.essImage (L.mapComposableArrows (n + 1)) (Y.precomp f)
have 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 sorry),
  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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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)
have succ : Eq (α :=
  (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶
    (Y.precomp f).δ₀.obj' 0 sorry)
  ((Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).map' 0 1 homMk₁._proof_4 sorry ≫
      app' e.hom 0 sorry :
    (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj (⟨0, sorry⟩ : Fin (n + 1 + 1)) ⟶
      (Y.precomp f).δ₀.obj' 0 sorry)
  ((isoOfHom L W (f'.s (W := W)) sorry ≪≫ L.objObjPreimageIso Z).hom ≫ (Y.precomp f).map' 0 1 homMk₁._proof_4 sorry :
    (Functor.obj (L.mapComposableArrows (n + 1)) (Y'.precomp (f'.f (W := W)))).obj' 0 sorry ⟶ (Y.precomp f).obj ⟨1, sorry⟩)
Tactic: refine ⟨Y'.precomp f'.f,
        ⟨isoMkSucc (isoOfHom L W _ f'.hs ≪≫ L.objObjPreimageIso Z) e ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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 ⋯
⊢ 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, ⋯⟩)
have succ : L.map (f'.f (W := W)) ≫ e.hom.app 0 = (L.map (f'.s (W := W)) ≫ Iso.hom (L.objObjPreimageIso Z)) ≫ f
Tactic: dsimp at hf' ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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
⊢ (L.mapComposableArrows n).essImage Y
have zero : ∀ (Y : ComposableArrows.{v_2, u_2} D 0), Functor.essImage (L.mapComposableArrows 0) 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']
Cleared hypotheses: n, Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (goal)
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
⊢ (L.mapComposableArrows n).essImage Y
have 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
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']
Cleared hypotheses: n, Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (hypothesis)
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.mapComposableArrows n).EssSurj
have this : (L.op.mapComposableArrows n).EssSurj
Tactic: have := essSurj_mapComposableArrows_of_hasRightCalculusOfFractions L.op W.op n
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows (hypothesis)
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).EssSurj
have this₁ : (L.mapComposableArrows n ⋙ Functor.rightOp (Equivalence.functor (opEquivalence D n))).EssSurj
Tactic: have := Functor.essSurj_of_iso (L.mapComposableArrowsOpIso n).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
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₂
⊢ LeftFractionRel (W := W) (z₁.fst (W := W)) (z₂.fst (W := W))
have 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))
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, _, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions (goal)
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₂
⊢ LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))
have 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₂),
  z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂ →
    ∀ (hft' : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
      LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))
Tactic: obtain ⟨Z, t₁, t₂, hst, _, hft', ht⟩ := h
Cleared hypotheses: h