ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PseudoMetrizableSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<VAR>r : ℝ≥0∞<VAR>F : ℕ → Set X<VAR>F_closed : ∀ (n : ℕ), IsClosed (F n)<VAR>F_mono : Monotone F<VAR>hU : IsOpen (⋃ n, F n)<VAR>hr : r < ⨆ i, μ (F i)<GOAL>∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ✝ : Measure α<VAR>p q : Set α → Prop<VAR>U s : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>X : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : PseudoMetrizableSpace X<VAR>inst✝ : MeasurableSpace X<VAR>μ : Measure X<VAR>A : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X<VAR>r : ℝ≥0∞<VAR>F : ℕ → Set X<VAR>F_closed : ∀ (n : ℕ), IsClosed (F n)<VAR>F_mono : Monotone F<VAR>hU : IsOpen (⋃ n, F n)<VAR>hr : r < ⨆ i, μ (F i)<VAR>n : ℕ<VAR>hn : r < μ (F n)<GOAL>∃ K ⊆ ⋃ n, F n, IsClosed K ∧ r < μ K
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x✝ : ↥(skewAdjoint.submodule R A)<VAR>x : A<VAR>hx : star x = -x<GOAL>↑((skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype) ⟨x, hx⟩) = ↑(LinearMap.id ⟨x, hx⟩)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x✝ : ↥(skewAdjoint.submodule R A)<VAR>x : A<VAR>hx : star x = -x<GOAL>x = ↑(LinearMap.id ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a < b<GOAL>insert b (Ioo a b) = Ioc a b
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n.succ → R<GOAL>vandermonde v = Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n.succ → R<GOAL>(Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => Fin.tail v i * vandermonde (Fin.tail v) i j) = Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>hs : IsOpen s<GOAL>IsOpen (s / t)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>hs : IsOpen s<GOAL>IsOpen (⋃ a ∈ t, (fun x => x / a) '' s)
<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>m1 : MeasurableSpace β<VAR>f : α → β<VAR>μ✝ ν✝ : Measure α<VAR>hf : MeasurableEmbedding f<VAR>μ ν : Measure β<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(Measure.comap f (μ + ν)) s = (Measure.comap f μ + Measure.comap f ν) s
<VAR>x y : ℝ<GOAL>√x = 0 ↔ x ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ᵐ * a⁺ᵐ = mabs a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a ⊔ a⁻¹ ⊔ 1 = mabs a
<VAR>α : Type v<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>M : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : MulAction M α<VAR>i : ℤ<VAR>g : G<VAR>a : α<GOAL>g ^ (↑(period g a) + i) • a = g ^ i • a
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>f : R[X]<GOAL>f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>b : OrthonormalBasis ι ℝ ℝ<GOAL>parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>e : ι ≃ Fin 1<GOAL>parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module ℝ F<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>e : ι ≃ Fin 1<VAR>B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b<GOAL>parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F✝<VAR>inst✝ : Module ℝ F✝<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>e : ι ≃ Fin 1<VAR>B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b<VAR>F : ℝ → Fin 1 → ℝ := fun t _i => t<VAR>A : Icc 0 1 = F '' Icc 0 1<GOAL>parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F✝<VAR>inst✝ : Module ℝ F✝<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>e : ι ≃ Fin 1<VAR>B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b<VAR>F : ℝ → Fin 1 → ℝ := fun t _i => t<VAR>A : Icc 0 1 = F '' Icc 0 1<VAR>H : ⇑(b.reindex e) = fun x => 1<GOAL>parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : Fintype ι'<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : AddCommGroup F✝<VAR>inst✝ : Module ℝ F✝<VAR>b : OrthonormalBasis ι ℝ ℝ<VAR>e : ι ≃ Fin 1<VAR>B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b<VAR>F : ℝ → Fin 1 → ℝ := fun t _i => t<VAR>A : Icc 0 1 = F '' Icc 0 1<VAR>H : ⇑(b.reindex e) = fun x => -1<GOAL>parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>(fun x => log x ^ n) =o[atTop] id
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>Tendsto (fun x => log x ^ n / id x) atTop (𝓝 0)
<VAR>x y : ℝ<VAR>n : ℕ<GOAL>∀ᶠ (x : ℝ) in atTop, id x = 0 → log x ^ n = 0
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>A : ℝ<VAR>habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A<VAR>Apos : 0 ≤ A<GOAL>∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ NumberField.house.c₁ K * (NumberField.house.c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s t : Multiset α<GOAL>s + a ::ₘ t = a ::ₘ (s + t)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>finj : Injective f<VAR>l₁ l₂ : List α<GOAL>map f (foldl List.erase l₁ l₂) = foldl (fun l a => l.erase (f a)) (map f l₁) l₂
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<GOAL>Submodule.comap reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>v : E<GOAL>(adjointAux (adjointAux A)) v = A v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>v : E<VAR>w : F<GOAL>⟪w, (adjointAux (adjointAux A)) v⟫_𝕜 = ⟪w, A v⟫_𝕜
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>x ⧏ 0 ↔ ∃ j, ∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∃ i, (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ moveLeft 0 i) ∧ ∀ (j : (moveLeft 0 i).RightMoves), x ⧏ (moveLeft 0 i).moveRight j) ∨ ∃ j, (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0) ∧ ∀ (j' : RightMoves 0), x.moveRight j ⧏ moveRight 0 j') ↔ ∃ j, ∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>B : C<GOAL>(underlyingIso (𝟙 B)).hom = ⊤.arrow
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>B : C<GOAL>(underlyingIso (𝟙 B)).hom = (underlyingIso (𝟙 B)).hom ≫ 𝟙 B
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>inst✝ : Invertible A<VAR>hA : A.IsHermitian<GOAL>star (x ⊕ᵥ y) ᵥ* fromBlocks A B Bᴴ D ⬝ᵥ (x ⊕ᵥ y) = star (x + (A⁻¹ * B) *ᵥ y) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) + star y ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>x : m → 𝕜<VAR>y : n → 𝕜<VAR>inst✝ : Invertible A<VAR>hA : A.IsHermitian<GOAL>star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* D ⬝ᵥ y) = star x ᵥ* A ⬝ᵥ x + star y ᵥ* Bᴴ ⬝ᵥ x + (star x ᵥ* B ⬝ᵥ y + star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y) + (star y ᵥ* D ⬝ᵥ y - star y ᵥ* (Bᴴ * (A⁻¹ * B)) ⬝ᵥ y)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>s : Set ι<GOAL>¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.total ι M R v) f = 0 ∧ f ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>T : Set (Set β)<VAR>s₁ : Set α<VAR>h₁ : s₁ ∈ S<VAR>s₂ : Set β<VAR>h₂ : s₂ ∈ T<GOAL>⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>T : Set (Set β)<VAR>s₁ : Set α<VAR>h₁ : s₁ ∈ S<VAR>s₂ : Set β<VAR>h₂ : s₂ ∈ T<VAR>x : α × β<VAR>hx : x ∈ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2<GOAL>x ∈ ⋂₀ S ×ˢ ⋂₀ T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>T : Set (Set β)<VAR>s₁ : Set α<VAR>h₁ : s₁ ∈ S<VAR>s₂ : Set β<VAR>h₂ : s₂ ∈ T<VAR>x : α × β<VAR>hx : ∀ i ∈ S ×ˢ T, x ∈ i.1 ×ˢ i.2<GOAL>x ∈ ⋂₀ S ×ˢ ⋂₀ T
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<VAR>h : ‖f‖ = 0<GOAL>f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E 0)<VAR>h : ‖f‖ = 0<GOAL>f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E ⊤)<VAR>h : ‖f‖ = 0<GOAL>f = 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : ↥(lp E p)<VAR>h : ‖f‖ = 0<VAR>hp : 0 < p.toReal<GOAL>f = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>(∃ I, lieIdealSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>K K' : LieSubalgebra R L<VAR>h : K ≤ K'<GOAL>(∀ (x y : ↥K'), ↑y ∈ K → ⁅↑x, ↑y⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<GOAL>(∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → w.GuitartExact
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C₁<VAR>inst✝² : Category.{v₂, u₂} C₂<VAR>inst✝¹ : Category.{v₃, u₃} C₃<VAR>inst✝ : Category.{v₄, u₄} C₄<VAR>T : C₁ ⥤ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ⥤ C₄<VAR>w : TwoSquare T L R B<GOAL>(∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<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>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v<GOAL>ker f = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<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>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v<VAR>h₁ : f.comp 0 = 0<GOAL>ker f = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring R₂<VAR>inst✝⁷ : Semiring R₃<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>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : ∀ (u v : ↥(ker f) →ₗ[R] M), f.comp u = f.comp v → u = v<VAR>h₁ : f.comp 0 = 0<GOAL>range 0 = ⊥
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<GOAL>φ.totalDegree = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<GOAL>n ≤ φ.totalDegree
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>n ≤ φ.totalDegree
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>(weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(weight 1) d ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>(d.sum fun i c => c) ≤ φ.support.sup fun s => ∑ x ∈ s.support, s x
<VAR>x : ℝ≥0∞<VAR>y z : ℝ<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<VAR>hyz : z < y<GOAL>x ^ y < x ^ z
<VAR>y z : ℝ<VAR>hyz : z < y<VAR>x : ℝ≥0<VAR>hx0 : 0 < ↑x<VAR>hx1 : ↑x < 1<GOAL>↑x ^ y < ↑x ^ z
<VAR>y z : ℝ<VAR>hyz : z < y<VAR>x : ℝ≥0<VAR>hx0 : 0 < x<VAR>hx1 : x < 1<GOAL>↑x ^ y < ↑x ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>m : γ → β<VAR>l : Filter γ<GOAL>Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ioi a ∩ Ioo b c = Ioo (max a b) c
<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₄<GOAL>Disjoint (range (inl R M M₂)) (range (inr R M M₂))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set (Set α)<VAR>b : β<GOAL>b ∈ f '' ⋃₀ s ↔ b ∈ ⋃₀ (image f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : Set (Set α)<VAR>b : β<GOAL>(∃ x, (∃ t ∈ s, x ∈ t) ∧ f x = b) ↔ ∃ i ∈ s, ∃ x ∈ i, f x = b
<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>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (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<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>IsCompact (⋃ b, bif b then s else t)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : CommRing K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : CommRing M<VAR>inst✝⁵ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f✝ : L →+* M<VAR>g✝ : L →+* N<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : ExpChar N p<VAR>inst✝ : IsPRadical i p<VAR>h : pNilradical M p = ⊥<VAR>f g : L →+* M<VAR>heq : (fun f => f.comp i) f = (fun f => f.comp i) g<VAR>x : L<GOAL>f x = g x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : CommRing K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : CommRing M<VAR>inst✝⁵ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f✝ : L →+* M<VAR>g✝ : L →+* N<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : ExpChar N p<VAR>inst✝ : IsPRadical i p<VAR>h : pNilradical M p = ⊥<VAR>f g : L →+* M<VAR>heq : (fun f => f.comp i) f = (fun f => f.comp i) g<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>hx : i y = x ^ p ^ n<GOAL>f x = g x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁸ : CommRing K<VAR>inst✝⁷ : CommRing L<VAR>inst✝⁶ : CommRing M<VAR>inst✝⁵ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f✝ : L →+* M<VAR>g✝ : L →+* N<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : ExpChar N p<VAR>inst✝ : IsPRadical i p<VAR>h : pNilradical M p = ⊥<VAR>f g : L →+* M<VAR>heq : (fun f => f.comp i) f = (fun f => f.comp i) g<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>hx : i y = x ^ p ^ n<GOAL>f x ^ p ^ n = g x ^ p ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<VAR>x : M<VAR>hx : x ≠ 0<GOAL>l.lookupFinsupp a = x ↔ x ∈ lookup a l
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>l : AList fun _x => M<VAR>a : α<VAR>x : M<VAR>hx : x ≠ 0<GOAL>(lookup a l).getD 0 = x ↔ x ∈ lookup a l
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁶ : PseudoEMetricSpace X<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G X<VAR>inst✝³ : IsometricSMul G X<VAR>inst✝² : PseudoEMetricSpace G<VAR>inst✝¹ : IsometricSMul G G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>x y : G<GOAL>edist x⁻¹ y = edist x y⁻¹
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>inst✝ : Finite β<VAR>f : α → β<VAR>H : Injective f<GOAL>Finite α
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>inst✝ : Finite β<VAR>f : α → β<VAR>H : Injective f<VAR>n : ℕ<VAR>e : β ≃ Fin n<GOAL>Finite α
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : PartialRefinement u s<VAR>hs : IsClosed s<VAR>i : ι<VAR>hi : i ∉ v.carrier<GOAL>∃ v', v < v'
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>v : PartialRefinement u s<VAR>hs : IsClosed s<VAR>i : ι<VAR>hi : i ∉ v.carrier<VAR>I : s ∩ ⋂ j, ⋂ (_ : j ≠ i), (v.toFun j)ᶜ ⊆ v.toFun i<GOAL>∃ v', v < v'