ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝¹⁶ : DecidableEq ι<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : CommRing B<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : CommRing C<VAR>inst✝¹¹ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁰ : Fintype ι'<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>inst✝ : Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>this : ∀ (x : Fin pb.dim), ↑x + 1 ≤ pb.dim<VAR>hn : n = pb.dim<VAR>h₂ : 2 ∣ pb.dim * (pb.dim - 1)<VAR>hne : ↑2 ≠ 0<VAR>hle : 1 ≤ pb.dim<GOAL>↑pb.dim * ↑pb.dim - (↑pb.dim * (↑pb.dim - ↑1) / ↑2 + ↑pb.dim) = ↑pb.dim * (↑pb.dim - ↑1) / ↑2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ -y = 0<GOAL>Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>inst✝ : Fintype α<VAR>F : Finset (Finset α)<GOAL>t ∈ (atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s = t
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemiring α<VAR>m n : PosNum<GOAL>↑m < ↑n ↔ m < n
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(T • z).im = z.im
<VAR>α : Type u_1<VAR>inst✝⁶ : MetricSpace α<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : IsUnifLocDoublingMeasure μ<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>E : Type u_2<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) → Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)
<VAR>α : Type u_1<VAR>z : ℤ<VAR>c : ℝ≥0<GOAL>|z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<GOAL>(setToL1 hT) ↑(indicatorConst 1 hs ⋯ x) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<GOAL>(setToL1SCLM α E μ hT) (indicatorConst 1 hs ⋯ x) = (T s) x
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂<GOAL>∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T₁ T₂ : Triangle C<VAR>hT₁ : T₁ ∈ distinguishedTriangles<VAR>hT₂ : T₂ ∈ distinguishedTriangles<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>c : T₁.obj₃ ⟶ T₂.obj₃<VAR>comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂<VAR>a : T₁.rotate.obj₃ ⟶ T₂.rotate.obj₃<VAR>ha₁ : T₁.rotate.mor₂ ≫ a = c ≫ T₂.rotate.mor₂<VAR>ha₂ : T₁.rotate.mor₃ ≫ (shiftFunctor C 1).map b = a ≫ T₂.rotate.mor₃<GOAL>∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>⟪gramSchmidt 𝕜 v j, v i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v i + ∑ i_1 ∈ Iio i, (⟪gramSchmidt 𝕜 v i_1, v i⟫_𝕜 / ↑‖gramSchmidt 𝕜 v i_1‖ ^ 2) • gramSchmidt 𝕜 v i_1⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<GOAL>⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v i⟫_𝕜 + ∑ x ∈ Iio i, ⟪gramSchmidt 𝕜 v x, v i⟫_𝕜 / ↑‖gramSchmidt 𝕜 v x‖ ^ 2 * ⟪gramSchmidt 𝕜 v j, gramSchmidt 𝕜 v x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<GOAL>⟪b j, b i⟫_𝕜 + ∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / ↑‖b x‖ ^ 2 * ⟪b j, b x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<GOAL>⟪b j, b i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<GOAL>∑ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / ↑‖b x‖ ^ 2 * ⟪b j, b x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<GOAL>∀ x ∈ Iio i, ⟪b x, v i⟫_𝕜 / ↑‖b x‖ ^ 2 * ⟪b j, b x⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<VAR>k : ι<VAR>hki' : k ∈ Iio i<VAR>hki : k < i<GOAL>⟪b k, v i⟫_𝕜 / ↑‖b k‖ ^ 2 * ⟪b j, b k⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>v : ι → E<VAR>i j : ι<VAR>hij : i < j<VAR>b : ι → E := gramSchmidt 𝕜 v<VAR>k : ι<VAR>hki' : k ∈ Iio i<VAR>hki : k < i<VAR>this : ⟪b j, b k⟫_𝕜 = 0<GOAL>⟪b k, v i⟫_𝕜 / ↑‖b k‖ ^ 2 * ⟪b j, b k⟫_𝕜 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Ico a b ↔ a < b
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>inst✝⁵ : Field 𝕂<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : TopologicalSpace 𝔸<VAR>inst✝¹ : TopologicalRing 𝔸<VAR>inst✝ : T2Space 𝔸<VAR>x : 𝔸ᵐᵒᵖ<GOAL>exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroOneClass M₀<VAR>s t✝ : Set ι<VAR>i : ι<VAR>t : Set κ<VAR>j : κ<GOAL>(s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>R : Type u_5<VAR>inst✝ : MulZeroOneClass M₀<VAR>s t✝ : Set ι<VAR>i : ι<VAR>t : Set κ<VAR>j : κ<GOAL>(if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → SeminormedGroup (π i)<VAR>inst✝ : SeminormedGroup E<VAR>f x : (i : ι) → π i<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_le : ∀ (i : ι), x ≤ as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<GOAL>⨅ i, as i = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : CompleteLinearOrder R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : OrderTopology R<VAR>x : R<VAR>as : ι → R<VAR>x_le : ∀ (i : ι), x ≤ as i<VAR>F : Filter ι<VAR>inst✝ : F.NeBot<VAR>as_lim : Tendsto as F (𝓝 x)<GOAL>∀ (w : R), x < w → ∃ i, as i < w
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α ⟹ β<VAR>g : α' ⟹ β'<GOAL>prod.fst ⊚ (f ⊗' g) = f ⊚ prod.fst
<VAR>n : ℕ<VAR>α α' β β' : TypeVec.{u_1} n<VAR>f : α ⟹ β<VAR>g : α' ⟹ β'<VAR>i : Fin2 n<GOAL>(prod.fst ⊚ (f ⊗' g)) i = (f ⊚ prod.fst) i
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.split p = List.map mk (List.splitOnP p s.data)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>j : ι<VAR>hj : j ∈ s<VAR>hjx : (p j) x ≠ 0<GOAL>q x ≤ (C • s.sup p) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>j : ι<VAR>hj : j ∈ s<VAR>hjx : (p j) x ≠ 0<VAR>this : (s.sup p) x ≠ 0<GOAL>q x ≤ (C • s.sup p) x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>j : ι<VAR>hj : j ∈ s<VAR>hjx : (p j) x ≠ 0<VAR>this : (s.sup p) x ≠ 0<VAR>y : E<VAR>hle : ε / ‖c‖ ≤ (s.sup p) y<VAR>hlt : (s.sup p) y < ε<GOAL>q y ≤ (C • s.sup p) y
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>j : ι<VAR>hj : j ∈ s<VAR>hjx : (p j) x ≠ 0<VAR>this : (s.sup p) x ≠ 0<VAR>y : E<VAR>hle : ε / ‖c‖ ≤ (s.sup p) y<VAR>hlt : (s.sup p) y < ε<VAR>i : ι<VAR>hi : i ∈ s<VAR>hiy : (s.sup p) y = (p i) y<GOAL>q y ≤ (C • s.sup p) y
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>q : Seminorm 𝕜 E<VAR>ε : ℝ<VAR>C : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), (∀ i ∈ s, (p i) x < ε) → ∀ j ∈ s, ε / ‖c‖ ≤ (p j) x → q x ≤ (C • p j) x<VAR>x : E<VAR>j : ι<VAR>hj : j ∈ s<VAR>hjx : (p j) x ≠ 0<VAR>this : (s.sup p) x ≠ 0<VAR>y : E<VAR>hle : ε / ‖c‖ ≤ (s.sup p) y<VAR>hlt : (s.sup p) y < ε<VAR>i : ι<VAR>hi : i ∈ s<VAR>hiy : (s.sup p) y = (p i) y<GOAL>q y ≤ C • (p i) y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<GOAL>(map Prod.mk f).seq g = (map (fun b a => (a, b)) g).seq f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>s : Set (α → α × β)<VAR>hs : s ∈ map (fun b a => (a, b)) g<VAR>t : Set α<VAR>ht : t ∈ f<GOAL>s.seq t ∈ (map Prod.mk f).seq g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>g : Filter β<VAR>s : Set (β → α × β)<VAR>hs : s ∈ map Prod.mk f<VAR>t : Set β<VAR>ht : t ∈ g<GOAL>s.seq t ∈ (map (fun b a => (a, b)) g).seq f
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂✝ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>S₂ : Type u_2<VAR>inst✝ : CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂✝ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>S₂ : Type u_2<VAR>inst✝ : CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>∀ (a : R), k (eval₂ f g (C a)) = eval₂ k (⇑k ∘ g) ((map f) (C a))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂✝ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>S₂ : Type u_2<VAR>inst✝ : CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>∀ (p q : MvPolynomial σ R), k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) → k (eval₂ f g q) = eval₂ k (⇑k ∘ g) ((map f) q) → k (eval₂ f g (p + q)) = eval₂ k (⇑k ∘ g) ((map f) (p + q))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂✝ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : R →+* S₁<VAR>S₂ : Type u_2<VAR>inst✝ : CommSemiring S₂<VAR>k : S₁ →+* S₂<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>∀ (p : MvPolynomial σ R) (n : σ), k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) → k (eval₂ f g (p * X n)) = eval₂ k (⇑k ∘ g) ((map f) (p * X n))
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<GOAL>AEMeasurable g μ
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<GOAL>AEMeasurable g μ
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))<GOAL>AEMeasurable g μ
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<GOAL>AEMeasurable g μ
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → ℝ≥0∞ := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<GOAL>AEMeasurable g μ
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → ℝ≥0∞ := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<VAR>x : α<GOAL>Tendsto (fun i => aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
<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 α<VAR>ι : Type u_5<VAR>f : ι → α → ℝ≥0∞<VAR>g : α → ℝ≥0∞<VAR>μ : Measure α<VAR>u : Filter ι<VAR>inst✝¹ : u.NeBot<VAR>inst✝ : u.IsCountablyGenerated<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) u (𝓝 (g a))<VAR>v : ℕ → ι<VAR>hv : Tendsto v atTop u<VAR>h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ<VAR>p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' => Tendsto f' atTop (𝓝 (g x))<VAR>hp : ∀ᵐ (x : α) ∂μ, p x fun n => f (v n) x<VAR>aeSeqLim : α → ℝ≥0∞ := fun x => if x ∈ aeSeqSet h'f p then g x else ⋯.some<GOAL>g =ᶠ[ae μ] aeSeqLim
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n (fun p => p.1 ^ p.2) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<VAR>n : ℕ∞<VAR>hneg : p.1 < 0<GOAL>ContDiffAt ℝ n (fun p => p.1 ^ p.2) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<VAR>n : ℕ∞<VAR>hpos : 0 < p.1<GOAL>ContDiffAt ℝ n (fun p => p.1 ^ p.2) p
<VAR>α : Type u_1<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>u v a : α<VAR>ha : a ∈ {x | Disjoint u x ∧ v ≤ x}<VAR>b : α<VAR>hb : b ∈ {x | Disjoint u x ∧ v ≤ x}<VAR>hab : (fun x => (x ⊔ u) \ v) a = (fun x => (x ⊔ u) \ v) b<VAR>h : ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v<GOAL>a = b
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>j : J<VAR>I : IsInitial j<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)<GOAL>colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>j : J<VAR>I : IsInitial j<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)<GOAL>inv (𝟙 (F.obj j)) = 𝟙 (F.obj j)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>j : J<VAR>I : IsInitial j<VAR>F : J ⥤ C<VAR>inst✝¹ : HasColimit F<VAR>inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)<GOAL>Classical.choose ⋯ = 𝟙 (F.obj j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>n : ℕ<GOAL>∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>n : ℕ<GOAL>∀ᵐ (x : α) ∂ν.restrict (spanningSets μ n), μ.rnDeriv ν x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>n : ℕ<GOAL>∫⁻ (x : α) in spanningSets μ n, μ.rnDeriv ν x ∂ν ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>n : ℕ<GOAL>μ (spanningSets μ n) ≠ ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z✝ : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : X ≃ Y<VAR>hf : Inducing ⇑f<GOAL>Continuous (⇑f ∘ f.invFun)
<VAR>A : Class<VAR>x : ZFSet<VAR>H : ∀ (y : ZFSet), A y ↔ y = x<VAR>y : ZFSet<VAR>x✝ : A.iota y<VAR>x' : ZFSet<VAR>h : {x | ∀ (y : ZFSet), A y ↔ y = x} x'<VAR>yx' : y ∈ ↑x'<GOAL>↑x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<VAR>b : β<VAR>h : ∀ (a' : α), r a' a → s (↑(f.collapseF a')) b<GOAL>¬s b ↑(⋯.fix (fun a IH => let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) a)