ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : r < 0<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x • r) l atBot
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<GOAL>∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<GOAL>∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<GOAL>∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : ∫ (x : ℝ) in (fun t => t ^ p) '' Ioi 0, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)<GOAL>∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Ioi 0, g y
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)<GOAL>∫ (x : ℝ) in Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)<GOAL>EqOn (fun x => (|p| * x ^ (p - 1)) • g (x ^ p)) (fun x => |p * x ^ (p - 1)| • g (x ^ p)) (Ioi 0)
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>g : ℝ → E<VAR>p : ℝ<VAR>hp : p ≠ 0<VAR>S : Set ℝ := Ioi 0<VAR>a1 : ∀ x ∈ S, HasDerivWithinAt (fun t => t ^ p) (p * x ^ (p - 1)) S x<VAR>a2 : InjOn (fun x => x ^ p) S<VAR>a3 : (fun t => t ^ p) '' S = S<VAR>this : ∫ (x : ℝ) in S, g x = ∫ (x : ℝ) in Ioi 0, |p * x ^ (p - 1)| • g (x ^ p)<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>(|p| * x ^ (p - 1)) • g (x ^ p) = |p * x ^ (p - 1)| • g (x ^ p)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g : R[X]<VAR>hf : f.Separable<VAR>hg : g.Separable<VAR>h : IsCoprime f g<GOAL>(f * g).Separable
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g : R[X]<VAR>hf : f.Separable<VAR>hg : g.Separable<VAR>h : IsCoprime f g<GOAL>IsCoprime (f * g) (derivative f * g + f * derivative g)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : Group H<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MulAction H β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>h : IsFundamentalDomain G s μ<VAR>g g' : G<GOAL>(fun g' => g * g' * g⁻¹) ((fun g' => g⁻¹ * g' * g) g') = g'
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : Group H<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MulAction H β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>h : IsFundamentalDomain G s μ<VAR>g g' : G<GOAL>(fun g' => g⁻¹ * g' * g) ((fun g' => g * g' * g⁻¹) g') = g'
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : Group H<VAR>inst✝⁷ : MulAction G α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MulAction H β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : NormedAddCommGroup E<VAR>s t : Set α<VAR>μ : Measure α<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MeasurableSMul G α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>h : IsFundamentalDomain G s μ<VAR>g g' : G<VAR>x : α<GOAL>(MulAction.toPerm g) ((fun x => { toFun := fun g' => g⁻¹ * g' * g, invFun := fun g' => g * g' * g⁻¹, left_inv := ⋯, right_inv := ⋯ } g' • x) x) = (fun x => g' • x) ((MulAction.toPerm g) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⨆ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⋂ i, ↑(f i) ↔ ∀ (i : ι), a ∈ f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>P.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i : ι<VAR>P Q : ChainComplex V ℕ<VAR>f : (i j : ℕ) → P.X i ⟶ Q.X j<GOAL>¬(ComplexShape.down ℕ).Rel 0 0
<VAR>a n✝ n : ℕ<GOAL>(2 * n + 1).bitIndices = 0 :: map (fun x => x + 1) n.bitIndices
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>s✝ t : Set Ω<VAR>S T : Set (Set Ω)<VAR>s : ι → Set Ω<GOAL>iIndepSets (fun i => {s i}) μ ↔ ∀ (t : Finset ι), μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i)
<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 : V<GOAL>o.oangle x x = 0
<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 : V<GOAL>↑(↑(‖x‖ ^ 2)).arg = 0
<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 : V<VAR>e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))<GOAL>(↑(‖x‖ ^ 2)).arg = 0
<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 : V<VAR>e_1✝ : Real.Angle = (ℝ ⧸ AddSubgroup.zmultiples (2 * π))<GOAL>0 ≤ ‖x‖ ^ 2
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y Z : C<VAR>P : Subobject Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : P.Factors g<GOAL>P.Factors (f ≫ g)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z✝ : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>P : MonoOver Z<VAR>h : Factors (Quotient.mk'' P) g<GOAL>Factors (Quotient.mk'' P) (f ≫ g)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n ~ l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate' n ~ l
<VAR>α β : GrpWithZero<VAR>e : ↑α ≃* ↑β<VAR>x✝ : (forget GrpWithZero).obj α<GOAL>(↑e ≫ ↑e.symm) x✝ = (𝟙 α) x✝
<VAR>α β : GrpWithZero<VAR>e : ↑α ≃* ↑β<VAR>x✝ : (forget GrpWithZero).obj β<GOAL>(↑e.symm ≫ ↑e) x✝ = (𝟙 β) x✝
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>p q : R[X]<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<GOAL>(p * p.mirror).natDegree = 2 * p.natDegree
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f✝ f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>N : Submodule R M<VAR>hfn : (map f N).FG<VAR>t : Finset P<VAR>ht : span R ↑t = map f N<GOAL>map f (span R ↑(t.preimage ⇑f ⋯)) = map f 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>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f✝ f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>N : Submodule R M<VAR>hfn : (map f N).FG<VAR>t : Finset P<VAR>ht : span R ↑t = map f N<GOAL>↑t ⊆ range ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f✝ f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>N : Submodule R M<VAR>hfn : (map f N).FG<VAR>t : Finset P<VAR>ht : span R ↑t = map f N<GOAL>map f N ≤ map f ⊤
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<GOAL>↑(padicNormE ↑q) = ↑(padicNorm p q)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>Submodule.span ℤ (eval {fun x => false} '' {nil}) = ⊤
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<GOAL>⊤ ≤ Submodule.span ℤ {eval {fun x => false} nil}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<GOAL>f ∈ Submodule.span ℤ {eval {fun x => false} nil}
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<GOAL>∃ a, a • eval {fun x => false} nil = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<GOAL>f default • eval {fun x => false} nil = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<GOAL>↑(f default) = f
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<VAR>x : ↑{fun x => false}<GOAL>↑(f default) x = f x
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>f : LocallyConstant ↑{fun x => false} ℤ<VAR>a✝ : f ∈ ⊤<GOAL>↑(f default) default = f default
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℂ → E<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℂ), f p
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℂ → E<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑Complex.polarCoord.symm p) = ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (measurableEquivRealProd.symm (↑polarCoord.symm p))
<VAR>a x z : ℂ<VAR>θ : ℝ<GOAL>(cos ↑θ + sin ↑θ * I).arg = toIocMod Real.two_pi_pos (-π) θ
<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>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : HasDerivAt f f' x<VAR>hf' : f' ≠ 0<VAR>z : 𝕜<GOAL>‖z‖ ≤ ‖f'‖⁻¹ * ‖(ContinuousLinearMap.smulRight 1 f') z‖
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hq : q.leadingCoeff = -1<VAR>hpq : p.degree < q.degree<GOAL>(p - q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hq : q.leadingCoeff = -1<VAR>hpq : p.degree < q.degree<VAR>this : (-q).coeff (-q).natDegree = 1<GOAL>(p - q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hq : q.leadingCoeff = -1<VAR>hpq : p.degree < q.degree<VAR>this : (-q).coeff (-q).natDegree = 1<GOAL>(p + -q).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Ring R<VAR>p✝ p q : R[X]<VAR>hq : q.leadingCoeff = -1<VAR>hpq : p.degree < q.degree<VAR>this : (-q).coeff (-q).natDegree = 1<GOAL>p.degree < (-q).degree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<GOAL>Measurable fun t => f (a, t) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<VAR>h : Measurable f := hf.measurable<GOAL>Measurable fun t => f (a, t) q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>a : α<VAR>q : ℚ<VAR>h : ∀ (a : ℚ), Measurable fun x => f x a<GOAL>Measurable fun t => f (a, t) q
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype p<VAR>k : Subtype pᶜ<GOAL>biproduct.ι (Subtype.restrict pᶜ f) k ≫ (biproduct.fromSubtype f pᶜ ≫ biproduct.toSubtype f p) ≫ biproduct.π (Subtype.restrict p f) j = biproduct.ι (Subtype.restrict pᶜ f) k ≫ 0 ≫ biproduct.π (Subtype.restrict p f) j
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype p<VAR>k : Subtype pᶜ<GOAL>(if h : p ↑k then biproduct.ι (Subtype.restrict p f) ⟨↑k, h⟩ else 0) ≫ biproduct.π (Subtype.restrict p f) j = 0
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>j : Subtype p<VAR>k : Subtype pᶜ<GOAL>0 ≫ biproduct.π (Subtype.restrict p f) j = 0
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>W' : C<VAR>g' : W' ⟶ ⨁ f<VAR>w : g' ≫ biproduct.toSubtype f p = 0<VAR>j : K<GOAL>((fun {W} g x => g ≫ biproduct.toSubtype f pᶜ) g' w ≫ biproduct.fromSubtype f pᶜ) ≫ biproduct.π f j = g' ≫ biproduct.π f j
<VAR>J : Type w<VAR>K✝ : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>K : Type<VAR>inst✝¹ : Finite K<VAR>inst✝ : HasFiniteBiproducts C<VAR>f : K → C<VAR>p : Set K<VAR>W' : C<VAR>g' : W' ⟶ ⨁ f<VAR>w : g' ≫ biproduct.toSubtype f p = 0<VAR>j : K<GOAL>(g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<VAR>h : a < 0<GOAL>(fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a : α<VAR>ha✝ : a ≠ 0<VAR>b c : α<VAR>ha : 0 < a<GOAL>(fun x => x * a) ⁻¹' [[b, c]] = [[b / a, c / a]]
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<GOAL>g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : 1 = (↑g).det<GOAL>g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1<GOAL>g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1<GOAL>↑g = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1<GOAL>!![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1<GOAL>!![↑g 0 0, ↑g 0 0 * ↑g 1 1 - 1; 1, ↑g 1 1] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 1<VAR>hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1<GOAL>!![↑g 0 0, ↑g 0 0 * ↑g 1 1 - 1; 1, ↑g 1 1] = !![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0, (1 * 0 + ↑g 0 0 * 1) * ↑g 1 1 + (1 * -1 + ↑g 0 0 * 0) * 1; (0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * ↑g 1 1 + (0 * -1 + 1 * 0) * 1]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hs_nonempty : s.Nonempty<VAR>hs_ne_univ : s ≠ univ<VAR>x y : β<GOAL>(piecewise s hs (const α x) (const α y)).range = {x, y}
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a⁻¹ < b⁻¹ ↔ b < a
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<GOAL>Submonoid.closure (Set.range cs.simple) = ⊤
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹<GOAL>Submonoid.closure (Set.range cs.simple) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>inst✝ : Nonempty ι<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<VAR>t : Set α<GOAL>t ∈ ⨅ i, l i ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι'✝ : Sort u_5<VAR>l✝ l' : Filter α<VAR>p✝ : ι✝ → Prop<VAR>s✝ : ι✝ → Set α<VAR>t✝ : Set α<VAR>i : ι✝<VAR>p' : ι'✝ → Prop<VAR>s' : ι'✝ → Set α<VAR>i' : ι'✝<VAR>ι : Type u_6<VAR>ι' : ι → Type u_7<VAR>inst✝ : Nonempty ι<VAR>l : ι → Filter α<VAR>s : (i : ι) → ι' i → Set α<VAR>p : (i : ι) → ι' i → Prop<VAR>hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)<VAR>h : Directed (fun x x_1 => x ≥ x_1) l<VAR>t : Set α<GOAL>(∃ i, t ∈ l i) ↔ ∃ a b, p ⟨a, b⟩.fst ⟨a, b⟩.snd ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq β<VAR>e : Perm α<VAR>f : α ↪ β<VAR>a : α<GOAL>(e.extendDomain f.toEquivRange) (f a) = f (e a)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : dist p₁ p₂ = dist p₁ p₃<GOAL>|(∡ p₁ p₂ p₃).toReal| < π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>|(∡ p₁ p₂ p₃).toReal| < π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>|(o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃))).toReal| < π / 2
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : Bornology.IsBounded E<GOAL>Bornology.IsBounded (Metric.cthickening δ E)
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : Bornology.IsBounded E<VAR>this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)<GOAL>Bornology.IsBounded (Metric.cthickening δ E)
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : Bornology.IsBounded E<VAR>this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)<GOAL>Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : InfClosed s<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<GOAL>t.sup' ht id ⊓ u.sup' hu id ∈ supClosure s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s : Set α<VAR>hs : InfClosed s<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s<VAR>u : Finset α<VAR>hu : u.Nonempty<VAR>hus : ↑u ⊆ s<GOAL>((t ×ˢ u).sup' ⋯ fun i => id i.1 ⊓ id i.2) ∈ supClosure s
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>¬a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b ≠ a + z • p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>b : B<VAR>m : M<VAR>hm : m ∈ p<GOAL>b • m ∈ p