ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>n : Type w<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Invertible 2<VAR>m : Type w<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>Q : QuadraticMap R (m → R) R<VAR>f : (n → R) →ₗ[R] m → R<VAR>i✝ j✝ : n<GOAL>(Q.comp f).toMatrix' i✝ j✝ = ((LinearMap.toMatrix' f)ᵀ * Q.toMatrix' * LinearMap.toMatrix' f) i✝ j✝
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ι → α → M<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, Measurable f<GOAL>Measurable fun x => (map (fun f => f x) s).prod
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : AddMonoid M<VAR>G : Type u_3<VAR>inst✝² : AddCommGroup G<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<GOAL>FiniteType R R[G] ↔ AddGroup.FG G
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>γ : HomologyMapData φ h₁ h₂<GOAL>homologyMap' φ h₁ h₂ = (h₁.iso.hom ≫ (homologyMap' (opMap φ) h₂.op h₁.op).unop) ≫ h₂.iso.inv
<VAR>C : Type u₁<VAR>inst✝¹⁰ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁸ : AddMonoid M<VAR>inst✝⁷ : HasShift C M<VAR>inst✝⁶ : HasShift D M<VAR>inst✝⁵ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁴ : L.IsLocalization W<VAR>inst✝³ : HasShift D M<VAR>inst✝² : L.CommShift M<VAR>X Y Z T : C<VAR>a : M<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Y Y<VAR>f : SmallShiftedHom W X Y a<VAR>n a' : M<VAR>h : a + n = a'<GOAL>(SmallHom.equiv W L) (f.shift n a' h) = (L.commShiftIso n).hom.app X ≫ (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫ (shiftFunctor D n).map ((L.commShiftIso a).hom.app Y) ≫ (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (L.commShiftIso a').inv.app Y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b : α<GOAL>s = s ∪ t ↔ t ⊆ s
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = 0<GOAL>b ≠ 0 ∧ a.gcd ↑b ≠ 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = 0<VAR>hb : b = 0<GOAL>b ≠ 0 ∧ a.gcd ↑b ≠ 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : J(a | b) = 0<VAR>hb : b ≠ 0<GOAL>b ≠ 0 ∧ a.gcd ↑b ≠ 1
<VAR>a : ℤ<VAR>b : ℕ<VAR>x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1<VAR>hb : b ≠ 0<VAR>h : a.gcd ↑b ≠ 1<GOAL>J(a | b) = 0
<VAR>a : ℤ<VAR>b : ℕ<VAR>x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1<VAR>hb : NeZero b<VAR>h : a.gcd ↑b ≠ 1<GOAL>J(a | b) = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<GOAL>IsNilpotent R (↥(toEnd R L M).range) M ↔ IsNilpotent R L M
<VAR>𝕜 : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁷ : Field 𝕜<VAR>inst✝¹⁶ : CharZero 𝕜<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : AddCommGroup M<VAR>inst✝¹³ : Algebra 𝕜 R<VAR>inst✝¹² : Module 𝕜 M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module Rᵐᵒᵖ M<VAR>inst✝⁹ : IsCentralScalar R M<VAR>inst✝⁸ : IsScalarTower 𝕜 R M<VAR>inst✝⁷ : TopologicalSpace R<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : TopologicalRing R<VAR>inst✝⁴ : TopologicalAddGroup M<VAR>inst✝³ : ContinuousSMul R M<VAR>inst✝² : ContinuousSMul Rᵐᵒᵖ M<VAR>inst✝¹ : T2Space R<VAR>inst✝ : T2Space M<VAR>x : tsze R M<GOAL>(exp 𝕜 x).snd = exp 𝕜 x.fst • x.snd
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>v : ℤ<GOAL>↑(filter (fun x => x ≡ v [ZMOD r]) (Ioc a b)).card = max (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : AddCommMonoid S<VAR>f : ℕ → R → S<VAR>hf : ∀ (i : ℕ), f i 0 = 0<VAR>n : ℕ<VAR>p : R[X]<VAR>hn : p.degree < ↑n<VAR>hp : ¬p = 0<GOAL>∑ i : Fin n, f (↑i) (p.coeff ↑i) = p.sum f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>generateFrom (⋃ n, memPartition t n) ≤ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>t : ℕ → Set α<VAR>ht : ∀ (n : ℕ), MeasurableSet (t n)<GOAL>∀ t_1 ∈ range t, MeasurableSet t_1
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p : P1<GOAL>Function.Injective ⇑f.linear ↔ Function.Injective ⇑f
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : P1 →ᵃ[k] P2<VAR>p : P1<VAR>h : ⇑f.linear = ⇑(Equiv.vaddConst (f p)).symm ∘ ⇑f ∘ ⇑(Equiv.vaddConst p)<GOAL>Function.Injective ⇑f.linear ↔ Function.Injective ⇑f
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>T x₀ = T.rayleighQuotient x₀ • x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • x₀ + b • T x₀ = 0<GOAL>T x₀ = T.rayleighQuotient x₀ • x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • x₀ + b • T x₀ = 0<VAR>hx₀ : ¬x₀ = 0<VAR>hb : ¬b = 0<VAR>c : ℝ := -b⁻¹ * a<GOAL>T x₀ = T.rayleighQuotient x₀ • x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • x₀ + b • T x₀ = 0<VAR>hx₀ : ¬x₀ = 0<VAR>hb : ¬b = 0<VAR>c : ℝ := -b⁻¹ * a<VAR>hc : T x₀ = c • x₀<GOAL>T x₀ = T.rayleighQuotient x₀ • x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • x₀ + b • T x₀ = 0<VAR>hx₀ : ¬x₀ = 0<VAR>hb : ¬b = 0<VAR>c : ℝ := -b⁻¹ * a<VAR>hc : T x₀ = c • x₀<VAR>this✝ : ‖x₀‖ ≠ 0<VAR>this : (fun x => ⟪x, x₀⟫_ℝ) (T x₀) = (fun x => ⟪x, x₀⟫_ℝ) (c • x₀)<GOAL>T.rayleighQuotient x₀ = c
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • x₀ + b • T x₀ = 0<VAR>hx₀ : ¬x₀ = 0<VAR>hb : ¬b = 0<VAR>c : ℝ := -b⁻¹ * a<VAR>hc : T x₀ = c • x₀<VAR>this✝ : ‖x₀‖ ≠ 0<VAR>this : ⟪T x₀, x₀⟫_ℝ = c * (‖x₀‖ * ‖x₀‖)<GOAL>T.reApplyInnerSelf x₀ = c * (‖x₀‖ * ‖x₀‖)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<GOAL>ClosedEmbedding ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>h : ClosedEmbedding ⇑(f ≫ g).val.base<GOAL>ClosedEmbedding ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>h : ClosedEmbedding ⇑(f.val.base ≫ g.val.base)<GOAL>ClosedEmbedding ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>h : ClosedEmbedding ⇑(f.val.base ≫ g.val.base)<GOAL>Function.Injective ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>h : ClosedEmbedding ⇑(f.val.base ≫ g.val.base)<GOAL>IsClosedMap ⇑f.val.base
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : Function.Surjective ⇑(Scheme.Hom.stalkMap (f ≫ g) x)<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝¹ : IsClosedImmersion g<VAR>inst✝ : IsClosedImmersion (f ≫ g)<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : Function.Surjective ⇑(Scheme.Hom.stalkMap g (f.val.base x) ≫ Scheme.Hom.stalkMap f x)<GOAL>Function.Surjective ⇑(Scheme.Hom.stalkMap f x)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid R<VAR>inst✝ : Archimedean R<VAR>f : α → ℕ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x • r) l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid R<VAR>inst✝ : Archimedean R<VAR>f : α → ℕ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>s : R<GOAL>∀ᶠ (a : α) in l, s ≤ f a • r
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedCancelAddCommMonoid R<VAR>inst✝ : Archimedean R<VAR>f : α → ℕ<VAR>hr : 0 < r<VAR>hf : Tendsto f l atTop<VAR>s : R<VAR>n : ℕ<VAR>hn : s ≤ n • r<GOAL>∀ᶠ (a : α) in l, s ≤ f a • r
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<GOAL>eVariationOn (f ∘ φ) t ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<GOAL>∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }), ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ φ) (↑i.2 (i_1 + 1))) ((f ∘ φ) (↑i.2 i_1)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<GOAL>∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 (i + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 i)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<GOAL>∑ j ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j))) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<VAR>x : ℕ<VAR>hx : x ∈ Finset.range (n, ⟨u, ⋯⟩).1<GOAL>edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x))) = edist (f (↑(n, ⟨fun i => φ (u (n - i)), ⋯⟩).2 (x + 1))) (f (↑(n, ⟨fun i => φ (u (n - i)), ⋯⟩).2 x))
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<VAR>x : ℕ<VAR>hx : x < (n, ⟨u, ⋯⟩).1<GOAL>edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x))) = edist (f (↑(n, ⟨fun i => φ (u (n - i)), ⋯⟩).2 (x + 1))) (f (↑(n, ⟨fun i => φ (u (n - i)), ⋯⟩).2 x))
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<VAR>x : ℕ<VAR>hx : x < (n, ⟨u, ⋯⟩).1<GOAL>edist (f (φ (u (n - 1 - x + 1)))) (f (φ (u (n - 1 - x)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>f : α → E<VAR>s : Set α<VAR>t : Set β<VAR>φ : β → α<VAR>hφ : AntitoneOn φ t<VAR>φst : MapsTo φ t s<VAR>n : ℕ<VAR>u : ℕ → β<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<VAR>x : ℕ<VAR>hx : x < (n, ⟨u, ⋯⟩).1<GOAL>edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
<VAR>T : Type u<VAR>inst✝ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>e : f ≅ g<GOAL>e.hom.left ≫ e.inv.left = 𝟙 f.left
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁶ : SetLike σ A<VAR>inst✝⁵ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝⁴ : GradedRing 𝒜<VAR>b : A<VAR>n✝ i : ι<VAR>inst✝³ : Sub ι<VAR>inst✝² : OrderedSub ι<VAR>inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ι<VAR>inst✝ : Decidable (i ≤ n)<VAR>a : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (↑a * b)) n) = if i ≤ n then ↑a * ↑(((decompose 𝒜) b) (n - i)) else 0
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>hK : K.IsRadical<GOAL>(Ideal.comap f K).IsRadical
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>hK : K.IsRadical<GOAL>(Ideal.comap f K).radical.IsRadical
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommRing P<VAR>m : ℤ<GOAL>mk (↑m) 1 = ↑m
<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>h : Subsingleton E<VAR>f : E → F<VAR>x : E<GOAL>HasFDerivAt f 0 x
<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>h : Subsingleton E<VAR>f : E → F<VAR>x : E<GOAL>HasFDerivWithinAt f 0 {x} x
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>k : ℕ<VAR>h : G.edist u v = ↑k<GOAL>↑k ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : C(α, β)<VAR>ι : Type u_5<VAR>S : ι → Set α<VAR>φ : (i : ι) → C(↑(S i), β)<VAR>hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩<VAR>hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x<VAR>i : ι<VAR>a✝ : ↑(S i)<GOAL>(restrict (S i) (liftCover S φ hφ hS)) a✝ = (φ i) a✝
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hfN : ∀ (ω : Ω), a ≤ f N ω<VAR>hfzero : 0 ≤ f 0<VAR>hab : a < b<GOAL>(b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hfN : ∀ (ω : Ω), a ≤ f N ω<VAR>hfzero : 0 ≤ f 0<VAR>hab : a < b<GOAL>∫ (a_1 : Ω), (b - a) * ↑(upcrossingsBefore a b f N a_1) ∂μ ≤ ∫ (x : Ω), (∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)) x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hfN : ∀ (ω : Ω), a ≤ f N ω<VAR>hfzero : 0 ≤ f 0<VAR>hab : a < b<GOAL>0 ≤ᶠ[ae μ] fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>hfN : ∀ (ω : Ω), a ≤ f N ω<VAR>hfzero : 0 ≤ f 0<VAR>hab : a < b<GOAL>(fun a_1 => (b - a) * ↑(upcrossingsBefore a b f N a_1)) ≤ᶠ[ae μ] ∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>x : M<VAR>i j : ι<VAR>hxi : x ∈ ℳ i<VAR>hxj : x ∈ ℳ j<VAR>hx : x ≠ 0<GOAL>i = j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : SetLike σ M<VAR>inst✝¹ : AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>inst✝ : Decomposition ℳ<VAR>x : M<VAR>i j : ι<VAR>hxi : x ∈ ℳ i<VAR>hxj : x ∈ ℳ j<VAR>hx : i ≠ j<GOAL>x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<GOAL>l.length = l.reduceOption.length + (filter Option.isNone l).length
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>(fun x => ε ≤ ↑‖f x‖₊) = fun x => ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>x : α<GOAL>ε ≤ ↑‖f x‖₊ ↔ ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = 0 ↔ SameRay ℝ x y
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>0 ≤ (↑⟪x, y⟫_ℝ + (o.areaForm x) y • I).re ∧ (↑⟪x, y⟫_ℝ + (o.areaForm x) y • I).im = 0 ↔ SameRay ℝ x y
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<GOAL>log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 + -(z * I)).arg ≠ π ∧ 1 + -(z * I) ≠ 0<GOAL>log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<GOAL>log (1 + z * I) + -log (1 - z * I) = log ((1 + z * I) / (1 - z * I))
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<GOAL>(1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<VAR>b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)<GOAL>(1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<VAR>b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)<VAR>b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)<GOAL>(1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<VAR>b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)<VAR>b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)<VAR>c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg<GOAL>(1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>z₁ : (1 + z * I).arg ≠ π ∧ 1 + z * I ≠ 0<VAR>z₂ : (1 - z * I).arg ≠ π ∧ 1 - z * I ≠ 0<VAR>b₁ : (1 + z * I).arg ∈ Set.Ioo (-(π / 2)) (π / 2)<VAR>b₂ : (1 - z * I)⁻¹.arg ∈ Set.Ioo (-(π / 2)) (π / 2)<VAR>c₁ : -(π / 2) + -(π / 2) < (1 + z * I).arg + (1 - z * I)⁻¹.arg<VAR>c₂ : (1 + z * I).arg + (1 - z * I)⁻¹.arg < π / 2 + π / 2<GOAL>(1 + z * I).arg + (1 - z * I)⁻¹.arg ∈ Set.Ioc (-π) π