awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u

Tactic:
simpa using hk
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ 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 ⋯))

Tactic:
have hg := iteration_map_succ_injectivity f hf
      (g₁ ≫ H.F.map u) (g₂ ≫ H.F.map u) (by simpa using hk)
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 ⋯))
⊢ 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 ⋯))

Tactic:
simp only [homOfLE_leOfHom, Category.assoc] at hg

Premises used: CategoryTheory.Category.assoc, CategoryTheory.homOfLE_leOfHom
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 ⋯))
⊢ 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 ⋯))

Tactic:
have := H.incl.naturality (u ≫ homOfLE (Order.le_succ k))
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 ⋯))
⊢ CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (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

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id] at this

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 κ
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
⊢ ∃ (a : Y ⟶ reflectionObj W Z κ), (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a = g

Tactic:
obtain ⟨j, g, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.TransfiniteCompositionOfShape.isColimit, rfl
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
refine_2 :
  ∀ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)) (hg' : f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)),
    ∃ (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
⊢ ∃ (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

Premises used: CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)
hg' : f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)
⊢ (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
      (g' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ j)) =
    g ≫
      { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl :
              Cocone H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F }.ι.app
        j

Tactic:
simp [reassoc_of% hg']
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)
hg' : f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)
⊢ ∃ (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:
exact ⟨g' ≫ H.incl.app (Order.succ j), by simp [reassoc_of% hg']⟩
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 κ
rw : W.isLocal.ι.leftAdjointObjIsDefined = ⊤
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
rw [Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top]

Premises used: CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 κ
h : ∀ (Z : C), W.isLocal.ι.leftAdjointObjIsDefined Z ↔ ⊤ Z
⊢ W.isLocal.ι.leftAdjointObjIsDefined = ⊤

Tactic:
ext Z
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 κ
Z : C
⊢ W.isLocal.ι.leftAdjointObjIsDefined Z ↔ ⊤ Z

Tactic:
simpa using (corepresentableBy Z hW).isCorepresentable

Premises used: CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.OrthogonalReflection.corepresentableBy
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
simpa using Cardinal.IsRegular.ne_zero Fact.out

Premises used: Cardinal.IsRegular.ne_zero, Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ Nonempty.{w + 1} κ.ord.ToType

Tactic:
have : Nonempty κ.ord.ToType := by simpa using Cardinal.IsRegular.ne_zero Fact.out
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
have : ∀ (this : OrderBot κ.ord.ToType), W.isLocal.ι.IsRightAdjoint
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
have := WellFoundedLT.toOrderBot κ.ord.ToType
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ ∀ (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
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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
⊢ ∀ (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
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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_3 :
  ∀ (Z : C) [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [HasCoproducts.{w, v, u} C],
    HasCoproductsOfShape (D₁ W Z) C
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
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
isRightAdjoint_ι W κ hW

Premises used: CategoryTheory.OrthogonalReflection.isRightAdjoint_ι