ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb✝ : limsup v f ≤ b<VAR>hb : limsup v f = b<GOAL>limsup (u + v) f ≤ a + b
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb✝ : limsup v f ≤ b<VAR>hb : limsup v f = b<VAR>hb' : ¬b = ⊤<GOAL>limsup (u + v) f ≤ a + b
<VAR>y : ℝ<VAR>hy : 0 < y<VAR>x : ℝ≥0∞<GOAL>(x ^ (1 / y)) ^ y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid A<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R[X] A<VAR>inst✝ : IsScalarTower R R[X] A<VAR>a : A<GOAL>((mkDerivation R) a) X = a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>a : ℤ<GOAL>↑p ^ n ∣ ↑a ↔ ↑p ^ n ∣ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>map f (tail ⟨s, al⟩) = (map f ⟨s, al⟩).tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s : Stream' (Option α)<VAR>al : s.IsSeq<GOAL>↑(map f (tail ⟨s, al⟩)) = ↑(map f ⟨s, al⟩).tail
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubgroup N<VAR>h : Independent p<GOAL>Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : ι → AddSubgroup N<VAR>h : Independent (⇑AddSubgroup.toIntSubmodule ∘ p)<GOAL>Function.Injective ⇑(sumAddHom fun i => (p i).subtype)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<GOAL>Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<VAR>key : Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto id (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProbaEquiv.symm μ))<GOAL>Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<VAR>key : Tendsto diracProba (map (⇑diracProbaEquiv.symm) F) (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto (⇑diracProbaEquiv.symm) (map (⇑diracProbaEquiv) (map (⇑diracProbaEquiv.symm) F)) (𝓝 (diracProbaEquiv.symm μ))<GOAL>Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<VAR>key : Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))<GOAL>Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ)) ↔ Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<VAR>key : Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))<GOAL>Tendsto (fun μ => ↑μ) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto id F (𝓝 μ)
<VAR>X : Type u_1<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>inst✝¹ : T0Space X<VAR>inst✝ : CompletelyRegularSpace X<VAR>μ : ↑(range diracProba)<VAR>F : Filter ↑(range diracProba)<VAR>key : Tendsto (diracProba ∘ ⇑diracProbaEquiv.symm) F (𝓝 (diracProba (diracProbaEquiv.symm μ))) ↔ Tendsto (⇑diracProbaEquiv.symm) F (𝓝 (diracProbaEquiv.symm μ))<GOAL>diracProba (diracProbaEquiv.symm μ) = ↑μ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.95146, u_1} C<VAR>inst✝³ : Category.{?u.95150, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.95146, u_1} C<VAR>inst✝³ : Category.{?u.95150, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.map s.s ≫ F.map S.g = 𝟙 (F.obj S.X₃)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.95146, u_1} C<VAR>inst✝³ : Category.{?u.95150, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)
<VAR>f : ℍ → ℂ<VAR>z : ℍ<GOAL>(f ∘ ↑ofComplex) ↑z = f z
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>r : R<VAR>a✝ : Nontrivial R<GOAL>(X ^ n + C r).leadingCoeff = 1
<VAR>b x✝ y✝ : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>logb b x < logb b y
<VAR>b x✝ y✝ : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>logb b |x| < logb b |y|
<VAR>b x✝ y✝ : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>|y| < |x|
<VAR>α β γ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : CommApplicative F<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>traverse pure s = s
<VAR>α β γ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : CommApplicative F<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>Multiset.toFinset <$> s.val = s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>h : Isometry Φ<GOAL>hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : S<GOAL>∃ b, IsInteger R (↑b • a)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : S<GOAL>∃ b, IsInteger R (a * (algebraMap R S) ↑b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<GOAL>(l.concat a).prod = l.prod * a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<VAR>e' : Fin (Fintype.card I) → R<VAR>h₁ : CompleteOrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges (G'.edgeSet ∩ s) = G'.deleteEdges s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>n : ℤ<GOAL>f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>r : R<GOAL>(X - C r).roots = {r}
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<VAR>hI : Irreducible (absNorm I)<VAR>h : IsUnit I<GOAL>IsUnit (absNorm I)
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>a b : Ideal S<VAR>hI : Irreducible (absNorm (a * b))<GOAL>IsUnit a ∨ IsUnit b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<GOAL>∏ x ∈ s, f x = ∏ xbar ∈ image Quotient.mk'' s, ∏ y ∈ filter (fun x => ⟦x⟧ = xbar) s, f y
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>R : Setoid α<VAR>inst✝ : DecidableRel Setoid.r<VAR>x : α<VAR>_hx : x ∈ s<GOAL>∏ y ∈ filter (fun x_1 => ⟦x_1⟧ = Quotient.mk'' x) s, f y = ∏ x ∈ filter (fun c' => Quotient.mk'' c' = Quotient.mk'' x) s, f x
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>this : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>this : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>this : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<VAR>this : ∏ x ∈ s, (z x)⁻¹ ^ w x ≤ ∑ x ∈ s, w x * (z x)⁻¹<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<VAR>this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹<GOAL>(∑ i ∈ s, w i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<VAR>this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹<GOAL>(∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<VAR>this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹<VAR>p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹<GOAL>(∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ ≤ ∏ i ∈ s, z i ^ w i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>w z : ι → ℝ<VAR>hs : s.Nonempty<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : ∑ i ∈ s, w i = 1<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i<VAR>s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹<VAR>this : (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ ≤ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹<VAR>p_pos₂ : 0 < (∏ i ∈ s, z i ^ w i)⁻¹<GOAL>∏ x ∈ s, (z x ^ w x)⁻¹ ≤ ∏ i ∈ s, (z i)⁻¹ ^ w i
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ g f : Perm α<GOAL>f.support.card = 0 ↔ f = 1
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PosMulStrictMono α<VAR>a0 : 0 < a<GOAL>∃ b, b * b ≤ a
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PosMulStrictMono α<VAR>a0 : 0 < a<VAR>ha : a < 1<GOAL>∃ b, b * b ≤ a
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : PosMulStrictMono α<VAR>a0 : 0 < a<VAR>ha : 1 ≤ a<GOAL>∃ b, b * b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<GOAL>∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>v i₁ : α<VAR>vi₁ : v * i₁ = 1<VAR>iv₁ : i₁ * v = 1<VAR>i₂ : α<VAR>vi₂ : v * i₂ = 1<VAR>iv₂ : i₂ * v = 1<GOAL>i₁ = i₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u✝ v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<VAR>u : Set α := {z | P x z}<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u✝ v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<VAR>u : Set α := {z | P x z}<VAR>A : IsClosed u<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u✝ v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<VAR>u : Set α := {z | P x z}<VAR>A : IsClosed u<VAR>B : IsOpen u<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u✝ v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<VAR>u : Set α := {z | P x z}<VAR>A : IsClosed u<VAR>B : IsOpen u<VAR>C : u.Nonempty<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u✝ v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x<VAR>h' : Transitive P<VAR>x y : α<VAR>u : Set α := {z | P x z}<VAR>A : IsClosed u<VAR>B : IsOpen u<VAR>C : u.Nonempty<VAR>D : u = univ<GOAL>P x y
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>riemannZeta (2 * ↑k) = ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k))
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>(-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! = ↑((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>n : ℕ<VAR>a₁ a₂ : 𝕎 k<VAR>bs : Fin (n + 1) → k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<GOAL>(succNthDefiningPoly p n a₁ a₂ bs).degree ≠ 0
<VAR>G : PGame<GOAL>G.Impartial ↔ G ≈ -G ∧ (∀ (i : G.LeftMoves), (G.moveLeft i).Impartial) ∧ ∀ (j : G.RightMoves), (G.moveRight j).Impartial
<VAR>X✝ Y✝ Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>x : ↑↑Y.toPresheafedSpace<GOAL>x ∈ Set.range ⇑((fun x => f) ((fun x => PUnit.unit) x)).val.base
<VAR>X✝ Y✝ Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>x : ↑↑Y.toPresheafedSpace<GOAL>x ∈ Set.univ
<VAR>X✝ Y✝ Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>x : ↑↑Y.toPresheafedSpace<GOAL>Function.Surjective ⇑((fun x => f) ((fun x => PUnit.unit) x)).val.base
<VAR>X✝ Y✝ Z : Scheme<VAR>𝒰 : X✝.OpenCover<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>inst✝¹ : ∀ (x : 𝒰.J), HasPullback (𝒰.map x ≫ f✝) g<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>x : ↑↑Y.toPresheafedSpace<GOAL>Epi ((fun x => f) ((fun x => PUnit.unit) x)).val.base
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<GOAL>∃ n u, x = ↑u * ϖ ^ n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>x : R<VAR>hx : x ≠ 0<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>n : ℕ<VAR>hn : Associated x (ϖ ^ n)<GOAL>∃ n u, x = ↑u * ϖ ^ n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>n : ℕ<VAR>u : Rˣ<VAR>hx : ϖ ^ n * ↑u ≠ 0<VAR>hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)<GOAL>∃ n_1 u_1, ϖ ^ n * ↑u = ↑u_1 * ϖ ^ n_1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>hirr : Irreducible ϖ<VAR>n : ℕ<VAR>u : Rˣ<VAR>hx : ϖ ^ n * ↑u ≠ 0<VAR>hn : Associated (ϖ ^ n * ↑u) (ϖ ^ n)<GOAL>ϖ ^ n * ↑u = ↑u * ϖ ^ n
<VAR>z : ℂ<GOAL>HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin z)
<VAR>z : ℂ<GOAL>(fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<GOAL>HasMFDerivAt I I' f x (mfderiv I I' f x)
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderiv I I' f x) (range ↑I) (↑(extChartAt I x) x)
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableAt I I' f x<GOAL>HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x))) (range ↑I) (↑I (↑(chartAt H x) x))
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>x y : (n : ℕ) → E n<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>H : longestPrefix x s < firstDiff x y<VAR>xs : x ∉ s<VAR>ys : y ∉ s<VAR>l_eq : longestPrefix y s = longestPrefix x s<GOAL>cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>x y : (n : ℕ) → E n<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>hne : s.Nonempty<VAR>H : longestPrefix x s < firstDiff x y<VAR>xs : x ∉ s<VAR>ys : y ∉ s<VAR>l_eq : longestPrefix y s = longestPrefix x s<GOAL>x ∈ cylinder y (longestPrefix x s)
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<GOAL>p ^ (k + l + 1) ∣ m.natAbs * n.natAbs
<VAR>p : ℕ<VAR>p_prime : Nat.Prime p<VAR>m n : ℤ<VAR>k l : ℕ<VAR>hpm : ↑(p ^ k) ∣ m<VAR>hpn : ↑(p ^ l) ∣ n<VAR>hpmn : ↑(p ^ (k + l + 1)) ∣ m * n<VAR>hpm' : p ^ k ∣ m.natAbs<VAR>hpn' : p ^ l ∣ n.natAbs<GOAL>p ^ (k + l + 1) ∣ (m * n).natAbs