ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>f : α → β<GOAL>(map (fun x => x) l).zip (map f l) = l.zip (map f l)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>F : DirectLimit G f ↪[L] P<VAR>x✝ : DirectLimit G f<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>((fun i => F.comp (of L ι G f i)) j) ((f i j hij) x) = ((fun i => F.comp (of L ι G f i)) i) x
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>F : DirectLimit G f ↪[L] P<VAR>x✝ : DirectLimit G f<VAR>i : ι<VAR>x : G i<GOAL>F ((of L ι G f i) x) = (lift L ι G f (fun i => F.comp (of L ι G f i)) ⋯) ((of L ι G f i) x)
<VAR>L : Language<VAR>ι : Type v<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁴ : (i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>inst✝³ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : Nonempty ι<VAR>P : Type u₁<VAR>inst✝ : L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>F : DirectLimit G f ↪[L] P<VAR>x✝ : DirectLimit G f<VAR>i : ι<VAR>x : G i<GOAL>F ((of L ι G f i) x) = (F.comp (of L ι G f i)) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsPathConnected (⇑h.symm '' s) ↔ IsPathConnected s
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y
<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>q : R[X]<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f ((fun a => eval a q) '' spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f (eval x q)) a = cfc f ((aeval a) q)
<VAR>V✝ : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V✝<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>p.support ⊆ (p.append q).support
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>0 ≤ z ↔ 0 ≤ re z ∧ im z = 0
<VAR>ι✝ : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → ℝ → E<VAR>bound : ℝ → ℝ<VAR>hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n => F n x) l (𝓝 (f x))<GOAL>Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))
<VAR>ι✝ : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F✝ : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f : ℝ → E<VAR>μ : Measure ℝ<VAR>ι : Type u_5<VAR>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>F : ι → ℝ → E<VAR>bound : ℝ → ℝ<VAR>hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<VAR>h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun n => F n x) l (𝓝 (f x))<GOAL>Tendsto (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g g' : G<VAR>hg : g ∈ N<VAR>hg' : g' ∈ N<VAR>hc : IsConj g g'<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<GOAL>normalClosure {⟨g', hg'⟩} = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<GOAL>normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<GOAL>normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<VAR>hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)<GOAL>normalClosure {⟨c * g * c⁻¹, hg'⟩} = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<VAR>hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)<GOAL>map (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) ⊤ ≤ normalClosure {⟨c * g * c⁻¹, hg'⟩}
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<VAR>hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)<GOAL>{⟨g, hg⟩} ⊆ ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩}))
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<VAR>hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)<GOAL>⟨g, hg⟩ ∈ comap (((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h) (normalClosure {⟨c * g * c⁻¹, hg'⟩})
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N✝ : Type u_5<VAR>inst✝ : Group N✝<VAR>N : Subgroup G<VAR>hn : N.Normal<VAR>g : G<VAR>hg : g ∈ N<VAR>ht : normalClosure {⟨g, hg⟩} = ⊤<VAR>c : G<VAR>hg' : c * g * c⁻¹ ∈ N<VAR>hc : IsConj g (c * g * c⁻¹)<VAR>h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N<VAR>hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).restrict N).codRestrict N h)<GOAL>⟨c * g * c⁻¹, ⋯⟩ ∈ normalClosure {⟨c * g * c⁻¹, hg'⟩}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<GOAL>(Ideal.homogeneousCore 𝒜 I).toIdeal.IsPrime
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<GOAL>(Ideal.homogeneousCore 𝒜 I).toSubmodule ≠ ⊤
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<GOAL>∀ {x y : A}, Homogeneous 𝒜 x → Homogeneous 𝒜 y → x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule → x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<VAR>x y : A<VAR>hx : Homogeneous 𝒜 x<VAR>hy : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule<GOAL>x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<VAR>x y : A<VAR>hx : Homogeneous 𝒜 x<VAR>hy : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule<VAR>H : x ∈ I ∨ y ∈ I<GOAL>x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule ∨ y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<VAR>x y : A<VAR>hx : Homogeneous 𝒜 x<VAR>hy : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule<VAR>H : x ∈ I ∨ y ∈ I<GOAL>x ∈ I → x ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<VAR>x y : A<VAR>hx : Homogeneous 𝒜 x<VAR>hy : Homogeneous 𝒜 y<VAR>hxy : x * y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule<VAR>H : x ∈ I ∨ y ∈ I<GOAL>y ∈ I → y ∈ (Ideal.homogeneousCore 𝒜 I).toSubmodule
<VAR>d : ℕ<VAR>a b : ℤ√↑d<VAR>ha : a.Nonneg<VAR>hb : b.Nonneg<GOAL>(a + b).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := ↑y } + { re := ↑z, im := ↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>({ re := ↑x, im := ↑y } + { re := ↑z, im := -↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } + { re := ↑z, im := ↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } + { re := ↑z, im := -↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := ↑x, im := -↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := ↑x, im := -↑y } + { re := -↑z, im := ↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := ↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } + { re := ↑z, im := ↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := ↑z, im := -↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } + { re := ↑z, im := -↑w }).Nonneg
<VAR>d x y : ℕ<VAR>ha : { re := -↑x, im := ↑y }.Nonneg<VAR>z w : ℕ<VAR>hb : { re := -↑z, im := ↑w }.Nonneg<GOAL>({ re := -↑x, im := ↑y } + { re := -↑z, im := ↑w }).Nonneg
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>IsSquare a ↔ a ^ (p / 2) = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>(∃ y, y ^ 2 = Units.mk0 a ha) ↔ IsSquare a
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>ha : a ≠ 0<GOAL>(∃ y, ↑y * ↑y = a) ↔ IsSquare a
<VAR>ι : Sort u_1<VAR>inst✝ : IsEmpty ι<VAR>f : ι → ℕ<GOAL>iInf f = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : MulOneClass G<VAR>x y : k<GOAL>{ toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun (x * y) = { toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun x * { toFun := (↑__src✝).toFun, map_one' := ⋯ }.toFun y
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>-(↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 3 + 36 * (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) - 216 * (↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)) = ↑C.u⁻¹ ^ 6 * (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f ⊤ μ<VAR>hmeas : StronglyMeasurable f<GOAL>∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f ⊤ μ<VAR>hmeas : StronglyMeasurable f<VAR>hbdd : eLpNormEssSup f μ < ⊤<GOAL>∃ M, eLpNormEssSup ({x | M ≤ ↑‖f x‖₊}.indicator f) μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f ⊤ μ<VAR>hmeas : StronglyMeasurable f<VAR>hbdd : eLpNormEssSup f μ < ⊤<GOAL>eLpNormEssSup ({x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}.indicator f) μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f ⊤ μ<VAR>hmeas : StronglyMeasurable f<VAR>hbdd : eLpNormEssSup f μ < ⊤<GOAL>eLpNormEssSup f (μ.restrict {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>p : ℝ≥0∞<VAR>f : α → β<VAR>hf : Memℒp f ⊤ μ<VAR>hmeas : StronglyMeasurable f<VAR>hbdd : eLpNormEssSup f μ < ⊤<GOAL>MeasurableSet {x | (eLpNorm f ⊤ μ + 1).toReal ≤ ↑‖f x‖₊}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁ w₂ : ι → k<VAR>p : ι → V<VAR>s : Finset V<VAR>hp : AffineIndependent k Subtype.val<VAR>w : V → k<VAR>hw₀ : ∑ x ∈ s, w x = 0<VAR>hw₁ : ∑ x ∈ s, w x • x = 0<GOAL>∀ x ∈ s, w x = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>w✝ w₁ w₂ : ι → k<VAR>p : ι → V<VAR>s : Finset V<VAR>hp : AffineIndependent k Subtype.val<VAR>w : V → k<VAR>hw₀ : ∑ x ∈ s.attach, w ↑x = 0<VAR>hw₁ : ∑ x ∈ s.attach, w ↑x • ↑x = 0<GOAL>∀ x ∈ s, w x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : OrderedAddCommMonoid β<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : SMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>c x : E<VAR>hx : x ∈ (fun z => c + z) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun z => c + z) ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : CompleteSpace F<VAR>μ : Measure 𝕜<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsNegInvariant<VAR>hcf : HasCompactSupport f₀<VAR>hf : ContDiff 𝕜 1 f₀<VAR>hg : LocallyIntegrable g₀ μ<VAR>x₀ : 𝕜<GOAL>HasDerivAt (f₀ ⋆[L, μ] g₀) ((deriv f₀ ⋆[L, μ] g₀) x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedAddCommGroup E''<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace 𝕜 E'<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝³ : CompleteSpace F<VAR>μ : Measure 𝕜<VAR>inst✝² : μ.IsAddLeftInvariant<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : μ.IsNegInvariant<VAR>hcf : HasCompactSupport f₀<VAR>hf : ContDiff 𝕜 1 f₀<VAR>hg : LocallyIntegrable g₀ μ<VAR>x₀ : 𝕜<GOAL>HasDerivAt (g₀ ⋆[L.flip, μ] f₀) ((g₀ ⋆[L.flip, μ] deriv f₀) x₀) x₀
<VAR>m : ℕ<VAR>l : List ℕ<VAR>i : Fin l.length<GOAL>(unbeta l).beta ↑i = l.get i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<GOAL>∃ x ∈ s, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>h : ∀ x ∈ s, ¬ClusterPt x f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>h : ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen i) ∧ iᶜ ∈ f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<GOAL>∃ ι U, (∀ (i : ι), IsOpen (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Finset ↑s<VAR>ht : s ⊆ ⋃ i ∈ t, U i<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Finset ↑s<VAR>ht : s ⊆ ⋃ i ∈ t, U i<GOAL>sᶜ ∈ f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Finset ↑s<VAR>ht : s ⊆ ⋃ i ∈ t, U i<GOAL>⋂ i ∈ t, (U i)ᶜ ⊆ sᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>hfs : f ≤ 𝓟 s<VAR>U : ↑s → Set X<VAR>hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen (U x)<VAR>hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f<VAR>t : Finset ↑s<VAR>ht : s ⊆ ⋃ i ∈ t, U i<GOAL>s ⊆ ⋃ i ∈ t, (U i)ᶜᶜ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>m : ℕ<GOAL>preNormEDS b c d (2 * (↑m + 2) + 1) = (preNormEDS b c d (↑m + 4) * preNormEDS b c d (↑m + 2) ^ 3 * if Even m then b else 1) - preNormEDS b c d (↑m + 1) * preNormEDS b c d (↑m + 3) ^ 3 * if Even m then 1 else b
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<GOAL>|a - b| < 1
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<VAR>this : a < ↑⌊a⌋ + 1<GOAL>|a - b| < 1
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<VAR>this✝ : a < ↑⌊a⌋ + 1<VAR>this : b < ↑⌊b⌋ + 1<GOAL>|a - b| < 1
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α✝<VAR>inst✝² : FloorRing α✝<VAR>z : ℤ<VAR>a✝ : α✝<VAR>α : Type u_4<VAR>inst✝¹ : LinearOrderedCommRing α<VAR>inst✝ : FloorRing α<VAR>a b : α<VAR>h : ⌊a⌋ = ⌊b⌋<VAR>this✝¹ : a < ↑⌊a⌋ + 1<VAR>this✝ : b < ↑⌊b⌋ + 1<VAR>this : ↑⌊a⌋ = ↑⌊b⌋<GOAL>|a - b| < 1