ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>f : G →* N<VAR>s : Set N<VAR>x : G<VAR>hx : x ∈ ⇑f ⁻¹' s<GOAL>f x ∈ closure s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<GOAL>ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), f i x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>H : Type u_3<VAR>inst✝¹¹ : TopologicalSpace H<VAR>E : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>I : ModelWithCorners 𝕜 E H<VAR>G : Type u_5<VAR>inst✝⁸ : CommMonoid G<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : ChartedSpace H G<VAR>inst✝⁵ : SmoothMul I G<VAR>E' : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_7<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_8<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H' M<VAR>s : Set M<VAR>x x₀ : M<VAR>t : Finset ι<VAR>f : ι → M → G<VAR>n : ℕ∞<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → ContMDiff I' I n (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<GOAL>ContMDiff I' I n fun x => ∏ᶠ (j : Subtype p), f (↑j) x
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : (i : I) → C i ⥤ D<VAR>i : I<VAR>X : C i<GOAL>{ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (𝟙 ⟨i, X⟩) = 𝟙 ({ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.obj ⟨i, X⟩)
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : (i : I) → C i ⥤ D<VAR>i : I<VAR>X Y✝¹ : C i<VAR>f : X ⟶ Y✝¹<VAR>Y✝ : C i<VAR>g : Y✝¹ ⟶ Y✝<GOAL>{ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f ≫ SigmaHom.mk g) = { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f) ≫ { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk g)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>x✝ y✝ z✝ : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x : α<VAR>y : β<VAR>r : ℝ≥0∞<VAR>z : α × β<GOAL>z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<GOAL>∠ p2 p3 p1 = 0
<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>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p3 p2 p1 = π<GOAL>∠ p2 p3 p1 = 0
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x✝ : V₁<GOAL>‖0 x✝‖ = 0 * ‖x✝‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>x✝ : V₁<GOAL>‖0 x✝‖ = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<VAR>h✝ : a ∈ s<GOAL>r a • f a = r a • f a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulZeroClass R M<VAR>s : Set α<VAR>r : α → R<VAR>f : α → M<VAR>a : α<VAR>h✝ : a ∉ s<GOAL>0 = r a • 0
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>u : α<VAR>h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ<VAR>p : α → Prop<GOAL>Liftp p x → p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>u : α<VAR>h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ<VAR>p : α → Prop<GOAL>(∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>u : α<VAR>h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ<VAR>p : α → Prop<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : x = abs ⟨a, f⟩<VAR>h' : ∀ (i : (P F).B a), p (f i)<GOAL>p u
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>u : α<VAR>h : ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ<VAR>p : α → Prop<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : x = abs ⟨a, f⟩<VAR>h' : ∀ (i : (P F).B a), p (f i)<VAR>i : (P F).B a<VAR>left✝ : i ∈ univ<VAR>hi : f i = u<GOAL>p u
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>n : ℕ<VAR>hn : upperCentralSeries G n = ⊤<GOAL>Group.IsNilpotent G'
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>n : ℕ<VAR>hn : upperCentralSeries G n = ⊤<GOAL>upperCentralSeries G' n = ⊤
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>G' : Type u_2<VAR>inst✝ : Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>n : ℕ<VAR>hn : upperCentralSeries G n = ⊤<GOAL>⊤ ≤ upperCentralSeries G' n
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length / 2 ≤ count b l
<VAR>l : List Bool<VAR>hl : Chain' (fun x x_1 => x ≠ x_1) l<VAR>b : Bool<GOAL>l.length - (2 - 1) ≤ 2 * count b l
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Preadditive C<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>M : Mat R<VAR>i j : ↑M<VAR>h : i ≠ j<GOAL>𝟙 M i j = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>Y - W.negPolynomial = W.polynomialY
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : NonUnitalNormedRing A<VAR>inst✝² : NormedSpace 𝕜 A<VAR>inst✝¹ : IsScalarTower 𝕜 A A<VAR>inst✝ : SMulCommClass 𝕜 A A<VAR>x : A<GOAL>‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖₊ = ‖x‖₊
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<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✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>s t : Submodule R M<GOAL>Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥s + Module.rank R ↥t
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M₁<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✝² : Module R M₃<VAR>inst✝¹ : Module R M'<VAR>inst✝ : HasRankNullity.{u, u_1} R<VAR>s t : Submodule R M<GOAL>Module.rank R ↥(s ⊔ t) ≤ Module.rank R ↥(s ⊔ t) + Module.rank R ↥(s ⊓ t)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>p : Fin n → R[X]<VAR>h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i<VAR>h_monic : ∀ (i : Fin n), (p i).Monic<GOAL>(vandermonde v).det = (of fun i j => eval (v i) (p j)).det
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x : P<GOAL>(intrinsicClosure 𝕜 s).Nonempty → s.Nonempty
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>s t : Set P<VAR>x : P<GOAL>intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : Ring 𝕜<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module 𝕜 V<VAR>inst✝¹ : TopologicalSpace P<VAR>inst✝ : AddTorsor V P<VAR>t : Set P<VAR>x : P<VAR>h : intrinsicClosure 𝕜 ∅ ≠ ∅<GOAL>False
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f : ℝ → α<GOAL>Tendsto (fun x => f (rexp x)) atTop l ↔ Tendsto f atTop l
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU : U ∈ p.basisSets<GOAL>∃ V ∈ p.basisSets, V + V ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>∃ V ∈ p.basisSets, V + V ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>(s.sup p).ball 0 (r / 2) ∈ p.basisSets ∧ (s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>(s.sup p).ball 0 (r / 2) + (s.sup p).ball 0 (r / 2) ⊆ U
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p : SeminormFamily 𝕜 E ι<VAR>U : Set E<VAR>hU✝ : U ∈ p.basisSets<VAR>s : Finset ι<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hU : U = (s.sup p).ball 0 r<GOAL>(s.sup p).ball (0 + 0) (r / 2 + r / 2) ⊆ U
<VAR>α : Type u_1<VAR>inst✝⁵ : Mul α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass α α (Function.swap HMul.hMul) LE.le<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>↑(Icc a b * Icc c d) ⊆ ↑(Icc (a * c) (b * d))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : 0 < b<GOAL>a * b⁻¹ ≤ c ↔ a ≤ c * b
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>StrictAnti fun p => ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>StrictAnti (∑ c : α, fun p => a c * b c ^ p)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ x ∈ univ, StrictAnti fun p => a x * b x ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>StrictAnti (HPow.hPow (b i))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x : E<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : 1 ≤ t<GOAL>x ∈ t • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>h : Convex 𝕜 s<VAR>x : E<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : 1 ≤ t<GOAL>t⁻¹ • x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>T : Set (Set X)<VAR>T_count : T.Countable<VAR>T_open : ∀ u ∈ T, IsOpen u<VAR>sT : s ⊆ ⋃ u ∈ T, u<VAR>hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>T : Set (Set X)<VAR>T_count : T.Countable<VAR>T_open : ∀ u ∈ T, IsOpen u<VAR>sT : s ⊆ ⋃ u ∈ T, u<VAR>hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ<VAR>T' : Set (Set X) := insert ∅ T<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>T : Set (Set X)<VAR>T_count : T.Countable<VAR>T_open : ∀ u ∈ T, IsOpen u<VAR>sT : s ⊆ ⋃ u ∈ T, u<VAR>hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ<VAR>T' : Set (Set X) := insert ∅ T<VAR>T'_count : T'.Countable<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>T : Set (Set X)<VAR>T_count : T.Countable<VAR>T_open : ∀ u ∈ T, IsOpen u<VAR>sT : s ⊆ ⋃ u ∈ T, u<VAR>hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ<VAR>T' : Set (Set X) := insert ∅ T<VAR>T'_count : T'.Countable<VAR>T'_ne : T'.Nonempty<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : SecondCountableTopology X<VAR>hf : LocallyIntegrableOn f s μ<VAR>T : Set (Set X)<VAR>T_count : T.Countable<VAR>T_open : ∀ u ∈ T, IsOpen u<VAR>sT : s ⊆ ⋃ u ∈ T, u<VAR>hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ<VAR>T' : Set (Set X) := insert ∅ T<VAR>T'_count : T'.Countable<VAR>T'_ne : T'.Nonempty<VAR>u : ℕ → Set X<VAR>hu : T' = range u<GOAL>∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ
<VAR>K : Type u<VAR>inst✝ : CommRing K<VAR>P : Sort v<VAR>x : RatFunc K<VAR>f : K[X] → K[X] → P<VAR>H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → q' * p = q * p' → f p q = f p' q'<VAR>p p' : K[X]<VAR>q q' : ↥K[X]⁰<VAR>h : (Localization.r K[X]⁰) (p, q) (p', q')<GOAL>(fun p q => f p ↑q) p q = (fun p q => f p ↑q) p' q'
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>ThreeAPFree (sphere x r)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x : E<GOAL>ThreeAPFree (sphere x 0)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : StrictConvexSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>ThreeAPFree (sphere x r)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<GOAL>(eval₂RingHom (C.comp (Quotient.mk I)) X) a = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<GOAL>(eval₂RingHom (C.comp (Quotient.mk I)) X) (a.sum fun n a => (monomial n) a) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<GOAL>eval₂ (C.comp (Quotient.mk I)) X (a.sum fun n a => (monomial n) a) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<GOAL>(a.sum fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<VAR>n : ℕ<VAR>x✝ : n ∈ a.support<GOAL>(fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) n (a.coeff n) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<VAR>n : ℕ<VAR>x✝ : n ∈ a.support<GOAL>eval₂ (C.comp (Quotient.mk I)) X ((monomial n) (a.coeff n)) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<VAR>n : ℕ<VAR>x✝ : n ∈ a.support<GOAL>(C.comp (Quotient.mk I)) (a.coeff n) * X ^ n = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<VAR>n : ℕ<VAR>x✝ : n ∈ a.support<VAR>m : ℕ<GOAL>((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a : R[X]<VAR>ha : a ∈ map C I<VAR>n : ℕ<VAR>x✝ : n ∈ a.support<VAR>m : ℕ<GOAL>(if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Finset α<GOAL>a ∈ stabilizer G ↑s ↔ ∀ ⦃b : α⦄, b ∈ ↑s → a • b ∈ ↑s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<GOAL>spectrum R (cfc f a) = f '' spectrum R a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : List Γ<VAR>i j : ℕ<VAR>h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length<GOAL>BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : List Γ<VAR>i j : ℕ<VAR>h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length<GOAL>l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l : List Γ<VAR>i j : ℕ<VAR>h : i ≤ j<GOAL>l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f f' : α → E<VAR>s : Set α<VAR>h : EqOn f f' s<VAR>x : α<VAR>xs : x ∈ s<GOAL>edist (f x) (f' x) = 0
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.all p = true ↔ ∀ (c : Char), c ∈ s.data → p c = true
<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>o.oangle (-x) y = o.oangle x (-y)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<VAR>i : ι<VAR>a b : π i<GOAL>update x i a ≤ update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>j : F<VAR>inst✝ : DecidableEq F<VAR>h2 : 2 = 0<GOAL>ofJ 1728 = ofJ0 F
<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>a / b < c / d ↔ a * d < c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : α<VAR>hx : x ∈ minimals (fun x x_1 => x ≤ x_1) s<GOAL>↑(f ⟨x, ⋯⟩) ∈ minimals (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : α<VAR>hx✝ : x ∈ minimals (fun x x_1 => x ≤ x_1) s<VAR>hx : x ∈ Subtype.val '' minimals (fun x x_1 => x ≤ x_1) univ<GOAL>↑(f ⟨x, ⋯⟩) ∈ minimals (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : { x // x ∈ s }<VAR>h : x ∈ minimals (fun x x_1 => x ≤ x_1) univ<VAR>hx : ↑x ∈ minimals (fun x x_1 => x ≤ x_1) s<GOAL>↑(f ⟨↑x, ⋯⟩) ∈ minimals (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝¹ t✝ : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : { x // x ∈ s }<VAR>h : x ∈ minimals (fun x x_1 => x ≤ x_1) univ<VAR>hx : ↑x ∈ minimals (fun x x_1 => x ≤ x_1) s<GOAL>t = Subtype.val ∘ ⇑f '' univ