ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<GOAL>I = P ^ i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : P ^ (i + 1) < I<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<VAR>h3 : P ^ (i + 1) ≠ 0<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<VAR>h3 : P ^ (i + 1) ≠ 0<GOAL>P ^ i ≤ I
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<VAR>h3 : P ^ (i + 1) ≠ 0<GOAL>normalizedFactors I ≤ Multiset.replicate i (normalize P)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<VAR>h3 : P ^ (i + 1) ≠ 0<GOAL>I ≠ 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P I : Ideal A<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>i : ℕ<VAR>hlt : normalizedFactors I ≤ Multiset.replicate i (normalize P)<VAR>hle : I ≤ P ^ i<VAR>P_prime' : Prime P<VAR>h1 : I ≠ ⊥<VAR>this : P ^ i ≠ 0<VAR>h3 : P ^ (i + 1) ≠ 0<GOAL>P ^ i ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>(reflection s) p = p ↔ p ∈ s
<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 : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>↑((orthogonalProjection s) p) -ᵥ p +ᵥ ↑((orthogonalProjection s) p) = p ↔ ↑((orthogonalProjection s) p) = p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<GOAL>Monic 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹⁸ : Zero X<VAR>inst✝¹⁷ : Zero Y<VAR>inst✝¹⁶ : CommSemiring M<VAR>inst✝¹⁵ : TopologicalSpace X<VAR>inst✝¹⁴ : TopologicalSpace Y<VAR>inst✝¹³ : TopologicalSpace R<VAR>inst✝¹² : TopologicalSpace S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : TopologicalSemiring R<VAR>inst✝⁸ : ContinuousStar R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : StarRing S<VAR>inst✝⁵ : TopologicalSemiring S<VAR>inst✝⁴ : ContinuousStar S<VAR>inst✝³ : Module M R<VAR>inst✝² : Module M S<VAR>inst✝¹ : ContinuousConstSMul M R<VAR>inst✝ : ContinuousConstSMul M S<VAR>φ : R →⋆ₙₐ[M] S<VAR>hφ : Continuous ⇑φ<VAR>x✝ : C(X, R)₀<GOAL>∀ (x : X), ({ toFun := { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }.toFun (star x✝)) x = (star ({ toFun := { toFun := ⇑φ, continuous_toFun := hφ, map_zero' := ⋯ }.comp, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }.toFun x✝)) x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>t : Multiset α<VAR>a b : α<GOAL>∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>t : Multiset α<VAR>a b : α<VAR>s u : Multiset α<VAR>h₁ : s ≤ 0<VAR>h₂ : s ≤ u<GOAL>s ≤ 0 ∩ u
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>t✝ : Multiset α<VAR>a✝ b a : α<VAR>t : Multiset α<VAR>IH : ∀ {s u : Multiset α}, s ≤ t → s ≤ u → s ≤ t ∩ u<VAR>s u : Multiset α<VAR>h₁ : s ≤ a ::ₘ t<VAR>h₂ : s ≤ u<GOAL>s ≤ (a ::ₘ t) ∩ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s✝ t✝ : Set α<VAR>h : Semiconj f fa fb<VAR>s t : Set β<VAR>hb : MapsTo fb s t<VAR>x : α<VAR>hx : x ∈ f ⁻¹' s<GOAL>fa x ∈ f ⁻¹' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>t : Set α := toMeasurable μ s<VAR>ht : t = toMeasurable μ s<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>t : Set α := toMeasurable μ s<VAR>ht : t = toMeasurable μ s<VAR>ht_m : MeasurableSet t<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hμs : μ s ≠ ⊤<VAR>t : Set α := toMeasurable μ s<VAR>ht : t = toMeasurable μ s<VAR>ht_m : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>(𝓕 fun x => cexp (-↑π * b * ↑x ^ 2)) = fun t => 1 / b ^ (1 / 2) * cexp (-↑π / b * ↑t ^ 2)
<VAR>α✝ : Type u_1<VAR>a : α✝<VAR>l₁ l₂ : List α✝<GOAL>[a].Disjoint l₂ ∧ l₁.Disjoint l₂ ↔ ¬a ∈ l₂ ∧ l₁.Disjoint l₂
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x < y<GOAL>derivWithin f S y < derivWithin f S x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field L'<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K L'<VAR>S : IntermediateField K L<VAR>inst✝¹ : Algebra L' L<VAR>inst✝ : IsScalarTower K L' L<VAR>U V : IntermediateField L' L<VAR>H : restrictScalars K U = restrictScalars K V<VAR>x : L<GOAL>x ∈ U ↔ x ∈ V
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹¹ : Ring R<VAR>inst✝¹⁰ : StrongRankCondition R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module.Free R M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module.Free R M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module.Free R M₁<VAR>ι : Type u_1<VAR>inst✝ : Unique ι<VAR>h : finrank R M = 1<VAR>v : M<VAR>i : ι<VAR>hv : v = 0<GOAL>((basisUnique ι h).repr v) i = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).sin * ‖x + y‖ = ‖y‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g = pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.6070, u_1} C<VAR>inst✝² : Category.{?u.6074, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>(fun n m => limMap { app := fun j => (F.obj j).d n m, naturality := ⋯ }) n m ≫ limit.π (F ⋙ eval C c m) j = 0 ≫ limit.π (F ⋙ eval C c m) j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.6070, u_1} C<VAR>inst✝² : Category.{?u.6074, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>limit.π (F ⋙ eval C c n) j ≫ { app := fun j => (F.obj j).d n m, naturality := ⋯ }.app j = 0 ≫ limit.π (F ⋙ eval C c m) j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.6070, u_1} C<VAR>inst✝² : Category.{?u.6074, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)<VAR>n m : ι<VAR>h : ¬c.Rel n m<VAR>j : J<GOAL>limit.π (F ⋙ eval C c n) j ≫ (F.obj j).d n m = 0 ≫ limit.π (F ⋙ eval C c m) j
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>J : Type u_3<VAR>inst✝³ : Category.{?u.6070, u_1} C<VAR>inst✝² : Category.{?u.6074, u_3} J<VAR>c : ComplexShape ι<VAR>inst✝¹ : HasZeroMorphisms C<VAR>F : J ⥤ HomologicalComplex C c<VAR>inst✝ : ∀ (n : ι), HasLimit (F ⋙ eval C c n)<VAR>i j : J<VAR>φ : i ⟶ j<VAR>n : ι<GOAL>𝟙 (limit (F ⋙ eval C c n)) ≫ limit.π (F ⋙ eval C c n) j = limit.π (F ⋙ eval C c n) i ≫ (F.map φ).f n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>↑⌊a⌋₊ = ⌊a⌋
<VAR>d : Nat<VAR>n : Int<VAR>a : Nat<VAR>d0 : d ≠ 0<VAR>a0 : a ≠ 0<GOAL>normalize (↑a * n) (a * d) ⋯ = normalize n d d0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>X Y : C<VAR>inst✝¹ : Simple X<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<VAR>w : IsIso f → False<GOAL>f = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X Y : C<VAR>hX : IsInitial X<VAR>hY : IsInitial Y<VAR>f : X ⟶ Y<GOAL>f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>X Y : C<VAR>hX : IsInitial X<VAR>hY : IsInitial Y<VAR>f : X ⟶ Y<GOAL>f ≫ hY.to X = 𝟙 X
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>UniqueMDiffOn 𝓘(𝕜, E) s ↔ UniqueDiffOn 𝕜 s
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : AddMonoidWithOne R<GOAL>1 = closure {1}
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : AddMonoidWithOne R<GOAL>AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<GOAL>IsNilpotent (P * X) ↔ IsNilpotent P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<GOAL>IsNilpotent (X * P) ↔ IsNilpotent P
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>β : Type u_3<VAR>α : ι → Type u<VAR>U : (i : ι) → UniformSpace (α i)<VAR>inst✝ : UniformSpace β<VAR>S : Set ι<GOAL>UniformSpace.comap S.restrict (uniformSpace fun i => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_9, u_1} C<VAR>inst✝⁸ : Category.{?u.45154, u_2} C₁<VAR>inst✝⁷ : Category.{?u.45158, u_3} C₂<VAR>inst✝⁶ : Category.{?u.45162, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_10, u_6} D₂<VAR>inst✝³ : Category.{?u.45174, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>g : L₁.obj Y ⟶ L₁.obj Z<GOAL>(homEquiv W L₁ L₂) (f ≫ g) = (homEquiv W L₁ L₂) f ≫ (homEquiv W L₁ L₂) g
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>i j : ℕ<VAR>h : i ≠ j<VAR>a : α<VAR>hj : j < (l.set i a).length<GOAL>(l.set i a).get ⟨j, hj⟩ = l.get ⟨j, ⋯⟩
<VAR>α✝ : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α✝<VAR>x✝ y z : α✝<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α✝<VAR>α : Type u_3<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<GOAL>IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>(a ⊔ b) ^ 2 = a * b * mabs (b / a)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝³ : (i : ι) → Module R (M₁ i)<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module R M₃<VAR>inst✝ : Module R M'<VAR>f✝ f' : MultilinearMap R M₁ M₂<VAR>f : MultilinearMap R M M₂<VAR>m : (i : Fin n) → M i.succ<VAR>x y : M 0<GOAL>f (cons (x + y) m) = f (cons x m) + f (cons y m)
<VAR>R : Type uR<VAR>inst✝⁶ : CommRing R<VAR>A : Type uA<VAR>inst✝⁵ : AddCommGroup A<VAR>A' : Type u_1<VAR>inst✝⁴ : AddCommGroup A'<VAR>B : Type uB<VAR>inst✝³ : AddCommGroup B<VAR>inst✝² : Module R A<VAR>inst✝¹ : Module R A'<VAR>inst✝ : Module R B<VAR>f : A →ₗ[R] B<VAR>r : R<VAR>c : CharacterModule B<VAR>x : A<GOAL>({ toFun := fun L => AddMonoidHom.comp L f.toAddMonoidHom, map_add' := ⋯ }.toFun (r • c)) x = ((RingHom.id R) r • { toFun := fun L => AddMonoidHom.comp L f.toAddMonoidHom, map_add' := ⋯ }.toFun c) x
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.21752, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.21759, u_2} D<VAR>inst✝ : HasStrictInitialObjects C<VAR>X : C<VAR>h : IsInitial X<VAR>F' : Discrete PEmpty.{1} ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ Functor.empty C<VAR>f : c'.pt ⟶ (asEmptyCocone X).pt<VAR>hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty.{1})).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.21752, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.21759, u_2} D<VAR>inst✝ : HasStrictInitialObjects C<VAR>X : C<VAR>h : IsInitial X<VAR>F' : Discrete PEmpty.{1} ⥤ C<VAR>c' : Cocone F'<VAR>α : F' ⟶ Functor.empty C<VAR>f : c'.pt ⟶ (asEmptyCocone X).pt<VAR>hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty.{1})).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : F' = Functor.empty C<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.21752, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.21759, u_2} D<VAR>inst✝ : HasStrictInitialObjects C<VAR>X : C<VAR>h : IsInitial X<VAR>c' : Cocone (Functor.empty C)<VAR>α : Functor.empty C ⟶ Functor.empty C<VAR>f : c'.pt ⟶ (asEmptyCocone X).pt<VAR>hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty.{1})).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.21752, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.21759, u_2} D<VAR>inst✝ : HasStrictInitialObjects C<VAR>X : C<VAR>h : IsInitial X<VAR>c' : Cocone (Functor.empty C)<VAR>α : Functor.empty C ⟶ Functor.empty C<VAR>f : c'.pt ⟶ (asEmptyCocone X).pt<VAR>hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (Functor.const (Discrete PEmpty.{1})).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : IsIso f<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>IsOpen (coborder s) ↔ ∀ (i : ι), IsOpen (coborder (Subtype.val ⁻¹' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>s : Set β<GOAL>(∀ (i : ι), IsOpen (Subtype.val ⁻¹' coborder s)) ↔ ∀ (i : ι), IsOpen (coborder (Subtype.val ⁻¹' s))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>h : a ≤ b<GOAL>1 / b ≤ 1 / a
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>h : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>s_meas : MeasurableSet s<VAR>μs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<GOAL>∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>h : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>s_meas : MeasurableSet s<VAR>μs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>K : Set G<VAR>Ks : K ⊆ s<VAR>K_comp : IsCompact K<VAR>hK : r < μ K<GOAL>∃ K ⊆ s, (fun s => IsCompact s ∧ IsClosed s) K ∧ r < μ K
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>h : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>s_meas : MeasurableSet s<VAR>μs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>K : Set G<VAR>Ks : K ⊆ s<VAR>K_comp : IsCompact K<VAR>hK : r < μ K<GOAL>closure K ⊆ s
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>h : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>s_meas : MeasurableSet s<VAR>μs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>K : Set G<VAR>Ks : K ⊆ s<VAR>K_comp : IsCompact K<VAR>hK : r < μ K<GOAL>r < μ (closure K)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.Ψ 2 = W.ψ₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<GOAL>IsOpenMap f ↔ ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<GOAL>(∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)) → IsOpenMap f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsOpen (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>∀ (i : ι), IsOpen (Subtype.val ⁻¹' (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<VAR>i : ι<GOAL>IsOpen (Subtype.val ⁻¹' (f '' s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s✝ : Set β<VAR>ι : Type u_3<VAR>U : ι → Opens β<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), IsOpenMap ((U i).carrier.restrictPreimage f)<VAR>s : Set α<VAR>hs : IsOpen s<VAR>i : ι<VAR>e_1✝ : ↥(U i) = ↑(U i).carrier<GOAL>Subtype.val ⁻¹' (f '' s) = (U i).carrier.restrictPreimage f '' (Subtype.val ⁻¹' s)