ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D✝<VAR>inst✝⁶ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>N : ℕ∞<VAR>hg : ContDiff 𝕜 N g<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<VAR>x : E<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i<GOAL>‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D✝ : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D✝<VAR>inst✝⁶ : NormedSpace 𝕜 D✝<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s s₁ t u : Set E<VAR>g : F → G<VAR>f : E → F<VAR>n : ℕ<VAR>N : ℕ∞<VAR>hg : ContDiff 𝕜 N g<VAR>hf : ContDiff 𝕜 N f<VAR>hn : ↑n ≤ N<VAR>x : E<VAR>C D : ℝ<VAR>hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g univ (f x)‖ ≤ C<VAR>hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f univ x‖ ≤ D ^ i<GOAL>‖iteratedFDerivWithin 𝕜 n (g ∘ f) univ x‖ ≤ ↑n ! * C * D ^ n
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>F : Filter X<GOAL>ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure s
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>F : Filter X<GOAL>(∀ ⦃s : Set X⦄, s ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ F → (s ∩ s').Nonempty) ↔ ∀ s ∈ F, ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty
<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<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>unit : p 1<VAR>a : M<VAR>l : List M<VAR>ih : (∀ x ∈ l, p x) → p l.prod<VAR>base : ∀ x ∈ a :: l, p x<GOAL>p (a :: l).prod
<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<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>unit : p 1<VAR>a : M<VAR>l : List M<VAR>ih : (∀ x ∈ l, p x) → p l.prod<VAR>base : ∀ x ∈ a :: l, p x<GOAL>p (a * l.prod)
<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<VAR>p : M → Prop<VAR>hom : ∀ (a b : M), p a → p b → p (a * b)<VAR>unit : p 1<VAR>a : M<VAR>l : List M<VAR>ih : (∀ x ∈ l, p x) → p l.prod<VAR>base : p a ∧ ∀ a ∈ l, p a<GOAL>p (a * l.prod)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : CommRing S<VAR>inst✝¹⁵ : IsDomain R<VAR>inst✝¹⁴ : Algebra R S<VAR>K : Type u_3<VAR>L✝ : Type u_4<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Algebra R K<VAR>inst✝¹¹ : IsFractionRing R K<VAR>inst✝¹⁰ : CommRing L✝<VAR>inst✝⁹ : Nontrivial L✝<VAR>inst✝⁸ : Algebra R L✝<VAR>inst✝⁷ : Algebra S L✝<VAR>inst✝⁶ : Algebra K L✝<VAR>inst✝⁵ : IsScalarTower R K L✝<VAR>inst✝⁴ : IsScalarTower R S L✝<VAR>inst✝³ : IsIntegrallyClosed R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : IsScalarTower R K S<VAR>s : S<VAR>hs : IsIntegral R s<VAR>L : Type u_2 := FractionRing S<GOAL>minpoly K s = map (algebraMap R K) (minpoly R s)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>υ : Type u_6<VAR>f : σ → MvPolynomial τ R<VAR>g : τ → MvPolynomial υ R<VAR>φ : MvPolynomial σ R<GOAL>(bind₁ g) ((bind₁ f) φ) = (bind₁ fun i => (bind₁ g) (f i)) φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>G : Type u_6<VAR>H : Type u_7<VAR>F : Type u_8<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : CommGroup H<VAR>φ : G →* H<VAR>ψ : M →* G<VAR>x✝ : M<GOAL>(φ.comp ψ⁻¹) x✝ = (φ.comp ψ)⁻¹ x✝
<VAR>a b c d m n e : ℤ<VAR>he : b = a * e<VAR>f : ℤ<VAR>hf : d = c * f<GOAL>b * d = a * c * (e * f)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : PushoutI φ →* K<VAR>i : ι<GOAL>((fun i => f.comp (of i), f.comp (base φ)).1 i).comp (φ i) = (fun i => f.comp (of i), f.comp (base φ)).2
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>x✝ : PushoutI φ →* K<GOAL>∀ (i : ι), ((fun f => lift (↑f).1 (↑f).2 ⋯) ((fun f => ⟨(fun i => f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (of i) = x✝.comp (of i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>x✝ : PushoutI φ →* K<GOAL>((fun f => lift (↑f).1 (↑f).2 ⋯) ((fun f => ⟨(fun i => f.comp (of i), f.comp (base φ)), ⋯⟩) x✝)).comp (base φ) = x✝.comp (base φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>x✝ : { f // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }<VAR>fst✝ : (i : ι) → G i →* K<VAR>snd✝ : H →* K<VAR>property✝ : ∀ (i : ι), ((fst✝, snd✝).1 i).comp (φ i) = (fst✝, snd✝).2<GOAL>(fun f => ⟨(fun i => f.comp (of i), f.comp (base φ)), ⋯⟩) ((fun f => lift (↑f).1 (↑f).2 ⋯) ⟨(fst✝, snd✝), property✝⟩) = ⟨(fst✝, snd✝), property✝⟩
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝³ : CommSemiring T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x : R<GOAL>x ∈ localizationLocalizationSubmodule M N ↔ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
<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>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝³ : CommSemiring T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x : R<GOAL>(∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) ↔ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z
<VAR>n m : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ last n<VAR>hj : j ≠ last n<GOAL>i.castPred hi = j.castPred hj ↔ i = j
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddTorsor G P<VAR>inhabited_h : Inhabited P<GOAL>Subsingleton G ↔ Subsingleton P
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>X Y : Ω → E<VAR>hXY : X =ᶠ[ae ℙ] Y<GOAL>pdf X ℙ μ = pdf Y ℙ μ
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>x : E<GOAL>x ∈ ker (id - p.subtype ∘ₗ f) ↔ x ∈ p
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>f : E →ₗ[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>x : E<GOAL>x = ↑(f x) ↔ x ∈ p
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>|a| ≤ 1 ↔ a * a ≤ 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : 0 < G.dist u v<GOAL>Set.univ.Nonempty
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>h : 0 < sInf (Set.range Walk.length)<GOAL>Set.univ.Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K : Set X<VAR>hK : IsCompact K<GOAL>(𝓝ˢ K).lift' closure = 𝓝ˢ K
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K : Set X<VAR>hK : IsCompact K<VAR>U : Set X<VAR>hU : U ∈ 𝓝ˢ K<GOAL>U ∈ (𝓝ˢ K).lift' closure
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K : Set X<VAR>hK : IsCompact K<VAR>U : Set X<VAR>hU : U ∈ 𝓝ˢ K<VAR>V : Set X<VAR>hVo : IsOpen V<VAR>hKV : K ⊆ V<VAR>hVU : closure V ⊆ U<GOAL>U ∈ (𝓝ˢ K).lift' closure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>s : ι → ℝ≥0∞<VAR>inst✝ : Nonempty ι<GOAL>a + iSup s = ⨆ b, a + s b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>s : ι → ℝ≥0∞<VAR>inst✝ : Nonempty ι<GOAL>⨆ b, s b + a = ⨆ b, a + s b
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>n : ℕ<GOAL>(C x * X).coeff n = if n = 1 then x else 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.PosDef<VAR>inst✝ : Invertible D<GOAL>(fromBlocks A B Bᴴ D).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>𝕜 : Type u_5<VAR>inst✝⁷ : CommRing 𝕜<VAR>inst✝⁶ : PartialOrder 𝕜<VAR>inst✝⁵ : StarRing 𝕜<VAR>inst✝⁴ : StarOrderedRing 𝕜<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>A : Matrix m m 𝕜<VAR>B : Matrix m n 𝕜<VAR>D : Matrix n n 𝕜<VAR>hD : D.PosDef<VAR>inst✝ : Invertible D<GOAL>(fromBlocks D Bᴴ B A).PosSemidef ↔ (A - B * D⁻¹ * Bᴴ).PosSemidef
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>s✝ t r✝ : Set α<VAR>s : ι → Set α<VAR>h : Pairwise (Disjoint on s)<VAR>i : ι<VAR>r : Set α<GOAL>↑(Sigma.mk i ⁻¹' (⇑(sigmaSet h) ⁻¹' r)) = r ∩ s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>⨆ i, (μ.restrict (spanningSets μ i)) s = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s✝ t : Set α<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<GOAL>⨆ i, (μ.restrict (spanningSets μ i)) s = ⨆ i, (μ.restrict (spanningSets μ i)) (toMeasurable μ s)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>V V₀ V₁ V₂ : Coalgebra F<VAR>f : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<VAR>h : V₀.V ≅ V₁.V<VAR>w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝<GOAL>V₁.str ≫ F.map h.inv = h.inv ≫ V₀.str
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>V V₀ V₁ V₂ : Coalgebra F<VAR>f : V₀ ⟶ V₁<VAR>g : V₁ ⟶ V₂<VAR>h : V₀.V ≅ V₁.V<VAR>w : autoParam (V₀.str ≫ F.map h.hom = h.hom ≫ V₁.str) _auto✝<GOAL>V₀.str ≫ F.map (h.hom ≫ h.inv) = V₀.str
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : NonUnitalSeminormedRing α<VAR>a b : α<GOAL>‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha✝ : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>r : R<VAR>h_spec : spectrum R a ⊆ {r}<VAR>ha : autoParam (p a) _auto✝<GOAL>a = (algebraMap R A) r
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<VAR>s : Set ↑Γ(X, ⊤)<GOAL>⇑X.isoSpec.hom.val.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<VAR>s : Set ↑Γ(X, ⊤)<GOAL>Function.Surjective ⇑X.isoSpec.hom.val.base
<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 : α<GOAL>a⁻¹ ^ 0 = (a ^ 0)⁻¹
<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 : α<VAR>n : ℕ<GOAL>a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>f : E → F<VAR>s : Set (E →L[𝕜] F)<VAR>x : E<GOAL>fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : Forall₂ R l₁.reverse l₂.reverse<GOAL>Forall₂ R l₁ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>l₁ : List α<VAR>l₂ : List β<VAR>h : Forall₂ R l₁.reverse l₂.reverse<GOAL>Forall₂ R l₁.reverse.reverse l₂.reverse.reverse
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>z : ProjectiveSpectrum 𝒜<GOAL>z ∈ ↑(basicOpen 𝒜 f) ↔ z ∈ ↑(⨆ i, basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>z : ProjectiveSpectrum 𝒜<GOAL>f ∉ z.asHomogeneousIdeal ↔ ∃ u ∈ Set.range fun i => basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f), z ∈ u
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ x ∈ p
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>p q : Submodule R E<VAR>S : Type u_5<VAR>inst✝² : Semiring S<VAR>M : Type u_6<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module S M<VAR>m : Submodule S M<VAR>h : IsCompl p q<VAR>x : E<GOAL>((p.prodEquivOfIsCompl q h).symm x).2 = 0 ↔ (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>F : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : IsScalarTower ℝ 𝕜 F<VAR>fr : F →L[ℝ] ℝ<VAR>x : F<VAR>lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'<VAR>h : ¬lm x = 0<GOAL>‖lm x‖ ≤ ‖fr‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>F : Type u_2<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : IsScalarTower ℝ 𝕜 F<VAR>fr : F →L[ℝ] ℝ<VAR>x : F<VAR>lm : F →ₗ[𝕜] 𝕜 := (↑fr).extendTo𝕜'<VAR>h : ¬lm x = 0<GOAL>‖lm x‖ ^ 2 ≤ ‖lm x‖ * (‖fr‖ * ‖x‖)
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>b ≤ a⁻¹ * c ↔ a * b ≤ c
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a✝ b✝ a b c : α<VAR>l₁ l₂ : List α<GOAL>Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>U : (Matrix m m 𝔸)ˣ<VAR>A : Matrix m m 𝔸<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>exp 𝕂 (↑U * A * ↑U⁻¹) = ↑U * exp 𝕂 A * ↑U⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<GOAL>nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc : c ≤ a % c + b % c<GOAL>(a + b) % c + c = a % c + b % c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(x ~ᵢ y) ↔ closure {x} = closure {y}
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactorsList<GOAL>p ∣ n
<VAR>p : ℕ<VAR>h : p ∈ primeFactorsList 0<GOAL>p ∣ 0
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactorsList<VAR>hn : n > 0<GOAL>p ∣ n
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>ha : a ≤ c<GOAL>a ∆ b = c ↔ c \ a = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>ha : a ≤ c<GOAL>a ∆ b = c ↔ a ∆ c = b
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u a : Finset α<VAR>r : ℕ<VAR>huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜<GOAL>u = ∅
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>u a✝ : Finset α<VAR>r : ℕ<VAR>huv : ∀ x ∈ u, ∃ y ∈ ∅, IsCompressed (u.erase x) (∅.erase y) 𝒜<VAR>a : α<VAR>ha : a ∈ u<GOAL>False
<VAR>m n✝ n : ℕ<GOAL>¬2 ∣ 2 * n + 1
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R✝ : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>a a' a₁✝ a₂✝ a₃ b b' b₁ b₂ b₃ c c₁ c₂ : R✝<VAR>R : Type u_2<VAR>inst✝ : Ring R<VAR>a₁ a₂ : R<GOAL>-(a₁ + a₂) = -a₁ + -a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>la : Filter α<VAR>pa : ι → Prop<VAR>sa : ι → Set α<VAR>lb : Filter β<VAR>pb : ι' → Prop<VAR>sb : ι' → Set β<VAR>f : α → β<VAR>r : α → α → Prop<GOAL>(∃ t ∈ la, t ×ˢ t ⊆ {x | (fun x => r x.1 x.2) x}) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : x ∈ Icc ↑a ↑b<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b : Subtype p<VAR>hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x<VAR>x : α<VAR>hx : ↑a ≤ x ∧ x ≤ ↑b<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η) a) s = ((Kernel.sum fun n => Kernel.sum fun m => κ.seq n ⊗ₖ η.seq m) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s✝ : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η) a) s = ∑' (n : ℕ) (n_1 : ℕ), ((κ.seq n ⊗ₖ η.seq n_1) a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>c : β<VAR>h : c ≠ 0<GOAL>u ~[l] const α c ↔ Tendsto u l (𝓝 c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>c : β<VAR>h : c ≠ 0<GOAL>Tendsto (u - fun x => c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasLeftHomology<VAR>inst✝² : S₂.HasLeftHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>F.map (leftHomologyMap φ) ≫ (S₂.mapLeftHomologyIso F).inv = (S₁.mapLeftHomologyIso F).inv ≫ leftHomologyMap (F.mapShortComplex.map φ)
<VAR>α✝ β : Type u<VAR>c✝ : Cardinal.{?u.232416}<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<GOAL>c ≤ #↑s ↔ ∃ p ⊆ s, #↑p = c
<VAR>α✝ β : Type u<VAR>c✝ : Cardinal.{?u.232416}<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<GOAL>(∃ p, #↑p = c) ↔ ∃ s_1, #↑(Subtype.val '' s_1) = c
<VAR>α✝ β : Type u<VAR>c✝ : Cardinal.{?u.232416}<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<GOAL>∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c
<VAR>α✝ β : Type u<VAR>c✝ : Cardinal.{?u.232416}<VAR>c : Cardinal.{u}<VAR>α : Type u<VAR>s : Set α<VAR>t : Set ↑s<GOAL>#↑t = c ↔ #↑(Subtype.val '' t) = c