ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : IsPurelyInseparable (↥L) E<VAR>y : ↥L<VAR>hx : (algebraMap (↥L) E) y ∈ separableClosure F E<GOAL>(algebraMap (↥L) E) y ∈ L
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<GOAL>∃ π, v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>∃ π, v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<GOAL>∃ π, v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<GOAL>∃ π, v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>∃ π, v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>v.intValuationDef π = ↑(ofAdd (-1))
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors)) = ofAdd (-1)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = -1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : π ∈ v.asIdeal<VAR>nmem : π ∉ v.asIdeal ^ 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : Associates.mk v.asIdeal ≤ Associates.mk (Ideal.span {π})<VAR>nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors<VAR>nmem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hlt : v.asIdeal ^ 2 < v.asIdeal<VAR>π : R<VAR>mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors<VAR>nmem : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors < 2<VAR>hπ : Associates.mk (Ideal.span {π}) ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{?u.41, u_3} E<VAR>F G : Karoubi C ⥤ D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<GOAL>φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{?u.41, u_3} E<VAR>F G : Karoubi C ⥤ D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<GOAL>φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{?u.41, u_3} E<VAR>F G : Karoubi C ⥤ D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<GOAL>F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{u_5, u_2} D<VAR>inst✝ : Category.{?u.41, u_3} E<VAR>F G : Karoubi C ⥤ D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<GOAL>𝟙 P = P.decompId_i ≫ P.decompId_p
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>primitiveRoots 1 R = {1}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ : R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>1 ∈ primitiveRoots 1 R ∧ ∀ x ∈ primitiveRoots 1 R, x = 1
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>α : E<VAR>halg : IsAlgebraic F α<GOAL>finSepDegree F ↥F⟮α⟯ = finrank F ↥F⟮α⟯ ↔ IsSeparable F α
<VAR>x : ℝ<VAR>hx : x ∈ Icc 0 π<GOAL>0 ≤ sin x
<VAR>x : ℝ<VAR>hx : x ∈ closure (Ioo 0 π)<GOAL>0 ≤ sin x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<GOAL>frobeniusPolyAux p n = X (n + 1) - ∑ i ∈ range n, ∑ j ∈ range (p ^ (n - i)), (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) * C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p ⟨j + 1, ⋯⟩) * p ^ (j - v p ⟨j + 1, ⋯⟩))
<VAR>l : List Char<VAR>s : String<GOAL>l.asString = s ↔ l = s.toList
<VAR>θ : ℝ<GOAL>(↑θ).toReal = θ ↔ -π < θ ∧ θ ≤ π
<VAR>θ : ℝ<GOAL>θ ∈ Set.Ioc (-π) (-π + 2 * π) ↔ -π < θ ∧ θ ≤ π
<VAR>θ : ℝ<GOAL>θ ∈ Set.Ioc (-π) π ↔ -π < θ ∧ θ ≤ π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>p : α → Prop<GOAL>(∃ s ∈ l, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<VAR>p : α → Prop<GOAL>(∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
<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>hf : Injective f<VAR>eq : f '' s = f '' t<GOAL>s = t
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₁ d₂ : ManyOneDegree<GOAL>d₁ ≤ d₂ → d₂ ≤ d₁ → d₁ = d₂
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₂ : ManyOneDegree<VAR>p✝ : Set ℕ<GOAL>of p✝ ≤ d₂ → d₂ ≤ of p✝ → of p✝ = d₂
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p✝¹ p✝ : Set ℕ<GOAL>of p✝¹ ≤ of p✝ → of p✝ ≤ of p✝¹ → of p✝¹ = of p✝
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p✝¹ p✝ : Set ℕ<VAR>hp : of p✝¹ ≤ of p✝<VAR>hq : of p✝ ≤ of p✝¹<GOAL>of p✝¹ = of p✝
<VAR>n d nd : ℕ<GOAL>(d, nd) ∈ map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors ↔ (d, nd) ∈ n.divisorsAntidiagonal
<VAR>n d nd : ℕ<GOAL>(d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>f : V1 →ᵃ[k] V2<VAR>x : V1<GOAL>f x = (⇑f.linear + fun x => f 0) x
<VAR>R L K : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv✝ : IsTranscendenceBasis R v<VAR>inst✝ : Nontrivial R<VAR>hv : IsTranscendenceBasis R v<VAR>hR : #R ≤ ℵ₀<VAR>hK : ℵ₀ < #K<VAR>this : ℵ₀ ≤ #ι<GOAL>max (max #R #ι) ℵ₀ = #ι
<VAR>R L K : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv✝ : IsTranscendenceBasis R v<VAR>inst✝ : Nontrivial R<VAR>hv : IsTranscendenceBasis R v<VAR>hR : #R ≤ ℵ₀<VAR>hK : ℵ₀ < #K<VAR>this : ℵ₀ ≤ #ι<GOAL>#R ≤ #ι
<VAR>R L K : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsAlgClosed K<VAR>ι : Type u<VAR>v : ι → K<VAR>hv✝ : IsTranscendenceBasis R v<VAR>inst✝ : Nontrivial R<VAR>hv : IsTranscendenceBasis R v<VAR>hR : #R ≤ ℵ₀<VAR>hK : ℵ₀ < #K<VAR>this : ℵ₀ ≤ #ι<GOAL>ℵ₀ ≤ max #R #ι
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<GOAL>t ⊆ balancedCoreAux 𝕜 s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<VAR>x : E<VAR>hx : x ∈ t<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<GOAL>x ∈ r • s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<VAR>x : E<VAR>hx : x ∈ t<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<GOAL>r⁻¹ • x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<VAR>x : E<VAR>hx : x ∈ t<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<GOAL>‖r⁻¹‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>h : t ⊆ s<VAR>ht : Balanced 𝕜 t<VAR>x : E<VAR>hx : x ∈ t<VAR>r : 𝕜<VAR>hr : 1 ≤ ‖r‖<GOAL>‖r‖⁻¹ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s✝ s : Set α<VAR>s_fin : s.Finite<VAR>s_mble : MeasurableSet s<GOAL>count s = ↑s_fin.toFinset.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a✝ b✝ c d a b : α<GOAL>(a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
<VAR>x y : ℝ<GOAL>sinh (-x) = -sinh x
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<GOAL>IsPreconnected {y | s.WSameSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : ↑s = ∅<GOAL>IsPreconnected {y | s.WSameSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>h : (↑s).Nonempty<GOAL>IsPreconnected {y | s.WSameSide x y}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>D : LieDerivation R L L<VAR>x : L<GOAL>⁅D, (ad R L) x⁆ = (ad R L) (D x)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝¹ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>a✝ : ℕ<GOAL>a ≠ 0 → a ^ ↑a✝ ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝¹ b c d : G₀<VAR>m n : ℕ<VAR>a : G₀<VAR>a✝ : ℕ<GOAL>a ≠ 0 → a ^ a✝ ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n✝ : ℕ<VAR>a : G₀<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>a ^ Int.negSucc n ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c d : G₀<VAR>m n✝ : ℕ<VAR>a : G₀<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(a ^ (n + 1))⁻¹ ≠ 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>s✝ t : Set E<VAR>inst✝ : Subsingleton ι<VAR>p : ι → E<VAR>s : Set ι<VAR>x : ι<VAR>hx : p x ∈ (convexHull 𝕜) (p '' s)<VAR>this : ((convexHull 𝕜) (p '' s)).Nonempty<GOAL>x ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>s✝ t : Set E<VAR>inst✝ : Subsingleton ι<VAR>p : ι → E<VAR>s : Set ι<VAR>x : ι<VAR>hx : p x ∈ (convexHull 𝕜) (p '' s)<VAR>this : s.Nonempty<GOAL>x ∈ s
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R✝ : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>R : Type u_14<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Module R α<VAR>x : R<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>blockDiagonal' (x • M) i✝ j✝ = (x • blockDiagonal' M) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R✝ : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>R : Type u_14<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Module R α<VAR>x : R<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>i✝ : (i : o) × m' i<VAR>j✝ : (i : o) × n' i<GOAL>(if h : i✝.fst = j✝.fst then x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) = x • if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>⟪x, y⟫_ℝ = 0 ↔ angle x y = π / 2
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>this : ∀ x ∈ closure s, p x<GOAL>p x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Monoid α<VAR>n : ℕ<VAR>a m : α<GOAL>IsSquare m ↔ ∃ c, m = c ^ 2
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>x : AddCircle T<GOAL>(homeomorphCircle hT) x = x.toCircle
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>x : ℝ<GOAL>(homeomorphCircle hT) ↑x = toCircle ↑x
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>x : ℝ<GOAL>expMapCircle (x * (T⁻¹ * (2 * π))) = expMapCircle (2 * π / T * x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>M : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : TopologicalSpace M<VAR>v : VectorMeasure α M<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(v.restrict ∅) i = ↑0 i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<VAR>h : a ≠ a'<GOAL>(single a b) a' = 0
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<GOAL>TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l = ⊥<GOAL>TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<GOAL>TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<GOAL>TendstoUniformlyOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) (fun y => (↑‖y - x‖)⁻¹ • (g y - g x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<GOAL>UniformCauchySeqOnFilter (fun n y => (↑‖y - x‖)⁻¹ • (f n y - f n x)) l (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<GOAL>TendstoUniformlyOnFilter (fun n z => (↑‖z - x‖)⁻¹ • (f n.1 z - f n.1 x) - (↑‖z - x‖)⁻¹ • (f n.2 z - f n.2 x)) 0 (l ×ˢ l) (𝓝 x)
<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this : l.NeBot<GOAL>∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε