ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<GOAL>HasFDerivAt f L x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ c * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ ε * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ ε * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ ε * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ ε * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<GOAL>∀ᶠ (x_1 : E) in 𝓝 0, ‖f (x + x_1) - f x - L x_1‖ ≤ ε * ‖x_1‖
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>hv : 0 ∈ ball 0 r<GOAL>0 ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<VAR>v_ne : v ≠ 0<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<VAR>v_ne : v ≠ 0<VAR>w : E<VAR>ρ : ℝ<VAR>w_mem : w ∈ sphere 0 1<VAR>hvw : v = ρ • w<VAR>hρ : ρ = ‖v‖<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<VAR>v_ne : v ≠ 0<VAR>w : E<VAR>ρ : ℝ<VAR>w_mem : w ∈ sphere 0 1<VAR>hvw : v = ρ • w<VAR>hρ : ρ = ‖v‖<VAR>norm_rho : ‖ρ‖ = ρ<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<VAR>v_ne : v ≠ 0<VAR>w : E<VAR>ρ : ℝ<VAR>w_mem : w ∈ sphere 0 1<VAR>hvw : v = ρ • w<VAR>hρ : ρ = ‖v‖<VAR>norm_rho : ‖ρ‖ = ρ<VAR>rho_pos : 0 ≤ ρ<VAR>y : E<VAR>yq : y ∈ q<VAR>hy : ‖w - y‖ < δ<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : E → F<VAR>hf : LipschitzWith C f<VAR>s : Set E<VAR>hs : sphere 0 1 ⊆ closure s<VAR>L : E →L[ℝ] F<VAR>x : E<VAR>hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v<VAR>ε : ℝ<VAR>εpos : 0 < ε<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : (↑C + ‖L‖ + 1) * δ = ε<VAR>q : Set E<VAR>hqs : q ⊆ s<VAR>q_fin : q.Finite<VAR>hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ<VAR>I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖<VAR>v : E<VAR>hv : v ∈ ball 0 r<VAR>v_ne : v ≠ 0<VAR>w : E<VAR>ρ : ℝ<VAR>w_mem : w ∈ sphere 0 1<VAR>hvw : v = ρ • w<VAR>hρ : ρ = ‖v‖<VAR>norm_rho : ‖ρ‖ = ρ<VAR>rho_pos : 0 ≤ ρ<VAR>y : E<VAR>yq : y ∈ q<VAR>hy : ‖w - y‖ < δ<VAR>this : ‖y - w‖ < δ<GOAL>v ∈ {x_1 | (fun x_2 => ‖f (x + x_2) - f x - L x_2‖ ≤ ε * ‖x_2‖) x_1}
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<VAR>c : R<GOAL>c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) = I.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : F.map (𝟙 X) ≫ I.toRightDerivedZero' F = (injectiveResolution X).toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) = I.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : I.toRightDerivedZero' F = (injectiveResolution X).toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) = I.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : I.toRightDerivedZero' F = (injectiveResolution X).toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0<VAR>h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom = (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) = I.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map (I.isoRightDerivedToHomotopyCategoryObj F).inv
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : I.toRightDerivedZero' F = (injectiveResolution X).toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0<VAR>h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom = (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0).map ((F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) = (injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasInjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X : C<VAR>I : InjectiveResolution X<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>h₁ : I.toRightDerivedZero' F = (injectiveResolution X).toRightDerivedZero' F ≫ HomologicalComplex.cyclesMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0<VAR>h₂ : (I.isoRightDerivedToHomotopyCategoryObj F).hom = (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))<GOAL>(injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) 0).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) = (injectiveResolution X).toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj (injectiveResolution X).cocomplex).homologyπ 0 ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map (desc (𝟙 X) I (injectiveResolution X))) 0 ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : Filter β<GOAL>f₁ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : SMulCommClass 𝕜 A A<VAR>inst✝ : IsScalarTower 𝕜 A A<VAR>a : 𝓜(𝕜, A)<GOAL>a.toProd ∈ {lr | ∀ (x y : A), lr.2 x * y = x * lr.1 y}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : U R (n + 1) = X * U R n + T R (n + 1)<GOAL>T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : U R (n + 1) = X * U R n + T R (n + 1)<VAR>h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)<GOAL>T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h₁ : U R (n + 1) = X * U R n + T R (n + 1)<VAR>h₂ : U R (n + 1 + 1) = X * U R (n + 1) + T R (n + 1 + 1)<VAR>h₃ : U R (n + 2) = 2 * X * U R (n + 1) - U R n<GOAL>T R (n + 2) = X * T R (n + 1) - (1 - X ^ 2) * U R n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>𝓤 α = comap (fun x => x.2 / x.1) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>𝓤 α = comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>map (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<GOAL>comap (Prod.mk 1 ∘ fun x => x.2 / x.1) (𝓤 α) ≤ 𝓤 α
<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<VAR>r : ℝ<VAR>hr : r < 0<GOAL>o.oangle (r • x) y = o.oangle (-x) y
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>inst✝⁵ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝⁴ : HasHomotopyCofiber φ<VAR>inst✝³ : DecidableRel c.Rel<VAR>inst✝² : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)<VAR>inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))<VAR>hc : ∀ (j : ι), ∃ i, c.Rel i j<VAR>D : Type u_3<VAR>inst✝ : Category.{u_4, u_3} D<VAR>H : HomologicalComplex C c ⥤ D<VAR>hH : (homotopyEquivalences C c).IsInvertedBy H<VAR>this : IsIso (H.map (π K))<GOAL>H.map (ι₀ K) = H.map (ι₁ K)
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>h : IsCompl W W'<GOAL>IsCompl (dualAnnihilator W) (dualAnnihilator W')
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤<GOAL>dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤<GOAL>⊥ = ⊥ ∧ ⊤ = ⊤
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<GOAL>(T⁻¹ • z).re = z.re - 1