ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X✝ : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>E : Aᵒᵖ<VAR>π : (S.arrows.diagram.op ⋙ P).cones.obj E<VAR>X Y : C<VAR>f : X ⟶ X✝<VAR>g : Y ⟶ X<VAR>hf : S.arrows f<GOAL>𝟙 ((unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).obj (op { obj := Over.mk (g ≫ f), property := ⋯ })) ≫ (fun Y f h => π.app (op { obj := Over.mk f, property := h })) Y (g ≫ f) ⋯ = (P ⋙ coyoneda.obj E).map g.op ((fun Y f h => π.app (op { obj := Over.mk f, property := h })) X f hf)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X✝ : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>E : Aᵒᵖ<VAR>π : (S.arrows.diagram.op ⋙ P).cones.obj E<VAR>X Y : C<VAR>f : X ⟶ X✝<VAR>g : Y ⟶ X<VAR>hf : S.arrows f<GOAL>𝟙 (unop E) ≫ π.app (op { obj := Over.mk (g ≫ f), property := ⋯ }) = π.app (op { obj := Over.mk f, property := hf }) ≫ P.map g.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f f' : S.arrows.categoryᵒᵖ<VAR>g : f ⟶ f'<GOAL>(unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).map g ≫ (fun f => ↑x (unop f).obj.hom ⋯) f' = (fun f => ↑x (unop f).obj.hom ⋯) f ≫ (S.arrows.diagram.op ⋙ P).map g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f f' : S.arrows.categoryᵒᵖ<VAR>g : f ⟶ f'<GOAL>(unop ((Functor.const S.arrows.categoryᵒᵖ).op.obj E)).map g ≫ (fun f => ↑x (unop f).obj.hom ⋯) f' = ↑x (g.unop.left ≫ (unop f).obj.hom) ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f f' : S.arrows.categoryᵒᵖ<VAR>g : f ⟶ f'<GOAL>𝟙 (unop E) ≫ ↑x (unop f').obj.hom ⋯ = ↑x (g.unop.left ≫ (unop f).obj.hom) ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f f' : S.arrows.categoryᵒᵖ<VAR>g : f ⟶ f'<GOAL>↑x (unop f').obj.hom ⋯ = ↑x (g.unop.left ≫ (unop f).obj.hom) ⋯
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>R : Presieve X<VAR>E : Aᵒᵖ<VAR>x : { x // x.SieveCompatible }<VAR>f f' : S.arrows.categoryᵒᵖ<VAR>g : f ⟶ f'<GOAL>g.unop.left ≫ (unop f).obj.hom = (unop f').obj.hom
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = 0 → x = y
<VAR>a b : Ordinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ω<VAR>hb : ↑n < ω<GOAL>↑m * ↑n < ω
<VAR>a b : Ordinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ω<VAR>hb : ↑n < ω<GOAL>↑(m * n) < ω
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≤ b<GOAL>Icc a b \ Ioc a b = {a}
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousSub G<VAR>b c : G<VAR>f : α → G<VAR>l : Filter α<GOAL>Tendsto (fun x => f x - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c)
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Div G✝<VAR>inst✝³ : ContinuousDiv G✝<VAR>G : Type u_1<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : ContinuousSub G<VAR>b c : G<VAR>f : α → G<VAR>l : Filter α<VAR>h : Tendsto (fun x => f x - b) l (𝓝 (c - b))<GOAL>Tendsto f l (𝓝 c)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p : P<GOAL>Coplanar k (insert p s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p : P<VAR>this : FiniteDimensional k ↥(vectorSpan k s)<GOAL>Coplanar k (insert p s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>h : Collinear k s<VAR>p : P<VAR>this : FiniteDimensional k ↥(vectorSpan k s)<GOAL>finrank k ↥(vectorSpan k (insert p s)) ≤ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<GOAL>⋃ i, ⋃ j, s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<GOAL>p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<GOAL>∀ (b : (gluing 𝒰 f g).diagram.R), Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p1 𝒰 f g ≫ f = Multicoequalizer.π (gluing 𝒰 f g).diagram b ≫ p2 𝒰 f g ≫ g
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : Infinite α<VAR>s : Set β<VAR>f : α → β<VAR>hi : Injective f<VAR>hf : ∀ (x : α), f x ∈ s<GOAL>s.Infinite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α<VAR>inst✝ : Infinite α<VAR>s : Set β<VAR>f : α → β<VAR>hi : Injective f<VAR>hf : range f ⊆ s<GOAL>s.Infinite
<VAR>q✝ : ℚ<VAR>x y : ℝ<VAR>h : Irrational (-x)<VAR>x✝ : x ∈ Set.range Rat.cast<VAR>q : ℚ<VAR>hx : ↑q = x<GOAL>↑(-q) = -x
<VAR>a b : EReal<VAR>h : a ≤ -b<GOAL>b ≤ -a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<GOAL>UnifTight (-f) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifTight f p μ<GOAL>∀ ⦃ε : ℝ≥0⦄, 0 < ε → ∃ s, μ s ≠ ⊤ ∧ ∀ (i : ι), eLpNorm (sᶜ.indicator (f i)) p μ ≤ ↑ε
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>n : ℕ<VAR>a b : R<VAR>h : ↑n * a = ↑n * b<VAR>w : n ≠ 0<GOAL>a = b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<GOAL>∀ᶠ (i : ι) in l, IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<GOAL>∀ᶠ (i : ι) in l, IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<GOAL>∀ᶠ (i : ι) in l, IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<VAR>h''i : AEStronglyMeasurable (φ i) (μ.restrict s)<GOAL>IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<VAR>h''i : AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>I : IntegrableOn (φ i) t μ<GOAL>IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<VAR>h''i : AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>I : IntegrableOn (φ i) t μ<VAR>A : IntegrableOn (fun x => φ i x • g x) (s \ u) μ<GOAL>IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<VAR>h''i : AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>I : IntegrableOn (φ i) t μ<VAR>A : IntegrableOn (fun x => φ i x • g x) (s \ u) μ<VAR>B : IntegrableOn (fun x => φ i x • g x) (s ∩ u) μ<GOAL>IntegrableOn (fun x => φ i x • g x) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>hs : MeasurableSet s<VAR>h'st : t ∈ 𝓝[s] x₀<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)<VAR>hiφ : Tendsto (fun e => ‖∫ (x : α) in t, φ e x ∂μ - 1‖) l (𝓝 0)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>hmg : IntegrableOn g s μ<VAR>hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)<VAR>u : Set α<VAR>u_open : IsOpen u<VAR>x₀u : x₀ ∈ u<VAR>ut : s ∩ u ⊆ t<VAR>hu : ∀ x ∈ u ∩ s, g x ∈ ball a 1<VAR>i : ι<VAR>hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < 1<VAR>h'i : ‖∫ (x : α) in t, φ i x ∂μ - 1‖ < 1<VAR>h''i : AEStronglyMeasurable (φ i) (μ.restrict s)<VAR>I : IntegrableOn (φ i) t μ<VAR>A : IntegrableOn (fun x => φ i x • g x) (s \ u) μ<VAR>B : IntegrableOn (fun x => φ i x • g x) (s ∩ u) μ<GOAL>s = s \ u ∪ s ∩ u
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁹ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁸ : Category.{max v u, w₂} E<VAR>F✝ : D ⥤ E<VAR>inst✝⁷ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁶ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝³ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F✝<VAR>inst✝² : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F✝<VAR>P✝ P : Cᵒᵖ ⥤ D<VAR>F : D ⥤ E<VAR>inst✝¹ : (F : D ⥤ E) → (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (F : D ⥤ E) → (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<GOAL>(𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv) ≫ (J.plusCompIso F (J.plusObj P)).inv = J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < a * b ↔ a * 1 < a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : CommSemigroup α<VAR>inst✝ : CommSemigroup β<VAR>f : α → β<VAR>a b : α<GOAL>f (max a b) * f (min a b) = f a * f b
<VAR>α : Type u_1<VAR>α₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β : α → Type u_4<VAR>β₁ : α₁ → Type u_5<VAR>β₂ : α₂ → Type u_6<VAR>γ : Type u_7<VAR>inst✝ : Nonempty γ<VAR>a : α<VAR>f : γ → β a<VAR>i : γ<VAR>g : γ → β a<VAR>h : mk a ∘ f = mk a ∘ g<GOAL>a = a ∧ HEq f g
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : Monoid γ<VAR>inst✝² : (i : ι) → AddMonoid (β i)<VAR>inst✝¹ : (i : ι) → DistribMulAction γ (β i)<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>r : γ<VAR>f : Π₀ (i : ι), β i<VAR>i✝ : ι<GOAL>(filter p (r • f)) i✝ = (r • filter p f) i✝
<VAR>z : ℂ<VAR>x : ℚ<GOAL>(z / ↑x).im = z.im / ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<GOAL>mulSupport f = ∅ ↔ f = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<GOAL>(∀ x ∉ ∅, f x = 1) ↔ ∀ (a : α), f a = 1 a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{u} → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : #ι < c.cof<VAR>hf : ∀ (i : ι), ∀ b < c, f i b < c<VAR>a : Ordinal.{u}<GOAL>Cardinal.lift.{u, u} #ι < c.cof
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(φ ⊔ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<GOAL>(∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<GOAL>EventuallyConst s⁻¹ (ae μ) ↔ EventuallyConst s (ae μ)
<VAR>N : ℕ<VAR>hn : N ≠ 0<VAR>χ : DirichletCharacter ℂ N<GOAL>(abscissaOfAbsConv fun n => χ ↑n) = 1
<VAR>R : Type u<VAR>σ : Type v<VAR>a a' a₁ a₂ : R<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>i : σ<VAR>f g : MvPolynomial σ R<GOAL>(pderiv i) (f * g) = (pderiv i) f * g + f * (pderiv i) g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.RespectsIso<VAR>X Y S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>h : P.diagonal g<GOAL>P.diagonal (pullback.fst f g)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasPullbacks C<VAR>P : MorphismProperty C<VAR>hP : P.StableUnderBaseChange<VAR>inst✝ : P.RespectsIso<VAR>X Y S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>h : P.diagonal g<GOAL>P ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)).left
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>(∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>(∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b
<VAR>α : Type u<VAR>β : Type u_1<VAR>b : ℕ<VAR>hb : 2 ≤ b<VAR>a n : ℕ<GOAL>(b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n✝ : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h : UniqueDiffOn 𝕜 s<VAR>f✝ g : 𝕜 → F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>a : 𝕜<GOAL>iteratedDeriv n (fun x => -f x) a = -iteratedDeriv n f a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>map (addRightEmbedding c) (Ioc a b) = Ioc (a + c) (b + c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedCancelAddCommMonoid α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c : α<GOAL>⇑(addRightEmbedding c) '' Set.Ioc a b = Set.Ioc (a + c) (b + c)
<VAR>a b c : ℤ<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>hk : Odd k<VAR>h : a * b = c ^ k<GOAL>b * a = ?m.13357 ^ k
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>ht : t * closure {1} = t<GOAL>tᶜ * closure {1} = tᶜ
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>ht : t * closure {1} = t<GOAL>tᶜ * closure {1} ⊆ tᶜ
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>ht : t * closure {1} = t<VAR>x : G<VAR>hx : x ∈ tᶜ<VAR>g : G<VAR>hg : g ∈ closure {1}<GOAL>(fun x x_1 => x * x_1) x g ∈ tᶜ
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>ht : t * closure {1} = t<VAR>x : G<VAR>hx : x ∈ tᶜ<VAR>g : G<VAR>hg : g ∈ closure {1}<VAR>H : (fun x x_1 => x * x_1) x g ∉ tᶜ<GOAL>False
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t✝ t : Set G<VAR>ht : t * closure {1} = t<VAR>x : G<VAR>hx : x ∈ tᶜ<VAR>g : G<VAR>hg : g ∈ closure {1}<VAR>H : (fun x x_1 => x * x_1) x g ∉ tᶜ<VAR>this : x ∈ t * closure {1}<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R N<VAR>A₁ : Type u_6<VAR>B₁ : Type u_7<VAR>A₂ : Type u_8<VAR>B₂ : Type u_9<VAR>inst✝⁶ : CommRing A₁<VAR>inst✝⁵ : CommRing B₁<VAR>inst✝⁴ : CommRing A₂<VAR>inst✝³ : CommRing B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Finite A₁ B₁<VAR>this✝ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<GOAL>Finite A₂ B₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : Module R N<VAR>A₁ : Type u_6<VAR>B₁ : Type u_7<VAR>A₂ : Type u_8<VAR>B₂ : Type u_9<VAR>inst✝⁶ : CommRing A₁<VAR>inst✝⁵ : CommRing B₁<VAR>inst✝⁴ : CommRing A₂<VAR>inst✝³ : CommRing B₂<VAR>inst✝² : Algebra A₁ B₁<VAR>inst✝¹ : Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>inst✝ : Finite A₁ B₁<VAR>this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra<VAR>this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra<VAR>this : IsScalarTower A₁ A₂ B₁<GOAL>Finite A₂ B₂