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
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
refine_1 :
  g₁ ≫ p.toColimitPresentation (P := W.isLocal).diag.map u ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₃ =
    g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
refine_1₁ :
  g₁ ≫ p.toColimitPresentation (P := W.isLocal).diag.map u ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₃ =
    g₂ ≫ p.toColimitPresentation (P := W.isLocal).diag.map v ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₃
refine_1₂ refine_1₃ :
  g₂ ≫ p.toColimitPresentation (P := W.isLocal).diag.map v ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₃ =
    g₂ ≫ p.toColimitPresentation (P := W.isLocal).diag.map v ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₃
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂

Tactic:
rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, And.left, CategoryTheory.Limits.ColimitPresentation.w, 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 : 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 : X ⟶ Z
refine_2 :
  ∀ (j : J) (g : X ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j),
    ∃ (a : Y ⟶ Z),
      (fun (g : Y ⟶ Z) ↦ f ≫ g) a =
        g ≫
          { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
                  Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
            j
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = 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 : 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
⊢ Eq (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) (g ≫ p.toColimitPresentation (P := W.isLocal).ι.app j))
    ((fun (g : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) g ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j)

Tactic:
simp
-- 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 κ
j : J
g : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j
⊢ ∃ (a : Y ⟶ Z),
    Eq (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) a)
      ((fun (g : Y ⟶ p.toColimitPresentation (P := W.isLocal).diag.obj j) ↦ f ≫ g) g ≫
        { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
                Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
          j)

Tactic:
exact ⟨g ≫ p.ι.app j, by simp⟩
-- 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 : HasCardinalFilteredColimits.{w, v, u} C κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
⊢ W.isLocal.IsClosedUnderColimitsOfShape J

Tactic:
have := W.isClosedUnderColimitsOfShape_isLocal J κ hW
-- 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 : HasCardinalFilteredColimits.{w, v, u} C κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
this : W.isLocal.IsClosedUnderColimitsOfShape J
⊢ PreservesColimitsOfShape J W.isLocal.ι

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : MorphismProperty.IsSmall.{w, v, u} W
inst_2 : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} ((f : (↑W.toSet : Type (max u v))) × ((↑f : Arrow C).left ⟶ Z))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : MorphismProperty.IsSmall.{w, v, u} W
inst_2 : LocallySmall.{w, v, u} C
inst_3 : HasCoproducts.{w, v, u} C
⊢ HasCoproductsOfShape (D₁ W Z) C

Tactic:
hasColimitsOfShape_of_equivalence
    (Discrete.equivalence (equivShrink.{w} _).symm)

Premises used: CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Equiv.symm, equivShrink
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (obj₁ (W := W))
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := sigmaObj (β := D₁ W Z) (obj₁ (W := W))) (ιLeft (W := W) f hf g) (l W Z) = g

Tactic:
Sigma.ι_desc _ _

