ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p₁ p₂ : Quiver.Path a b<VAR>q₁ q₂ : Quiver.Path b c<VAR>h : p₁.length = p₂.length<GOAL>p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>q : Quiver.Path b c<GOAL>Function.Injective fun p => p.comp q
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p : Quiver.Path a b<GOAL>Function.Injective p.comp
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p₁ p₂ : Quiver.Path a b<VAR>q : Quiver.Path b c<GOAL>p₁.comp q = p₂.comp q ↔ p₁ = p₂
<VAR>V : Type u<VAR>Quiver V<VAR>a b c : V<VAR>p : Quiver.Path a b<VAR>q₁ q₂ : Quiver.Path b c<GOAL>p.comp q₁ = p.comp q₂ ↔ q₁ = q₂
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>c : V<VAR>q : Quiver.Path b c<GOAL>(p.comp q).toList = q.toList ++ p.toList
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>p : Quiver.Path a b<GOAL>List.Chain (fun x y => Nonempty (y ⟶ x)) b p.toList
<VAR>V : Type u<VAR>Quiver V<VAR>∀ (a b : V), Subsingleton (a ⟶ b)<VAR>a b : V<GOAL>Function.Injective Quiver.Path.toList
<VAR>V : Type u<VAR>Quiver V<VAR>a b : V<VAR>∀ (a b : V), Subsingleton (a ⟶ b)<VAR>p q : Quiver.Path a b<GOAL>p.toList = q.toList ↔ p = q
<VAR>V : Type u₁<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F : V ⥤q W<VAR>a : V<GOAL>F.mapPath Quiver.Path.nil = Quiver.Path.nil
<VAR>V : Type u₁<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F : V ⥤q W<VAR>a b c : V<VAR>p : Quiver.Path a b<VAR>e : b ⟶ c<GOAL>F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)
<VAR>V : Type u₁<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F : V ⥤q W<VAR>a b : V<VAR>p : Quiver.Path a b<VAR>c : V<VAR>q : Quiver.Path b c<GOAL>F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)
<VAR>V : Type u₁<VAR>Quiver V<VAR>W : Type u₂<VAR>Quiver W<VAR>F : V ⥤q W<VAR>a b : V<VAR>f : a ⟶ b<GOAL>F.mapPath f.toPath = (F.map f).toPath
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>n : SimplexCategoryᵒᵖ<GOAL>f.cechNerve.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y), f.cechNerve.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom<VAR>F : f ⟶ g<VAR>n : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.Arrow.mapCechNerve F).app n = CategoryTheory.Limits.WidePullback.lift ((CategoryTheory.Limits.WidePullback.base fun x => f.hom) ≫ F.right) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) i ≫ F.left) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>f.augmentedCechNerve.right = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>f.augmentedCechNerve.left = f.cechNerve
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>i : SimplexCategoryᵒᵖ<GOAL>f.augmentedCechNerve.hom.app i = CategoryTheory.Limits.WidePullback.base fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom<VAR>F : f ⟶ g<GOAL>(CategoryTheory.Arrow.mapAugmentedCechNerve F).left = CategoryTheory.Arrow.mapCechNerve F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback g.right (fun x => g.left) fun x => g.hom<VAR>F : f ⟶ g<GOAL>(CategoryTheory.Arrow.mapAugmentedCechNerve F).right = F.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.SimplicialObject.cechNerve.obj f = f.cechNerve
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.SimplicialObject.cechNerve.map F = CategoryTheory.Arrow.mapCechNerve F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<GOAL>(CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).right = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<GOAL>∀ {X Y : SimplexCategoryᵒᵖ} (g : X ⟶ Y), (CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.map g = CategoryTheory.Limits.WidePullback.lift (CategoryTheory.Limits.WidePullback.base fun x => f.hom) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) i)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y) (n : SimplexCategoryᵒᵖ), (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).left.app n = CategoryTheory.Limits.WidePullback.lift ((CategoryTheory.Limits.WidePullback.base fun x => X.hom) ≫ F.right) (fun i => CategoryTheory.Limits.WidePullback.π (fun x => X.hom) i ≫ F.left) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<GOAL>∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).right = F.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<VAR>n : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).left.obj n = CategoryTheory.Limits.widePullback f.right (fun x => f.left) fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<VAR>i : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.SimplicialObject.augmentedCechNerve.obj f).hom.app i = CategoryTheory.Limits.WidePullback.base fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : X ⟶ F.augmentedCechNerve<GOAL>(CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).left = G.left.app (Opposite.op (SimplexCategory.mk 0)) ≫ CategoryTheory.Limits.WidePullback.π (fun x => F.hom) 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : X ⟶ F.augmentedCechNerve<GOAL>(CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G).right = G.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F<VAR>x : SimplexCategoryᵒᵖ<GOAL>(CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).left.app x = CategoryTheory.Limits.WidePullback.lift (X.hom.app x ≫ G.right) (fun i => X.left.map ((SimplexCategory.mk 0).const (Opposite.unop x) i).op ≫ G.left) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F<GOAL>(CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G).right = G.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : X ⟶ F.augmentedCechNerve<GOAL>(CategoryTheory.SimplicialObject.cechNerveEquiv X F).symm G = CategoryTheory.SimplicialObject.equivalenceRightToLeft X F G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>X : CategoryTheory.SimplicialObject.Augmented C<VAR>F : CategoryTheory.Arrow C<VAR>G : CategoryTheory.SimplicialObject.Augmented.toArrow.obj X ⟶ F<GOAL>(CategoryTheory.SimplicialObject.cechNerveEquiv X F) G = CategoryTheory.SimplicialObject.equivalenceLeftToRight X F G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>n : SimplexCategory<GOAL>f.cechConerve.obj n = CategoryTheory.Limits.widePushout f.left (fun x => f.right) fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>x y : SimplexCategory<VAR>g : x ⟶ y<GOAL>f.cechConerve.map g = CategoryTheory.Limits.WidePushout.desc (CategoryTheory.Limits.WidePushout.head fun x => f.hom) (fun i => CategoryTheory.Limits.WidePushout.ι (fun x => f.hom) ((SimplexCategory.Hom.toOrderHom g) i)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom<VAR>F : f ⟶ g<VAR>n : SimplexCategory<GOAL>(CategoryTheory.Arrow.mapCechConerve F).app n = CategoryTheory.Limits.WidePushout.desc (F.left ≫ CategoryTheory.Limits.WidePushout.head fun x => g.hom) (fun i => F.right ≫ CategoryTheory.Limits.WidePushout.ι (fun x => g.hom) i) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<GOAL>f.augmentedCechConerve.right = f.cechConerve
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<GOAL>f.augmentedCechConerve.left = f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>i : SimplexCategory<GOAL>f.augmentedCechConerve.hom.app i = CategoryTheory.Limits.WidePushout.head fun x => f.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom<VAR>F : f ⟶ g<GOAL>(CategoryTheory.Arrow.mapAugmentedCechConerve F).right = CategoryTheory.Arrow.mapCechConerve F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f g : CategoryTheory.Arrow C<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom<VAR>F : f ⟶ g<GOAL>(CategoryTheory.Arrow.mapAugmentedCechConerve F).left = F.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<GOAL>∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.CosimplicialObject.cechConerve.map F = CategoryTheory.Arrow.mapCechConerve F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.CosimplicialObject.cechConerve.obj f = f.cechConerve
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<GOAL>∀ {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y), CategoryTheory.CosimplicialObject.augmentedCechConerve.map F = CategoryTheory.Arrow.mapAugmentedCechConerve F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.CosimplicialObject.augmentedCechConerve.obj f = f.augmentedCechConerve
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F.augmentedCechConerve ⟶ X<GOAL>(CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).right = CategoryTheory.Limits.WidePushout.ι (fun x => F.hom) 0 ≫ G.right.app (SimplexCategory.mk 0)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F.augmentedCechConerve ⟶ X<GOAL>(CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G).left = G.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X<GOAL>(CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).left = G.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X<VAR>x : SimplexCategory<GOAL>(CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G).right.app x = CategoryTheory.Limits.WidePushout.desc (G.left ≫ X.hom.app x) (fun i => G.right ≫ X.right.map ((SimplexCategory.mk 0).const x i)) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X<GOAL>(CategoryTheory.CosimplicialObject.cechConerveEquiv F X).symm G = CategoryTheory.CosimplicialObject.equivalenceRightToLeft F X G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>∀ (n : ℕ) (f : CategoryTheory.Arrow C), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>F : CategoryTheory.Arrow C<VAR>X : CategoryTheory.CosimplicialObject.Augmented C<VAR>G : F.augmentedCechConerve ⟶ X<GOAL>(CategoryTheory.CosimplicialObject.cechConerveEquiv F X) G = CategoryTheory.CosimplicialObject.equivalenceLeftToRight F X G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>ι : Type w<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>Finite ι<VAR>X : C<VAR>j : ι<GOAL>(CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv ≫ CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j = CategoryTheory.Limits.Pi.π (fun x => X) j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>ι : Type w<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>Finite ι<VAR>X : C<VAR>j : ι<GOAL>(CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).hom ≫ CategoryTheory.Limits.Pi.π (fun x => X) j = CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>self : HasFTaylorSeriesUpToOn n f p s<VAR>x : E<GOAL>x ∈ s → (p x 0).uncurry0 = f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>self : HasFTaylorSeriesUpToOn n f p s<VAR>m : ℕ<GOAL>↑m ≤ n → ContinuousOn (fun x => p x m) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>self : HasFTaylorSeriesUpToOn n f p s<VAR>m : ℕ<GOAL>↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun x => p x m) (p x m.succ).curryLeft s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>x : E<VAR>hx : x ∈ s<GOAL>p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f f₁ : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>h₁ : ∀ x ∈ s, f₁ x = f x<GOAL>HasFTaylorSeriesUpToOn n f₁ p s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>t : Set E<VAR>hst : t ⊆ s<GOAL>HasFTaylorSeriesUpToOn n f p t
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hmn : m ≤ n<GOAL>HasFTaylorSeriesUpToOn m f p s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).uncurry0 = f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpToOn ⊤ f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpToOn ⊤ f p s ↔ (∀ x ∈ s, (p x 0).uncurry0 = f x) ∧ ∀ (m : ℕ), ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : x ∈ s<GOAL>HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : s ∈ 𝓝 x<GOAL>HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : s ∈ 𝓝 x<GOAL>∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p y 1)) y
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>x : E<VAR>n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>h : HasFTaylorSeriesUpToOn n f p s<VAR>hn : 1 ≤ n<VAR>hx : s ∈ 𝓝 x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔ HasFTaylorSeriesUpToOn (↑n) f p s ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x => p x (n + 1)) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>s : Set E<VAR>f : E → F<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s<GOAL>HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s