ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>i₁ : ι<GOAL>(LinearMap.mul R B).compr₂ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ (ℬ i₁).subtype = (LinearMap.mul R (𝒜 ᵍ⊗[R] ℬ) ∘ₗ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ }).compl₂ { toFun := fun b => 1 ᵍ⊗ₜ[R] b, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ (ℬ i₁).subtype
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<VAR>i₁ : ι<VAR>b₁ : ↥(ℬ i₁)<VAR>b₂ : B<GOAL>1 ᵍ⊗ₜ[R] (↑b₁ * b₂) = 1 ᵍ⊗ₜ[R] ↑b₁ * 1 ᵍ⊗ₜ[R] b₂
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin (n + 1)<GOAL>snoc f a i.rev = cons a (f ∘ rev) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>s t : Set ι<VAR>f g : ι → α<VAR>h : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>i = j ∨ Disjoint (f i) (f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>s t : Set ι<VAR>f g : ι → α<VAR>h : s.PairwiseDisjoint f<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>¬Disjoint (f i) (f j) → i = j
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : { j // j ≠ i } → ↑I<GOAL>({ toFun := fun t => ⟨((↑p).comp (Cube.insertAt i).toContinuousMap).curry t, ⋯⟩, continuous_toFun := ⋯ }.toFun 0) t = const t
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : { j // j ≠ i } → ↑I<GOAL>(Cube.insertAt i) (0, t) i = 0
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : { j // j ≠ i } → ↑I<GOAL>({ toFun := fun t => ⟨((↑p).comp (Cube.insertAt i).toContinuousMap).curry t, ⋯⟩, continuous_toFun := ⋯ }.toFun 1) t = const t
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : ↑(Ω^ N X x)<VAR>t : { j // j ≠ i } → ↑I<GOAL>(Cube.insertAt i) (1, t) i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : ℕ<VAR>n : Fin m → ℕ<VAR>inst✝ : ∀ (i : Fin m), NeZero (n i)<VAR>i : Fin m<VAR>j : Fin (n i)<GOAL>↑(finPiFinEquiv (Pi.single i j)) = ↑j * ∏ j : Fin ↑i, n (Fin.castLE ⋯ j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : ℕ<VAR>n : Fin m → ℕ<VAR>inst✝ : ∀ (i : Fin m), NeZero (n i)<VAR>i : Fin m<VAR>j : Fin (n i)<GOAL>∀ (x : Fin m), x ≠ i → ↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : ℕ<VAR>n : Fin m → ℕ<VAR>inst✝ : ∀ (i : Fin m), NeZero (n i)<VAR>i : Fin m<VAR>j : Fin (n i)<VAR>x : Fin m<VAR>hx : x ≠ i<GOAL>↑(Pi.single i j x) * ∏ j : Fin ↑x, n (Fin.castLE ⋯ j) = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<GOAL>upperCrossingTime a b f N n ω ≤ lowerCrossingTime a b f N n ω
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>φ : α ≃ₜ β<VAR>s : Set β<GOAL>(interior s).Nonempty ↔ (interior (⇑φ ⁻¹' s)).Nonempty
<VAR>a : ℤ<VAR>ha : IsUnit a<GOAL>a ^ 2 = 1
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>ι : Type u_7<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set E<GOAL>IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝³ : SeminormedRing 𝕜<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>ι : Type u_7<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set E<VAR>x✝ : Finite ↑I<GOAL>IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hb : AddLECancellable b<VAR>hba : b ≤ a<GOAL>a - b < c ↔ a < c + b
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α✝<VAR>inst✝³ : LinearOrderedAddCommGroup α✝<VAR>inst✝² : OrderTopology α✝<VAR>l : Filter β<VAR>f g : β → α✝<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}<VAR>a : α<VAR>this✝ : TopologicalSpace α := Preorder.topology α<VAR>this : OrderTopology α := { topology_eq_generate_intervals := rfl }<GOAL>⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a
<VAR>q : ℝ<VAR>hq' : 1 < q<GOAL>(q - 1) ^ φ 0 ≤ eval q (cyclotomic 0 ℝ)
<VAR>q : ℝ<VAR>hq' : 1 < q<GOAL>(q - 1) ^ φ 1 ≤ eval q (cyclotomic 1 ℝ)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>G H : ModuleCat R<VAR>f✝ : G ⟶ H<VAR>M N : ModuleCat R<VAR>f : M ⟶ N<VAR>y : ↑N<VAR>m : ↑M<GOAL>(cokernel.π f) (y + f m) = (cokernel.π f) y
<VAR>n m : ℕ<VAR>hzero : n ≠ 0<VAR>h : m ∣ n<VAR>hdiff : m ≠ n<GOAL>m.divisors ⊆ n.properDivisors
<VAR>n m : ℕ<VAR>hzero : n ≠ 0<VAR>h : m ∣ n<VAR>hdiff : m ≠ n<GOAL>∀ ⦃x : ℕ⦄, x ∈ m.divisors → x ∈ n.properDivisors
<VAR>n m : ℕ<VAR>hzero : n ≠ 0<VAR>h : m ∣ n<VAR>hdiff : m ≠ n<VAR>x : ℕ<VAR>hx : x ∈ m.divisors<GOAL>x ∈ n.properDivisors
<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✝¹ : Fintype α<VAR>inst✝ : CommMonoid β<VAR>s t : Finset α<VAR>h : IsCompl s t<VAR>f : α → β<GOAL>∏ x ∈ s.disjUnion t ⋯, f x = ∏ i : α, f i
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L✝ : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ : V → E<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>v : V<GOAL>‖fourierSMulRight L f v‖ = 2 * π * ‖L v‖ * ‖f v‖
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>map✝¹ : R[X] →+* S<VAR>map_surjective✝¹ : Function.Surjective ⇑map✝¹<VAR>ker_map✝¹ : RingHom.ker map✝¹ = Ideal.span {f}<VAR>algebraMap_eq✝¹ : algebraMap R S = map✝¹.comp C<VAR>map✝ : R[X] →+* S<VAR>map_surjective✝ : Function.Surjective ⇑map✝<VAR>ker_map✝ : RingHom.ker map✝ = Ideal.span {f}<VAR>algebraMap_eq✝ : algebraMap R S = map✝.comp C<VAR>eq : ∀ (x : R[X]), { map := map✝¹, map_surjective := map_surjective✝¹, ker_map := ker_map✝¹, algebraMap_eq := algebraMap_eq✝¹ }.map x = { map := map✝, map_surjective := map_surjective✝, ker_map := ker_map✝, algebraMap_eq := algebraMap_eq✝ }.map x<GOAL>map✝¹ = map✝
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.16014, u_2} D<VAR>inst✝² : Category.{?u.16018, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝¹ : EffectiveEpi π<VAR>inst✝ : HasPullback π π<VAR>hP : Nonempty (IsLimit (Fork.ofι (P.map π.op) ⋯))<GOAL>Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.16014, u_2} D<VAR>inst✝² : Category.{?u.16018, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝¹ : EffectiveEpi π<VAR>inst✝ : HasPullback π π<VAR>hP : ∀ (y : P.obj (op X)), P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y = P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y → ∃! x, P.map π.op x = y<GOAL>Function.Bijective (MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.16014, u_2} D<VAR>inst✝² : Category.{?u.16018, u_3} E<VAR>P : Cᵒᵖ ⥤ Type u_4<VAR>X B : C<VAR>π : X ⟶ B<VAR>inst✝¹ : EffectiveEpi π<VAR>inst✝ : HasPullback π π<VAR>hP : ∀ (y : P.obj (op X)), P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).fst.op y = P.map (PullbackCone.mk (pullback.fst π π) (pullback.snd π π) ⋯).snd.op y → ∃! x, P.map π.op x = y<GOAL>∀ (b : ↑{x | P.map (pullback.fst π π).op x = P.map (pullback.snd π π).op x}), ∃! a, MapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯ a = b
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddTorsor G P<VAR>x y : P<GOAL>(pointReflection x) y = (Equiv.symm (pointReflection x)) y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>f✝ g✝ : Arrow C<VAR>inst✝³ : HasImage f✝.hom<VAR>inst✝² : HasImage g✝.hom<VAR>sq✝ : f✝ ⟶ g✝<VAR>f g : Arrow C<VAR>inst✝¹ : HasImage f.hom<VAR>inst✝ : HasImage g.hom<VAR>sq : f ⟶ g<VAR>map : image f.hom ⟶ image g.hom<VAR>map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝<VAR>map' : image f.hom ⟶ image g.hom<VAR>map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right<GOAL>(map = map') = True
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>f✝ g✝ : Arrow C<VAR>inst✝³ : HasImage f✝.hom<VAR>inst✝² : HasImage g✝.hom<VAR>sq✝ : f✝ ⟶ g✝<VAR>f g : Arrow C<VAR>inst✝¹ : HasImage f.hom<VAR>inst✝ : HasImage g.hom<VAR>sq : f ⟶ g<VAR>map : image f.hom ⟶ image g.hom<VAR>map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝<VAR>map' : image f.hom ⟶ image g.hom<VAR>map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right<GOAL>map = map'
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f : WithLp ⊤ (α × β)<GOAL>‖(WithLp.equiv ⊤ (α × β)) f‖₊ = ‖f‖₊
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : GroupWithZero K<VAR>inst✝ : Fintype K<VAR>a : K<VAR>h : ¬a = 0<GOAL>a ^ q = a
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>logb b y < logb b x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hxy : x < y<GOAL>log x < log y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>Q : QuadraticMap R M N<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower S R M<VAR>inst✝¹ : Module S N<VAR>inst✝ : IsScalarTower S R N<VAR>a : S<VAR>x y : M<GOAL>polar (⇑Q) x (a • y) = a • polar (⇑Q) x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>F : (i : α) → i ∈ s → β<GOAL>{y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>hs : s.Finite<VAR>F : (i : α) → i ∈ s → β<VAR>this : Finite ↑s<GOAL>{y | ∃ x, ∃ (hx : x ∈ s), F x hx = y}.Finite
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : Field k<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : AddTorsor E PE<VAR>f : k → PE<VAR>a b : k<VAR>h : slope f a b = 0<GOAL>f a = f b
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<GOAL>x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<GOAL>(∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔ x ∈ ⊥
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<VAR>hR : ¬IsField R<GOAL>(∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → x ∈ ⊥
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<GOAL>x ∈ ⊥ → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<VAR>hR : ¬IsField R<GOAL>(∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → ∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
<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 R<VAR>v : HeightOneSpectrum R<VAR>inst✝ : Algebra R K<VAR>hK : IsFractionRing R K<VAR>x : K<GOAL>(∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) → ∀ (i : HeightOneSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>h : 0 < r ∨ Nonempty β<GOAL>sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>h : 0 < r ∨ Nonempty β<VAR>hr : r < 0<GOAL>sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>h : 0 < 0 ∨ Nonempty β<GOAL>sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>x : (b : β) → π b<VAR>r : ℝ<VAR>h : 0 < r ∨ Nonempty β<VAR>hr : 0 < r<GOAL>sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
<VAR>c d : ℝ≥0∞<VAR>r p q a b : ℝ≥0<GOAL>(↑a).toReal ≤ (↑b).toReal ↔ ↑a ≤ ↑b
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : AddCommMonoid α<VAR>inst✝⁴ : AddCommMonoid β<VAR>inst✝³ : AddCommMonoid γ<VAR>inst✝² : Module R α<VAR>inst✝¹ : Module R β<VAR>inst✝ : Module R γ<VAR>f : α →ₗ[R] β →ₗ[R] γ<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(((kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C₁<VAR>inst✝¹ : Category.{u_5, u_2} C₂<VAR>inst✝ : Category.{u_6, u_3} C₃<VAR>W : MorphismProperty C₁<VAR>F : C₁ ⥤ C₂<VAR>G : C₂ ⥤ C₃<GOAL>(W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<GOAL>U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<GOAL>(∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i) ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = univ) ∧ U = ⋂ x, V ↑x ∧ U = ⋂ i, V i
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>bi : M<VAR>hbi : bi ∈ Finset.image (⇑b) Finset.univ<GOAL>b.reindexFinsetRange ⟨bi, hbi⟩ = ↑⟨bi, hbi⟩
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : 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<VAR>V' : Type u_9<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x : M<VAR>b' : Basis ι' R M'<VAR>e : ι ≃ ι'<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq M<VAR>i : ι<VAR>hbi : b i ∈ Finset.image (⇑b) Finset.univ<GOAL>b.reindexFinsetRange ⟨b i, hbi⟩ = ↑⟨b i, hbi⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] (f.extend I).target ∩ ↑(f.extend I).symm ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>↑(f.extend I).symm ⁻¹' s ∩ range ↑I =ᶠ[𝓝 (↑(f.extend I) x)] ↑I.symm ⁻¹' f.target ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>univ ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I) =ᶠ[𝓝 (↑(f.extend I) x)] ↑I.symm ⁻¹' f.target ∩ (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>↑I.symm ⁻¹' f.target ∈ 𝓝 (↑(f.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t s : Set M<VAR>x : M<VAR>hx : x ∈ f.source<GOAL>↑I.symm (↑(f.extend I) x) ∈ f.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a : α<VAR>y : β<VAR>h : 𝓝[<] a ≠ ⊥<VAR>h' : Tendsto f (𝓝[<] a) (𝓝 y)<VAR>h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)<GOAL>leftLim f a = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a : α<VAR>y : β<VAR>h : 𝓝[<] a ≠ ⊥<VAR>h' : Tendsto f (𝓝[<] a) (𝓝 y)<VAR>h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)<GOAL>limUnder (𝓝[<] a) f = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace β<VAR>hα : TopologicalSpace α<VAR>h'α : OrderTopology α<VAR>inst✝ : T2Space β<VAR>f : α → β<VAR>a : α<VAR>y : β<VAR>h : 𝓝[<] a ≠ ⊥<VAR>h' : Tendsto f (𝓝[<] a) (𝓝 y)<VAR>h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y)<VAR>this : (𝓝[<] a).NeBot<GOAL>limUnder (𝓝[<] a) f = y
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>ρ : Measure (α × β)<VAR>inst✝ : IsProbabilityMeasure ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.prod ν).fst s = μ s
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L ≃ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>minpoly K σ.toLinearMap = X ^ orderOf σ - C 1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L ≃ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>(Polynomial.aeval σ.toLinearMap) (X ^ orderOf σ - C 1) = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : CommRing L<VAR>inst✝¹ : IsDomain L<VAR>inst✝ : Algebra K L<VAR>σ : L ≃ₐ[K] L<VAR>hσ : IsOfFinOrder σ<GOAL>∀ (q : K[X]), q.Monic → (Polynomial.aeval σ.toLinearMap) q = 0 → (X ^ orderOf σ - C 1).degree ≤ q.degree
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : NonUnitalSemiring A<VAR>inst✝² : Module R A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : IsScalarTower R A A<VAR>a b x✝ : A<GOAL>(mulRight R (a * b)) x✝ = (mulRight R b ∘ₗ mulRight R a) x✝