awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
have hZ : CategoryStruct.comp (Y := succ W Z) (toSucc W Z) (inv (toSucc W Z)) = 𝟙 Z
Tactic: have hZ := IsIso.hom_inv_id (toSucc W Z)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ : CategoryStruct.comp (Y := succ W Z) (toSucc W Z) (inv (toSucc W Z)) = 𝟙 Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
have hZ₁ : CategoryStruct.comp (Y := step W Z) (toStep W Z)
    (CategoryStruct.comp (Y := succ W Z) (fromStep W Z) (inv (toSucc W Z))) =
  𝟙 Z
Tactic: simp only [Category.assoc] at hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
⊢ IsIso (Y := succ W Z) (toSucc W Z)
have refine_2 : ∀ (f : succ W Z ⟶ Z) (hf : Eq.{v + 1} (α := Z ⟶ Z) ((fun (g : succ W Z ⟶ Z) ↦ toSucc W Z ≫ g) f) (𝟙 Z)),
  IsIso (Y := succ W Z) (toSucc W Z)
Tactic: obtain ⟨f, hf⟩ := (isLocal_isLocal_toSucc W Z _ hZ).2 (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ IsIso (Y := succ W Z) (toSucc W Z)
have refine_2 : f ≫ toSucc W Z = 𝟙 (succ W Z)
Tactic: refine ⟨f, hf, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ f ≫ toSucc W Z = 𝟙 (succ W Z)
have refine_2 : Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
  Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
have refine_2 : ∀ (d : D₁ W Z),
  Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
refine_2 :
  ∀ (d : D₁ W Z),
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
      Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
have refine_2₁ : pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
  pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
d : D₁ W Z
⊢ Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
have hf₁ : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
Tactic: simp only [Category.assoc] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
have refine_2 : Eq (α := d.obj₂ (W := W) ⟶ succ W Z)
  (((CategoryStruct.comp (Y :=
          pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
            (D₁.t W Z) (D₁.l W Z))
          (Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
          (Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit) ≫
        f) ≫
      toStep W Z) ≫
    fromStep W Z)
  (CategoryStruct.comp (Y :=
    pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W))) (D₁.t W Z)
      (D₁.l W Z))
    (Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
    (Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit))
Tactic: simp only [Category.comp_id, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Eq (α := d.obj₂ (W := W) ⟶ succ W Z)
    (((CategoryStruct.comp (Y :=
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
              (D₁.t W Z) (D₁.l W Z))
            (Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
            (Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit) ≫
          f) ≫
        toStep W Z) ≫
      fromStep W Z)
    (CategoryStruct.comp (Y :=
      pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
        (D₁.t W Z) (D₁.l W Z))
      (Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
      (Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit))
have refine_2 : Eq (α := (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).left ⟶ step W Z)
  ((↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫
    (CategoryStruct.comp (Y :=
          pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
            (D₁.t W Z) (D₁.l W Z))
          (Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
          (Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit) ≫
        f) ≫
      toStep W Z)
  ((↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫
    Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
Tactic: refine D₂.condition _ d.1.2 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
j : κ.ord.ToType
⊢ ¬IsMax j
have this : NoMaxOrder.{w} κ.ord.ToType
Tactic: have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
⊢ ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)), f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)
have simp : ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)),
  f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j) ≫ Iso.inv (iterationObjSuccIso W Z κ j)
Tactic: simp only [iteration_map_succ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
⊢ ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)),
    f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j) ≫ Iso.inv (iterationObjSuccIso W Z κ j)
have obtain : ∀ (g' : Y ⟶ succ W ((iteration W Z κ).obj j)) (hg' : f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j)),
  ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)),
    f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j) ≫ Iso.inv (iterationObjSuccIso W Z κ j)
Tactic: obtain ⟨g', hg'⟩ := toSucc_surjectivity f hf g
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g
have left : IsCardinalPresentable.{w, v, u} X κ
Tactic: obtain ⟨_, _⟩ := hW f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g
have right : IsCardinalPresentable.{w, v, u} Y κ
Tactic: obtain ⟨_, _⟩ := hW f hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g
have refine_1 : ∀ (g₁ g₂ : Y ⟶ reflectionObj W Z κ)
  (h :
    Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ) ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₁)
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)),
  g₁ = g₂
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
refine_1 :
  ∀ (g₁ g₂ : Y ⟶ reflectionObj W Z κ)
    (h :
      Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ) ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₁)
        ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)),
    g₁ = g₂
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g
have refine_2 : ∀ (g : X ⟶ reflectionObj W Z κ), ∃ (a : Y ⟶ reflectionObj W Z κ), (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a = g
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
g₁ g₂ : Y ⟶ reflectionObj W Z κ
h :
  Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ) ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₁)
    ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)
⊢ ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
    Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
    g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j = g₁ ∧
      g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j = g₂
have obtain : ∀ (j₁ : κ.ord.ToType) (g₁ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₁)
  (h :
    Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ)
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
        (g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁))
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)),
  ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
    Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
    g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
        g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁ ∧
      g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j = g₂
Tactic: obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₁
Cleared hypotheses: g₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
g₂ : Y ⟶ reflectionObj W Z κ
j₁ : κ.ord.ToType
g₁ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₁
h :
  Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ)
    ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
      (g₁ ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁))
    ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)
⊢ ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
    Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
    g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
        g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁ ∧
      g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j = g₂
have obtain : ∀ (j₂ : κ.ord.ToType) (g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₂)
  (h :
    Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ)
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
        (g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁))
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
        (g₂ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app
            j₂))),
  ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
    Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
    g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
        g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁ ∧
      g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
        g₂ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₂
Tactic: obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₂
Cleared hypotheses: g₂, h