ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<GOAL>‖Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int‖ = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<GOAL>(∫⁻ (a : α), ↑‖↑↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) a‖₊ ∂μ).toReal = (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<GOAL>∫⁻ (a : α), ↑‖↑↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) a‖₊ ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<GOAL>(fun a => ↑‖↑↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) a‖₊) =ᶠ[ae μ] fun a => ENNReal.ofReal ‖fs n a - f a‖
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<GOAL>(fun a => ↑‖↑↑(Integrable.toL1 (fs n - f) ⋯) a‖₊) =ᶠ[ae μ] fun a => ENNReal.ofReal ‖fs n a - f a‖
<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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<VAR>x : α<VAR>hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x<GOAL>(fun a => ↑‖↑↑(Integrable.toL1 (fs n - f) ⋯) a‖₊) x = (fun a => ENNReal.ofReal ‖fs n a - f a‖) 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✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => fs n a) atTop (𝓝 (f a))<VAR>f_measurable : AEStronglyMeasurable f μ<VAR>fs_int : ∀ (n : ℕ), Integrable (fs n) μ<VAR>f_int : Integrable f μ<VAR>lintegral_norm_tendsto_zero : Tendsto (fun n => (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)<VAR>n : ℕ<VAR>x : α<VAR>hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x<GOAL>↑‖↑↑(Integrable.toL1 (fs n - f) ⋯) x‖₊ = ENNReal.ofReal ‖fs n x - f x‖
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : Set ↑↑X.toPresheafedSpace<GOAL>IsCompact U ∧ IsOpen U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, ↑↑i
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : Set ↑↑X.toPresheafedSpace<GOAL>Opens.IsBasis (Set.range fun U => ↑U)
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>X : Scheme<VAR>U : Set ↑↑X.toPresheafedSpace<GOAL>∀ (i : ↑X.affineOpens), IsCompact ↑↑i
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>2 ∣ n.centralBinom
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>2 ∣ n.pred.succ.centralBinom
<VAR>R : Type uR<VAR>A₁ : Type uA₁<VAR>A₂ : Type uA₂<VAR>A₃ : Type uA₃<VAR>A₁' : Type uA₁'<VAR>A₂' : Type uA₂'<VAR>A₃' : Type uA₃'<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A₁<VAR>inst✝¹⁰ : Semiring A₂<VAR>inst✝⁹ : Semiring A₃<VAR>inst✝⁸ : Semiring A₁'<VAR>inst✝⁷ : Semiring A₂'<VAR>inst✝⁶ : Semiring A₃'<VAR>inst✝⁵ : Algebra R A₁<VAR>inst✝⁴ : Algebra R A₂<VAR>inst✝³ : Algebra R A₃<VAR>inst✝² : Algebra R A₁'<VAR>inst✝¹ : Algebra R A₂'<VAR>inst✝ : Algebra R A₃'<VAR>e✝ e : A₁ ≃ₐ[R] A₂<VAR>y : R<VAR>x : A₁<VAR>h : (algebraMap R A₂) y = e x<GOAL>(algebraMap R A₁) y = x
<VAR>z : ℂ<VAR>h₁ : z ≠ I<VAR>h₂ : z ≠ -I<GOAL>(cexp (-z.arctan * I) - cexp (z.arctan * I)) * I / 2 / ((cexp (z.arctan * I) + cexp (-z.arctan * I)) / 2) = z
<VAR>z : ℂ<VAR>h₁ : z ≠ I<VAR>h₂ : z ≠ -I<GOAL>(1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
<VAR>z : ℂ<VAR>h₁ : z ≠ I<VAR>h₂ : z ≠ -I<VAR>z₁ : 1 + z * I ≠ 0<GOAL>(1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
<VAR>z : ℂ<VAR>h₁ : z ≠ I<VAR>h₂ : z ≠ -I<VAR>z₁ : 1 + z * I ≠ 0<VAR>z₂ : 1 - z * I ≠ 0<GOAL>(1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
<VAR>z : ℂ<VAR>h₁ : z ≠ I<VAR>h₂ : z ≠ -I<VAR>z₁ : 1 + z * I ≠ 0<VAR>z₂ : 1 - z * I ≠ 0<VAR>key : cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)<GOAL>(1 - cexp (2 * (z.arctan * I))) / (cexp (2 * (z.arctan * I)) + 1) * I = z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∈ support R M ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p : PrimeSpectrum R<GOAL>(∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0) ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal
<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✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p : Seminorm 𝕜 E<VAR>r : ℝ<VAR>x : E<GOAL>x ∈ ⇑p ⁻¹' Metric.ball 0 r ↔ x ∈ {x | p x < r}
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Continuous' g<GOAL>Continuous' fun x => f <$> g x
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Continuous' g<GOAL>Continuous' fun x => g x >>= pure ∘ f
<VAR>α : Type u<VAR>α' : Type u_1<VAR>β✝ : Type v<VAR>β' : Type u_2<VAR>γ✝ : Type u_3<VAR>φ : Type u_4<VAR>inst✝⁵ : OmegaCompletePartialOrder α<VAR>inst✝⁴ : OmegaCompletePartialOrder β✝<VAR>inst✝³ : OmegaCompletePartialOrder γ✝<VAR>inst✝² : OmegaCompletePartialOrder φ<VAR>inst✝¹ : OmegaCompletePartialOrder α'<VAR>inst✝ : OmegaCompletePartialOrder β'<VAR>β γ : Type v<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Continuous' g<GOAL>Continuous' fun x => pure ∘ f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)<VAR>hmn : m + 1 ≤ n<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>hg : ContDiffWithinAt 𝕜 m g s x₀<VAR>ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)<VAR>hmn : m + 1 ≤ n<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>this : ∀ (k : ℕ), ↑k ≤ m → ContDiffWithinAt 𝕜 (↑k) (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀<GOAL>ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t✝ u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F → G<VAR>g : E → F<VAR>t : Set F<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)<VAR>ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)<VAR>hgt : t ∈ 𝓝[g '' s] g x₀<VAR>m : ℕ<VAR>hg : ContDiffWithinAt 𝕜 (↑m) g s x₀<VAR>hmn : ↑m + 1 ≤ n<VAR>this : ∀ (k : ℕ), ↑k ≤ ↑m → ContDiffWithinAt 𝕜 (↑k) (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀<GOAL>ContDiffWithinAt 𝕜 (↑m) (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>IsClosed (Set.range mk)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>IsClosed univ
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>B : Set α<VAR>hB : (M.disjointSum N h).Base B<GOAL>∃ BM BN, M.Base BM ∧ N.Base BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>B : Set α<VAR>hB : M.Base (B ∩ M.E) ∧ N.Base (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E<GOAL>∃ BM BN, M.Base BM ∧ N.Base BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>B : Set α<VAR>hB : M.Base (B ∩ M.E) ∧ N.Base (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E<GOAL>B = B ∩ M.E ∪ B ∩ N.E
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S✝ S T : Subgroupoid C<VAR>h : S ≤ T<VAR>x✝¹ x✝ : ↑S.objs<VAR>s : C<VAR>hs : s ∈ S.objs<VAR>t : C<VAR>ht : t ∈ S.objs<GOAL>(inclusion h).obj ⟨s, hs⟩ = (inclusion h).obj ⟨t, ht⟩ → ⟨s, hs⟩ = ⟨t, ht⟩
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>MorphismProperty.StableUnderBaseChange @QuasiCompact
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace := HasAffineProperty.isLocal_affineProperty @QuasiCompact<GOAL>MorphismProperty.StableUnderBaseChange @QuasiCompact
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace := HasAffineProperty.isLocal_affineProperty @QuasiCompact<GOAL>AffineTargetMorphismProperty.StableUnderBaseChange fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace := HasAffineProperty.isLocal_affineProperty @QuasiCompact<GOAL>∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace ↑↑Y.toPresheafedSpace → CompactSpace ↑↑(pullback f g).toPresheafedSpace
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>this✝¹ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace := HasAffineProperty.isLocal_affineProperty @QuasiCompact<VAR>X Y S : Scheme<VAR>inst✝¹ : IsAffine S<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>h : CompactSpace ↑↑Y.toPresheafedSpace<VAR>𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g<VAR>this✝ : Finite 𝒰.J<VAR>this : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace<GOAL>CompactSpace ↑↑(pullback f g).toPresheafedSpace
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>ι : Sort u_1<VAR>hι : Nonempty ι<VAR>S : ι → Subfield K<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : K<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<GOAL>∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ (φ (↑p ^ k) / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ k} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ k)<GOAL>Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List ι<VAR>f : M → N → P<VAR>hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → M<VAR>f₂ : ι → N<GOAL>(map (fun i => f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List ι<VAR>f : M → N → P<VAR>hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → M<VAR>f₂ : ι → N<GOAL>foldl (fun x y => x * f (f₁ y) (f₂ y)) 1 l = f (foldl (fun x y => x * f₁ y) 1 l) (foldl (fun x y => x * f₂ y) 1 l)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List ι<VAR>f : M → N → P<VAR>hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d<VAR>hf' : f 1 1 = 1<VAR>f₁ : ι → M<VAR>f₂ : ι → N<GOAL>∀ (a : M) (b : N) (i : ι), f (a * f₁ i) (b * f₂ i) = f a b * f (f₁ i) (f₂ i)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<GOAL>univ.encard = PartENat.withTopEquiv (PartENat.card α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTop α<VAR>a : α<GOAL>Ioc a ⊤ = Ioi a
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
<VAR>z τ : ℂ<VAR>hτ : τ.im ≤ 0<GOAL>jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : ∀ (n : ℤ), jacobiTheta₂'_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)<GOAL>jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : ∀ (n : ℤ), jacobiTheta₂'_term n (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂'_term (n + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term (n + 1) z τ)<GOAL>cexp (-↑π * I * (τ + 2 * z)) * ∑' (c : ℤ), (jacobiTheta₂'_term ((Equiv.subRight 1) c + 1) z τ - 2 * ↑π * I * jacobiTheta₂_term ((Equiv.subRight 1) c + 1) z τ) = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_5 u_4}<VAR>ha : a < o.bmex f<GOAL>∃ i, ∃ (hi : i < o), f i hi = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_5 u_4}<VAR>ha : a < o.bmex f<VAR>i : (Quotient.out o).α<VAR>hi : o.familyOfBFamily f i = a<GOAL>∃ i, ∃ (hi : i < o), f i hi = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>(starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s t : Set α<VAR>f g : α → M<VAR>a : α<GOAL>(s.mulIndicator f = fun x => 1) ↔ Disjoint (mulSupport f) s
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : n ≤ m<VAR>t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := pellZd_add a1 n (m - n)<GOAL>pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)