ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖<GOAL>∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : OpensMeasurableSpace α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>a b x : α<VAR>inst✝ : SecondCountableTopology α<VAR>f g : δ → α<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>Measurable fun a => Min.min (f a) (g a)
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<GOAL>μ s₁ ≤ μ s₂
<VAR>Ω : Type u_1<VAR>inst✝ : MeasurableSpace Ω<VAR>μ : ProbabilityMeasure Ω<VAR>s₁ s₂ : Set Ω<VAR>h : s₁ ⊆ s₂<GOAL>μ.toFiniteMeasure s₁ ≤ μ.toFiniteMeasure s₂
<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.155546}<VAR>f : (a : Ordinal.{?u.155546}) → a < o → α<VAR>i : Ordinal.{?u.155546}<VAR>hi : i < o<GOAL>(type fun x x_1 => x < x_1) = o
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>∏ x ∈ Ico 1 p, ↑x = -1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>∏ x ∈ Ico 1 (p - succ 0).succ, ↑x = -1
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : H → M'<VAR>x : H<VAR>s : Set H<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g) s x ↔ P (↑f' ∘ g) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : H → M'<VAR>x : H<VAR>s : Set H<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<VAR>hcont : ContinuousWithinAt (↑f ∘ g) s x<GOAL>P (↑f ∘ g) s x ↔ P (↑f' ∘ g) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : H → M'<VAR>x : H<VAR>s : Set H<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<VAR>hcont : ContinuousWithinAt (↑f ∘ g) s x<GOAL>P (↑(f.symm ≫ₕ f') ∘ ↑f ∘ g) s x ↔ P (↑f' ∘ g) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : H → M'<VAR>x : H<VAR>s : Set H<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<VAR>hcont : ContinuousWithinAt (↑f ∘ g) s x<GOAL>↑(f.symm ≫ₕ f') ∘ ↑f ∘ g =ᶠ[𝓝[s] x] ↑f' ∘ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>b : β<GOAL>b ∈ filter p (s.biUnion f) ↔ b ∈ s.biUnion fun a => filter p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Finset β<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>b : β<GOAL>(∃ a ∈ s, b ∈ f a) ∧ p b ↔ ∃ a ∈ s, b ∈ f a ∧ p b
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>s : Finset ι<VAR>f : ι → R[A]<GOAL>∑ i ∈ s, (f i).support.inf degt = (Multiset.map (fun f => f.support.inf degt) (Multiset.map (fun i => f i) s.val)).sum
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹¹ : SemilatticeSup B<VAR>inst✝¹⁰ : OrderBot B<VAR>inst✝⁹ : SemilatticeInf T<VAR>inst✝⁸ : OrderTop T<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝³ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : AddCommMonoid T<VAR>inst✝¹ : CovariantClass T T (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass T T (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>degb : A → B<VAR>degt : A → T<VAR>degt0 : 0 ≤ degt 0<VAR>degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)<VAR>s : Finset ι<VAR>f : ι → R[A]<GOAL>∑ i ∈ s, (f i).support.inf degt = (Multiset.map ((fun f => f.support.inf degt) ∘ fun i => f i) s.val).sum
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<VAR>h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u<GOAL>Tendsto f x (𝓝 a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : OrderTopology α<VAR>f : β → α<VAR>a : α<VAR>x : Filter β<VAR>hu : ∃ u, a < u<VAR>hl : ∃ l, l < a<VAR>h : ∀ (l u : α), l < a → a < u → ∀ᶠ (b : β) in x, l < f b ∧ f b < u<GOAL>∀ i < a, ∀ (i_2 : α), a < i_2 → ∀ᶠ (a : β) in x, f a ∈ Ioo i i_2
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s' s : ↥S<VAR>m : M<GOAL>1 • s • s' • m = 1 • (s' * s) • m
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>s' s : ↥S<VAR>m : M<GOAL>s • s' • m = s' • s • m
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>s.Productive ↔ t.Productive
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>(∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>X : StructuredArrow S T<GOAL>(eqToHom ⋯).right = eqToHom ⋯
<VAR>a b : ℝ<VAR>n✝ : ℕ<VAR>n : ℤ<VAR>h : -1 < ↑n ∨ ↑n ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
<VAR>n m : ℕ<VAR>a : Fin 1<GOAL>↑a = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>x : M × N<GOAL>toProd (inl x.1 * inr x.2) = x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<VAR>n✝¹ n✝ : ℕ<GOAL>((taylor 0 ∘ₗ monomial n✝¹) 1).coeff n✝ = ((LinearMap.id ∘ₗ monomial n✝¹) 1).coeff n✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a b c : α<GOAL>Codisjoint (￢￢a) b ↔ Codisjoint a b
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<GOAL>(coeff R n✝) ((d⁄dX R) X) = (coeff R n✝) 1
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<GOAL>(if n✝ + 1 = 1 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<GOAL>(if n✝ = 0 then ↑n✝ + 1 else 0) = if n✝ = 0 then 1 else 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>u : M₀ˣ<GOAL>inverse ↑u * ↑u = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>last n ∉ map castSuccEmb univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n : ℕ<GOAL>univ = Finset.cons (last n) (map castSuccEmb univ) ⋯
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖x + y + z‖ * ‖x + y + z‖ = (‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖) / 2 - ‖x - z‖ * ‖x - z‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>x y z : E<GOAL>‖2 • x + y‖ * ‖2 • x + y‖ + ‖2 • z + y‖ * ‖2 • z + y‖ = 2 * (‖x + y + z‖ * ‖x + y + z‖ + ‖x - z‖ * ‖x - z‖)
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<VAR>h_mul : MeasurableEmbedding fun x => x * g<GOAL>∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>p : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype p<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : NonUnitalRing R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : NoZeroDivisors R<VAR>A : Matrix m n R<VAR>v : m → R<GOAL>v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>x y z : α<VAR>inst✝ : DecompositionMonoid α<VAR>H1 : IsRelPrime x z<VAR>H2 : IsRelPrime y z<VAR>x✝ : α<VAR>h : x✝ ∣ x * y<VAR>hz : x✝ ∣ z<GOAL>IsUnit x✝
<VAR>α : Type u_1<VAR>inst✝¹ : CommMonoid α<VAR>x y z : α<VAR>inst✝ : DecompositionMonoid α<VAR>H1 : IsRelPrime x z<VAR>H2 : IsRelPrime y z<VAR>a b : α<VAR>ha : a ∣ x<VAR>hb : b ∣ y<VAR>h : a * b ∣ x * y<VAR>hz : a * b ∣ z<GOAL>IsUnit (a * b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>inst✝ : Decidable (g a ∈ s)<GOAL>∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>b ^ logb b x = |x|
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>b ^ logb b x ∈ Ioi 0
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>|x| ∈ Ioi 0
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>log (b ^ logb b x) = log |x|
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_ne_one : b ≠ 1<VAR>hx : x ≠ 0<GOAL>log x / log b * log b = log x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>p q : R[X]<VAR>inst✝³ : CommRing T<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<VAR>a : T<GOAL>(C a).rootSet S = ∅
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<GOAL>∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<GOAL>∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<VAR>r : ℝ<VAR>hr : r ∈ Ioo (dist z c) R₁<GOAL>‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<VAR>r : ℝ<VAR>hr : r ∈ Ioo (dist z c) R₁<VAR>hr₀ : 0 < r<GOAL>‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<VAR>r : ℝ<VAR>hr : r ∈ Ioo (dist z c) R₁<VAR>hr₀ : 0 < r<VAR>hd : DiffContOnCl ℂ (dslope f c) (ball c r)<GOAL>‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<VAR>r : ℝ<VAR>hr : r ∈ Ioo (dist z c) R₁<VAR>hr₀ : 0 < r<VAR>hd : DiffContOnCl ℂ (dslope f c) (ball c r)<GOAL>∀ z ∈ frontier (ball c r), ‖dslope f c z‖ ≤ R₂ / r
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f✝ : ℂ → E<VAR>c z z₀ : ℂ<VAR>f : ℂ → ℂ<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : dist z c < R₁<VAR>hR₁ : 0 < R₁<VAR>r : ℝ<VAR>hr : r ∈ Ioo (dist z c) R₁<VAR>hr₀ : 0 < r<VAR>hd : DiffContOnCl ℂ (dslope f c) (ball c r)<GOAL>z ∈ closure (ball c r)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>x : ℙ K V<GOAL>x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>S : Set (ℙ K V)<VAR>x : ℙ K V<GOAL>(∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>f' g' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>c p : ℝ<VAR>n : ℕ∞<VAR>m : ℕ<VAR>hf : ContDiffAt ℝ (↑m) f x<VAR>h : ↑m ≤ p<GOAL>ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>f' g' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>c p : ℝ<VAR>n : ℕ∞<VAR>m : ℕ<VAR>hf : ContDiffWithinAt ℝ (↑m) f Set.univ x<VAR>h : ↑m ≤ p<GOAL>ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
<GOAL>1 / 2 / (√3 / 2) = 1 / √3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<GOAL>1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>h_ind_eq : s.indicator (mk f hf) =ᶠ[ae μ] f<GOAL>AEStronglyMeasurable' m₂ f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>h_ind_eq : s.indicator (mk f hf) =ᶠ[ae μ] f<GOAL>StronglyMeasurable (s.indicator (mk f hf))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m₂ m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Zero E<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>f : α → E<VAR>hs_m : MeasurableSet s<VAR>hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)<VAR>hf : AEStronglyMeasurable' m f μ<VAR>hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0<VAR>h_ind_eq : s.indicator (mk f hf) =ᶠ[ae μ] f<VAR>hf_ind : StronglyMeasurable (s.indicator (mk f hf))<GOAL>StronglyMeasurable (s.indicator (mk f hf))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>y : ↥M<GOAL>(algEquiv M S) (mk x y) = mk' S x y
<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>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<GOAL>Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g 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>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<VAR>K_compact : IsCompact K<GOAL>Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (𝓝[>] 0) (𝓝 (∫ (x : E), lineDeriv ℝ f x v * g 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>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<VAR>K_compact : IsCompact K<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun a => n⁻¹ • (f (a + n • v) - f a) * g a) μ
<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>hf : LipschitzWith C f<VAR>h'f : HasCompactSupport f<VAR>hg : Continuous g<VAR>v : E<VAR>K : Set E := cthickening ‖v‖ (tsupport f)<VAR>K_compact : IsCompact K<GOAL>∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ᵐ (a : E) ∂μ, ‖n⁻¹ • (f (a + n • v) - f a) * g a‖ ≤ K.indicator (fun x => ↑C * ‖v‖ * ‖g x‖) a