ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this✝ : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<VAR>this : IsCofiltered J<VAR>u : (j : J') → F'.obj j<VAR>hu : u ∈ F'.sections<GOAL>(fun j => (u { down := j }).down) ∈ F.sections
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this✝ : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<VAR>this : IsCofiltered J<VAR>u : (j : J') → F'.obj j<VAR>hu : u ∈ F'.sections<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>h : F'.map { down := f } (u { down := j }) = u { down := j' }<GOAL>F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
<VAR>J : Type u<VAR>inst✝³ : Category.{w, u} J<VAR>inst✝² : IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>inst✝¹ : ∀ (j : J), Finite (F.obj j)<VAR>inst✝ : ∀ (j : J), Nonempty (F.obj j)<VAR>J' : Type (max w v u) := AsSmall J<VAR>down : J' ⥤ J := AsSmall.down<VAR>F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}<VAR>this✝¹ : ∀ (i : J'), Nonempty (F'.obj i)<VAR>this✝ : ∀ (i : J'), Finite (F'.obj i)<VAR>h✝ : Nonempty J<VAR>this : IsCofiltered J<VAR>u : (j : J') → F'.obj j<VAR>hu : u ∈ F'.sections<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>h : { down := F.map f (u { down := j }).down } = u { down := j' }<GOAL>F.map f ((fun j => (u { down := j }).down) j) = (fun j => (u { down := j }).down) j'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : a ⊔ c ≤ b ⊔ c<GOAL>a \ c ≤ b \ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>h : a ⊔ c ≤ b ⊔ c<GOAL>(a ⊔ c) \ c ≤ (b ⊔ c) \ c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>x y : X<VAR>hd : Disjoint (𝓝 x) (𝓝 y)<VAR>he : x = y<GOAL>False
<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 x✝² x✝¹ : ℤ<VAR>hij : ¬(ComplexShape.up ℤ).Rel x✝² x✝¹<VAR>x✝ : ↑(AddCommGrp.of (Cochain F G x✝²))<GOAL>((fun i j => AddCommGrp.ofHom ↑(δ_hom ℤ F G i j)) x✝² x✝¹) x✝ = 0 x✝
<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 x✝⁵ x✝⁴ x✝³ : ℤ<VAR>x✝² : (ComplexShape.up ℤ).Rel x✝⁵ x✝⁴<VAR>x✝¹ : (ComplexShape.up ℤ).Rel x✝⁴ x✝³<VAR>x✝ : ↑((fun i => AddCommGrp.of (Cochain F G i)) x✝⁵)<GOAL>((fun i j => AddCommGrp.ofHom ↑(δ_hom ℤ F G i j)) x✝⁵ x✝⁴ ≫ (fun i j => AddCommGrp.ofHom ↑(δ_hom ℤ F G i j)) x✝⁴ x✝³) x✝ = 0 x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>s : Set α<VAR>hs : s ∈ 𝓝[≤] a<GOAL>∃ b ≤ a, Icc b a ∈ 𝓝[≤] a ∧ Icc b a ⊆ s
<VAR>V : Type u_1<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module ℝ V<VAR>inst✝¹ : ContinuousSMul ℝ V<VAR>inst✝ : ContinuousAdd V<VAR>K : ConvexBody V<VAR>h_zero : 0 ∈ K<VAR>a b : ℝ≥0<VAR>h : a ≤ b<GOAL>a • K ≤ b • K
<VAR>V : Type u_1<VAR>inst✝⁴ : TopologicalSpace V<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module ℝ V<VAR>inst✝¹ : ContinuousSMul ℝ V<VAR>inst✝ : ContinuousAdd V<VAR>K : ConvexBody V<VAR>h_zero : 0 ∈ K<VAR>a b : ℝ≥0<VAR>h : a ≤ b<GOAL>a • ↑K ⊆ b • ↑K
<VAR>T : Type u<VAR>inst✝ : TopologicalSpace T<GOAL>Pretopology.toGrothendieck (Opens T) (pretopology T) = grothendieckTopology T
<VAR>T : Type u<VAR>inst✝ : TopologicalSpace T<GOAL>Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) = grothendieckTopology T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝ : MeasurableSpace α<GOAL>Measurable fun p => (↑p).toReal
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>w z : ℂ<VAR>h : w.re ≤ z.re<GOAL>‖↑n ^ w‖ ≤ ‖↑n ^ z‖
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>w z : ℂ<VAR>h : w.re ≤ z.re<GOAL>↑n ^ w.re ≤ ↑n ^ z.re
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>s : Cocone F<VAR>U V : (Opens ↑↑s.pt)ᵒᵖ<VAR>i : U ⟶ V<GOAL>s.pt.presheaf.map i ≫ limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))) { pt := s.pt.presheaf.obj V, π := { app := fun j => (s.ι.app (unop j)).c.app V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))).inv = (limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) { pt := s.pt.presheaf.obj U, π := { app := fun j => (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))).inv) ≫ (limit (pushforwardDiagramToColimit F).leftOp).map ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop).op
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>s : Cocone F<VAR>U V : (Opens ↑↑s.pt)ᵒᵖ<VAR>i : U ⟶ V<VAR>j : Jᵒᵖ<GOAL>(s.pt.presheaf.map i ≫ limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))) { pt := s.pt.presheaf.obj V, π := { app := fun j => (s.ι.app (unop j)).c.app V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))).inv) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V))) = ((limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) { pt := s.pt.presheaf.obj U, π := { app := fun j => (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))).inv) ≫ (limit (pushforwardDiagramToColimit F).leftOp).map ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop).op) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>s : Cocone F<VAR>U V : (Opens ↑↑s.pt)ᵒᵖ<VAR>i : U ⟶ V<VAR>j : Jᵒᵖ<VAR>w : (Opens.map (colimit.ι (F ⋙ forget C) (unop j) ≫ colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop = eqToHom ⋯ ≫ (Opens.map (((forget C).mapCocone s).ι.app (unop j))).map i.unop ≫ eqToHom ⋯<GOAL>(s.pt.presheaf.map i ≫ limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))) { pt := s.pt.presheaf.obj V, π := { app := fun j => (s.ι.app (unop j)).c.app V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))).inv) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V))) = ((limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) { pt := s.pt.presheaf.obj U, π := { app := fun j => (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))).inv) ≫ (limit (pushforwardDiagramToColimit F).leftOp).map ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop).op) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))
<VAR>J : Type u'<VAR>inst✝⁴ : Category.{v', u'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimitsOfShape J TopCat<VAR>inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)<VAR>inst✝ : HasLimitsOfShape Jᵒᵖ C<VAR>F : J ⥤ PresheafedSpace C<VAR>s : Cocone F<VAR>U V : (Opens ↑↑s.pt)ᵒᵖ<VAR>i : U ⟶ V<VAR>j : Jᵒᵖ<VAR>w : (Opens.map (colimit.ι (F ⋙ forget C) (unop j))).map ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop) = eqToHom ⋯ ≫ (Opens.map (((forget C).mapCocone s).ι.app (unop j))).map i.unop ≫ eqToHom ⋯<GOAL>(s.pt.presheaf.map i ≫ limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))) { pt := s.pt.presheaf.obj V, π := { app := fun j => (s.ι.app (unop j)).c.app V ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))).inv) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V))) = ((limit.lift ((pushforwardDiagramToColimit F).leftOp ⋙ (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) { pt := s.pt.presheaf.obj U, π := { app := fun j => (s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯), naturality := ⋯ } } ≫ (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))).inv) ≫ (limit (pushforwardDiagramToColimit F).leftOp).map ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).map i.unop).op) ≫ (limit.π (pushforwardDiagramToColimit F).leftOp j).app (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop V)))
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SecondCountableTopology H<VAR>s : Set M<VAR>hs : ⋃ x ∈ s, (chartAt H x).source = univ<VAR>hsc : s.Countable<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SecondCountableTopology H<VAR>s : Set M<VAR>hs : ⋃ x ∈ s, (chartAt H x).source = univ<VAR>hsc : s.Countable<VAR>this : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SecondCountableTopology H<VAR>s : Set M<VAR>hs : ⋃ x ∈ s, (chartAt H x).source = univ<VAR>hsc : s.Countable<VAR>this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source<VAR>this : Encodable ↑s<GOAL>SecondCountableTopology M
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SecondCountableTopology H<VAR>s : Set M<VAR>hs : ⋃ x, (chartAt H ↑x).source = univ<VAR>hsc : s.Countable<VAR>this✝ : ∀ (x : M), SecondCountableTopology ↑(chartAt H x).source<VAR>this : Encodable ↑s<GOAL>SecondCountableTopology M
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k ∈ Ico 2 (2 ^ n + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1))
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>f : k → E<VAR>a b r : k<VAR>hab : a < b<VAR>h₀ : 0 < r<VAR>h₁ : r < 1<GOAL>f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>v : V<VAR>s : AffineSubspace k P<GOAL>(v +ᵥ s).direction = s.direction
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>v : V<VAR>s : AffineSubspace k P<GOAL>Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : OpenEmbedding f<VAR>s : Set Y<VAR>hs : s ⊆ range f<GOAL>IsOpen s ↔ IsOpen (f ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h : ⟪x, y⟫_𝕜 = 0<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h : ⟪x, y⟫_𝕜 = 0<GOAL>2 = 0 ∨ re ⟪x, y⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h : ⟪x, y⟫_𝕜 = 0<GOAL>re ⟪x, y⟫_𝕜 = 0
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>Submodule.comap (↑f) (Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}) = Submodule.comap (↑f) (Submodule.span R (⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}))
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} = ⇑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>{m | ∃ x n, ⁅↑x, ↑n⁆ = m} = (fun a => f a) '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<GOAL>HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ<GOAL>HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>r : ℝ<VAR>hnr : ↑(finrank ℝ E) < r<VAR>this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ<GOAL>∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ < ⊤
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>x₀ : 𝕜<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖deriv f x₀‖ ≤ C
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 1
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume (1 / 2) 1
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>IntervalIntegrable (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) volume (-(1 / 2)) (-1)
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>(fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) = fun x => ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>-(1 / 2) = 1 / 2 - 1
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>-1 = 0 - 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid R<VAR>inst✝ : StarAddMonoid R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x + y)
<VAR>P : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Membership P L<VAR>inst✝² : ProjectivePlane P L<VAR>inst✝¹ : Finite P<VAR>inst✝ : Finite L<VAR>l : L<GOAL>2 < pointCount P l
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>(W.map φ).c₄ = φ W.c₄
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>A : Type v<VAR>inst✝ : CommRing A<VAR>φ : R →+* A<GOAL>φ W.b₂ ^ 2 - 24 * φ W.b₄ = φ (W.b₂ ^ 2 - 24 * W.b₄)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>p✝ q✝ : ℚ<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedField K<VAR>p q : ℚ<GOAL>p < q → ↑p < ↑q
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<GOAL>Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 (ENNReal.toReal 0))<GOAL>Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<GOAL>Tendsto (fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) (v.filterAt x) (𝓝 0)
<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>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<VAR>this : Tendsto (ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) (v.filterAt x) (𝓝 0)<GOAL>(ENNReal.toReal ∘ fun a => (∫⁻ (y : α) in a, ↑‖f y - f x‖₊ ∂μ) / μ a) =ᶠ[v.filterAt x] fun a => ⨍ (y : α) in a, ‖f y - f x‖ ∂μ