ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>f g : α → ℝ<VAR>hf : StronglyMeasurable f<VAR>hfi : IntegrableOn f s μ<VAR>hg : StronglyMeasurable g<VAR>hgi : IntegrableOn g s μ<VAR>hgf : ∀ (t : Set α), MeasurableSet t → μ t < ⊤ → ∫ (x : α) in t, g x ∂μ = ∫ (x : α) in t, f x ∂μ<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h_meas_nonneg_g : MeasurableSet {x | 0 ≤ g x}<VAR>h_meas_nonneg_f : MeasurableSet {x | 0 ≤ f x}<VAR>h_meas_nonpos_g : MeasurableSet {x | g x ≤ 0}<VAR>h_meas_nonpos_f : MeasurableSet {x | f x ≤ 0}<GOAL>∫ (x : α) in {x | f x ≤ 0}, f x ∂μ.restrict s ≤ ∫ (x : α) in {x | g x ≤ 0}, g x ∂μ.restrict s
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>C : ℝ<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>a : α<GOAL>‖f a‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>C : ℝ<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>a : α<VAR>this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)<GOAL>‖f a‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>C : ℝ<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>a : α<VAR>this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)<GOAL>∀ (x : ι), ‖F x‖ ≤ C → ‖↑(F x) a‖ ≤ C
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>C : ℝ<VAR>F : ι → ↥(lp E ⊤)<VAR>hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>a : α<VAR>this : Tendsto (fun k => ‖↑(F k) a‖) l (𝓝 ‖f a‖)<VAR>k : ι<VAR>hCFk : ‖F k‖ ≤ C<GOAL>‖↑(F k) a‖ ≤ C
<VAR>n : ℕ<GOAL>n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0
<VAR>n k : ℕ<GOAL>n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<GOAL>AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i)) = F.submodule.toAddSubmonoid
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<GOAL>AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i)) ≤ F.submodule.toAddSubmonoid
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<GOAL>F.submodule.toAddSubmonoid ≤ AddSubmonoid.closure (⋃ i, ⇑(single R i) '' ↑(F.N i))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<GOAL>Exact ⇑g₁₂ ⇑g₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<VAR>h₁₂ : ∀ (x : X₁), (g₁₂.comp ↑e₁) x = ((↑e₂).comp f₁₂) x<GOAL>Exact ⇑g₁₂ ⇑g₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<VAR>h₁₂ : ∀ (x : X₁), (g₁₂.comp ↑e₁) x = ((↑e₂).comp f₁₂) x<VAR>h₂₃ : ∀ (x : X₂), (g₂₃.comp ↑e₂) x = ((↑e₃).comp f₂₃) x<GOAL>Exact ⇑g₁₂ ⇑g₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<VAR>h₁₂ : ∀ (x : X₁), g₁₂ (e₁ x) = e₂ (f₁₂ x)<VAR>h₂₃ : ∀ (x : X₂), g₂₃ (e₂ x) = e₃ (f₂₃ x)<GOAL>Exact ⇑g₁₂ ⇑g₂₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<VAR>h₁₂ : ∀ (x : X₁), g₁₂ (e₁ x) = e₂ (f₁₂ x)<VAR>h₂₃ : ∀ (x : X₂), g₂₃ (e₂ x) = e₃ (f₂₃ x)<GOAL>⇑g₂₃ ∘ ⇑g₁₂ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>N : Type u_4<VAR>N' : Type u_5<VAR>P : Type u_6<VAR>P' : Type u_7<VAR>inst✝⁸ : AddGroup M<VAR>inst✝⁷ : AddGroup N<VAR>inst✝⁶ : AddGroup P<VAR>f : M →+ N<VAR>g : N →+ P<VAR>X₁ : Type u_8<VAR>X₂ : Type u_9<VAR>X₃ : Type u_10<VAR>Y₁ : Type u_11<VAR>Y₂ : Type u_12<VAR>Y₃ : Type u_13<VAR>inst✝⁵ : AddCommMonoid X₁<VAR>inst✝⁴ : AddCommMonoid X₂<VAR>inst✝³ : AddCommMonoid X₃<VAR>inst✝² : AddCommMonoid Y₁<VAR>inst✝¹ : AddCommMonoid Y₂<VAR>inst✝ : AddCommMonoid Y₃<VAR>e₁ : X₁ ≃+ Y₁<VAR>e₂ : X₂ ≃+ Y₂<VAR>e₃ : X₃ ≃+ Y₃<VAR>f₁₂ : X₁ →+ X₂<VAR>f₂₃ : X₂ →+ X₃<VAR>g₁₂ : Y₁ →+ Y₂<VAR>g₂₃ : Y₂ →+ Y₃<VAR>comm₁₂ : g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂<VAR>comm₂₃ : g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃<VAR>H : Exact ⇑f₁₂ ⇑f₂₃<VAR>h₁₂ : ∀ (x : X₁), g₁₂ (e₁ x) = e₂ (f₁₂ x)<VAR>h₂₃ : ∀ (x : X₂), g₂₃ (e₂ x) = e₃ (f₂₃ x)<GOAL>∀ (y : Y₂), g₂₃ y = 0 → y ∈ Set.range ⇑g₁₂
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E 2 μ)<VAR>hg : AEStronglyMeasurable' m (↑↑g) μ<GOAL>⟪f, g⟫_𝕜 = ⟪↑((condexpL2 E 𝕜 hm) f), g⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E 2 μ)<VAR>hg : AEStronglyMeasurable' m (↑↑g) μ<GOAL>⟪f - ↑((orthogonalProjection (lpMeas E 𝕜 m 2 μ)) f), g⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f✝ : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y✝ z✝ : E<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConvexOn 𝕜 (Set.Icc x y) f<VAR>hz : z ∈ Set.Icc x y<GOAL>f z ≤ max (f x) (f y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f✝ : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x✝ y✝ z✝ : E<VAR>f : 𝕜 → β<VAR>x y z : 𝕜<VAR>hf : ConvexOn 𝕜 [x-[𝕜]y] f<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>f z ≤ max (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s s₁ s₂ : Set α<VAR>t : Finset α<VAR>a b : α<VAR>m n : ℕ<GOAL>G.CliqueFreeOn ∅ n ↔ n ≠ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖f‖ = SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖ = ∑ x ∈ (toSimpleFunc f).range, (μ (↑(toSimpleFunc f) ⁻¹' {x})).toReal • ‖x‖
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : ‖f z - 1‖ = ‖z - 1‖<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : normSq (f z - 1) = normSq (z - 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : (f z - 1) * (starRingEnd ℂ) (f z - 1) = (z - 1) * (starRingEnd ℂ) (z - 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : (f z - 1) * ((starRingEnd ℂ) (f z) - (starRingEnd ℂ) 1) = (z - 1) * ((starRingEnd ℂ) z - (starRingEnd ℂ) 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : f z * (starRingEnd ℂ) (f z) - (starRingEnd ℂ) (f z) - (f z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1) = z * (starRingEnd ℂ) z - (starRingEnd ℂ) z - (z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : ↑(‖z‖ ^ 2) - (starRingEnd ℂ) (f z) - (f z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1) = z * (starRingEnd ℂ) z - (starRingEnd ℂ) z - (z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : ↑(‖z‖ ^ 2) - (starRingEnd ℂ) (f z) - (f z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1) = ↑(‖z‖ ^ 2) - (starRingEnd ℂ) z - (z * (starRingEnd ℂ) 1 - (starRingEnd ℂ) 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : (starRingEnd ℂ) (f z) + (f z - 1) = (starRingEnd ℂ) z + (z - 1)<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h : f 1 = 1<VAR>z : ℂ<VAR>this : (starRingEnd ℂ) (f z) + f z = (starRingEnd ℂ) z + z<GOAL>z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)
<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>∫⁻ (a : α), s.indicator f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
<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>∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ
<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>⨆ x, ((↑x).restrict s).lintegral μ ≤ ⨆ x, (↑x).lintegral μ
<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<VAR>φ : α →ₛ ℝ≥0∞<VAR>hφ : ↑φ ≤ fun a => f a<GOAL>∃ i', ((↑⟨φ, hφ⟩).restrict s).lintegral μ ≤ (↑i').lintegral μ
<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<VAR>φ : α →ₛ ℝ≥0∞<VAR>hφ : ↑φ ≤ fun a => f a<VAR>x : α<GOAL>↑(φ.restrict s) x ≤ (fun a => s.indicator f a) x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z T : C<VAR>n : ℕ<VAR>α : Ext X Y n<VAR>m : ℕ<VAR>β₁ β₂ : Ext Y Z m<VAR>p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>(α.comp (β₁ + β₂) h).hom = (α.comp β₁ h + α.comp β₂ h).hom
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p✝ q : ℝ≥0∞<VAR>inst✝⁴ : (i : α) → NormedAddCommGroup (E i)<VAR>𝕜 : Type u_3<VAR>inst✝³ : NormedRing 𝕜<VAR>inst✝² : (i : α) → Module 𝕜 (E i)<VAR>inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)<VAR>inst✝ : DecidableEq α<VAR>p : ℝ≥0∞<VAR>i : α<VAR>a : E i<VAR>j : α<VAR>hij : j ≠ i<GOAL>↑(lp.single p i a) j = 0
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<VAR>h : IsEmpty ((i : δ) → π i)<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝³ : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝² : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝¹ : DecidableEq δ<VAR>s✝ t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y : (i : δ) → π i<VAR>i : δ<VAR>inst✝ : Fintype δ<VAR>s : Finset δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ<VAR>x : (i : δ) → π i<GOAL>∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ ≤ ∫⁻ (x : (i : δ) → π i), g x ∂Measure.pi μ
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<GOAL>ContinuousInv G
<VAR>G✝ : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁵ : TopologicalSpace G✝<VAR>inst✝⁴ : Group G✝<VAR>inst✝³ : TopologicalGroup G✝<VAR>inst✝² : TopologicalSpace α<VAR>f : α → G✝<VAR>s : Set α<VAR>x : α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalSpace G<VAR>hinv : Tendsto (fun x => x⁻¹) (𝓝 1) (𝓝 1)<VAR>hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1)<VAR>hconj : ∀ (x₀ : G), Tendsto (fun x => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)<VAR>x₀ : G<GOAL>ContinuousAt (fun a => a⁻¹) x₀
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>n : ℕ<GOAL>(coeff R m) (X s ^ n) = if m = single s n then 1 else 0
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>p n : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hdvd : p ^ n ∣ Nat.card G<GOAL>Nat.card ↥⊥ = p ^ 0
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>x ∈ (Opens.map f.val.base).obj ⊤
<VAR>X✝ : LocallyRingedSpace<VAR>U : Opens ↑X✝.toTopCat<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>x ∈ ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopology E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<GOAL>MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopology E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<VAR>this : Continuous (Function.uncurry g)<GOAL>MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : LocallyCompactSpace 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : OpensMeasurableSpace E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : CompleteSpace F<VAR>f : E → F<VAR>v : E<VAR>inst✝ : SecondCountableTopology E<VAR>hf : Continuous f<VAR>this✝¹ : MeasurableSpace 𝕜 := borel 𝕜<VAR>this✝ : BorelSpace 𝕜<VAR>g : E × E → 𝕜 → F := fun p t => f (p.1 + t • p.2)<VAR>this : Continuous (Function.uncurry g)<VAR>M_meas : MeasurableSet {q | DifferentiableAt 𝕜 (g q.1) q.2}<GOAL>MeasurableSet {p | LineDifferentiableAt 𝕜 f p.1 p.2}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{?u.22043, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>Z : C<VAR>t₁ : z₁.Y' ⟶ Z<VAR>t₂ : z₂.Y' ⟶ Z<VAR>hst : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hft : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<GOAL>LeftFractionRel z₂ z₁
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>J.toPlus P ≫ J.plusMap η ≫ (J.isoToPlus Q hQ).inv = η
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>(J.toPlus P ≫ J.plusMap η) ≫ (J.isoToPlus Q hQ).inv = η
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>J.toPlus P ≫ J.plusMap η = η ≫ (J.isoToPlus Q hQ).hom
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝² : Category.{max v u, w} D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>J.toPlus P ≫ J.plusMap η = η ≫ J.toPlus Q
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g : Perm (Fin 5)<VAR>h : 3 ∈ g.cycleType<GOAL>(g * g).IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<GOAL>(c * g' * (c * g')).IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<GOAL>(c * (g' * (c * g'))).IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<GOAL>(c * (g' * g' * c)).IsThreeCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<GOAL>orderOf g' ∣ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<GOAL>∀ b ∈ g'.cycleType, b ∣ 2