ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ f.right.app P = F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ g.right.app P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>(compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫ f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd) = (compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫ g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>yonedaEquiv ((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫ f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)) = yonedaEquiv ((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst) ≫ g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>(Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) ((f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst))))) = (Φ.right.map (yonedaEquiv.symm (Opposite.unop x).snd)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) ((g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).1))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))))
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>x : Holor α [d]<GOAL>CPRankMax 0 (x ⊗ 0)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y₁ y₂ : Holor α ds<VAR>hy₁ : y₁.CPRankMax1<VAR>hy₂ : CPRankMax n y₂<GOAL>CPRankMax (n + 1) (x ⊗ (y₁ + y₂))
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y₁ y₂ : Holor α ds<VAR>hy₁ : y₁.CPRankMax1<VAR>hy₂ : CPRankMax n y₂<GOAL>CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y₁ y₂ : Holor α ds<VAR>hy₁ : y₁.CPRankMax1<VAR>hy₂ : CPRankMax n y₂<GOAL>CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y₁ y₂ : Holor α ds<VAR>hy₁ : y₁.CPRankMax1<VAR>hy₂ : CPRankMax n y₂<GOAL>CPRankMax 1 (x ⊗ y₁)
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y₁ y₂ : Holor α ds<VAR>hy₁ : y₁.CPRankMax1<VAR>hy₂ : CPRankMax n y₂<GOAL>CPRankMax n (x ⊗ y₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<GOAL>SeparatingDual R V ↔ Function.Injective ⇑(ContinuousLinearMap.coeLM R).flip
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<GOAL>(∀ (x : V), ¬x = 0 → ∃ f, ¬f x = 0) ↔ ∀ (a : V), (ContinuousLinearMap.coeLM R).flip a = 0 → a = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>v : V<GOAL>(¬v = 0 → ∃ f, ¬f v = 0) ↔ (ContinuousLinearMap.coeLM R).flip v = 0 → v = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>v : V<GOAL>(¬∃ f, ¬f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : TopologicalRing R<VAR>inst✝² : TopologicalAddGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : SeparatingDual R V<VAR>v : V<GOAL>(∀ (f : V →L[R] R), f v = 0) → v = 0 ↔ (∀ (x : V →L[R] R), ((ContinuousLinearMap.coeLM R).flip v) x = 0 x) → v = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<VAR>v : E := (hT.eigenvectorBasis hn) i<GOAL>HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<VAR>v : E := (hT.eigenvectorBasis hn) i<VAR>μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)<GOAL>HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<VAR>v : E := (hT.eigenvectorBasis hn) i<VAR>μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)<GOAL>HasEigenvector T (↑(RCLike.re μ)) v
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<VAR>v : E := (hT.eigenvectorBasis hn) i<VAR>μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)<VAR>key : HasEigenvector T μ v<GOAL>HasEigenvector T (↑(RCLike.re μ)) v
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>hn : FiniteDimensional.finrank 𝕜 E = n<VAR>i : Fin n<VAR>v : E := (hT.eigenvectorBasis hn) i<VAR>μ : 𝕜 := ↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯)<VAR>key : HasEigenvector T μ v<VAR>re_μ : ↑(RCLike.re μ) = μ<GOAL>HasEigenvector T (↑(RCLike.re μ)) v
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>dist ↑z ↑(w.center (dist z w)) + dist ↑w ↑(w.center (dist z w)) = w.im * (rexp (dist z w) - 1)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>c : R<GOAL>(C c * X).support ⊆ {1}
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : lowerCrossingTime a b f N n ω < N<GOAL>upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧ lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>M : ℕ<VAR>hNM : N ≤ M<VAR>h : lowerCrossingTime a b f N n ω < N<VAR>h' : upperCrossingTime a b f N n ω < N<GOAL>upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧ lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>r : ℝ<GOAL>P.f =O[atTop] fun x => x ^ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : MonoidWithZero β<VAR>inst✝ : ContinuousMul β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<GOAL>FinStronglyMeasurable (f * g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : MonoidWithZero β<VAR>inst✝ : ContinuousMul β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<GOAL>∀ (n : ℕ), μ (support ↑((fun n => hf.approx n * hg.approx n) n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : MonoidWithZero β<VAR>inst✝ : ContinuousMul β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<VAR>n : ℕ<GOAL>μ (support ↑((fun n => hf.approx n * hg.approx n) n)) < ⊤
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>(X * p).content = p.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>(Multiset.map (X * p).coeff (X * p).support.val).gcd = (Multiset.map p.coeff p.support.val).gcd
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support<GOAL>Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support).val = Multiset.map p.coeff p.support.val
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support<GOAL>Multiset.map (fun x => (X * p).coeff x.succ) p.support.val = Multiset.map p.coeff p.support.val
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support<GOAL>(fun x => (X * p).coeff x.succ) = p.coeff
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support<VAR>a : ℕ<GOAL>(X * p).coeff a.succ = p.coeff a
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support<VAR>a : ℕ<GOAL>(p * X).coeff a.succ = p.coeff a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s = ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (v.limRatioMeas hρ)) s ≤ ρ s
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>ρ s ≤ (μ.withDensity (v.limRatioMeas hρ)) s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<VAR>p : ℤ<GOAL>(δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<VAR>p : ℤ<VAR>eq : φ₁.f p = (dNext p) h.hom + (prevD p) h.hom + φ₂.f p<GOAL>(δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<VAR>p : ℤ<VAR>eq : φ₁.f p = F.d p (p + 1) ≫ h.hom (p + 1) p + h.hom p (p - 1) ≫ G.d (p - 1) p + φ₂.f p<GOAL>(δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<VAR>p : ℤ<VAR>eq : φ₁.f p = F.d p (p + 1) ≫ h.hom (p + 1) p + h.hom p (p - 1) ≫ G.d (p - 1) p + φ₂.f p<GOAL>(Cochain.mk fun p q x => h.hom p q).v p (p - 1) ⋯ ≫ G.d (p - 1) p + Int.negOnePow 0 • F.d p (p + 1) ≫ (Cochain.mk fun p q x => h.hom p q).v (p + 1) p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>φ₁ φ₂ : F ⟶ G<VAR>h : Homotopy φ₁ φ₂<VAR>p : ℤ<VAR>eq : φ₁.f p = F.d p (p + 1) ≫ h.hom (p + 1) p + h.hom p (p - 1) ≫ G.d (p - 1) p + φ₂.f p<GOAL>h.hom p (p - 1) ≫ G.d (p - 1) p + F.d p (p + 1) ≫ h.hom (p + 1) p = F.d p (p + 1) ≫ h.hom (p + 1) p + h.hom p (p - 1) ≫ G.d (p - 1) p + φ₂.f p - φ₂.f p
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NeZero μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<GOAL>⨍ (x : α), f x ∂μ ∈ s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NeZero μ<VAR>hs : Convex ℝ s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<GOAL>(μ univ)⁻¹ • μ ≪ μ
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹¹ : Category.{v, u} V<VAR>inst✝¹⁰ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁹ : Category.{?u.75509, u_2} W<VAR>inst✝⁸ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁷ : Category.{?u.75534, u_3} W₁<VAR>inst✝⁶ : Category.{?u.75538, u_4} W₂<VAR>inst✝⁵ : HasZeroMorphisms W₁<VAR>inst✝⁴ : HasZeroMorphisms W₂<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>α : Type u_5<VAR>inst✝³ : AddRightCancelSemigroup α<VAR>inst✝² : One α<VAR>inst✝¹ : DecidableEq α<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X : α → W₁<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>n : α<GOAL>(fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0