ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>i : (X.affineCover.pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g := pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)<VAR>this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = X.affineCover.pullbackHom (pullback.fst f g) i<GOAL>Q (pullback.fst (X.affineCover.map i ≫ f) g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>i : (X.affineCover.pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g := pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)<VAR>this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = X.affineCover.pullbackHom (pullback.fst f g) i<GOAL>Q g
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 3 ≠ 0<GOAL>W.Ψ₃.leadingCoeff = 3
<VAR>f✝ : StieltjesFunction<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<GOAL>(c • f).measure = c • f.measure
<VAR>f✝ : StieltjesFunction<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>x✝ : a < b<GOAL>(c • f).measure (Ioc a b) = (c • f.measure) (Ioc a b)
<VAR>f✝ : StieltjesFunction<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>x✝ : a < b<GOAL>ofReal (↑(c • f) b - ↑(c • f) a) = c • ofReal (↑f b - ↑f a)
<VAR>f✝ : StieltjesFunction<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>x✝ : a < b<GOAL>ofReal (↑c * ↑f b - ↑c * ↑f a) = c • ofReal (↑f b - ↑f a)
<VAR>f✝ : StieltjesFunction<VAR>c : ℝ≥0<VAR>f : StieltjesFunction<VAR>a b : ℝ<VAR>x✝ : a < b<GOAL>↑c • ofReal (↑f b - ↑f a) = c • ofReal (↑f b - ↑f a)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a / b ≤ c ↔ a ≤ b * c + (b - 1)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : 0 < b<GOAL>a < b * c + b ↔ a ≤ b * c + (b - 1)
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<GOAL>IsTopologicalBasis (SetLike.coe '' Set.range X.basicOpen)
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<GOAL>SetLike.coe '' Set.range X.basicOpen = Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) '' (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<VAR>x✝ : Set ↑↑X.toPresheafedSpace<GOAL>x✝ ∈ SetLike.coe '' Set.range X.basicOpen ↔ x✝ ∈ Set.preimage ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) '' (SetLike.coe '' Set.range PrimeSpectrum.basicOpen)
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<VAR>x✝ : Set ↑↑X.toPresheafedSpace<GOAL>(∃ x ∈ Set.range X.basicOpen, ↑x = x✝) ↔ ∃ x, (∃ x_1 ∈ Set.range PrimeSpectrum.basicOpen, ↑x_1 = x) ∧ ⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) ⁻¹' x = x✝
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<GOAL>inner_ 𝕜 (I • x) y = (starRingEnd 𝕜) I * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<GOAL>inner_ 𝕜 (I • x) y = (starRingEnd 𝕜) I * inner_ 𝕜 x y
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<GOAL>4⁻¹ * (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖I • I • x + y‖ * 𝓚 ‖I • I • x + y‖ - I * 𝓚 ‖I • I • x - y‖ * 𝓚 ‖I • I • x - y‖) = 4⁻¹ * (-I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖I • I • x + y‖ * 𝓚 ‖I • I • x + y‖ - I * 𝓚 ‖I • I • x - y‖ * 𝓚 ‖I • I • x - y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖) - -I * (𝓚 ‖x - y‖ * 𝓚 ‖x - y‖) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖) - -I * (𝓚 ‖x - y‖ * 𝓚 ‖x - y‖) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ - I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖) - -I * (𝓚 ‖x - y‖ * 𝓚 ‖x - y‖) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ - I * 𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖) - -I * (𝓚 ‖x - y‖ * 𝓚 ‖x - y‖) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ + -(𝓚 ‖I • x + -y‖ * 𝓚 ‖I • x + -y‖) + I * (𝓚 ‖x + -y‖ * 𝓚 ‖x + -y‖) + -(I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖)) = -I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖) + -(-I * (𝓚 ‖x + -y‖ * 𝓚 ‖x + -y‖)) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ + -(𝓚 ‖I • x + -y‖ * 𝓚 ‖I • x + -y‖)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>hI : ¬I = 0<VAR>x y : E<VAR>hI' : -I * I = 1<VAR>h₁ : ‖-x - y‖ = ‖x + y‖<VAR>h₂ : ‖-x + y‖ = ‖x - y‖<GOAL>𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ + -(𝓚 ‖I • x + -y‖ * 𝓚 ‖I • x + -y‖) + I * (𝓚 ‖x + -y‖ * 𝓚 ‖x + -y‖) + -(I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖)) = -(I * (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖)) + - -(I * (𝓚 ‖x + -y‖ * 𝓚 ‖x + -y‖)) + 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ + -(𝓚 ‖I • x + -y‖ * 𝓚 ‖I • x + -y‖)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>f : M₁ →ₗ[R] M₁<GOAL>(toLinAlgEquiv v₁) ((toMatrixAlgEquiv v₁) f) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(f.restrict s).lintegral μ = f.lintegral (μ.restrict s)
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>(↑p).IsConjExponent ↑q ↔ p.IsConjExponent q
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>1 < p → ((↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ p⁻¹ + q⁻¹ = 1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R B<VAR>S : Subalgebra R A<VAR>ι : Type u_4<VAR>inst✝ : Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>h : K i ≤ T<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ (Set.inclusion h x) = (f i) x
<GOAL>((1 + √5) / 2) ^ 2 - ((1 + √5) / 2 + 1) = 0
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>x : β<GOAL>f.lim * x = (f * const abv x).lim
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>hf : HasFPowerSeriesOnBall f 0 x r<GOAL>∀ᶠ (z : E) in 𝓝 x, f z = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝¹ : Category.{v₂, v₁} I<VAR>F : Iᵒᵖ ⥤ C<VAR>inst✝ : HasColimit F<VAR>i : I<GOAL>(coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i = coyoneda.map (colimit.ι F (op i)).op
<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>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(deriv fun x => 1 - ε x) =ᶠ[atTop] fun z => -deriv ε z
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>x : ℝ<VAR>hx : 1 < x<GOAL>deriv (fun x => 1 - ε x) x = -deriv ε x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>(fun z => -deriv ε z) =o[atTop] fun x => x⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>deriv ε =o[atTop] fun x => x⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>R : Type u_4<VAR>inst✝¹ : SMul R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>c : R<GOAL>c • sSup s = ⨆ i ∈ s, c • i
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>φ.nilRankAux b = (φ.polyCharpoly b').natTrailingDegree
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] norm<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a<GOAL>‖f.lim‖ ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] norm<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(f - const norm f.lim) j‖ < a<GOAL>‖f.lim‖ ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] norm<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(f - const norm f.lim) j‖ < a<GOAL>‖f.lim - ↑f N + ↑f N‖ ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] norm<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(f - const norm f.lim) j‖ < a<GOAL>max ‖f.lim - ↑f N‖ ‖↑f N‖ ≤ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] norm<VAR>a : ℝ<VAR>ha : 0 < a<VAR>hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a<VAR>N : ℕ<VAR>hN : ∀ j ≥ N, ‖↑(f - const norm f.lim) j‖ < a<GOAL>max ‖↑f N - f.lim‖ ‖↑f N‖ ≤ a
<VAR>p q : ℝ<VAR>hp : 0 ≤ p<GOAL>↑(p * q).toNNReal = ↑(p.toNNReal * q.toNNReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a a₁ a₂ : α<GOAL>∏' (x : β), 1 = 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<GOAL>o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<GOAL>(-o).oangle (r • ((-o).rotation (-↑(π / 2))) x) (r • ((-o).rotation (-↑(π / 2))) x + x) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)<GOAL>(-o).oangle (r • ((-o).rotation (-↑(π / 2))) x) (r • ((-o).rotation (-↑(π / 2))) x + r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)) = ↑(Real.arctan r⁻¹)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<VAR>hr : ¬r = 0<VAR>hx : x = r⁻¹ • ((-o).rotation ↑(π / 2)) (r • ((-o).rotation (-↑(π / 2))) x)<GOAL>r • ((-o).rotation (-↑(π / 2))) x ≠ 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<GOAL>D.t' j i i = pullback.fst (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v, u₁} C<VAR>C' : Type u₂<VAR>inst✝ : Category.{v, u₂} C'<VAR>D : GlueData C<VAR>i j : D.J<GOAL>D.t' j i i = (D.t' j i i ≫ pullback.snd (D.f i i) (D.f i j)) ≫ inv (pullback.snd (D.f i i) (D.f i j))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → β<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → ℝ<VAR>hf : UniformIntegrable f p μ<GOAL>UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / ↑n) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → β<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → ℝ<VAR>hf : UniformIntegrable f p μ<VAR>n : ℕ<GOAL>(∑ i ∈ Finset.range n, f i) / ↑n = (↑n)⁻¹ • ∑ i ∈ Finset.range n, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f✝ : ι → α → β<VAR>hp : 1 ≤ p<VAR>f : ℕ → α → ℝ<VAR>hf : UniformIntegrable f p μ<VAR>n : ℕ<VAR>x : α<GOAL>((∑ i ∈ Finset.range n, f i) / ↑n) x = ((↑n)⁻¹ • ∑ i ∈ Finset.range n, f i) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>f : α → F<VAR>C : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊<GOAL>C • μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>f : α → F<VAR>C : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊<GOAL>∫⁻ (a : α), s.indicator (fun x => ↑C ^ p.toReal) a ∂μ ≤ ∫⁻ (x : α), ↑‖f x‖₊ ^ p.toReal ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>f : α → F<VAR>C : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊<GOAL>∀ᵐ (a : α) ∂μ, s.indicator (fun x => ↑C ^ p.toReal) a ≤ ↑‖f a‖₊ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>hp : p ≠ 0<VAR>hp' : p ≠ ⊤<VAR>f : α → F<VAR>C : ℝ≥0<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊<VAR>x : α<VAR>hx : x ∈ s → C ≤ ‖f x‖₊<GOAL>s.indicator (fun x => ↑C ^ p.toReal) x ≤ ↑‖f x‖₊ ^ p.toReal
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>inst✝ : SecondCountableTopologyEither E F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<GOAL>(v.prod w).addHaar = v.addHaar.prod w.addHaar
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>inst✝ : SecondCountableTopologyEither E F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>this : FiniteDimensional ℝ E<GOAL>(v.prod w).addHaar = v.addHaar.prod w.addHaar
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : Fintype ι'<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>inst✝ : SecondCountableTopologyEither E F<VAR>v : Basis ι ℝ E<VAR>w : Basis ι' ℝ F<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : FiniteDimensional ℝ F<GOAL>(v.prod w).addHaar = v.addHaar.prod w.addHaar
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<GOAL>(lift f).range = ⨆ i, (f i).range
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<GOAL>⨆ i, (f i).range ≤ (lift f).range
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<GOAL>∀ (i : ι), (f i).range ≤ (lift f).range
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N✝ : Type u_3<VAR>inst✝² : Monoid N✝<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Group (G i)<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : (i : ι) → G i →* N<VAR>i : ι<VAR>x : G i<GOAL>(f i) x ∈ (lift f).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>f✝ g : α → β<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : β → α<VAR>hf : ∀ (x y : β), f x = f y<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>f✝ g : α → β<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>f : β → α<VAR>hf : ∀ (x y : β), f x = f y<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>x✝ : β<GOAL>f x✝ = f default
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a + c + 1 < b + d
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hab : a < b<VAR>hcd : c < d<GOAL>a + (c + 1) < b + d
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(map f) ((bind₁ g) φ) = (bind₁ fun i => (map f) (g i)) ((map f) φ)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* S<VAR>g : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(eval₂Hom C fun i => (map f) (g i)) ((map f) φ) = (bind₁ fun i => (map f) (g i)) ((map f) φ)
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>‖mapL f‖ ≤ ∏ i : ι, ‖f i‖
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>∀ (x : ⨂[𝕜] (i : ι), E i), ‖(mapL f) x‖ ≤ (∏ i : ι, ‖f i‖) * ‖x‖