ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<VAR>b : ι<VAR>hb : b ∈ s<VAR>hPb : f b ^ e b ≤ P<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<VAR>b : ι<VAR>hb : b ∈ s<VAR>hPb : f b ^ e b ≤ P<VAR>this : (f a).IsPrime<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this✝¹ : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<VAR>b : ι<VAR>hb : b ∈ s<VAR>hPb : f b ^ e b ≤ P<VAR>this✝ : (f a).IsPrime<VAR>this : (f b).IsPrime<GOAL>False
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this✝¹ : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<VAR>b : ι<VAR>hb : b ∈ s<VAR>hPb : f b ^ e b ≤ P<VAR>this✝ : (f a).IsPrime<VAR>this : (f b).IsPrime<GOAL>a ≠ b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Ideal R<VAR>e : ι → ℕ<VAR>this✝¹ : DecidableEq ι := Classical.decEq ι<VAR>a : ι<VAR>s : Finset ι<VAR>ha : a ∉ s<VAR>prime : ∀ i ∈ insert a s, Prime (f i)<VAR>coprime : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → f i ≠ f j<VAR>ih : (s.inf fun i => f i ^ e i) = ∏ i ∈ s, f i ^ e i<VAR>P : Ideal R<VAR>hPa : f a ^ e a ≤ P<VAR>hPs : ∏ x ∈ s, f x ^ e x ≤ P<VAR>hPp : P.IsPrime<VAR>b : ι<VAR>hb : b ∈ s<VAR>hPb : f b ^ e b ≤ P<VAR>this✝ : (f a).IsPrime<VAR>this : (f b).IsPrime<GOAL>f a = f b
<VAR>A : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} A<VAR>inst✝ : Abelian A<VAR>X : SimplicialObject A<VAR>n : ℕ<VAR>j : Fin (n + 1)<VAR>x✝ : n + 1 ≤ ↑j + (n + 1)<GOAL>(Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ j.succ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : OrderedCommGroup α<VAR>inst✝ : OrderedCommGroup β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<GOAL>Monovary f g⁻¹ ↔ Antivary f g
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<GOAL>μ (f '' s) ≤ (comap f μ) s
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β✝<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝ : α → β✝<VAR>β : Type u_8<VAR>inst✝ : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>s : Set α<GOAL>μ (f '' s) ≤ (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n + 1), u k = (⨆ k, ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S : ShortComplex (CochainComplex C ℤ)<VAR>σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting<VAR>n : ℤ<GOAL>(homOfDegreewiseSplit S σ).f n = (↑(cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>‖z1 + z2‖ ≥ ‖z1‖
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<VAR>hne : ¬‖z1‖ = ‖z2‖<GOAL>max ‖z1‖ ‖z2‖ ≥ ‖z1‖
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>χ₄ ↑n = (-1) ^ (n / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>(if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>(if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>(if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>(if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<GOAL>(if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
<VAR>n : ℕ<VAR>hn : n % 2 = 1<VAR>help : ∀ m < 4, m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)<GOAL>(if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<GOAL>HasDerivWithinAt (fun t => f (x + t • c • v)) (c • f') ((fun t => x + t • c • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<VAR>A : HasDerivAt g c 0<GOAL>HasDerivWithinAt (fun t => f (x + t • c • v)) (c • f') ((fun t => x + t • c • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<VAR>A : HasDerivAt g c 0<VAR>B : HasDerivWithinAt (fun t => f (x + t • v)) f' s' (g 0)<GOAL>HasDerivWithinAt (fun t => f (x + t • c • v)) (c • f') ((fun t => x + t • c • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<VAR>A : HasDerivAt g c 0<VAR>B : HasDerivWithinAt (fun t => f (x + t • v)) f' s' (g 0)<VAR>Z : HasDerivWithinAt ((fun t => f (x + t • v)) ∘ g) (c • f') (g ⁻¹' s') 0<GOAL>HasDerivWithinAt (fun t => f (x + t • c • v)) (c • f') ((fun t => x + t • c • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<VAR>A : HasDerivAt g c 0<VAR>B : HasDerivWithinAt (fun t => f (x + t • v)) f' s' (g 0)<VAR>Z : HasDerivWithinAt (fun x_1 => f (x + x_1 • c • v)) (c • f') ((fun t => t * c) ⁻¹' ((fun t => x + t • v) ⁻¹' s)) 0<GOAL>HasDerivWithinAt (fun t => f (x + t • c • v)) (c • f') ((fun t => x + t • c • v) ⁻¹' s) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasDerivWithinAt (fun t => f (x + t • v)) f' ((fun t => x + t • v) ⁻¹' s) 0<VAR>c : 𝕜<VAR>g : 𝕜 → 𝕜 := fun t => c • t<VAR>s' : Set 𝕜 := (fun t => x + t • v) ⁻¹' s<VAR>A : HasDerivAt g c 0<VAR>B : HasDerivWithinAt (fun t => f (x + t • v)) f' s' (g 0)<VAR>Z : HasDerivWithinAt (fun x_1 => f (x + x_1 • c • v)) (c • f') ((fun t => t * c) ⁻¹' ((fun t => x + t • v) ⁻¹' s)) 0<VAR>t : 𝕜<GOAL>t ∈ (fun t => x + t • c • v) ⁻¹' s ↔ t ∈ (fun t => t * c) ⁻¹' ((fun t => x + t • v) ⁻¹' s)
<VAR>q : ℍ<GOAL>(exp ℝ q).im = (exp ℝ q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<GOAL>Tendsto (fun n => ↑(hf.approxBounded c n) x) atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<GOAL>Tendsto (fun n => ↑(hf.approxBounded c n) x) atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖) • ↑(hf.approx n) x) atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖) • ↑(hf.approx n) x) atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖) • ↑(hf.approx n) x) atTop (𝓝 (1 • f x))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<VAR>this : min 1 (c / ‖f x‖) = 1<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<VAR>this : min 1 (c / ‖f x‖) = 1<GOAL>Tendsto (fun n => min 1 (c / ‖↑(hf.approx n) x‖)) atTop (𝓝 (min 1 (c / ‖f x‖)))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f✝ g : α → β✝<VAR>inst✝² : TopologicalSpace β✝<VAR>β : Type u_5<VAR>f : α → β<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedSpace ℝ β<VAR>m : MeasurableSpace α<VAR>hf : StronglyMeasurable f<VAR>c : ℝ<VAR>x : α<VAR>hfx : ‖f x‖ ≤ c<VAR>h_tendsto : Tendsto (fun n => ↑(hf.approx n) x) atTop (𝓝 (f x))<VAR>hfx0 : ¬‖f x‖ = 0<VAR>this : min 1 (c / ‖f x‖) = 1<GOAL>Tendsto (fun n => c / ‖↑(hf.approx n) x‖) atTop (𝓝 (c / ‖f x‖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h : b₁ < b₂<VAR>x : α<GOAL>x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioc (max a₁ a₂) b₁
<VAR>p : ℕ → Prop<GOAL>nth p 0 = sInf (setOf p)
<VAR>p : ℕ → Prop<GOAL>sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable (fun x => rexp (f x)) μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable (fun x => rexp (f x)) μ<VAR>this : f = fun x => log (rexp (f x))<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>x✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : MeasureTheory.Measure α<VAR>hf : AEMeasurable (fun x => rexp (f x)) μ<VAR>this : f = fun x => log (rexp (f x))<GOAL>AEMeasurable (fun x => log (rexp (f x))) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : DivisionRing β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>K : α<VAR>K0 : K > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, K ≤ abv (↑f j)<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>abv (↑(f * f.inv hf - 1) j) < ε
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (-x) = -WittVector.ghostFun x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f✝ : α → β<VAR>f : α → ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y<GOAL>∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑1 * dist x y
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>x : F<GOAL>(X - C x).natSepDegree = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>hind : X.str = ⊤<VAR>F : Presheaf C X<VAR>it : IsTerminal (F.obj (op ⊥))<VAR>c : C<VAR>U : TopologicalSpace.Opens ↑X<VAR>s : Sieve U<VAR>hs : s ∈ (Opens.grothendieckTopology ↑X).sieves U<GOAL>Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>hind : X.str = ⊤<VAR>F : Presheaf C X<VAR>it : IsTerminal (F.obj (op ⊥))<VAR>c : C<VAR>s : Sieve ⊥<VAR>hs : s ∈ (Opens.grothendieckTopology ↑X).sieves ⊥<GOAL>Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : TopCat<VAR>hind : X.str = ⊤<VAR>F : Presheaf C X<VAR>it : IsTerminal (F.obj (op ⊥))<VAR>c : C<VAR>U : TopologicalSpace.Opens ↑X<VAR>s : Sieve U<VAR>hs : s ∈ (Opens.grothendieckTopology ↑X).sieves U<VAR>hne : U ≠ ⊥<GOAL>Presieve.IsSheafFor (F ⋙ coyoneda.obj (op c)) s.arrows
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≤ b<VAR>ht : b = ⊤ → a = ⊤<GOAL>a.toReal ≤ b.toReal
<VAR>b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : ⊤ ≤ b<VAR>ht : b = ⊤ → ⊤ = ⊤<GOAL>⊤.toReal ≤ b.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a ≤ b<VAR>ht : b = ⊤ → a = ⊤<VAR>ha : a ≠ ⊤<GOAL>a.toReal ≤ b.toReal
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>Integrable (μ[f|m]) μ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>n : ℕ<VAR>b : Basis (Fin n) R M<VAR>k : Fin n<VAR>a✝ : Nontrivial R<GOAL>b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<GOAL>IsUnit (c 0)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : Fin (n + 1)<VAR>hr : 1 = c i<GOAL>IsUnit (c 0)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : Fin (n + 1)<VAR>hr : 1 = c i<GOAL>c 0 ≤ c i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a b x y : R<VAR>n m : ℕ<VAR>ha : 1 ≤ a<VAR>h : m ≠ 0<GOAL>a ≤ a ^ m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>S : Set (LieSubmodule R L M)<GOAL>⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p = ⋂ s ∈ S, ↑s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>S : Set (LieSubmodule R L M)<VAR>m : M<GOAL>m ∈ ⋂ p ∈ {x | ∃ s ∈ S, ↑s = x}, ↑p ↔ m ∈ ⋂ s ∈ S, ↑s
<VAR>Ω : Type u_1<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝⁴ : SMul R ℝ≥0<VAR>inst✝³ : SMul R ℝ≥0∞<VAR>inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>inst✝ : TopologicalSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>c : ℝ≥0<GOAL>μ.testAgainstNN (const Ω c) = c * μ.mass
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<VAR>hq : ¬q = 0<GOAL>(p * q).mirror = p.mirror * q.mirror
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<VAR>hq : ¬q = 0<GOAL>p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) = p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<VAR>hq : ¬q = 0<GOAL>p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) = p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<GOAL>(ofFinsupp f).hsum.coeff g = (f.sum fun x => id).coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<GOAL>∑ᶠ (i : α), (f i).coeff g = (∑ x ∈ f.support, id (f x)).coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<GOAL>∑ᶠ (i : α), (coeff.addMonoidHom g) (f i) = (coeff.addMonoidHom g) (∑ x ∈ f.support, f x)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<GOAL>(Function.support fun i => (coeff.addMonoidHom g) (f i)) ⊆ ↑f.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<VAR>x : α<VAR>h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)<GOAL>x ∈ ↑f.support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<VAR>x : α<VAR>h : x ∈ Function.support fun i => (coeff.addMonoidHom g) (f i)<GOAL>¬f x = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<VAR>g : Γ<VAR>x : α<VAR>h : f x = 0<GOAL>x ∉ Function.support fun i => (coeff.addMonoidHom g) (f i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab✝ : a ≤ b<VAR>hf✝ : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>c d : ℝ<VAR>hca : c ≤ a<VAR>hab : a ≤ b<VAR>hbd : b ≤ d<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ioc c d))] f<VAR>hfi : IntervalIntegrable f μ c d<GOAL>∫ (x : ℝ) in a..b, f x ∂μ ≤ ∫ (x : ℝ) in c..d, f x ∂μ