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 : 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
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
⊢ (fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g)
      (Multicoequalizer.desc (D₂.multispanIndex W Z) T
        (fun (x : (D₂.multispanShape W Z).R) ↦
          match (motive := (x : (D₂.multispanShape W Z).R) → MultispanIndex.right (D₂.multispanIndex W Z) x ⟶ T) x with
          | PUnit.unit => pushout.desc (Sigma.desc f) g ⋯)
        ⋯) =
    g

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 : 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
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

Tactic:
exact ⟨Multicoequalizer.desc _ _ (fun ⟨⟩ ↦ pushout.desc (Sigma.desc f) g)
      (fun d ↦ (hT d.1.1.hom d.1.2).1 (by simp [reassoc_of% d.2.2])), 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 : 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)
⊢ IsIso (Y := succ W Z) (toSucc W Z) ↔ W.isLocal Z

Tactic:
⟨fun _ X Y f hf ↦ ?_, fun hZ ↦ ?_⟩

Premises used: Iff.intro
-- 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 :
  IsIso (Y := succ W Z) (toSucc W Z) →
    ∀ (X Y : C) (f : X ⟶ Y) (hf : W f), Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
refine_2 : ∀ (hZ : W.isLocal Z), IsIso (Y := succ W Z) (toSucc W Z)
⊢ IsIso (Y := succ W Z) (toSucc W Z) ↔ W.isLocal Z

Tactic:
refine ⟨fun _ X Y f hf ↦ ?_, fun hZ ↦ ?_⟩
-- 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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
⊢ 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
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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
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_1₁ : ∀ (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
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)
h_1 : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g₁ g₂ : Y ⟶ Z
h : Eq.{v + 1} (α := X ⟶ Z) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₁) ((fun (g : Y ⟶ Z) ↦ f ≫ g) g₂)
⊢ Eq (α := X ⟶ step W Z) (f ≫ g₁ ≫ toStep W Z) (f ≫ g₂ ≫ toStep W Z)

Tactic:
simp [reassoc_of% 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)
h_1 : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
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₂

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

Premises used: CategoryTheory.OrthogonalReflection.toSucc, CategoryTheory.OrthogonalReflection.D₂.condition, CategoryTheory.cancel_mono
-- 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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := succ W Z) (toSucc W Z) (inv (toSucc W Z)) = 𝟙 Z

Tactic:
have hZ := IsIso.hom_inv_id (toSucc W Z)
-- 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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ : CategoryStruct.comp (Y := succ W Z) (toSucc W Z) (inv (toSucc W Z)) = 𝟙 Z
⊢ CategoryStruct.comp (Y := step W Z) (toStep W Z)
      (CategoryStruct.comp (Y := succ W Z) (fromStep W Z) (inv (toSucc W Z))) =
    𝟙 Z

Tactic:
simp only [Category.assoc] at hZ

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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ :
  CategoryStruct.comp (Y := step W Z) (toStep W Z)
      (CategoryStruct.comp (Y := succ W Z) (fromStep W Z) (inv (toSucc W Z))) =
    𝟙 Z
⊢ (fun (g : Y ⟶ Z) ↦ f ≫ g)
      (CategoryStruct.comp (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W))) (D₁.ιRight (W := W) f hf g)
        (CategoryStruct.comp (Y :=
          pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
            (D₁.t W Z) (D₁.l W Z))
          (pushout.inl (D₁.t W Z) (D₁.l W Z) :
            sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)) ⟶
              pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
                (D₁.t W Z) (D₁.l W Z))
          (CategoryStruct.comp (Y := succ W Z) (fromStep W Z) (inv (toSucc W Z)) :
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
                (D₁.t W Z) (D₁.l W Z) ⟶
              Z))) =
    g

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

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)
h : IsIso (Y := succ W Z) (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
g : X ⟶ Z
hZ :
  CategoryStruct.comp (Y := step W Z) (toStep W Z)
      (CategoryStruct.comp (Y := succ W Z) (fromStep W Z) (inv (toSucc W Z))) =
    𝟙 Z
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g

Tactic:
exact ⟨D₁.ιRight f hf g ≫ pushout.inl _ _ ≫ fromStep W Z ≫ inv (toSucc W Z),
        by simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc, hZ]⟩
-- 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)
hZ : W.isLocal Z
refine_2 :
  ∀ (f : succ W Z ⟶ Z) (hf : Eq.{v + 1} (α := Z ⟶ Z) ((fun (g : succ W Z ⟶ Z) ↦ toSucc W Z ≫ g) f) (𝟙 Z)),
    IsIso (Y := succ W Z) (toSucc W Z)
