awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂)
⊢ g₁ = g₂
have refine_1 : ∀ (j : κ.ord.ToType) (g₁ 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₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j))
      ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
        (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j))),
  g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
Tactic: obtain ⟨j, g₁, g₂, rfl, rfl⟩ :
      ∃ (j : κ.ord.ToType) (g₁' g₂' : Y ⟶ H.F.obj j), g₁' ≫ H.incl.app j = g₁ ∧
        g₂' ≫ H.incl.app j = g₂ := by
      obtain ⟨j₁, g₁, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₁
      obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₂
      exact ⟨max j₁ j₂, g₁ ≫ H.F.map (homOfLE (le_max_left _ _)),
        g₂ ≫ H.F.map (homOfLE (le_max_right _ _)), by simp⟩
Cleared hypotheses: g₁, 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 κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
⊢ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
have refine_1 : ∀ (k : κ.ord.ToType) (u : j ⟶ k)
  (hk :
    (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
      (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u),
  g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
Tactic: obtain ⟨k, u, hk⟩ := IsCardinalPresentable.exists_eq_of_isColimit' κ H.isColimit
      (f ≫ g₁) (f ≫ g₂) (by simpa)
-- 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 κ
right : IsCardinalPresentable.{w, v, u} Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk :
  (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u
⊢ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
have hg : Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
  ((g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u) ≫ (iteration W Z κ).map (homOfLE sorry))
  ((g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u) ≫ (iteration W Z κ).map (homOfLE sorry))
Tactic: have hg := iteration_map_succ_injectivity f hf
      (g₁ ≫ H.F.map u) (g₂ ≫ H.F.map u) (by simpa using hk)
-- 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 κ
right : IsCardinalPresentable.{w, v, u} Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk :
  (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u
hg :
  Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
    ((g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u) ≫ (iteration W Z κ).map (homOfLE ⋯))
    ((g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u) ≫ (iteration W Z κ).map (homOfLE ⋯))
⊢ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
have hg₁ : Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
  (g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE sorry))
  (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE sorry))
Tactic: simp only [homOfLE_leOfHom, Category.assoc] at hg
Cleared hypotheses: hg
-- 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 κ
right : IsCardinalPresentable.{w, v, u} Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk :
  (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u
hg :
  Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
    (g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
    (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
⊢ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
have this : Eq (α :=
  H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j ⟶
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) (Order.succ k))
  (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (u ≫ homOfLE sorry) ≫
    H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k))
  (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j ≫
    Functor.map (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) (u ≫ homOfLE sorry))
Tactic: have := H.incl.naturality (u ≫ homOfLE (Order.le_succ k))
-- 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 κ
right : IsCardinalPresentable.{w, v, u} Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk :
  (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u
hg :
  Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
    (g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
    (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
this :
  Eq (α :=
    H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) (Order.succ k))
    (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (u ≫ homOfLE ⋯) ≫
      H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k))
    (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j ≫
      Functor.map (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) (u ≫ homOfLE ⋯))
⊢ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
have this₁ : CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (Order.succ k))
    (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (u ≫ homOfLE sorry))
    (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) =
  H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
Tactic: simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id] at this
Cleared hypotheses: this
-- 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 : X ⟶ reflectionObj W Z κ
⊢ ∃ (a : Y ⟶ reflectionObj W Z κ), (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a = g
have refine_2 : ∀ (j : κ.ord.ToType) (g : X ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
  ∃ (a : Y ⟶ reflectionObj W Z κ),
    (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a =
      g ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl :
                Cocone H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F }.ι.app
          j
Tactic: obtain ⟨j, g, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g
Cleared hypotheses: 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 κ
j : κ.ord.ToType
g : X ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
⊢ ∃ (a : Y ⟶ reflectionObj W Z κ),
    (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a =
      g ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl :
                Cocone H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F }.ι.app
          j
have refine_2 : ∀ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)) (hg' : f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE sorry)),
  ∃ (a : Y ⟶ reflectionObj W Z κ),
    (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a =
      g ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl :
                Cocone H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F }.ι.app
          j
Tactic: obtain ⟨g', hg'⟩ := iteration_map_succ_surjectivity f hf 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
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 κ
⊢ W.isLocal.ι.IsRightAdjoint
have rw : W.isLocal.ι.leftAdjointObjIsDefined = ⊤
Tactic: rw [Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} 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 κ
⊢ W.isLocal.ι.leftAdjointObjIsDefined = ⊤
have h : ∀ (Z : C), W.isLocal.ι.leftAdjointObjIsDefined Z ↔ ⊤ Z
Tactic: ext 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
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsSmall.{w, v, u} W
inst_3 : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
inst_4 : HasColimitsOfSize.{w, w, v, u} C
⊢ W.isLocal.ι.IsRightAdjoint
have this : Nonempty.{w + 1} κ.ord.ToType
Tactic: have : Nonempty κ.ord.ToType := by simpa using Cardinal.IsRegular.ne_zero Fact.out
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsSmall.{w, v, u} W
inst_3 : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
inst_4 : HasColimitsOfSize.{w, w, v, u} C
this : Nonempty.{w + 1} κ.ord.ToType
⊢ W.isLocal.ι.IsRightAdjoint
have have : ∀ (this : OrderBot κ.ord.ToType), W.isLocal.ι.IsRightAdjoint
Tactic: have := WellFoundedLT.toOrderBot κ.ord.ToType
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsSmall.{w, v, u} W
inst_3 : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
inst_4 : HasColimitsOfSize.{w, w, v, u} C
this_1 : Nonempty.{w + 1} κ.ord.ToType
this : OrderBot κ.ord.ToType
⊢ W.isLocal.ι.IsRightAdjoint
have this₁ : ∀ (Z : C) [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [HasCoproducts.{w, v, u} C], HasCoproductsOfShape (D₁ W Z) C
Tactic: have := D₁.hasCoproductsOfShape.{w} W
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsSmall.{w, v, u} W
inst_3 : LocallySmall.{w, v, u} C
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
inst_4 : HasColimitsOfSize.{w, w, v, u} C
this_1 : Nonempty.{w + 1} κ.ord.ToType
this_2 : OrderBot κ.ord.ToType
this :
  ∀ (Z : C) [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [HasCoproducts.{w, v, u} C],
    HasCoproductsOfShape (D₁ W Z) C
⊢ W.isLocal.ι.IsRightAdjoint
have this₁ : ∀ (Z : C) [inst_5 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))]
  [inst_6 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))] [inst_7 : HasPushouts.{v, u} C] [IsSmall.{w, v, u} W]
  [LocallySmall.{w, v, u} C] [HasColimitsOfSize.{w, w, v, u} C],
  HasColimitsOfShape (WalkingMultispan (D₂.multispanShape W Z)) C
Tactic: have := D₂.hasColimitsOfShape.{w} W
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
⊢ IsCardinalLocallyPresentable.{w, v, u} W.isLocal.FullSubcategory κ
have this : W.isLocal.ι.IsRightAdjoint
Tactic: have := isRightAdjoint_ι_isLocal W κ hW
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
this : W.isLocal.ι.IsRightAdjoint
⊢ IsCardinalLocallyPresentable.{w, v, u} W.isLocal.FullSubcategory κ
have this₁ : W.isLocal.ι.IsCardinalAccessible κ
Tactic: have := MorphismProperty.isCardinalAccessible_ι_isLocal W κ hW
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
⊢ IsCardinalPresentable (C := Functor.{v, v', u, u'} Cᵒᵖ A) (freeYoneda X M) κ
have preservesColimitOfShape : autoParam
  (∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M))))
  Functor.IsCardinalAccessible.preservesColimitOfShape._autoParam
Tactic: constructor