ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<GOAL>𝓝[↑(extChartAt I x).symm ⁻¹' insert x s ∩ range ↑I] ↑(extChartAt I x) x = 𝓝[insert (↑(extChartAt I x) x) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)] ↑(extChartAt I x) x
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(lineMap a b) r ≤ (lineMap a b) r' ↔ a ≤ b
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : LinearOrderedField k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a b : E<VAR>r r' : k<VAR>h : r < r'<GOAL>(1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<GOAL>((resolution k G).d 1 0 ≫ ε k G).hom = Action.Hom.hom 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<VAR>x : ↑((resolution k G).X 1).V<GOAL>((resolution k G).d 1 0 ≫ ε k G).hom x = (Action.Hom.hom 0) x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Monoid G<VAR>x : ↑((resolution k G).X 1).V<VAR>this : (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0<GOAL>((resolution k G).d 1 0 ≫ ε k G).hom x = (Action.Hom.hom 0) x
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>h : M.E ⊆ M.closure I<GOAL>M.Base I
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>h : M.E ⊆ M.closure I<GOAL>M.Basis I M.E
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b x : α<GOAL>x ∈ Ico a b ↔ a ≤ x ∧ x < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>x : α × α<GOAL>(↑s ∩ ↑t).offDiag = (↑s).offDiag ∩ (↑t).offDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>g : β → γ<GOAL>range (g ∘ f) ⊆ range g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>g : β → γ<GOAL>g '' range f ⊆ range g
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hxz : x ≠ z<GOAL>swap y z * swap x y * swap y z = swap z x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hxz : x ≠ z<GOAL>swap y z * swap x y * (swap y z)⁻¹ = swap z x
<VAR>m n✝ n : ℕ<GOAL>n.div2 = n / 2
<VAR>m n✝ n : ℕ<GOAL>n % 2 + 2 * n.div2 = n
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>addHaarMeasure (piIcc01 ι) = volume
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<GOAL>addHaarMeasure (piIcc01 ι) = volume ↑(piIcc01 ι) • addHaarMeasure (piIcc01 ι)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : ℕ → Set α<VAR>t : ℕ → Set β<GOAL>⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = (⋃ n, s n) ×ˢ ⋃ n, t n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : ℕ → Set α<VAR>t : ℕ → Set β<GOAL>⋃ n, s (unpair n).1 ×ˢ t (unpair n).2 = ⋃ x, s x.1 ×ˢ t x.2
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>inst✝³ : Category.{u_9, u_1} C₁<VAR>inst✝² : Category.{u_8, u_2} C₂<VAR>inst✝¹ : Category.{u_7, u_3} C₃<VAR>F : C₁ ⥤ C₂ ⥤ C₃<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X : GradedObject I C₁<VAR>Y : GradedObject J C₂<VAR>A : C₃<VAR>k : K<VAR>inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>f g : mapBifunctorMapObj F p X Y k ⟶ A<VAR>h : ∀ (i : I) (j : J) (hij : p (i, j) = k), ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g<GOAL>f = g
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>inst✝³ : Category.{u_9, u_1} C₁<VAR>inst✝² : Category.{u_8, u_2} C₂<VAR>inst✝¹ : Category.{u_7, u_3} C₃<VAR>F : C₁ ⥤ C₂ ⥤ C₃<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X : GradedObject I C₁<VAR>Y : GradedObject J C₂<VAR>A : C₃<VAR>k : K<VAR>inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>f g : mapBifunctorMapObj F p X Y k ⟶ A<VAR>h : ∀ (i : I) (j : J) (hij : p (i, j) = k), ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g<GOAL>∀ (i : I × J) (hij : p i = k), (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ f = (((mapBifunctor F I J).obj X).obj Y).ιMapObj p i k hij ≫ g
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>h : x ≠ y<VAR>z : α<VAR>hx : z = x<GOAL>z ∈ (swap x y).support ↔ z ∈ {x, y}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y : α<VAR>h : x ≠ y<VAR>z : α<VAR>hx : ¬z = x<GOAL>z ∈ (swap x y).support ↔ z ∈ {x, y}
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<GOAL>oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<GOAL>oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<VAR>h2 : -I * (I * ↑(1 / x)) = 1 / ↑x<GOAL>oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<VAR>h2 : -I * (I * ↑(1 / x)) = 1 / ↑x<VAR>h3 : ↑x ^ (3 / 2) ≠ 0<GOAL>oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<VAR>h2 : -I * (I * ↑(1 / x)) = 1 / ↑x<VAR>h3 : ↑x ^ (3 / 2) ≠ 0<VAR>h4 : (↑x).arg ≠ π<GOAL>oddKernel (↑a) x = 1 / x ^ (3 / 2) * sinKernel (↑a) (1 / x)
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<VAR>h2 : -I * (I * ↑(1 / x)) = 1 / ↑x<VAR>h3 : ↑x ^ (3 / 2) ≠ 0<VAR>h4 : (↑x).arg ≠ π<GOAL>jacobiTheta₂'' (↑a) (I * ↑x) = ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * jacobiTheta₂'' (↑a) (I * ↑x) / (-2 * ↑π))
<VAR>x : ℝ<VAR>hx : 0 < x<VAR>a : ℝ<VAR>h1 : -1 / (I * ↑(1 / x)) = I * ↑x<VAR>h2 : -I * (I * ↑(1 / x)) = 1 / ↑x<VAR>h3 : ↑x ^ (3 / 2) ≠ 0<VAR>h4 : (↑x).arg ≠ π<VAR>J : ℂ<GOAL>J = ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * J / (-2 * ↑π))
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹⁰ : OrderedSemiring 𝕜<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : AddCommMonoid F<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module 𝕜 F<VAR>s : Set E<VAR>inst✝³ : Semiring 𝕝<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : Module 𝕝 F<VAR>inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕝] F<VAR>hf : IsOpenMap ⇑f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : f x ≠ f y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ interior (⇑f '' s)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝¹⁰ : OrderedSemiring 𝕜<VAR>inst✝⁹ : TopologicalSpace E<VAR>inst✝⁸ : TopologicalSpace F<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : AddCommMonoid F<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module 𝕜 F<VAR>s : Set E<VAR>inst✝³ : Semiring 𝕝<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : Module 𝕝 F<VAR>inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝<VAR>hs : StrictConvex 𝕜 s<VAR>f : E →ₗ[𝕝] F<VAR>hf : IsOpenMap ⇑f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : f x ≠ f y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) = a • f x + b • f y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<GOAL>x ≠ y → (fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) x y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<GOAL>(¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) → x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<VAR>hyp : ¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<VAR>hyp : ¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v<GOAL>x ∈ connectedComponent y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<VAR>hyp : ¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v<GOAL>∀ (i : { s // IsClopen s ∧ y ∈ s }), x ∈ ↑i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<VAR>hyp : ¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v<VAR>w : Set X<VAR>hw : IsClopen w<VAR>hy : y ∈ w<GOAL>x ∈ ↑⟨w, ⋯⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>h : TotallyDisconnectedSpace X<VAR>x : X<VAR>x✝¹ : x ∈ univ<VAR>y : X<VAR>x✝ : y ∈ univ<VAR>hyp : ¬∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v<VAR>w : Set X<VAR>hw : IsClopen w<VAR>hy : y ∈ w<VAR>hx : x ∉ ↑⟨w, ⋯⟩<GOAL>False
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<VAR>hr : ¬r = 0<GOAL>(x * (single b) r).coeff (a + b) = x.coeff a * r
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝¹ : OrderedCancelAddCommMonoid Γ<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<VAR>hr : ¬r = 0<GOAL>∑ x_1 ∈ addAntidiagonal ⋯ ⋯ (a + b), x.coeff x_1.1 * ((single b) r).coeff x_1.2 = x.coeff a * r
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>seminormFromBounded' f x = f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>⨆ y, f x * (f y / f y) = f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>⨆ y, f x * (f y / f y) ≤ f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>f x ≤ ⨆ y, f x * (f y / f y)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<GOAL>(fun s => s.sum fun x e => e) = fun m => Multiset.card (toMultiset m)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>(m.sum fun x e => e) = Multiset.card (toMultiset m)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n ≠ 0<VAR>ha : 1 < a<GOAL>1 < a ^ n
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j : ι<VAR>r : c.Rel i j<GOAL>(C.xPrevIso r).inv ≫ C.dTo j = C.d i j
<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>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f✝ g : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Zero β<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t<GOAL>∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
<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>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f✝ g : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Zero β<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>f_nn : ∀ᵐ (t : α) ∂μ, 0 ≤ f t<VAR>G : α → β<VAR>hG_meas : Measurable G<VAR>hG_mem : range G ⊆ Preorder.toLE.1 0<VAR>hG_ae_eq : f =ᶠ[ae μ] G<GOAL>∃ g, Measurable g ∧ 0 ≤ g ∧ f =ᶠ[ae μ] g
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<GOAL>∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<VAR>a : Solution₁ d<VAR>H : 1 < a.x ∧ 0 < a.y ∧ ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n<GOAL>a = a₁
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<VAR>a : Solution₁ d<VAR>Hx : 1 < a.x<VAR>Hy : 0 < a.y<VAR>H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n<VAR>n₁ : ℤ<VAR>hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁<GOAL>a = a₁
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a₁ : Solution₁ d<VAR>ha₁ : IsFundamental a₁<VAR>a : Solution₁ d<VAR>Hx : 1 < a.x<VAR>Hy : 0 < a.y<VAR>H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n<VAR>n₁ : ℤ<VAR>hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁<VAR>n₂ : ℤ<VAR>hn₂ : a = a₁ ^ n₂ ∨ a = -a₁ ^ n₂<GOAL>a = a₁
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>c : Set (Set α)<VAR>H1 : ∀ s ∈ c, x ∈ s<VAR>H2 : ∀ s ∈ c, IsPreconnected s<GOAL>IsPreconnected (⋃₀ c)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>c : Set (Set α)<VAR>H1 : ∀ s ∈ c, x ∈ s<VAR>H2 : ∀ s ∈ c, IsPreconnected s<GOAL>∀ y ∈ ⋃₀ c, ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v : Set α<VAR>x : α<VAR>c : Set (Set α)<VAR>H1 : ∀ s ∈ c, x ∈ s<VAR>H2 : ∀ s ∈ c, IsPreconnected s<VAR>y : α<VAR>s : Set α<VAR>sc : s ∈ c<VAR>ys : y ∈ s<GOAL>∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>inst✝² : Fintype ↑(G.neighborSet x.1)<VAR>inst✝¹ : Fintype ↑(H.neighborSet x.2)<VAR>inst✝ : Fintype ↑((G □ H).neighborSet x)<VAR>this : Fintype ↑((G □ H).neighborSet x) := boxProdFintypeNeighborSet x<GOAL>(G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯
<VAR>v : Multiset ℕ<VAR>h : ∀ p ∈ v, Nat.Prime p<GOAL>Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v
<VAR>v : Multiset ℕ<VAR>h : ∀ p ∈ v, Nat.Prime p<VAR>this : (fun p h => Coe.coe ⟨p, h⟩) = fun p x => id p<GOAL>Multiset.map Coe.coe (Multiset.pmap (fun p hp => ⟨p, hp⟩) v h) = v
<VAR>ι : Sort u_1<VAR>f✝ : ι → ℝ≥0<VAR>inst✝ : IsEmpty ι<VAR>f : ι → ℝ≥0<GOAL>⨅ i, f i = 0
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>a b : α<VAR>h : R b a<GOAL>destutter' R b (a :: l) = b :: destutter' R a l
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(univBall c r).target = ball c r
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(univUnitBall.trans' (unitBallBall c r hr) ⋯).target = ball c r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : BorelSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : BorelSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (π i)<VAR>inst✝ : ∀ (i : ι), BorelSpace (π i)<GOAL>MeasurableSpace.pi ≤ borel ((i : ι) → π i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹² : TopologicalSpace α<VAR>inst✝¹¹ : MeasurableSpace α<VAR>inst✝¹⁰ : BorelSpace α<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : BorelSpace β<VAR>inst✝⁶ : TopologicalSpace γ<VAR>inst✝⁵ : MeasurableSpace γ<VAR>inst✝⁴ : BorelSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>ι : Type u_6<VAR>π : ι → Type u_7<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (π i)<VAR>inst✝ : ∀ (i : ι), BorelSpace (π i)<VAR>this : inst✝¹ = fun i => borel (π i)<GOAL>MeasurableSpace.pi ≤ borel ((i : ι) → π i)
<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>f : G →* N<VAR>G' : Subgroup G<VAR>H K : Subgroup ↥G'<GOAL>Injective ⇑G'.subtype
<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>s : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<GOAL>dist ((-2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ) • v +ᵥ p) s.center = dist p s.center
<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>s : Sphere P<VAR>p : P<VAR>v : V<VAR>hv : ¬v = 0<GOAL>-2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ = 0 ∨ -2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ = -2 * ⟪v, p -ᵥ s.center⟫_ℝ / ⟪v, v⟫_ℝ
<VAR>p x ε y : ℝ<GOAL>y ∈ QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ↔ y ∈ closedBall x ε
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b ab : ℤ<VAR>h : a + b = ab<VAR>n : ℤ<GOAL>n + b + a = n + ab
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>K : CochainComplex C ℤ<VAR>a b n : ℤ<GOAL>((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f n = (XIsoOfEq K ⋯).hom
<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<GOAL>HasFDerivWithinAt f f' univ x ↔ 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<GOAL>HasFDerivAtFilter f f' x (𝓝 x) ↔ HasFDerivAt f f' x
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M₄<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>p.prod q = map (inl R M M₂) p ⊔ map (inr R M M₂) q
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>A B : Matrix m n α<VAR>x : n → α<GOAL>(A - B) *ᵥ x = A *ᵥ x - B *ᵥ x
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : HasZeroMorphisms V<VAR>α : Type u_2<VAR>inst✝² : AddRightCancelSemigroup α<VAR>inst✝¹ : One α<VAR>inst✝ : DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>i j : α<VAR>h : i ≠ j + 1<GOAL>(if h : i = j + 1 then eqToHom ⋯ ≫ d j else 0) = 0