ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<GOAL>∀ {x y z : C(X, Y)}, x.Homotopic y → y.Homotopic z → x.Homotopic z
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>hgen : generator (map ϕ N) = 0<GOAL>N = ⊥
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>hgen : generator (map ϕ N) = 0<GOAL>∀ x ∈ N, x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>hgen : generator (map ϕ N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr x) i = (b.repr 0) i
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>hgen : generator (map ϕ N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr x) i = (b.repr 0) i
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_1<VAR>b✝ b : Basis ι R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N<VAR>inst✝ : (map ϕ N).IsPrincipal<VAR>hgen : generator (map ϕ N) = 0<VAR>x : M<VAR>hx : x ∈ N<VAR>i : ι<GOAL>(b.repr x) i = 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>inst✝¹ : Infinite α<VAR>inst✝ : Finite β<VAR>f : α → β<GOAL>∃ x y, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f : α → β<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : Nonempty α<GOAL>(∃ i, True ∧ ∀ y ∈ Ici i, f y = f i) ↔ ∃ i, ∀ (j : α), i ≤ j → f j = f i
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>a : ℕ<VAR>ha1 : a % 2 = 1<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>a : ℕ<VAR>ha1 : a % 2 = 1<VAR>ha0 : ↑a ≠ 0<VAR>hp' : Fact (p % 2 = 1)<GOAL>legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>a : ℕ<VAR>ha1 : a % 2 = 1<VAR>ha0 : ↑a ≠ 0<VAR>hp' : Fact (p % 2 = 1)<VAR>ha0' : ↑↑a ≠ 0<GOAL>legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>A : CostructuredArrow S T<VAR>P Q : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>g : Q ⟶ op A<VAR>inst✝¹ : Mono f.unop.left.op<VAR>inst✝ : Mono g.unop.left.op<VAR>h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op<GOAL>g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>A : CostructuredArrow S T<VAR>P Q : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>g : Q ⟶ op A<VAR>inst✝¹ : Mono f.unop.left.op<VAR>inst✝ : Mono g.unop.left.op<VAR>h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op<GOAL>g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>A : CostructuredArrow S T<VAR>P Q : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>g : Q ⟶ op A<VAR>inst✝¹ : Mono f.unop.left.op<VAR>inst✝ : Mono g.unop.left.op<VAR>h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op<GOAL>(Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
<VAR>x y : ℝ≥0∞<GOAL>(x * y).log = x.log + y.log
<VAR>y : ℝ≥0∞<GOAL>(0 * y).log = log 0 + y.log
<VAR>y : ℝ≥0∞<GOAL>(⊤ * y).log = ⊤.log + y.log
<VAR>x y : ℝ≥0∞<VAR>x_real : 0 < x.toReal<GOAL>(x * y).log = x.log + y.log
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app Y = (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map Y.decompId_i ≫ (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi C) n).app { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } ≫ (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙ alternatingFaceMapComplex (Karoubi C) ⋙ HomologicalComplex.eval (Karoubi C) (ComplexShape.down ℕ) n).map Y.decompId_p<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _[n]) ≫ PInfty.f n) ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _[n]) = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ ((𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _[n]) ≫ PInfty.f n) ≫ 𝟙 (KaroubiFunctorCategoryEmbedding.obj { X := Y.X, p := 𝟙 Y.X, idem := ⋯ } _[n])) ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<GOAL>(P₁.f n).f = Y.p.app (op [n]) ≫ P₂.f n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<GOAL>((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])).f = Y.p.app (op [n]) ≫ (P₄.f n).f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<GOAL>Y.p.app (op [n]) ≫ (PInfty.f n).f ≫ Y.p.app (op [n]) = Y.p.app (op [n]) ≫ (P₄.f n).f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<VAR>π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p<GOAL>Y.p.app (op [n]) ≫ (PInfty.f n).f ≫ Y.p.app (op [n]) = Y.p.app (op [n]) ≫ (P₄.f n).f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<VAR>π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p<VAR>eq : (π.app (op [n]) ≫ PInfty.f n).f = (PInfty.f n ≫ π.app (op [n])).f<GOAL>Y.p.app (op [n]) ≫ (PInfty.f n).f ≫ Y.p.app (op [n]) = Y.p.app (op [n]) ≫ (P₄.f n).f
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : Karoubi (SimplicialObject C)<VAR>n : ℕ<VAR>Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj Y<VAR>Y₂ : SimplicialObject C := Y.X<VAR>Y₃ : SimplicialObject (Karoubi C) := ((whiskering C (Karoubi C)).obj (toKaroubi C)).obj Y.X<VAR>Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi C := (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).obj ((toKaroubi (SimplexCategoryᵒᵖ ⥤ C)).obj Y.X)<VAR>P₁ : K[Y₁] ⟶ K[Y₁] := PInfty<VAR>P₂ : K[Y₂] ⟶ K[Y₂] := PInfty<VAR>P₃ : K[Y₃] ⟶ K[Y₃] := PInfty<VAR>P₄ : K[Y₄] ⟶ K[Y₄] := PInfty<VAR>h₃₂ : (P₃.f n).f = P₂.f n<VAR>h₄₃ : P₄.f n = P₃.f n<VAR>h₁₄ : PInfty.f n = (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op [n]) ≫ PInfty.f n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op [n])<VAR>π : Y₄ ⟶ Y₄ := (toKaroubi (SimplexCategoryᵒᵖ ⥤ C) ⋙ karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C).map Y.p<VAR>eq : (π.app (op [n])).f ≫ (PInfty.f n).f = (PInfty.f n).f ≫ (π.app (op [n])).f<GOAL>Y.p.app (op [n]) ≫ (PInfty.f n).f ≫ Y.p.app (op [n]) = Y.p.app (op [n]) ≫ (P₄.f n).f
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s : Set X<VAR>h : s.Subsingleton<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>dimH s = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s : Set X<VAR>h : s.Subsingleton<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>dimH s ≤ 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s : Set X<VAR>h : s.Subsingleton<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<GOAL>μH[↑0] s ≠ ⊤
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun z => Real.exp (a.re * Real.log (abs z))) =o[l] fun x => ‖cexp (↑b * x)‖
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>Tendsto (fun x => b * x.re - a.re * Real.log (abs x)) l atTop
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : 0 < b<GOAL>(fun x => a.re * Real.log (abs x)) =o[l] fun x => b * x.re
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>F : BraidedFunctor C D<VAR>X Y : C<GOAL>F.μ X Y ≫ F.map (β_ X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ F.μ Y X
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>F : BraidedFunctor C D<VAR>X Y : C<GOAL>F.μ X Y ≫ inv (F.μ X Y) ≫ (β_ (F.obj X) (F.obj Y)).hom ≫ F.μ Y X = (β_ (F.obj X) (F.obj Y)).hom ≫ F.μ Y X
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>hsur : Function.Surjective ⇑(algebraMap R A)<VAR>X : Set M<GOAL>restrictScalars R (span A X) = span R X
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>hsur : Function.Surjective ⇑(algebraMap R A)<VAR>X : Set M<VAR>m : M<VAR>hm : m ∈ restrictScalars R (span A X)<GOAL>m ∈ span R X
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>hsur : Function.Surjective ⇑(algebraMap R A)<VAR>X : Set M<VAR>m✝ : M<VAR>hm✝ : m✝ ∈ restrictScalars R (span A X)<VAR>a : A<VAR>m : M<VAR>hm : m ∈ span R X<GOAL>a • m ∈ span R X
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module A M<VAR>inst✝ : IsScalarTower R A M<VAR>hsur : Function.Surjective ⇑(algebraMap R A)<VAR>X : Set M<VAR>m✝ : M<VAR>hm✝ : m✝ ∈ restrictScalars R (span A X)<VAR>m : M<VAR>hm : m ∈ span R X<VAR>r : R<GOAL>(algebraMap R A) r • m ∈ span R X
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>(fun x => x ^ p) =o[atTop] fun x => x ^ q
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p q : ℕ<VAR>hpq : p < q<GOAL>∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CanonicallyOrderedCommSemiring α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>m n : ℕ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CanonicallyOrderedCommSemiring α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>↑(m - n) = ↑m - ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : CanonicallyOrderedCommSemiring α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>↑(m - n) = ↑m - ↑n
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.1672, u_1} C<VAR>P : Karoubi (Karoubi C)<GOAL>P.p.f ≫ P.p.f = P.p.f
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.1672, u_1} C<VAR>X✝ Y✝ : Karoubi (Karoubi C)<VAR>f : X✝ ⟶ Y✝<GOAL>f.f.f = ((fun P => { X := P.X.X, p := P.p.f, idem := ⋯ }) X✝).p ≫ f.f.f ≫ ((fun P => { X := P.X.X, p := P.p.f, idem := ⋯ }) Y✝).p
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<GOAL>smul α φ 1 m = m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y : Cᵒᵖ<VAR>π : X ⟶ Y<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<GOAL>∀ (Y : C) (f : Y ⟶ Opposite.unop X), (Presheaf.imageSieve φ m).arrows f → (A.val.map f.op) (smul α φ 1 m) = (A.val.map f.op) m
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop X<VAR>m₀ : (forget AddCommGrp).obj (M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.val.map f.op) m<GOAL>(A.val.map f.op) (smul α φ 1 m) = (φ.app (Opposite.op Y)) m₀
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X Y✝ : Cᵒᵖ<VAR>π : X ⟶ Y✝<VAR>r r' : ↑(R.val.obj X)<VAR>m m' : ↑(A.val.obj X)<VAR>Y : C<VAR>f : Y ⟶ Opposite.unop X<VAR>m₀ : (forget AddCommGrp).obj (M₀.presheaf.obj (Opposite.op Y))<VAR>hm₀ : (φ.app (Opposite.op Y)) m₀ = (A.val.map f.op) m<GOAL>(φ.app (Opposite.op Y)) m₀ = (φ.app (Opposite.op Y)) m₀
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesAt f pf x n<VAR>hg : HasFiniteFPowerSeriesAt g pg x m<GOAL>HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)