awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
⊢ ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ

Tactic:
have (k : K) : IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ := by
    dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
rw : IsCardinalPresentable (e.functor.obj c.pt) κ
⊢ IsCardinalPresentable.{w, v, u} c.pt κ

Tactic:
rw [← isCardinalPresentable_iff_of_isEquivalence c.pt κ e.functor]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.isCardinalPresentable_iff_of_isEquivalence, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable (e.functor.obj c.pt) κ

Tactic:
isCardinalPresentable_of_isColimit' _
    (isColimitOfPreserves e.functor hc) κ hK

Premises used: CategoryTheory.ShrinkHoms.toShrinkHoms, CategoryTheory.Equivalence.functor, CategoryTheory.ShrinkHoms.fromShrinkHoms, CategoryTheory.isCardinalPresentable_of_isColimit', CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
K : Type u'
inst_2 : Category.{v', u'} K
inst_3 : HasLimitsOfShape.{v', u', w, w + 1} Kᵒᵖ (Type w)
Y : Functor.{v', v, u', u} K C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
hK : HasCardinalLT (Arrow.{v', u'} K) κ
inst_5 : ∀ (k : K), IsCardinalPresentable.{w, v, u} (Y.obj k) κ
e : Equivalence.{v, w, u, u} C (ShrinkHoms.{u} C) := ShrinkHoms.equivalence C
this : ∀ (k : K), IsCardinalPresentable ((Y ⋙ e.functor).obj k) κ
⊢ IsCardinalPresentable (e.functor.obj c.pt) κ

Tactic:
exact isCardinalPresentable_of_isColimit' _
    (isColimitOfPreserves e.functor hc) κ hK

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.isCardinalPresentable_of_isColimit', CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
⊢ ∀ (j : J), isCardinalPresentable.{w, v, u} C κ (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j)

Tactic:
have := hX.prop_diag_obj
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this :
  ∀ (j : J), isCardinalPresentable.{w, v, u} C κ (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j)
⊢ ∀ (j : J), IsCardinalPresentable.{w, v, u} (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j) κ

Tactic:
simp only [isCardinalPresentable_iff] at this ⊢

Premises used: CategoryTheory.isCardinalPresentable_iff
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this :
  ∀ (j : J), IsCardinalPresentable.{w, v, u} (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j) κ
⊢ IsCardinalPresentable.{w, v, u} X κ

Tactic:
isCardinalPresentable_of_isColimit _ hX.isColimit κ hJ

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.isCardinalPresentable_of_isColimit, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
J : Type u'
inst_3 : Category.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', w, w + 1} Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow.{v', u'} J) κ
X : C
hX : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
this :
  ∀ (j : J), IsCardinalPresentable.{w, v, u} (hX.toColimitPresentation (P := isCardinalPresentable C κ).diag.obj j) κ
⊢ IsCardinalPresentable.{w, v, u} X κ

Tactic:
exact isCardinalPresentable_of_isColimit _ hX.isColimit κ hJ

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.isCardinalPresentable_of_isColimit, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
inst : Category.{v, u} C
κ_1 : Cardinal.{w}
inst_1 : Fact κ_1.IsRegular
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
inst : Category.{v, u} C
κ_1 : Cardinal.{w}
inst_1 : Fact κ_1.IsRegular
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsLocallyPresentable.{w, v, u} C
obtain :
  ∀ (κ : Cardinal.{w}) (hκ : Fact κ.IsRegular) (h' : IsCardinalLocallyPresentable.{w, v, u} C κ),
    ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ

Tactic:
obtain ⟨κ, hκ, h'⟩ := IsLocallyPresentable.exists_cardinal C

Premises used: CategoryTheory.IsLocallyPresentable.exists_cardinal
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
h' : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ

Tactic:
⟨κ, hκ, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
hκ : Fact κ.IsRegular
h' : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ ∃ (κ : Cardinal.{w}) (x : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ

Tactic:
exact ⟨κ, hκ, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsAccessibleCategory.{w, v, u} C
X : C
obtain :
  ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular), IsCardinalAccessibleCategory.{w, v, u} C κ → IsPresentable.{w, v, u} X
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal C

