ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁵ : LinearOrderedRing α<VAR>inst✝⁴ : LinearOrderedRing β<VAR>inst✝³ : FloorRing α<VAR>inst✝² : FloorRing β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>a✝ : α<VAR>b : β<VAR>f : F<VAR>hf : StrictMono ⇑f<VAR>a : α<GOAL>fract (f a) = f (fract a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝ : ∀ (a : α), IsFiniteMeasure (κ a)<VAR>t : Set Ω<VAR>h_indep : IndepSet t t κ μα<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝ : ∀ (a : α), IsFiniteMeasure (κ a)<VAR>t : Set Ω<VAR>h_indep : IndepSet t t κ μα<VAR>a : α<VAR>h_0_1_top : (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤<GOAL>(κ a) t = 0 ∨ (κ a) t = 1
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hf : Integrable f μ<VAR>h_int : Integrable (llr μ ν) μ<VAR>hfμ : Integrable (fun x => rexp (f x)) μ<VAR>hfν : AEMeasurable f ν<GOAL>Integrable (llr (μ.tilted f) ν) μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>hf : Integrable f μ<VAR>h_int : Integrable (llr μ ν) μ<VAR>hfμ : Integrable (fun x => rexp (f x)) μ<VAR>hfν : AEMeasurable f ν<GOAL>Integrable (fun x => f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u₁ u₂ : UniformSpace α<VAR>h : u₁ ≤ u₂<VAR>a : α<GOAL>𝓝 a ≤ 𝓝 a
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u₁ u₂ : UniformSpace α<VAR>h : u₁ ≤ u₂<VAR>a : α<GOAL>(𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<GOAL>(LieModule.traceForm R (↥H) L).Nondegenerate
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>x : Rˣ<GOAL>(x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>x y : E<GOAL>x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t
<VAR>h : IsField ℤ<VAR>a : ℤ<GOAL>2 * a = 1 → 1 = a + a
<VAR>h : IsField ℤ<VAR>a : ℤ<GOAL>2 * a = 1 → 1 = 2 * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P✝ Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>P : Cubic R<GOAL>P.toPoly = 0 ↔ P = 0
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<GOAL>(map ι f) x = x ↔ 0 < LinearMap.det ↑f
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : IsEmpty ι<GOAL>(map ι f) x = x ↔ 0 < LinearMap.det ↑f
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x : Orientation R M ι<VAR>f : M ≃ₗ[R] M<VAR>h : Fintype.card ι = finrank R M<VAR>h✝ : Nonempty ι<GOAL>(map ι f) x = x ↔ 0 < LinearMap.det ↑f
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<GOAL>sSup (a • s) = a • sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>sSup (a • ∅) = a • sSup ∅
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<VAR>hs : s.Nonempty<GOAL>sSup (a • s) = a • sSup s
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Ici<GOAL>Indep (limsup s atBot) (limsup s atBot) κ μα
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Ici<VAR>hnsp : ∀ (i : ι), BddBelow (ns i)<GOAL>Indep (limsup s atBot) (limsup s atBot) κ μα
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Ici<VAR>hnsp : ∀ (i : ι), BddBelow (ns i)<GOAL>∀ (t : Set ι), BddBelow t → tᶜ ∈ atBot
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Ici<VAR>hnsp : ∀ (i : ι), BddBelow (ns i)<GOAL>Directed (fun x x_1 => x ≤ x_1) ns
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>inst✝⁴ : IsMarkovKernel κ<VAR>inst✝³ : IsProbabilityMeasure μ<VAR>inst✝² : SemilatticeInf ι<VAR>inst✝¹ : NoMinOrder ι<VAR>inst✝ : Nonempty ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>ns : ι → Set ι := Set.Ici<VAR>hnsp : ∀ (i : ι), BddBelow (ns i)<GOAL>∀ (n : ι), ∃ a, n ∈ ns a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<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>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>k : ℕ<VAR>ih : lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) k = baseChange A (lowerCentralSeries R L M k)<GOAL>lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] M) (k + 1) = baseChange A (lowerCentralSeries R L M (k + 1))
<VAR>α β : Type u<VAR>c : Cardinal.{?u.233529}<VAR>x : α<GOAL>2 ≤ #α ↔ ∃ y, y ≠ x
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>p : α → Prop<VAR>hp : ComputablePred p<GOAL>RePred p
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>f : α → Bool<VAR>hf : Computable f<VAR>hp : ComputablePred fun a => f a = true<GOAL>RePred fun a => f a = true
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>f : α → Bool<VAR>hf : Computable f<VAR>hp : ComputablePred fun a => f a = true<GOAL>Partrec fun a => Part.assert (f a = true) fun x => Part.some ()
<VAR>α : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : Primcodable α<VAR>inst✝ : Primcodable σ<VAR>f : α → Bool<VAR>hf : Computable f<VAR>hp : ComputablePred fun a => f a = true<VAR>n : α<VAR>a : Unit<GOAL>(a ∈ bif f n then Part.some () else Part.none) ↔ a ∈ Part.assert (f n = true) fun x => Part.some ()
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<GOAL>(∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>hv : CompleteLattice.Independent fun i => Submodule.span R {v i}<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<GOAL>LinearIndependent R v
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>hv : CompleteLattice.Independent fun i => Submodule.span R {v i}<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<VAR>i : ι<VAR>r : R<VAR>hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))<GOAL>r = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<VAR>i : ι<VAR>r : R<VAR>hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))<VAR>hv : Disjoint (Submodule.span R {v i}) (⨆ j, ⨆ (_ : j ≠ i), Submodule.span R {v j})<GOAL>r = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<VAR>i : ι<VAR>r : R<VAR>hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))<VAR>hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥<GOAL>r = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<VAR>i : ι<VAR>r : R<VAR>hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))<VAR>hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥<VAR>this : r • v i ∈ ⊥<GOAL>r = 0
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>M : Type u_5<VAR>v : ι → M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥<VAR>i : ι<VAR>r : R<VAR>hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))<VAR>hv : Submodule.span R {v i} ⊓ Submodule.span R (Set.range fun i_1 => v ↑i_1) = ⊥<VAR>this : r • v i ∈ ⊥<GOAL>r ∈ torsionOf R M (v i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<GOAL>Filter.coprodᵢ f = ⊥ ↔ (∃ i, IsEmpty (α i)) ∨ f = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝³ : GroupWithZero G₀<VAR>inst✝² : TopologicalSpace G₀<VAR>inst✝¹ : HasContinuousInv₀ G₀<VAR>inst✝ : ContinuousMul G₀<VAR>f g : α → G₀<VAR>l : Filter α<VAR>a b : G₀<VAR>hf : Tendsto f l (𝓝 a)<VAR>hg : Tendsto g l (𝓝 b)<VAR>hy : b ≠ 0<GOAL>Tendsto (f / g) l (𝓝 (a / b))
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>cexp (log x) = x
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<GOAL>A f L r ε ∈ 𝓝[>] x
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<GOAL>∃ u ∈ Ioi x, Ioo x u ⊆ A f L r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<GOAL>∃ u ∈ Ioi x, Ioo x u ⊆ A f L r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<GOAL>∃ u ∈ Ioi x, Ioo x u ⊆ A f L r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<VAR>x' : ℝ<VAR>hx' : x' ∈ Ioo x (x + r' - s)<GOAL>∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>L : F<VAR>r ε x r' : ℝ<VAR>rr' : r' ∈ Ioc (r / 2) r<VAR>hr' : ∀ y ∈ Icc x (x + r'), ∀ z ∈ Icc x (x + r'), ‖f z - f y - (z - y) • L‖ ≤ ε * r<VAR>s : ℝ<VAR>s_gt : r / 2 < s<VAR>s_lt : s < r'<VAR>this : s ∈ Ioc (r / 2) r<VAR>x' : ℝ<VAR>hx' : x' ∈ Ioo x (x + r' - s)<VAR>A : Icc x' (x' + s) ⊆ Icc x (x + r')<GOAL>∀ y ∈ Icc x' (x' + s), ∀ z ∈ Icc x' (x' + s), ‖f z - f y - (z - y) • L‖ ≤ ε * r
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>inst✝ : (i : Fin (n + 1)) → Preorder (α i)<VAR>i : Fin (n + 1)<VAR>x : α i<VAR>p : (j : Fin n) → α (i.succAbove j)<VAR>q : (j : Fin (n + 1)) → α j<GOAL>i.insertNth x p ≤ q ↔ x ≤ q i ∧ p ≤ fun j => q (i.succAbove j)
<VAR>x y : ℝ<VAR>h : x * y < 1<VAR>hy : y ≤ 0<GOAL>arctan x + arctan y < π / 2
<VAR>x y : ℝ<VAR>h : x * y < 1<VAR>hy : 0 < y<GOAL>arctan x + arctan y < π / 2
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : NonAssocSemiring R<VAR>inst✝³ : Semiring k<VAR>inst✝² : One G<VAR>g_hom : Type u_3<VAR>inst✝¹ : FunLike g_hom G R<VAR>inst✝ : OneHomClass g_hom G R<VAR>f : k →+* R<VAR>g : g_hom<GOAL>(liftNC ↑f ⇑g) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>r : ℝ≥0<VAR>h₀ : edist x y ≠ 0<VAR>htop : edist x y ≠ ⊤<VAR>hr : edist (f x) (f y) = ↑r * edist x y<GOAL>r = ratio f
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>f : F<GOAL>HasDerivWithinAt (fun y => c y • f) (c' • f) s x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>f : F<VAR>this : HasDerivWithinAt (fun y => c y • f) (c x • 0 + c' • f) s x<GOAL>HasDerivWithinAt (fun y => c y • f) (c' • f) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>x✝ : Option α<VAR>g : γ → α<VAR>x : Option γ<VAR>H : ∀ (a : α), a ∈ Option.map g x → p a<GOAL>pmap f (Option.map g x) H = pmap (fun a h => f (g a) h) x ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>hq : q ≠ 0<VAR>h : ¬p = 1<GOAL>q * p ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ decode₂ α n ↔ a ∈ decode n ∧ encode a = n
<VAR>R : Type u_4<VAR>S : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Module R M<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>B : BilinForm S M<VAR>ι : Type u_1<VAR>inst✝ : Finite ι<VAR>hB : B.Nondegenerate<VAR>b : Basis ι S M<GOAL>B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>cos (angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫_ℝ
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>‖x‖ * ‖y‖ = 0 → ⟪x, y⟫_ℝ = 0
<VAR>o : Ordinal.{u}<VAR>h : o < ω<GOAL>o < ℵ₀.ord
<VAR>o : Ordinal.{0}<VAR>h' : o < type fun x x_1 => x < x_1<VAR>h : Ordinal.lift.{u, 0} o < ω<GOAL>Ordinal.lift.{u, 0} o < ℵ₀.ord
<VAR>o : Ordinal.{0}<VAR>h' : o < type fun x x_1 => x < x_1<VAR>h : Ordinal.lift.{u, 0} o < ω<GOAL>(typein (fun x x_1 => x < x_1) (enum (fun x x_1 => x < x_1) o h')).card < ℵ₀
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : StarRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : Semiring C<VAR>inst✝² : StarRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : StarModule R C<VAR>S T : StarSubalgebra R A<VAR>h : S.toSubalgebra = T.toSubalgebra<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<VAR>h4 : 0 ≤ᶠ[ae μ] X * Y<GOAL>integral μ (X * Y) = integral μ X * integral μ Y
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<VAR>h4 : 0 ≤ᶠ[ae μ] X * Y<GOAL>(∫⁻ (a : Ω), ENNReal.ofReal ((X * Y) a) ∂μ).toReal = (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ).toReal * (∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<VAR>h4 : 0 ≤ᶠ[ae μ] X * Y<GOAL>(∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ).toReal = ((∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ).toReal
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<VAR>h4 : 0 ≤ᶠ[ae μ] X * Y<GOAL>∫⁻ (a : Ω), ENNReal.ofReal (X a) * ENNReal.ofReal (Y a) ∂μ = (∫⁻ (a : Ω), ENNReal.ofReal (X a) ∂μ) * ∫⁻ (a : Ω), ENNReal.ofReal (Y a) ∂μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>hXY : IndepFun X Y μ<VAR>hXp : 0 ≤ X<VAR>hYp : 0 ≤ Y<VAR>hXm : AEMeasurable X μ<VAR>hYm : AEMeasurable Y μ<VAR>h1 : AEMeasurable (fun a => ENNReal.ofReal (X a)) μ<VAR>h2 : AEMeasurable (fun a => ENNReal.ofReal (Y a)) μ<VAR>h3 : AEMeasurable (X * Y) μ<VAR>h4 : 0 ≤ᶠ[ae μ] X * Y<GOAL>IndepFun (fun a => ENNReal.ofReal (X a)) (fun a => ENNReal.ofReal (Y a)) μ
<VAR>x y : ℝ<VAR>f g : CauSeq ℚ abs<GOAL>mk (f * g) = mk f * mk g
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ z ⊓ y = (x ⊓ y) \ z
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid M₂<VAR>f g : M →+ M₂<VAR>h : f.toNatLinearMap = g.toNatLinearMap<VAR>x : M<GOAL>f x = g x