⊢ IsIso (Y := succ W Z) (toSucc W Z)

Tactic:
obtain ⟨f, hf⟩ := (isLocal_isLocal_toSucc W Z _ hZ).2 (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc, And.right
-- 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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ IsIso (Y := succ W Z) (toSucc W Z)

Tactic:
⟨f, hf, ?_⟩

Premises used: And.intro, Exists.intro, CategoryTheory.IsIso.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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
refine_2 : f ≫ toSucc W Z = 𝟙 (succ W Z)
⊢ IsIso (Y := succ W Z) (toSucc W Z)

Tactic:
refine ⟨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 : 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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
refine_2 :
  Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
⊢ f ≫ toSucc W Z = 𝟙 (succ W Z)

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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
refine_2 :
  Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)

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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
refine_2 :
  ∀ (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 ≫ f ≫ toSucc 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 ≫ 𝟙 (succ W Z)
refine_2₁ :
  pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)

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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
d : D₁ W Z
⊢ toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z

Tactic:
simp only [Category.assoc] at hf

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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
refine_2 :
  Eq (α := d.obj₂ (W := W) ⟶ succ W Z)
    (((CategoryStruct.comp (Y :=
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
              (D₁.t W Z) (D₁.l 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) ≫
          f) ≫
        toStep W Z) ≫
      fromStep W Z)
    (CategoryStruct.comp (Y :=
      pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
        (D₁.t W Z) (D₁.l 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 ≫ f ≫ toSucc 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 ≫ 𝟙 (succ W Z)

Tactic:
simp only [Category.comp_id, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id
-- 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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
⊢ Eq (α := d.obj₂ (W := W) ⟶ succ W Z)
    (((CategoryStruct.comp (Y :=
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
              (D₁.t W Z) (D₁.l 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) ≫
          f) ≫
        toStep W Z) ≫
      fromStep W Z)
    (CategoryStruct.comp (Y :=
      pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
        (D₁.t W Z) (D₁.l 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))

Tactic:
D₂.condition _ d.1.2 ?_

Premises used: CategoryTheory.OrthogonalReflection.D₁.obj₂, Sigma.fst, CategoryTheory.OrthogonalReflection.D₂.condition, 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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
d : D₁ W Z
hf : toStep W Z ≫ fromStep W Z ≫ f = 𝟙 Z
refine_2 :
  Eq (α := (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).left ⟶ step W Z)
    ((↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫
      (CategoryStruct.comp (Y :=
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
              (D₁.t W Z) (D₁.l 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) ≫
          f) ≫
        toStep W Z)
    ((↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫
      Sigma.ι (D₁.obj₂ (W := W)) d ≫ pushout.inl (D₁.t W Z) (D₁.l W Z))
⊢ Eq (α := d.obj₂ (W := W) ⟶ succ W Z)
    (((CategoryStruct.comp (Y :=
            pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
              (D₁.t W Z) (D₁.l 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) ≫
          f) ≫
        toStep W Z) ≫
      fromStep W Z)
    (CategoryStruct.comp (Y :=
      pushout (X := sigmaObj (β := D₁ W Z) (D₁.obj₁ (W := W))) (Y := sigmaObj (β := D₁ W Z) (D₁.obj₂ (W := W)))
        (D₁.t W Z) (D₁.l 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))

Tactic:
refine D₂.condition _ d.1.2 ?_

Premises used: Sigma.fst, CategoryTheory.OrthogonalReflection.D₂.condition, 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)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    pushout.inr (D₁.t W Z) (D₁.l W Z) ≫ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)

Tactic:
simp [reassoc_of% 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
Z₀ X Y : C
⊢ W.isLocal.isLocal ((succStruct W Z).toSucc Z₀)

Tactic:
isLocal_isLocal_toSucc W Z₀

Premises used: CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc, CategoryTheory.Limits.colimit
-- 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
Z₀ X Y : C
⊢ W.isLocal.isLocal ((succStruct W Z).toSucc Z₀)

Tactic:
exact isLocal_isLocal_toSucc W Z₀

Premises used: CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc
-- 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
⊢ NoMaxOrder.{w} κ.ord.ToType

Tactic:
have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
-- 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
this : NoMaxOrder.{w} κ.ord.ToType
⊢ ¬IsMax j

Tactic:
not_isMax j

Premises used: not_isMax
-- 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
this : NoMaxOrder.{w} κ.ord.ToType
⊢ ¬IsMax j

Tactic:
exact not_isMax j

Premises used: not_isMax