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
j : κ.ord.ToType
⊢ (iteration W Z κ).map (homOfLE ⋯) = toSucc W ((iteration W Z κ).obj j) ≫ Iso.inv (iterationObjSuccIso W Z κ j)

Tactic:
(succStruct W Z).iterationFunctor_map_succ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ, CategoryTheory.OrthogonalReflection.succStruct
-- 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
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g₁ g₂ : Y ⟶ (iteration W Z κ).obj j
hg : f ≫ g₁ = f ≫ g₂
⊢ Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ j)) (g₁ ≫ (iteration W Z κ).map (homOfLE ⋯))
    (g₂ ≫ (iteration W Z κ).map (homOfLE ⋯))

Tactic:
simp [iteration_map_succ, reassoc_of% (toSucc_injectivity f hf _ _ hg)]

Premises used: CategoryTheory.OrthogonalReflection.toSucc_injectivity, CategoryTheory.OrthogonalReflection.iteration_map_succ
-- 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
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
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)
⊢ ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)), f ≫ g' = g ≫ (iteration W Z κ).map (homOfLE ⋯)

Tactic:
simp only [iteration_map_succ]

Premises used: CategoryTheory.OrthogonalReflection.iteration_map_succ
-- 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
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
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)
⊢ ∃ (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

Premises used: CategoryTheory.OrthogonalReflection.toSucc_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
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
g' : Y ⟶ succ W ((iteration W Z κ).obj j)
hg' : f ≫ g' = g ≫ toSucc W ((iteration W Z κ).obj j)
⊢ f ≫ g' ≫ Iso.inv (iterationObjSuccIso W Z κ j) =
    g ≫ toSucc W ((iteration W Z κ).obj j) ≫ Iso.inv (iterationObjSuccIso W Z κ 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
X Y : C
f : X ⟶ Y
hf : W f
j : κ.ord.ToType
g : X ⟶ (iteration W Z κ).obj j
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:
exact ⟨g' ≫ (iterationObjSuccIso W Z κ j).inv, by 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
⊢ W.isLocal.isLocal (Y := reflectionObj W Z κ) (reflection W Z κ)

Tactic:
W.isLocal.isLocal.transfiniteCompositionsOfShape_le κ.ord.ToType _
    ⟨transfiniteCompositionOfShapeReflection W Z κ⟩

Premises used: CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflection, CategoryTheory.ObjectProperty.isLocal, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, Nonempty.intro, Cardinal.ord, CategoryTheory.MorphismProperty.isLocal, Ordinal.ToType
-- 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
⊢ IsCardinalPresentable.{w, v, u} X κ

Tactic:
obtain ⟨_, _⟩ := hW f hf
-- 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 κ
⊢ IsCardinalPresentable.{w, v, u} Y κ

Tactic:
obtain ⟨_, _⟩ := hW f hf
-- 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 κ
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g

Tactic:
⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- 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 κ
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₂
refine_2 :
  ∀ (g : X ⟶ reflectionObj W Z κ), ∃ (a : Y ⟶ reflectionObj W Z κ), (fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) a = g
⊢ Function.Bijective (β := X ⟶ reflectionObj W Z κ) fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g

Tactic:
refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- 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₁ 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₂)
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₂
⊢ ∃ (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₂

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₁ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₁
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₂))
⊢ (g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (homOfLE ⋯)) ≫
        H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (max j₁ j₂) =
      g₁ ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁ ∧
    (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (homOfLE ⋯)) ≫
        H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (max j₁ j₂) =
      g₂ ≫ { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₂

Tactic:
simp
-- 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₁ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₁
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:
exact ⟨max j₁ j₂, g₁ ≫ H.F.map (homOfLE (le_max_left _ _)),
        g₂ ≫ H.F.map (homOfLE (le_max_right _ _)), by simp⟩
-- 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₁ 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₂)
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
⊢ g₁ = g₂

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⟩

Premises used: Cardinal.ord, Ordinal.ToType, 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₁ 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
⊢ (f ≫ g₁) ≫
      { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl :
              Cocone H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F }.ι.app
        j =
    (f ≫ g₂) ≫
      { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j

Tactic:
simpa
-- 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
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
⊢ 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)

Premises used: CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit', CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.CategoryStruct.comp, CategoryTheory.TransfiniteCompositionOfShape.isColimit