awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₂)
⊢ g₁ ≫
      { pt := Z, ι := p.toColimitPresentation (P := W.isLocal).ι :
              Cocone p.toColimitPresentation (P := W.isLocal).diag }.ι.app
        j₁ =
    g₂
have 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₂
Tactic: obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₂
Cleared hypotheses: g₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₂))
⊢ 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₂
have refine_1 : g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
Tactic: dsimp at h ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₂
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
have 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₂
Tactic: obtain ⟨j₃, u, v, huv⟩ :=
        IsCardinalPresentable.exists_eq_of_isColimit κ p.isColimit (f ≫ g₁) (f ≫ g₂)
          (by simpa)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
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
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
have huv₁ : 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
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
have 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₂
Tactic: rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₂
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
have 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₃
Tactic: rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₃
⊢ g₁ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₁ = g₂ ≫ p.toColimitPresentation (P := W.isLocal).ι.app j₂
have 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₃
Tactic: rw [← p.w u, ← p.w v, reassoc_of% ((p.prop_diag_obj j₃ _ hf).1 huv)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
⊢ ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
have 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
Tactic: obtain ⟨j, g, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
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 κ
⊢ PreservesColimitsOfShape J W.isLocal.ι
have this : W.isLocal.IsClosedUnderColimitsOfShape J
Tactic: have := W.isClosedUnderColimitsOfShape_isLocal J κ hW
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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)
have 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) φ₂)),
  φ₁ = φ₂
Tactic: refine fun T hT ↦ ⟨fun φ₁ φ₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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) φ₂)),
    φ₁ = φ₂
⊢ W.isLocal.isLocal (Y := succ W Z) (toSucc W Z)
have 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
Tactic: refine fun T hT ↦ ⟨fun φ₁ φ₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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) φ₂)
⊢ φ₁ = φ₂
have refine_1 : Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ = Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (hypothesis)
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) φ₂)
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
have h₁ : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
Tactic: simp only [Category.assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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 ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
have 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 ≫ φ₂
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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 ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
have 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 ≫ φ₂
Tactic: ext d
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
⊢ 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 ≫ φ₂
have 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 ≫ φ₂))
Tactic: apply (hT d.1.1.hom d.1.2).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
⊢ ∃ (a : succ W Z ⟶ T), (fun (g : succ W Z ⟶ T) ↦ toSucc W Z ≫ g) a = g
have 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
Tactic: choose f hf using fun (d : D₁ W Z) ↦ (hT d.1.1.hom d.1.2).2 (d.2 ≫ g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
have 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
Tactic: refine ⟨fun _ X Y f hf ↦ ?_, fun hZ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
⊢ IsIso (Y := succ W Z) (toSucc W Z) ↔ W.isLocal Z
have refine_2 : ∀ (hZ : W.isLocal Z), IsIso (Y := succ W Z) (toSucc W Z)
Tactic: refine ⟨fun _ X Y f hf ↦ ?_, fun hZ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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
have 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₂
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
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₂
⊢ Function.Bijective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g
have refine_1₁ : ∀ (g : X ⟶ Z), ∃ (a : Y ⟶ Z), (fun (g : Y ⟶ Z) ↦ f ≫ g) a = g
Tactic: refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