ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>compare a b = Ordering.lt ↔ a < b
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) = Ordering.lt ↔ a < b
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>StrictMono (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictMono f
<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<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.fst (𝒰.map j ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>C✝ : Type u<VAR>inst✝⁵ : Category.{v, u} C✝<VAR>inst✝⁴ : HasZeroMorphisms C✝<VAR>X✝ Y✝ : C✝<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasCokernel f✝<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : f ≫ g = 0<VAR>inst✝ : HasCokernel f<GOAL>colimit.ι (parallelPair f 0) zero ≫ cokernel.desc f g h = 0
<VAR>C✝ : Type u<VAR>inst✝⁵ : Category.{v, u} C✝<VAR>inst✝⁴ : HasZeroMorphisms C✝<VAR>X✝ Y✝ : C✝<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasCokernel f✝<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : f ≫ g = 0<VAR>inst✝ : HasCokernel f<GOAL>((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) ≫ cokernel.desc f g h = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Function.Injective ⇑f<GOAL>(map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<GOAL>diagonal v i ⬝ᵥ w = v i * w i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>u v w : m → α<VAR>i : m<VAR>this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0<GOAL>diagonal v i ⬝ᵥ w = v i * w i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>(⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>p : MonoidAlgebra k G → Prop<VAR>f : MonoidAlgebra k G<VAR>hM : ∀ (g : G), p ((of k G) g)<VAR>hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)<GOAL>p f
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>p : MonoidAlgebra k G → Prop<VAR>f : MonoidAlgebra k G<VAR>hM : ∀ (g : G), p ((of k G) g)<VAR>hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)<GOAL>p 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Monoid G<VAR>p : MonoidAlgebra k G → Prop<VAR>f : MonoidAlgebra k G<VAR>hM : ∀ (g : G), p ((of k G) g)<VAR>hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)<VAR>hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)<VAR>g : G<VAR>r : k<GOAL>p (Finsupp.single g r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<GOAL>s ⊆ balancedCore 𝕜 t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<GOAL>s ⊆ ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<VAR>a : 𝕜<VAR>ha : 1 ≤ ‖a‖<GOAL>s ⊆ a • t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<VAR>a : 𝕜<VAR>ha : 1 ≤ ‖a‖<GOAL>a • a⁻¹ • s ⊆ a • t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<VAR>a : 𝕜<VAR>ha : 1 ≤ ‖a‖<GOAL>‖a⁻¹‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>ht : 0 ∈ t<VAR>hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t<VAR>a : 𝕜<VAR>ha : 1 ≤ ‖a‖<GOAL>‖a‖⁻¹ ≤ 1
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<GOAL>f = g
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<GOAL>f 0 = g 0
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>inhabited_h : Inhabited ι<GOAL>f 0 = g 0
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>inhabited_h : Inhabited ι<GOAL>f (Pi.single default 0) = g (Pi.single default 0)
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<VAR>P : F[X]<GOAL>(ofPowerSeries ℤ F) ↑P = ↑↑P
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>b : ℝ≥0∞<GOAL>(↑a * b).toNNReal = a * b.toNNReal
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>H : Raised n m<GOAL>n.dist m ≤ 1
<VAR>α : Type u_1<VAR>n m : ℕ<VAR>H : Raised n m<VAR>H1 : n ≤ m<VAR>H2 : m ≤ n + 1<GOAL>n.dist m ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ filter (fun x => x < i) s, (1 - f j)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ : CommRing α<VAR>inst✝ : LinearOrder ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s, 1 - ∑ i ∈ s, (f i * ∏ j ∈ filter (fun x => x < i) s, (1 - f j)) * ∏ j ∈ filter (fun j => i < j) s, 1 = 1 - ∑ i ∈ s, f i * ∏ j ∈ filter (fun x => x < i) s, (1 - f j)
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>h : ‖x‖ = ‖y‖<GOAL>SameRay ℝ x y ↔ x = y
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x : F<VAR>h : ‖x‖ = ‖0‖<GOAL>SameRay ℝ x 0 ↔ x = 0
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>h : ‖x‖ = ‖y‖<VAR>hy : y ≠ 0<GOAL>SameRay ℝ x y ↔ x = y
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<GOAL>liminf (u + v) f = ⊤
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<GOAL>∀ (z : ℝ), ↑z < ⊤ → ↑z ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<VAR>x : ℝ<GOAL>↑x < ⊤ → ↑x ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<VAR>x y : ℝ<VAR>left✝ : ⊥ < ↑y<VAR>hy : ↑y < liminf v f<GOAL>↑x < ⊤ → ↑x ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<VAR>x y : ℝ<VAR>left✝ : ⊥ < ↑y<VAR>hy : ↑y < liminf v f<VAR>a✝ : ↑x < ⊤<GOAL>↑x ≤ liminf (u + v) f
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>h : liminf u f = ⊤<VAR>h' : liminf v f ≠ ⊥<VAR>x y : ℝ<VAR>left✝ : ⊥ < ↑y<VAR>hy : ↑y < liminf v f<VAR>a✝ : ↑x < ⊤<GOAL>↑(x - y) + ↑y ≤ liminf (u + v) f
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁵ : DecidableEq α<VAR>inst✝⁴ : DecidableEq M<VAR>inst✝³ : Zero M<VAR>inst✝² : DecidableEq P<VAR>inst✝¹ : Zero P<VAR>inst✝ : Zero N<VAR>F : M → N → P<VAR>F0 : F 0 0 = 0<VAR>f₁ f₂ : α →₀ M<VAR>g : α →₀ N<VAR>hF : ∀ (g : N), Function.Injective fun f => F f g<VAR>a✝ : α<GOAL>a✝ ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a✝ ∈ f₁.neLocus f₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius
<VAR>m n✝¹ n✝ a n : ℕ<VAR>x y : ℤ<VAR>he : ↑x = ↑y<VAR>hl : x.natAbs ≤ n / 2<GOAL>x.natAbs ≤ y.natAbs
<VAR>m n✝¹ n✝ a n : ℕ<VAR>x y : ℤ<VAR>he : ↑n ∣ y - x<VAR>hl : x.natAbs ≤ n / 2<GOAL>x.natAbs ≤ y.natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x y : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>he : y - x = ↑n * m<GOAL>x.natAbs ≤ y.natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x y : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>he : y = ↑n * m + x<GOAL>x.natAbs ≤ y.natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<GOAL>x.natAbs ≤ (↑n * m + x).natAbs
<VAR>m n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<GOAL>x.natAbs ≤ (↑n * 0 + x).natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>x.natAbs ≤ (↑n * m + x).natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 ≤ (↑n * m + x).natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 + x.natAbs ≤ (↑n * m + x).natAbs + x.natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 + n / 2 ≤ (↑n * m + x - x).natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 + n / 2 ≤ n * m.natAbs
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 + n / 2 ≤ n
<VAR>m✝ n✝¹ n✝ a n : ℕ<VAR>x : ℤ<VAR>hl : x.natAbs ≤ n / 2<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>n / 2 * 2 ≤ n
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>x : R<VAR>y : R[X]<GOAL>y ∈ RingHom.ker (evalRingHom x) ↔ y ∈ Ideal.span {X - C x}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommSemiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<GOAL>(aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((aeval x) p)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommSemiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<GOAL>(eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p = (eval₂Hom (algebraMap R B) fun i => (algebraMap A B) (x i)) p
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<GOAL>Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>q n : ℕ<VAR>x y : R<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x + y) ^ q ^ n = x ^ q ^ n + y ^ q ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : 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>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α →₀ M<GOAL>filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x
<VAR>a : ℝ<GOAL>‖↑a‖ = ‖a‖
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DiscreteTopology α<VAR>β : Type u_2<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ x ∈ s
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>f : α → S.obj (op PUnit.{u + 1})<GOAL>eval S α (typesGlue S hs α f) = f
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>f : α → S.obj (op PUnit.{u + 1})<VAR>x : α<GOAL>eval S α (typesGlue S hs α f) x = f x
<VAR>S : Type uᵒᵖ ⥤ Type u<VAR>hs : IsSheaf typesGrothendieckTopology S<VAR>α : Type u<VAR>f : α → S.obj (op PUnit.{u + 1})<VAR>x : α<GOAL>S.map (↾fun x => PUnit.unit).op (f ((↾fun x_1 => x) (Classical.choose ⋯))) = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>x y : α × β<GOAL>(a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<GOAL>∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<GOAL>∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<VAR>hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊<GOAL>∫ (a : α), ∑' (i : ι), f i a ∂μ = ∑' (i : ι), ∫ (a : α), f i a ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<VAR>hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊<GOAL>∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖f n a‖ ≤ (fun i a => ↑‖f i a‖₊) n a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<VAR>hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊<GOAL>AEStronglyMeasurable (fun a => ∑' (n : ι), (fun i a => ↑‖f i a‖₊) n a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<VAR>hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊<GOAL>HasFiniteIntegral (fun a => ∑' (n : ι), (fun i a => ↑‖f i a‖₊) n a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>ι : Type u_4<VAR>inst✝ : Countable ι<VAR>f : ι → α → G<VAR>hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ<VAR>hf' : ∑' (i : ι), ∫⁻ (a : α), ↑‖f i a‖₊ ∂μ ≠ ⊤<VAR>hG : CompleteSpace G<VAR>hf'' : ∀ (i : ι), AEMeasurable (fun x => ↑‖f i x‖₊) μ<VAR>hhh : ∀ᵐ (a : α) ∂μ, Summable fun n => ↑‖f n a‖₊<GOAL>∀ᵐ (a : α) ∂μ, HasSum (fun n => f n a) (∑' (i : ι), f i a)
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>h : n ≠ 0<GOAL>(C a).coeff n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g✝ g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>x✝ : ∃ g, ∀ (x : ↑s), f ↑x = ↑(g x)<VAR>x : α<VAR>hx : x ∈ s<VAR>g : ↑s → ↑t<VAR>hg : ∀ (x : ↑s), f ↑x = ↑(g x)<GOAL>↑(g ⟨x, hx⟩) ∈ t
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : Zero M<VAR>inst✝ : LinearOrder M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>s.indicator f a ≤ {a | 0 ≤ f a}.indicator f a
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<GOAL>x + 1 ≤ y ↔ x < y
<VAR>x y : PartENat<VAR>hx : x ≠ ⊤<VAR>h : x + 1 ≤ y<GOAL>x < y
<VAR>y : PartENat<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>h : ↑m + 1 ≤ y<GOAL>↑m < y
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>h : ↑m + 1 ≤ ⊤<GOAL>↑m < ⊤
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m + 1 ≤ ↑n<GOAL>↑m < ↑n
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m + 1 ≤ ↑n<GOAL>m < n
<VAR>m : ℕ<VAR>hx : ↑m ≠ ⊤<VAR>n : ℕ<VAR>h : ↑m + 1 ≤ ↑n<GOAL>m.succ ≤ n
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<VAR>this : NoZeroDivisors ℕ<GOAL>p ^ e * n ∈ p.succ.smoothNumbers
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<VAR>this : NoZeroDivisors ℕ<VAR>hp' : p ^ e ≠ 0<GOAL>p ^ e * n ∈ p.succ.smoothNumbers
<VAR>p n : ℕ<VAR>hp : p ≠ 0<VAR>e : ℕ<VAR>hn : n ∈ p.smoothNumbers<VAR>this : NoZeroDivisors ℕ<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<GOAL>q < p.succ