ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = -L.prod<VAR>hhd : hd ∈ s<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Set R<VAR>C : R → Prop<VAR>h1 : C 1<VAR>hneg1 : C (-1)<VAR>hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)<VAR>ha : ∀ {x y : R}, C x → C y → C (x + y)<VAR>h0 : C 0<VAR>hd : R<VAR>tl : List R<VAR>ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)<VAR>HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1<VAR>L : List R<VAR>HL' : ∀ x ∈ L, x ∈ s<VAR>HP : tl.prod = -L.prod<VAR>hhd : hd = -1<GOAL>∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
<VAR>R : Type u_1<VAR>inst✝¹ : MonoidWithZero R<VAR>inst✝ : Nontrivial R<VAR>hm : Squarefree 0<GOAL>False
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<VAR>a : α<VAR>nth_partNum_eq : g.partNums.get? n = some a<GOAL>∃ gp, g.s.get? n = some gp ∧ gp.a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : Field K<VAR>R₁ : Type u_4<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : IsDomain R₁<VAR>inst✝⁴ : Algebra R₁ K<VAR>inst✝³ : IsFractionRing R₁ K<VAR>I✝ J : FractionalIdeal R₁⁰ K<VAR>K' : Type u_5<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R₁ K'<VAR>inst✝ : IsFractionRing R₁ K'<VAR>I : FractionalIdeal R₁⁰ K<VAR>h : K ≃ₐ[R₁] K'<GOAL>map (↑h) I⁻¹ = (map (↑h) I)⁻¹
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝¹ : CompleteLinearOrder γ<VAR>inst✝ : DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ liminf f (𝓝 x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f✝ : X → Y<VAR>s : Set X<VAR>hs : IsLocallyClosed s<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsLocallyClosed (range f)<GOAL>IsLocallyClosed (f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f✝ f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsLocallyClosed (range f)<VAR>t : Set Y<VAR>ht : IsLocallyClosed t<VAR>hs : IsLocallyClosed (f ⁻¹' t)<GOAL>IsLocallyClosed (f '' (f ⁻¹' t))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f✝ f : X → Y<VAR>hf : Inducing f<VAR>hf' : IsLocallyClosed (range f)<VAR>t : Set Y<VAR>ht : IsLocallyClosed t<VAR>hs : IsLocallyClosed (f ⁻¹' t)<GOAL>IsLocallyClosed (t ∩ range f)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>o.card = 1 ↔ o = 1
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Ico b c = Ico (b + a) (c + a)
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>dist a c ≤ dist a b + dist b c
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤ (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>a b c : ℍ<GOAL>0 < dist (↑b) ((starRingEnd ℂ) ↑b)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ s ⊔ t<GOAL>∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ closure (↑s ∪ ↑t)<GOAL>∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ closure (↑s ∪ ↑t)<GOAL>∀ x ∈ ↑s ∪ ↑t, ∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ closure (↑s ∪ ↑t)<GOAL>∃ y ∈ s, ∃ z ∈ t, y * z = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ closure (↑s ∪ ↑t)<GOAL>∀ (x y : C), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → (∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y) → ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = x * y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<VAR>h : x ∈ closure (↑s ∪ ↑t)<GOAL>∀ (x : C), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>y : C<VAR>hy : y ∈ s<VAR>z : C<VAR>hz : z ∈ t<GOAL>y * z ∈ s ⊔ t
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>inst✝ : ∀ (i : ι), CompleteSpace ↥(F i)<VAR>hFortho : OrthogonalFamily 𝕜 (fun i => ↥(F i)) fun i => (F i).subtypeₗᵢ<VAR>hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure<GOAL>⊤ ≤ (⨆ i, LinearMap.range (F i).subtypeₗᵢ.toLinearMap).topologicalClosure
<VAR>X : Type ?u.719<VAR>Y : ?m.713<VAR>A : Type ?u.722<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace A<VAR>X₁ : Type u_1<VAR>X₂ : Type u_2<VAR>Y₁ : Sort u_3<VAR>Y₂ : Sort u_4<VAR>Z₁ : Type u_5<VAR>Z₂ : Type u_6<VAR>inst✝³ : TopologicalSpace X₁<VAR>inst✝² : TopologicalSpace X₂<VAR>inst✝¹ : TopologicalSpace Z₁<VAR>inst✝ : TopologicalSpace Z₂<VAR>f₁ : X₁ → Y₁<VAR>g₁ : Z₁ → Y₁<VAR>f₂ : X₂ → Y₂<VAR>g₂ : Z₂ → Y₂<VAR>mapX : X₁ → X₂<VAR>contX : Continuous mapX<VAR>mapY : Y₁ → Y₂<VAR>mapZ : Z₁ → Z₂<VAR>contZ : Continuous mapZ<VAR>commX : f₂ ∘ mapX = mapY ∘ f₁<VAR>commZ : g₂ ∘ mapZ = mapY ∘ g₁<GOAL>Continuous (Function.mapPullback mapX mapY mapZ commX commZ)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α✝<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁶ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝⁵ : TopologicalSpace β✝<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : TopologicalSpace δ<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>p : α → Prop<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>ContinuousOn (fun a => if p a then f a else g a) s
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α✝<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁶ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝⁵ : TopologicalSpace β✝<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : TopologicalSpace δ<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>p : α → Prop<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α✝<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁶ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝⁵ : TopologicalSpace β✝<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : TopologicalSpace δ<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>p : α → Prop<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α✝<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁶ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝⁵ : TopologicalSpace β✝<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : TopologicalSpace δ<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>p : α → Prop<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>ContinuousOn f (s ∩ {a | p a})
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : TopologicalSpace α✝<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁶ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝⁵ : TopologicalSpace β✝<VAR>inst✝⁴ : TopologicalSpace γ<VAR>inst✝³ : TopologicalSpace δ<VAR>α : Type u_7<VAR>β : Type u_8<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>p : α → Prop<VAR>inst✝ : (a : α) → Decidable (p a)<VAR>s : Set α<VAR>f g : α → β<VAR>hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a<VAR>hf : ContinuousOn f (s ∩ closure {a | p a})<VAR>hg : ContinuousOn g (s ∩ closure {a | ¬p a})<GOAL>ContinuousOn g (s ∩ {a | ¬p a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Icc a b = Icc (e a) (e b)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>g : G<VAR>hg : g ∈ s<VAR>n : G<GOAL>n ∈ s ↔ g * n * g⁻¹ ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : r ≠ 0<VAR>a : ℝ<VAR>ha : a ∈ Ioo (-1) 1<VAR>hp : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : r ≠ 0<VAR>a : ℝ<VAR>ha : a ∈ Ioo (-1) 1<VAR>hp : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x<VAR>this : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : r ≠ 0<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>a : ℝ<VAR>ha : a ∈ Ioo 0 1<VAR>C : ℝ<VAR>hC : C > 0<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this✝ : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<VAR>this : ↑r < ↑r / ↑a<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this✝ : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<VAR>this : r < r / a<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this✝ : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<VAR>this : ↑r < ↑(r / a)<GOAL>↑r < p.radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this✝ : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<VAR>this : ↑r < ↑(r / a)<VAR>n : ℕ<GOAL>‖p n‖ * ↑(r / a) ^ n ≤ C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0<VAR>h₀ : 0 < ↑r<VAR>a✝ : ℝ<VAR>ha✝ : a✝ ∈ Ioo (-1) 1<VAR>hp✝ : (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a✝ ^ x<VAR>this✝ : (∃ a ∈ Ioo (-1) 1, (fun n => ‖p n‖ * ↑r ^ n) =O[atTop] fun x => a ^ x) ↔ ∃ a ∈ Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n<VAR>C : ℝ<VAR>hC : C > 0<VAR>a : ℝ≥0<VAR>ha : ↑a ∈ Ioo 0 1<VAR>hp : ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * ↑a ^ n<VAR>this : ↑r < ↑(r / a)<VAR>n : ℕ<GOAL>‖p n‖ * ↑r ^ n ≤ C * ↑a ^ n
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>p : ι →₀ R<VAR>n : N<VAR>i : ι<GOAL>((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = (p.sum fun i m => Finsupp.single i (m • n)) i
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<GOAL>Integrable f μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover μ l fun i => Ioc (a i) (b i)<GOAL>Integrable f μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover μ l fun i => Ioc (a i) (b i)<GOAL>∀ᶠ (x : ι) in l, ∫ (x : ℝ) in a x..b x, ‖f x‖ ∂μ ≤ I → ∫ (x : ℝ) in Ioc (a x) (b x), ‖f x‖ ∂μ ≤ I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : Measure ℝ<VAR>l : Filter ι<VAR>inst✝² : l.NeBot<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) μ<VAR>ha : Tendsto a l atBot<VAR>hb : Tendsto b l atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<VAR>hφ : AECover μ l fun i => Ioc (a i) (b i)<VAR>i : ι<VAR>hai : a i ≤ 0<VAR>hbi : 0 ≤ b i<VAR>ht : ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<GOAL>∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂μ ≤ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>ι' : Type u_8<VAR>μ : ι → ι' → Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sum fun n => sum (μ n)) s = (sum fun p => μ p.1 p.2) s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (f '' s) volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>(Measure.comap f (volume.withDensity fun x => ENNReal.ofReal (g x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s✝ : Set E<VAR>f✝ : E → E<VAR>f'✝ : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f : ℝ → ℝ<VAR>hf : MeasurableEmbedding f<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<VAR>g : ℝ → ℝ<VAR>hg : ∀ᵐ (x : ℝ), x ∈ f '' s → 0 ≤ g x<VAR>hg_int : IntegrableOn g (f '' s) volume<VAR>f' : ℝ → ℝ<VAR>hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
<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<GOAL>sᶜ ∈ cocompact X ↔ ∃ t, IsCompact t ∧ s ⊆ t
<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<GOAL>(∃ t, IsCompact t ∧ tᶜ ⊆ sᶜ) ↔ ∃ t, IsCompact t ∧ s ⊆ t
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>p : Submodule R L<GOAL>(lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>p : Submodule R L<GOAL>(lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
<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 y : V<GOAL>x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0