ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))<VAR>this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g<GOAL>f = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))<VAR>this : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g<VAR>x✝ : Multiplicative (α →₀ M)<GOAL>f x✝ = g x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H✝ : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : MulOneClass N<VAR>f g : Multiplicative (α →₀ M) →* N<VAR>H : ∀ (x : α) (y : M), f (Multiplicative.ofAdd (single x y)) = g (Multiplicative.ofAdd (single x y))<VAR>this : ∀ (x : α →₀ M), (MonoidHom.toAdditive'' f) x = (MonoidHom.toAdditive'' g) x<VAR>x✝ : Multiplicative (α →₀ M)<GOAL>f x✝ = g x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a ⊔ b) \ a = b \ a
<VAR>a b m n p : ℕ<GOAL>a.factorizationLCMLeft b ∣ a
<VAR>b m n p : ℕ<GOAL>factorizationLCMLeft 0 b ∣ 0
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<GOAL>a.factorizationLCMLeft b ∣ a
<VAR>a m n p : ℕ<VAR>ha : a ≠ 0<GOAL>a.factorizationLCMLeft 0 ∣ a
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMLeft b ∣ a
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMLeft b ∣ a.factorization.prod fun x x_1 => x ^ x_1
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorizationLCMLeft b ∣ ∏ x ∈ (a.lcm b).factorization.support, x ^ a.factorization x
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.factorization.support ⊆ (a.lcm b).factorization.support
<VAR>a b m n p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<GOAL>IntegrableOn f (iUnion s) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<GOAL>∑' (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ < ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<VAR>B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)<GOAL>∑' (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ < ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<VAR>B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)<GOAL>∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<VAR>B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)<VAR>S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩<GOAL>∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<VAR>B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)<VAR>S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩<VAR>S'' : ∑' (a : ι), ↑⟨∫ (x : X) in s a, ↑‖f x‖₊ ∂μ, ⋯⟩ = ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ↑‖f x‖₊ ∂μ, ⋯⟩)<GOAL>∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝¹ : Countable ι<VAR>μ : Measure X<VAR>inst✝ : NormedAddCommGroup E<VAR>f : X → E<VAR>s : ι → Set X<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>hi : ∀ (i : ι), IntegrableOn f (s i) μ<VAR>h : Summable fun i => ∫ (x : X) in s i, ‖f x‖ ∂μ<VAR>B : ∀ (i : ι), ∫⁻ (a : X) in s i, ↑‖f a‖₊ ∂μ = ENNReal.ofReal (∫ (a : X) in s i, ↑‖f a‖₊ ∂μ)<VAR>S' : Summable fun i => ⟨∫ (x : X) in s i, ↑‖f x‖₊ ∂μ, ⋯⟩<VAR>S'' : ∑' (a : ι), ENNReal.ofReal (∫ (x : X) in s a, ‖f x‖ ∂μ) = ENNReal.ofReal ↑(∑' (b : ι), ⟨∫ (x : X) in s b, ‖f x‖ ∂μ, ⋯⟩)<GOAL>∑' (b : ι), ENNReal.ofReal (∫ (a : X) in s b, ↑‖f a‖₊ ∂μ) < ⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : ℝ[X]<VAR>a✝ : X<GOAL>((g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound) a✝ = ↑((Polynomial.aeval f) g) a✝
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : ℝ[X]<VAR>a✝ : X<GOAL>Polynomial.eval (↑((↑f).attachBound a✝)) g = Polynomial.eval (↑f a✝) g
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>inst✝³ : Fintype ↑G.edgeSet<VAR>inst✝² : Fintype ↑G₁.edgeSet<VAR>inst✝¹ : Fintype ↑G₂.edgeSet<VAR>inst✝ : Fintype V<GOAL>G.edgeFinset.card ≤ (Fintype.card V).choose 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<GOAL>QuasiSober α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<GOAL>∀ {S : Set α}, IsIrreducible S → IsClosed S → ∃ x, IsGenericPoint x S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<GOAL>∃ x, IsGenericPoint x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<GOAL>∃ x, IsGenericPoint x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this : QuasiSober ↑U<GOAL>∃ x, IsGenericPoint x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this : QuasiSober ↑U<VAR>H : IsPreirreducible (Subtype.val ⁻¹' t)<GOAL>∃ x, IsGenericPoint x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<GOAL>∃ x, IsGenericPoint x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<GOAL>IsGenericPoint (↑H.genericPoint) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' closure t<GOAL>IsGenericPoint (↑H.genericPoint) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>IsGenericPoint (↑H.genericPoint) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>closure {↑H.genericPoint} ≤ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>t ≤ closure {↑H.genericPoint}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>t ≤ closure (Subtype.val '' closure (Subtype.val ⁻¹' t))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>t ∩ ↑⟨U, hU⟩ ⊆ Subtype.val '' closure (Subtype.val ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>S : Set (Set α)<VAR>hS : ∀ (s : ↑S), IsOpen ↑s<VAR>hS' : ∀ (s : ↑S), QuasiSober ↑↑s<VAR>hS'' : ⋃₀ S = ⊤<VAR>t : Set α<VAR>h : IsIrreducible t<VAR>h' : IsClosed t<VAR>x : α<VAR>hx : x ∈ t<VAR>U : Set α<VAR>hU : U ∈ S<VAR>hU' : x ∈ U<VAR>this✝ : QuasiSober ↑U<VAR>H : IsIrreducible (Subtype.val ⁻¹' t)<VAR>this : H.genericPoint ∈ Subtype.val ⁻¹' t<GOAL>Subtype.val '' (Subtype.val ⁻¹' t) ⊆ Subtype.val '' closure (Subtype.val ⁻¹' t)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>X.toΓSpecSheafedSpace.c.app (op (basicOpen r)) = X.toΓSpecCApp r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<GOAL>sup f = lsub f ∨ succ (sup f) = lsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f = lsub f<GOAL>sup f = lsub f ∨ succ (sup f) = lsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>h : sup f < lsub f<GOAL>sup f = lsub f ∨ succ (sup f) = lsub f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>(p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>(p.sum fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>∀ b ∈ p.support, b ≠ p.natDegree → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) b (p.coeff b) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>p.natDegree ∉ p.support → (fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hqd0 : q.natDegree ≠ 0<GOAL>(fun a b => (C b * q ^ a).coeff (p.natDegree * q.natDegree)) p.natDegree (p.coeff p.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
<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>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>g : F →ₗᵢ[𝕜] G<VAR>hf : ContDiff 𝕜 n f<VAR>x : E<VAR>i : ℕ<VAR>hi : ↑i ≤ n<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>inst✝ : Field k<VAR>f : k⟦X⟧<VAR>hf : f ≠ 0<GOAL>↑f.Unit_of_divided_by_X_pow_order = divided_by_X_pow_order hf
<VAR>n : ℕ<GOAL>↑n ∈ slitPlane ↔ n ≠ 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k✝ l : ℕ+<VAR>f : Mˣ →* Nˣ<VAR>k : ℕ+<VAR>ζ : Mˣ<VAR>h : ζ ∈ ↑(rootsOfUnity k M)<GOAL>f ζ ∈ rootsOfUnity k N
<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>ι₁ : Type u_3<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>p₁ : ι₁ → P<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_4<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>p₂ : ι₂ → P<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>⟪(s₁.weightedVSub p₁) w₁, (s₂.weightedVSub p₂) w₂⟫_ℝ = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
<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>ι₁ : Type u_3<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>p₁ : ι₁ → P<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_4<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>p₂ : ι₂ → P<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>(-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ * ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖)) / 2 = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
<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>ι₁ : Type u_3<VAR>s₁ : Finset ι₁<VAR>w₁ : ι₁ → ℝ<VAR>p₁ : ι₁ → P<VAR>h₁ : ∑ i ∈ s₁, w₁ i = 0<VAR>ι₂ : Type u_4<VAR>s₂ : Finset ι₂<VAR>w₂ : ι₂ → ℝ<VAR>p₂ : ι₂ → P<VAR>h₂ : ∑ i ∈ s₂, w₂ i = 0<GOAL>(-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero M<VAR>l : List (ι →₀ M)<VAR>x : ι<GOAL>x ∈ foldr (fun x x_1 => x.support ⊔ x_1) ∅ l ↔ ∃ f ∈ l, x ∈ f.support
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero M<VAR>l : List (ι →₀ M)<VAR>x : ι<GOAL>x ∈ foldr (fun x x_1 => x.support ∪ x_1) ∅ l ↔ ∃ f ∈ l, f x ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Monoid α<VAR>n✝ n : ℕ<VAR>a : α<GOAL>IsSquare ((a * a) ^ n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : β × γ → δ<VAR>g : α → β<VAR>h : α → γ<VAR>x : α<VAR>s : Set α<VAR>y : β × γ<VAR>hf : ContinuousAt f (g x, h x)<VAR>hg : ContinuousWithinAt g s x<VAR>hh : ContinuousWithinAt h s x<VAR>e : (g x, h x) = y<GOAL>ContinuousWithinAt (fun x => f (g x, h x)) s x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<GOAL>∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<VAR>pderiv_true_x : (pderiv true) x = 1<GOAL>∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>x : MvPolynomial Bool R := MvPolynomial.X true<VAR>y : MvPolynomial Bool R := MvPolynomial.X false<VAR>pderiv_true_x : (pderiv true) x = 1<VAR>pderiv_true_y : (pderiv true) y = 0<GOAL>∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • X
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>(C r).vars = ∅
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>c : α<VAR>hc : c ∈ (a :: b :: l).getLast?<GOAL>(a :: b :: l).dropLast ++ [c] = a :: b :: l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a b : α<VAR>l : List α<VAR>c : α<VAR>hc : c ∈ (b :: l).getLast?<GOAL>(a :: b :: l).dropLast ++ [c] = a :: b :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>p : (a : β) → a ∈ map f s → Prop<VAR>h : ∀ (x : α) (H : x ∈ s), p (f x) ⋯<VAR>x : β<VAR>hx : x ∈ map f s<GOAL>p x hx
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s✝ : Finset α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>p : (a : β) → a ∈ map f s → Prop<VAR>h : ∀ (x : α) (H : x ∈ s), p (f x) ⋯<VAR>y : α<VAR>hy : y ∈ s<VAR>hx : f y ∈ map f s<GOAL>p (f y) hx
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂
<VAR>u v m n : ℤ<GOAL>¬n % 2 = 0 ↔ n % 2 = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : Set P<VAR>p : P<VAR>h : p ∈ affineSpan k s<GOAL>Coplanar k (insert p s) ↔ Coplanar k s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>f : ι → α<VAR>g : ι → β<VAR>s : Set ι<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>(∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → f i • g j + f j • g i ≤ f i • g i + f j • g j) ↔ ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>hf : f.LimZero<VAR>hg : g.LimZero<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abv (↑f j) < ε / 2 ∧ abv (↑g j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : abv (↑f j) < ε / 2<VAR>H₂ : abv (↑g j) < ε / 2<GOAL>abv (↑(f + g) j) < ε
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<GOAL>s.FG
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<GOAL>∃ S, S.Finite ∧ (closure L).toFun S = s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Finset N<VAR>h : (closure L).toFun ↑t = Substructure.map f.toHom s<GOAL>(closure L).toFun (⇑f ⁻¹' ↑t) = s