Premises used: CategoryTheory.IsAccessibleCategory.exists_cardinal
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalAccessibleCategory.{w, v, u} C κ
obtain :
  ∀ (w_1 : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} w_1 → ∀ (h : w_1.IsCardinalFilteredGenerator κ), IsPresentable.{w, v, u} X
⊢ IsPresentable.{w, v, u} X

Tactic:
obtain ⟨_, _, h⟩ := HasCardinalFilteredGenerator.exists_generator C κ

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_generator
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsAccessibleCategory.{w, v, u} C
X : C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h_1 : IsCardinalAccessibleCategory.{w, v, u} C κ
w_1 : ObjectProperty.{v, u} C
w_2 : ObjectProperty.EssentiallySmall.{w, v, u} w_1
h : w_1.IsCardinalFilteredGenerator κ
⊢ IsPresentable.{w, v, u} X

Tactic:
apply h.presentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.presentable
-- Module: Mathlib.CategoryTheory.Presentable.LocallyPresentable
Goal:
C : Type u
hC : Category.{v, u} C
inst : IsLocallyPresentable.{w, v, u} C
X : C
⊢ IsPresentable.{w, v, u} X

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
⊢ 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
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
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
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ 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
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
refine_1 :
  ∀ (g₁ g₂ : Y ⟶ Z) (h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)), g₁ = g₂
refine_2 : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ 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
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
g₁ g₂ : Y ⟶ Z
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
refine_1 :
  ∀ (j₁ : J) (g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁)
    (h :
      Eq.{v + 1} (α := X ⟶ Z)
        ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₁))
        ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)),
    g₁ ≫
        { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
                Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
          j₁ =
      g₂
⊢ g₁ = g₂

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

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, rfl, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
g₂ : Y ⟶ Z
j₁ : J
g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁
h :
  Eq.{v + 1} (α := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₁))
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
refine_1 :
  ∀ (j₂ : J) (g₂ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₂)
    (h :
      Eq.{v + 1} (α := X ⟶ Z)
        ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₁))
        ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₂ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₂))),
    g₁ ≫
        { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
                Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
          j₁ =
      g₂ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₂
⊢ g₁ ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j₁ =
    g₂

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

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, rfl, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
j₁ : J
g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₂
h :
  Eq.{v + 1} (α := X ⟶ Z)
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₁))
    ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g₂ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₂))
refine_1 :
  g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
⊢ g₁ ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j₁ =
    g₂ ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₂

Tactic:
dsimp at h ⊢
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
j₁ : J
g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₂
h :
  f ≫ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ =
    f ≫ g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
⊢ (f ≫ g₁) ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j₁ =
    (f ≫ g₂) ≫ { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι }.ι.app j₂

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
j₁ : J
g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₂
h :
  f ≫ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ =
    f ≫ g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
refine_1 :
  ∀ (j₃ : J) (u : j₁ ⟶ j₃) (v : j₂ ⟶ j₃)
    (huv :
      (f ≫ g₁) ≫ p.toColimitPresentation (P := W.isLocal).diag.map u =
        (f ≫ g₂) ≫ p.toColimitPresentation (P := W.isLocal).diag.map v),
    g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂

Tactic:
obtain ⟨j₃, u, v, huv⟩ :=
        IsCardinalPresentable.exists_eq_of_isColimit κ p.isColimit (f ≫ g₁) (f ≫ g₂)
          (by simpa)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit, CategoryTheory.CategoryStruct.comp, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst_3 : Fact κ.IsRegular
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
Z : C
h_1 : ObjectProperty.colimitsOfShape.{v', u', v, u} W.isLocal J Z
X Y : C
f : X ⟶ Y
hf : W f
p : ObjectProperty.ColimitOfShape.{v', u', v, u} W.isLocal J Z
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
j₁ : J
g₁ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j₂
h :
  f ≫ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ =
    f ≫ g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv :
  (f ≫ g₁) ≫ p.toColimitPresentation (P := W.isLocal).diag.map u =
    (f ≫ g₂) ≫ p.toColimitPresentation (P := W.isLocal).diag.map v
⊢ f ≫ g₁ ≫ p.toColimitPresentation (P := W.isLocal).diag.map u =
    f ≫ g₂ ≫ p.toColimitPresentation (P := W.isLocal).diag.map v

Tactic:
simp only [Category.assoc] at huv

Premises used: CategoryTheory.Category.assoc