awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ Eq (α := c.pt ⟶ Y) (c.π.app { down := WalkingParallelPair.zero } ≫ f : c.pt ⟶ Y)
    (c.π.app { down := WalkingParallelPair.zero } ≫ g : c.pt ⟶ Y)
have h₁ : Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
      { down := WalkingParallelPairHom.left } ≫
    c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
  c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
    (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
      { down := WalkingParallelPairHom.left :
        ULift.{w, 0}
          (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
            ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
Tactic: have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
        { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
    c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
        { down := WalkingParallelPairHom.left :
          ULift.{w, 0}
            (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
              ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
⊢ Eq (α := c.pt ⟶ Y) (c.π.app { down := WalkingParallelPair.zero } ≫ f : c.pt ⟶ Y)
    (c.π.app { down := WalkingParallelPair.zero } ≫ g : c.pt ⟶ Y)
have h₂ : Functor.map (Functor.obj (Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))) c.pt)
      { down := WalkingParallelPairHom.right } ≫
    c.π.app { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair } =
  c.π.app { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ≫
    (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map
      { down := WalkingParallelPairHom.right :
        ULift.{w, 0}
          (ULiftHom.objDown { down := WalkingParallelPair.zero : ULift.{w, 0} WalkingParallelPair } ⟶
            ULiftHom.objDown { down := WalkingParallelPair.one : ULift.{w, 0} WalkingParallelPair }) }
Tactic: have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ {J : Type w} [inst_1 : SmallCategory J] [FinCategory J] (F : Functor.{w, v, w, u} J C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofiltered.{v, u} C
have this₁ : IsCofilteredOrEmpty.{v, u} C
Tactic: have : IsCofilteredOrEmpty C := by
    refine ⟨?_, ?_⟩
    · intro X Y
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
      exact ⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
    · intro X Y f g
      obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
      refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩
      have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
      have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
      simp_all
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := op (IsFiltered.coeq f.unop g.unop) ⟶ Y) (Quiver.Hom.op (IsFiltered.coeqHom f.unop g.unop) ≫ f)
    (Quiver.Hom.op (IsFiltered.coeqHom f.unop g.unop) ≫ g)
have rw : Eq (α := op (IsFiltered.coeq f.unop.op.unop g.unop.op.unop) ⟶ Y)
  (Quiver.Hom.op (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
  (Quiver.Hom.op (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
Tactic: rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := op (IsFiltered.coeq f.unop.op.unop g.unop.op.unop) ⟶ Y)
    (Quiver.Hom.op (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop))
have e_f : Eq (α := unop Y ⟶ IsFiltered.coeq f.unop.op.unop g.unop.op.unop)
  (f.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
  (g.unop ≫ IsFiltered.coeqHom f.unop.op.unop g.unop.op.unop)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := X ⟶ op (IsCofiltered.eq f.unop g.unop)) (f ≫ Quiver.Hom.op (IsCofiltered.eqHom f.unop g.unop))
    (g ≫ Quiver.Hom.op (IsCofiltered.eqHom f.unop g.unop))
have rw : Eq (α := X ⟶ op (IsCofiltered.eq f.unop.op.unop g.unop.op.unop))
  (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop))
  (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop))
Tactic: rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsCofilteredOrEmpty.{v, u} C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ Eq (α := X ⟶ op (IsCofiltered.eq f.unop.op.unop g.unop.op.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop))
    (Quiver.Hom.op (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop))
have e_f : Eq (α := IsCofiltered.eq f.unop.op.unop g.unop.op.unop ⟶ unop X)
  (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ f.unop)
  (IsCofiltered.eqHom f.unop.op.unop g.unop.op.unop ≫ g.unop)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.CostructuredArrow (goal)
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
⊢ IsFiltered A
have refine : (J : Type u₁) →
  {x : SmallCategory J} → {x_1 : FinCategory J} → (F : J ⥤ A ⥤ Type u₁) → limit (colimit F.flip) ⟶ colimit (limit F)
Tactic: refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.CostructuredArrow (hypothesis)
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
⊢ limit (colimit F.flip) ⟶ colimit (limit F)
have this : ∀ (b : B), PreservesLimitsOfShape (C := (↑((R ⋙ CostructuredArrow.functor L).obj b) : Type u₁) ⥤ Type u₁) J colim
Tactic: haveI : ∀ b, PreservesLimitsOfShape J
      (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by
    simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α]
    exact filtered_colim_preservesFiniteLimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.CostructuredArrow (goal)
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : IsFiltered B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered.{u₁, u₁} (CostructuredArrow L (R.obj b))
J : Type u₁
x : SmallCategory J
x_1 : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape (C := (↑((R ⋙ CostructuredArrow.functor L).obj b) : Type u₁) ⥤ Type u₁) J colim
⊢ limit (colimit F.flip) ⟶ colimit (limit F)
have refine : limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F
Tactic: refine lim.map ((colimitIsoColimitGrothendieck L F.flip).hom ≫
    (inv (colimit.pre (CostructuredArrow.grothendieckProj L ⋙ F.flip) R'))) ≫
    (colimitLimitIso (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip).inv ≫
    colim.map ?_ ≫
    colimit.pre _ R' ≫
    (colimitIsoColimitGrothendieck L (limit F)).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.CostructuredArrow (hypothesis)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
⊢ IsFiltered.{v₁, u₁} A
have this : ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
Tactic: haveI : ∀ b, IsFiltered (CostructuredArrow _ ((sB.inverse ⋙ R ⋙ sT.functor).obj b)) :=
    fun b => IsFiltered.of_equivalence (sC b.1).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.CostructuredArrow (hypothesis)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
this :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
⊢ IsFiltered.{v₁, u₁} A
have this₁ : IsFiltered (AsSmall A)
Tactic: haveI := isFiltered_of_isFiltered_costructuredArrow_small
    (sA.inverse ⋙ L ⋙ sT.functor) (sB.inverse ⋙ R ⋙ sT.functor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
⊢ Nonempty (StructuredArrow d F)
have obtain : ∀ (c : C) (f : d ⟶ F.obj c), Nonempty (StructuredArrow d F)
Tactic: obtain ⟨c, ⟨f⟩⟩ := h₁ d
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
⊢ IsFiltered (StructuredArrow d F)
have this : Nonempty (StructuredArrow d F)
Tactic: have : Nonempty (StructuredArrow d F) := by
    obtain ⟨c, ⟨f⟩⟩ := h₁ d
    exact ⟨.mk f⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
⊢ IsFiltered (StructuredArrow d F)
have suffices : IsFilteredOrEmpty (StructuredArrow d F)
Tactic: suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
⊢ IsFilteredOrEmpty (StructuredArrow d F)
have refine_1 : ∀ (f g : StructuredArrow d F), ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
Tactic: refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
refine_1 : ∀ (f g : StructuredArrow d F), ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
⊢ IsFilteredOrEmpty (StructuredArrow d F)
have refine_2 : ∀ (f g : StructuredArrow d F) (η μ : f ⟶ g), ∃ (Z : StructuredArrow d F) (h : g ⟶ Z), η ≫ h = μ ≫ h
Tactic: refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
have refine_1 : ∀ (c : C) (t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c)
  (ht :
    (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
      (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t),
  ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
Tactic: obtain ⟨c, ⟨t, ht⟩⟩ := h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right))
        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
have refine_1 : f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
Tactic: refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
refine_1 : f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
have refine_1₁ : g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
Tactic: refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
d : D
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ ∃ (Z : StructuredArrow d F) (h : g ⟶ Z), η ≫ h = μ ≫ h
have refine_2 : Eq (α :=
  f ⟶
    StructuredArrow.mk (Y := IsFiltered.coeq (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))
      (f.hom ≫
        F.map
          (StructuredArrow.Hom.right η ≫
            IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))))
  (η ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) sorry)
  (μ ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) sorry)
Tactic: refine ⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
      StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d : D
⊢ IsCofiltered (CostructuredArrow F d)
have suffices : IsFiltered (CostructuredArrow F d)ᵒᵖ
Tactic: suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d : D
⊢ IsFiltered (CostructuredArrow F d)ᵒᵖ
have suffices : IsFiltered (StructuredArrow (op d) F.op)
Tactic: suffices IsFiltered (StructuredArrow (op d) F.op) from
    IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d : D
⊢ IsFiltered (StructuredArrow (op d) F.op)
have h₃ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: apply isFiltered_structuredArrow_of_isFiltered_of_exists
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d : D
h₃ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ IsFiltered (StructuredArrow (op d) F.op)
have h₄ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
Tactic: apply isFiltered_structuredArrow_of_isFiltered_of_exists
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d_1 : D
d : Dᵒᵖ
⊢ ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
have h₃ : ∀ (c : C) (t : F.obj c ⟶ unop d), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
Tactic: obtain ⟨c, ⟨t⟩⟩ := h₁ d.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
d_1 : D
d : Dᵒᵖ
c : Cᵒᵖ
s s' : d ⟶ F.op.obj c
⊢ ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
have h₃ : ∀ (c' : C) (t : c' ⟶ unop c) (ht : F.map t ≫ s.unop = F.map t ≫ s'.unop),
  ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
Tactic: obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ F.Final
have suffices : ∀ (d : D), IsFiltered (StructuredArrow d F)
Tactic: suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
⊢ F.Initial
have suffices : ∀ (d : D), IsCofiltered (CostructuredArrow F d)
Tactic: suffices ∀ d, IsCofiltered (CostructuredArrow F d) from
    initial_of_isCofiltered_costructuredArrow F
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
⊢ ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True
have obtain : ∀ (c₀ : C) (f : IsFiltered.max.{v₂, u₂} (F.obj c) (F.obj c') ⟶ F.obj c₀), ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True
Tactic: obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))