Premises used: CategoryTheory.OrthogonalReflection.D₁.obj₁, CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (obj₂ (W := W))
d : D₁ W Z
⊢ Eq (α := d.obj₁ (W := W) ⟶ sigmaObj (β := D₁ W Z) (obj₂ (W := W)))
    (CategoryStruct.comp (Y := sigmaObj (β := D₁ W Z) (obj₁ (W := W))) (Sigma.ι (obj₁ (W := W)) d) (t W Z))
    ((↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫
      Sigma.ι (obj₂ (W := W)) d)

Tactic:
apply ι_colimMap

Premises used: CategoryTheory.Limits.ι_colimMap
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (obj₂ (W := W))
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ Eq (α := X ⟶ sigmaObj (β := D₁ W Z) (obj₂ (W := W)))
    (CategoryStruct.comp (Y := sigmaObj (β := D₁ W Z) (obj₁ (W := W))) (ιLeft (W := W) f hf g) (t W Z))
    (f ≫ ιRight (W := W) f hf g)

Tactic:
apply ι_colimMap

Premises used: CategoryTheory.Limits.ι_colimMap
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : MorphismProperty.IsSmall.{w, v, u} W
inst_5 : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v}
    ((f : (↑W.toSet : Type (max u v))) ×
      { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
        (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : MorphismProperty.IsSmall.{w, v, u} W
inst_5 : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : MorphismProperty.IsSmall.{w, v, u} W
inst_5 : LocallySmall.{w, v, u} C
inst_6 : HasColimitsOfSize.{w, w, v, u} C
⊢ HasColimitsOfShape (WalkingMultispan (multispanShape W Z)) C

Tactic:
hasColimitsOfShape_of_equivalence (equivSmallModel.{w} _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := multispanShape W Z) (multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ step W Z
h : f ≫ g₁ = f ≫ g₂
⊢ Eq (α := Y ⟶ succ W Z) (g₁ ≫ fromStep W Z) (g₂ ≫ fromStep W Z)

Tactic:
Multicoequalizer.condition (D₂.multispanIndex W Z)
    ⟨⟨Arrow.mk f, hf⟩, ⟨g₁, g₂⟩, h⟩

Premises used: CategoryTheory.Limits.Multicoequalizer.condition, Prod.mk, CategoryTheory.Limits.colimit, CategoryTheory.OrthogonalReflection.D₂.multispanIndex, Subtype.mk, Sigma.mk, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ Eq (α := X ⟶ step W Z) (f ≫ g₁ ≫ toStep W Z) (f ≫ g₂ ≫ toStep W Z)

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 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
⊢ Eq (α := Y ⟶ succ W Z) (g₁ ≫ toSucc W Z) (g₂ ≫ toSucc W Z)

Tactic:
simpa using D₂.condition f hf (g₁ := g₁ ≫ toStep W Z) (g₂ := g₂ ≫ toStep W Z)
    (by simp [reassoc_of% hg])

Premises used: CategoryTheory.OrthogonalReflection.D₂.condition
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ Eq (α := X ⟶ succ W Z) (f ≫ D₁.ιRight (W := W) f hf g ≫ pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ fromStep W Z)
    (g ≫ toSucc W Z)

Tactic:
simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc]

Premises used: CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_t_assoc, CategoryTheory.Limits.pushout.condition_assoc
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
⊢ W.isLocal.isLocal (Y := succ W Z) (toSucc W Z)

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

Premises used: CategoryTheory.ObjectProperty.isLocal, 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 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
refine_1 :
  ∀ (T : C) (hT : W.isLocal T) (φ₁ φ₂ : succ W Z ⟶ T)
    (h :
      Eq.{v + 1} (α := Z ⟶ T) ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₁)
        ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₂)),
    φ₁ = φ₂
refine_2 :
  ∀ (T : C) (hT : W.isLocal T) (g : Z ⟶ T), ∃ (a : succ W Z ⟶ T), (fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) a = g
⊢ W.isLocal.isLocal (Y := succ W Z) (toSucc W Z)

Tactic:
refine fun T hT ↦ ⟨fun φ₁ φ₂ 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 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h :
  Eq.{v + 1} (α := Z ⟶ T) ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₁) ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₂)
refine_1 :
  Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
⊢ φ₁ = φ₂

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h :
  Eq.{v + 1} (α := Z ⟶ T) ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₁) ((fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) φ₂)
⊢ toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂

Tactic:
simp only [Category.assoc] at h

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
refine_1 :
  Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
refine_1 :
  ∀ (d : D₁ W Z),
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
      Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
refine_1₁ :
  pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
ext d
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
d : D₁ W Z
refine_1 :
  Eq.{v + 1} (α := (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).left ⟶ T)
    ((fun (g : (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
      (Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁))
    ((fun (g : (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
      (Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂))
⊢ Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Sigma.ι (D₁.obj₂ (W := W)) d ≫
      pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
apply (hT d.1.1.hom d.1.2).1

Premises used: CategoryTheory.Arrow.hom, Sigma.fst, And.left, Subtype.val, Subtype.property
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
d : D₁ W Z
⊢ Eq.{v + 1} (α := (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).left ⟶ T)
    ((fun (g : (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
      (Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁))
    ((fun (g : (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
      (Sigma.ι (D₁.obj₂ (W := W)) d ≫
        pushout.inl (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂))

Tactic:
simp only [← D₁.ι_comp_t_assoc, pushout.condition_assoc, h]

Premises used: CategoryTheory.OrthogonalReflection.D₁.ι_comp_t_assoc, CategoryTheory.Limits.pushout.condition_assoc
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
⊢ pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
h
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
⊢ pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
g : Z ⟶ T
refine_2 :
  ∀
    (f :
      (d : D₁ W Z) →
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T)
    (hf :
      ∀ (d : D₁ W Z),
        (fun
                (g :
                  (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶
                    T) ↦
              (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
            (f d) =
          d.snd (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z) ≫ g),
    ∃ (a : succ W Z ⟶ T), (fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) a = g
⊢ ∃ (a : succ W Z ⟶ T), (fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) a = g

Tactic:
choose f hf using fun (d : D₁ W Z) ↦ (hT d.1.1.hom d.1.2).2 (d.2 ≫ g)

Premises used: CategoryTheory.Arrow.hom, Sigma.fst, And.right, CategoryTheory.CategoryStruct.comp, Sigma.snd, Subtype.val, Subtype.property