ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>a b c✝ d x✝ y z : P<VAR>r R : ℝ<VAR>c x : P<GOAL>inversion c (dist x c) x = x
<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>a b c d x✝ y z : P<VAR>r R : ℝ<VAR>x : P<GOAL>inversion x (dist x x) x = x
<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>a b c✝ d x✝ y z : P<VAR>r R : ℝ<VAR>c x : P<VAR>hne : x ≠ c<GOAL>inversion c (dist x c) x = x
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<VAR>hu' : u ≠ 0<GOAL>p ≤ addOrderOf u • ‖u‖
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu : IsOfFinAddOrder u<VAR>hu' : u ≠ 0<VAR>n : ℕ<VAR>hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))<GOAL>p ≤ addOrderOf u • ‖u‖
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu' : u ≠ 0<VAR>n : ℕ<VAR>hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))<VAR>hu : ↑(addOrderOf u) ≠ 0<GOAL>p ≤ addOrderOf u • ‖u‖
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu' : u ≠ 0<VAR>n : ℕ<VAR>hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))<VAR>hu : ↑(addOrderOf u) ≠ 0<GOAL>p * 1 ≤ addOrderOf u • ‖u‖
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>hu' : u ≠ 0<VAR>n : ℕ<VAR>hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))<VAR>hu : ↑(addOrderOf u) ≠ 0<GOAL>n ≠ 0
<VAR>p : ℝ<VAR>hp : Fact (0 < p)<VAR>u : AddCircle p<VAR>n : ℕ<VAR>hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))<VAR>hu : ↑(addOrderOf u) ≠ 0<VAR>hu' : n = 0<GOAL>u = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<GOAL>span 0 = ⊥
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>h : Irreducible ϖ<VAR>n : ℕ<GOAL>(addVal R) (ϖ ^ n) = ↑n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<GOAL>∃ s, IsLinearOrder α s ∧ r ≤ s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>s : α → α → Prop<VAR>hs₁ : IsPartialOrder α s<VAR>rs : r ≤ s<VAR>hs₂ : ∀ z ∈ S, s ≤ z → z = s<GOAL>∃ s, IsLinearOrder α s ∧ r ≤ s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>s : α → α → Prop<VAR>hs₁ : IsPartialOrder α s<VAR>rs : r ≤ s<VAR>hs₂ : ∀ z ∈ S, s ≤ z → z = s<VAR>this : IsPartialOrder α s<GOAL>∃ s, IsLinearOrder α s ∧ r ≤ s
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>s : α → α → Prop<VAR>hs₁ : IsPartialOrder α s<VAR>rs : r ≤ s<VAR>hs₂ : ∀ z ∈ S, s ≤ z → z = s<VAR>this : IsPartialOrder α s<GOAL>∀ (a b : α), s a b ∨ s b a
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>s : α → α → Prop<VAR>hs₁ : IsPartialOrder α s<VAR>rs : r ≤ s<VAR>hs₂ : ∀ z ∈ S, s ≤ z → z = s<VAR>this : IsPartialOrder α s<VAR>x y : α<GOAL>s x y ∨ s y x
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝ : IsPartialOrder α r<VAR>S : Set (α → α → Prop) := {s | IsPartialOrder α s}<VAR>hS : ∀ c ⊆ S, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub<VAR>s : α → α → Prop<VAR>hs₁ : IsPartialOrder α s<VAR>rs : r ≤ s<VAR>hs₂ : ∀ z ∈ S, s ≤ z → z = s<VAR>this : IsPartialOrder α s<VAR>x y : α<VAR>h : ¬s x y ∧ ¬s y x<GOAL>False
<GOAL>HasSum (fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)) (π ^ 3 / 32)
<GOAL>(fun n => 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n => 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)
<GOAL>(-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! * Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) = π ^ 3 / 32
<GOAL>1 / 4 ∈ Icc 0 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>IsLeast {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖} ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>IsClosed {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ∏ i_1 : ι, ‖i i_1‖})
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : Codisjoint p p'<VAR>x : M<GOAL>∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>h : Codisjoint p p'<VAR>x : M<GOAL>x ∈ p ⊔ p'
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>K : Set Y<VAR>Kf : K ⊆ range f<GOAL>IsCompact (f ⁻¹' K) ↔ IsCompact K
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>(swap a b) b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s✝ : Sym α n<VAR>a b : α<VAR>s s' : Sym α n'<GOAL>↑(s.append s') = ↑((Sym.cast ⋯) (s'.append s))
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>b < c / a ↔ a * b < c
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>N : Type u_9<VAR>x₀ x : H<VAR>y₀ y : H'<VAR>ϕ : E →L[𝕜] E'<GOAL>inCoordinates E (TangentSpace I) E' (TangentSpace I') x₀ x y₀ y ϕ = ϕ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>N : Type u_9<VAR>x₀ x : H<VAR>y₀ y : H'<VAR>ϕ : E →L[𝕜] E'<GOAL>((tangentBundleCore I' H').coordChange ((tangentBundleCore I' H').indexAt y) ((tangentBundleCore I' H').indexAt y₀) y).comp (ϕ.comp ((tangentBundleCore I H).coordChange ((tangentBundleCore I H).indexAt x₀) ((tangentBundleCore I H).indexAt x) x)) = ϕ
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z p : P<GOAL>Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : E) in 𝓝 x, ‖f x_1 - f x - f' (x_1 - x)‖ ≤ c * ‖x_1 - x‖
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<GOAL>mgf X 0 t = 0
<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>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>hxf : x ∈ f.source<VAR>hxf' : x ∈ f'.source<GOAL>((f.extend I).symm ≫ f'.extend I).source ∈ 𝓝[range ↑I] ↑(f.extend I) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>hxf : x ∈ f.source<VAR>hxf' : x ∈ f'.source<GOAL>↑(f.extend I) x ∈ ((f.extend I).symm ≫ f'.extend I).source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>hxf : x ∈ f.source<VAR>hxf' : x ∈ f'.source<GOAL>↑(f.extend I) x ∈ ↑(f.extend I) '' (f.source ∩ f'.source)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R M'<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : StrongRankCondition R<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Free R M'<VAR>m n : Type v<VAR>inst✝¹ : Finite m<VAR>inst✝ : Finite n<GOAL>Module.rank R (Matrix m n R) = lift.{u, v} (#m * #n)
<VAR>p✝ : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p✝)<VAR>inst✝² : Fintype ι<VAR>p : ℝ≥0∞<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → PseudoMetricSpace (β i)<VAR>hp : p ≠ ⊤<VAR>x y : PiLp p β<GOAL>dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>m : MeasurableSpace α<VAR>T T' : Set α → F →L[ℝ] G''<VAR>hTT' : ∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x<VAR>f : α →ₛ F<GOAL>∑ x ∈ f.range, (T (↑f ⁻¹' {x})) x ≤ ∑ x ∈ f.range, (T' (↑f ⁻¹' {x})) x
<VAR>α : Type u_1<VAR>f : α → α<VAR>a : α<VAR>n i : ℕ<VAR>h : i < n<GOAL>(iterate f a n).get? i = some (f^[i] a)
<VAR>x y : ℝ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>rexp (log (x * y)) = rexp (log x + log y)
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>𝓝 = update pure 0 (⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ))
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<GOAL>pure 0 ≤ ⨅ γ, ⨅ (_ : γ ≠ 0), 𝓟 (Iio γ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>h'r : r < 1<GOAL>Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>h : Commute f g<VAR>μ : R<VAR>k : ℕ<GOAL>MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : Commute ((f - μ • 1) ^ k) g<GOAL>MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : Commute ((f - μ • 1) ^ k) g<VAR>x : M<VAR>hx : x ∈ ↑((f.genEigenspace μ) k)<GOAL>g x ∈ ↑((f.genEigenspace μ) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f g : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : Commute ((f - μ • 1) ^ k) g<VAR>x : M<VAR>hx : ((f - μ • 1) ^ k) x = 0<GOAL>((f - μ • 1) ^ k) (g x) = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<GOAL>f x = 1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<VAR>cont : ContinuousAt f x<GOAL>f x = 1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<VAR>cont : ContinuousAt f x<VAR>clo : x ∈ closure (c '' {0}ᶜ)<GOAL>f x = 1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<VAR>cont : ContinuousAt f x<VAR>clo : x ∈ closure (c '' {0}ᶜ)<VAR>fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))<GOAL>f x = 1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this✝ : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<VAR>cont : ContinuousAt f x<VAR>clo : x ∈ closure (c '' {0}ᶜ)<VAR>fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))<VAR>this : f '' (c '' {0}ᶜ) ⊆ {1}<GOAL>f x = 1
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : UniformSpace K<VAR>inst✝² : TopologicalDivisionRing K<VAR>inst✝¹ : CompletableTopField K<VAR>inst✝ : UniformAddGroup K<VAR>x : hat K<VAR>x_ne : x ≠ 0<VAR>this✝ : T1Space (hat K)<VAR>f : hat K → hat K := fun x => x * x.hatInv<VAR>c : K → hat K := fun x => ↑K x<VAR>cont : ContinuousAt f x<VAR>clo : x ∈ closure (c '' {0}ᶜ)<VAR>this : f '' (c '' {0}ᶜ) ⊆ {1}<VAR>fxclo : f x ∈ closure {1}<GOAL>f x = 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>x : G'<GOAL>(∫ (a : α) in s, ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 ht hμt 1)) a ∂μ) • x = (μ (t ∩ s)).toReal • x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>s : Set M<GOAL>span R (-s) = -span R s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>s : Set M<GOAL>span R (-s) ≤ -span R s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>s : Set M<GOAL>-span R s ≤ span R (-s)
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<VAR>h' : ∀ x ∈ [[a, b]], x ≠ 0<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h : 0 ∉ [[a, b]]<VAR>h' : ∀ x ∈ [[a, b]], x ≠ 0<VAR>heq : ∀ x ∈ [[a, b]], x * x⁻¹ = 1<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>α : Type u_1<VAR>l : List α<GOAL>powersetCardAux 0 l = [0]
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝ y✝ z : X<VAR>r✝ s : ℝ<VAR>x y : X<VAR>r : ℝ<VAR>h : y ∈ ball x r<VAR>a : X<GOAL>a ∈ ball x r ↔ a ∈ ball y r
<VAR>X : Type u_1<VAR>inst✝¹ : PseudoMetricSpace X<VAR>inst✝ : IsUltrametricDist X<VAR>x✝ y✝ z : X<VAR>r✝ s : ℝ<VAR>x y : X<VAR>r : ℝ<VAR>a : X<VAR>h : dist y x < r<GOAL>dist a x < r ↔ dist a y < r
<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>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra T S<GOAL>rootSet 0 S = ∅
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>x = midpoint R x y ↔ x = y
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>X : C<VAR>inst✝ : ArtinianObject X<VAR>h : ¬IsZero X<GOAL>∃ Y, Simple (underlying.obj Y)