Skip to content

Commit

Permalink
bump to nightly-2023-04-27-10
Browse files Browse the repository at this point in the history 
mathlib commit leanprover-community/mathlib@9b2b58d
  • Loading branch information
@leanprover-community-bot
leanprover-community-bot committed Apr 27, 2023
1 parent 24e5c72 commit 7700f7f
Show file tree
Hide file tree
Showing 6 changed files with 221 additions and 57 deletions.
2 changes: 1 addition & 1 deletion Mathbin/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -429,7 +429,7 @@ theorem gramSchmidtOrthonormalBasis_det :
(gramSchmidtOrthonormalBasis h f).toBasis.det f =
∏ i, ⟪gramSchmidtOrthonormalBasis h f i, f i⟫ :=
by
convert Matrix.det_of_upper_triangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
convert Matrix.det_of_upperTriangular (gramSchmidtOrthonormalBasis_inv_blockTriangular h f)
ext i
exact ((gramSchmidtOrthonormalBasis h f).repr_apply_apply (f i) i).symm
#align gram_schmidt_orthonormal_basis_det gramSchmidtOrthonormalBasis_det
Expand Down
2 changes: 1 addition & 1 deletion Mathbin/CategoryTheory/Limits/Final.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -477,7 +477,7 @@ def colimitCompCoyonedaIso (d : D) [IsIso (colimit.pre (coyoneda.obj (op d)) F)]
lean 3 declaration is
forall {C : Type.{u1}} [_inst_1 : CategoryTheory.Category.{u1, u1} C] {D : Type.{u1}} [_inst_2 : CategoryTheory.Category.{u1, u1} D] {F : CategoryTheory.Functor.{u1, u1, u1, u1} C _inst_1 D _inst_2} {d : D} {f₁ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X))} {f₂ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X))}, (EqvGen.{u1} (Sigma.{u1, u1} C (fun (j : C) => CategoryTheory.Functor.obj.{u1, u1, u1, succ u1} C _inst_1 Type.{u1} CategoryTheory.types.{u1} (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 Type.{u1} CategoryTheory.types.{u1} F (CategoryTheory.Functor.obj.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2) (Opposite.op.{succ u1} D d))) j)) (CategoryTheory.Limits.Types.Quot.Rel.{u1, u1} C _inst_1 (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 Type.{u1} CategoryTheory.types.{u1} F (CategoryTheory.Functor.obj.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2) (Opposite.op.{succ u1} D d)))) f₁ f₂) -> (CategoryTheory.Zigzag.{u1, u1} (CategoryTheory.StructuredArrow.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.StructuredArrow.category.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X)) f₁) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X)) f₁)) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X)) f₂) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (CategoryTheory.Functor.obj.{u1, u1, u1, u1} C _inst_1 D _inst_2 F X)) f₂)))
but is expected to have type
forall {C : Type.{u1}} [_inst_1 : CategoryTheory.Category.{u1, u1} C] {D : Type.{u1}} [_inst_2 : CategoryTheory.Category.{u1, u1} D] {F : CategoryTheory.Functor.{u1, u1, u1, u1} C _inst_1 D _inst_2} {d : D} {f₁ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X))} {f₂ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X))}, (EqvGen.{u1} (Sigma.{u1, u1} C (fun (j : C) => Prefunctor.obj.{succ u1, succ u1, u1, succ u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) Type.{u1} (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} Type.{u1} (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} Type.{u1} CategoryTheory.types.{u1})) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} C _inst_1 Type.{u1} CategoryTheory.types.{u1} (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 Type.{u1} CategoryTheory.types.{u1} F (Prefunctor.obj.{succ u1, succ u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.toCategoryStruct.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2))) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2)) (Opposite.op.{succ u1} D d)))) j)) (CategoryTheory.Limits.Types.Quot.Rel.{u1, u1} C _inst_1 (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 Type.{u1} CategoryTheory.types.{u1} F (Prefunctor.obj.{succ u1, succ u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.toCategoryStruct.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2))) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2)) (Opposite.op.{succ u1} D d)))) f₁ f₂) -> (CategoryTheory.Zigzag.{u1, u1} (CategoryTheory.StructuredArrow.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.instCategoryStructuredArrow.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₁) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₁)) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₂) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₂)))
forall {C : Type.{u1}} [_inst_1 : CategoryTheory.Category.{u1, u1} C] {D : Type.{u1}} [_inst_2 : CategoryTheory.Category.{u1, u1} D] {F : CategoryTheory.Functor.{u1, u1, u1, u1} C _inst_1 D _inst_2} {d : D} {f₁ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X))} {f₂ : Sigma.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X))}, (EqvGen.{u1} (Sigma.{u1, u1} C (fun (j : C) => Prefunctor.obj.{succ u1, succ u1, u1, succ u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) TypeMax.{u1, u1} (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} TypeMax.{u1, u1} (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} TypeMax.{u1, u1} CategoryTheory.types.{u1})) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} C _inst_1 TypeMax.{u1, u1} CategoryTheory.types.{u1} (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 TypeMax.{u1, u1} CategoryTheory.types.{u1} F (Prefunctor.obj.{succ u1, succ u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.toCategoryStruct.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2))) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2)) (Opposite.op.{succ u1} D d)))) j)) (CategoryTheory.Limits.Types.Quot.Rel.{u1, u1} C _inst_1 (CategoryTheory.Functor.comp.{u1, u1, u1, u1, u1, succ u1} C _inst_1 D _inst_2 TypeMax.{u1, u1} CategoryTheory.types.{u1} F (Prefunctor.obj.{succ u1, succ u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.toCategoryStruct.{u1, u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2))) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Category.toCategoryStruct.{u1, succ u1} (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, succ u1} (Opposite.{succ u1} D) (CategoryTheory.Category.opposite.{u1, u1} D _inst_2) (CategoryTheory.Functor.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.Functor.category.{u1, u1, u1, succ u1} D _inst_2 Type.{u1} CategoryTheory.types.{u1}) (CategoryTheory.coyoneda.{u1, u1} D _inst_2)) (Opposite.op.{succ u1} D d)))) f₁ f₂) -> (CategoryTheory.Zigzag.{u1, u1} (CategoryTheory.StructuredArrow.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.instCategoryStructuredArrow.{u1, u1, u1, u1} C _inst_1 D _inst_2 d F) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₁) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₁)) (CategoryTheory.StructuredArrow.mk.{u1, u1, u1, u1} C _inst_1 D _inst_2 d (Sigma.fst.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₂) F (Sigma.snd.{u1, u1} C (fun (X : C) => Quiver.Hom.{succ u1, u1} D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) d (Prefunctor.obj.{succ u1, succ u1, u1, u1} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} C (CategoryTheory.Category.toCategoryStruct.{u1, u1} C _inst_1)) D (CategoryTheory.CategoryStruct.toQuiver.{u1, u1} D (CategoryTheory.Category.toCategoryStruct.{u1, u1} D _inst_2)) (CategoryTheory.Functor.toPrefunctor.{u1, u1, u1, u1} C _inst_1 D _inst_2 F) X)) f₂)))
Case conversion may be inaccurate. Consider using '#align category_theory.functor.final.zigzag_of_eqv_gen_quot_rel CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_relₓ'. -/
theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶ F.obj X}
(t : EqvGen (Types.Quot.Rel.{v, v} (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
Expand Down
Loading

0 comments on commit 7700f7f

Please sign in to comment.