ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>hz_re : z.re ≤ 0<VAR>hz_im : z.im ≤ 0<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : (-z).re ≤ 0<VAR>hz_im : (-z).im ≤ 0<GOAL>‖f (-z)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<GOAL>‖f (-z)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<GOAL>‖(f ∘ Neg.neg) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)<GOAL>‖(f ∘ Neg.neg) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)<GOAL>∃ c < 2, ∃ B, (f ∘ Neg.neg) =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>‖(f ∘ Neg.neg) ↑x‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Iio 0 ×ℂ Iio 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Iio 0 ×ℂ Iio 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ x ≤ 0, ‖f ↑x‖ ≤ C<VAR>him : ∀ x ≤ 0, ‖f (↑x * I)‖ ≤ C<VAR>z : ℂ<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<VAR>H : MapsTo Neg.neg (Ioi 0 ×ℂ Ioi 0) (Iio 0 ×ℂ Iio 0)<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>‖(f ∘ Neg.neg) (↑x * I)‖ ≤ C
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).Φ n = Polynomial.map f (W.Φ n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(X * (mapRingHom f) (W.ΨSq n) - (mapRingHom f) (W.preΨ (n + 1)) * (mapRingHom f) (W.preΨ (n - 1)) * if Even n then 1 else (mapRingHom f) W.Ψ₂Sq) = (mapRingHom f) (X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq)
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<GOAL>r = s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : { center := p, radius := r }.center ∈ affineSpan ℝ (Set.range s.points) ∧ Set.range s.points ⊆ Metric.sphere { center := p, radius := r }.center { center := p, radius := r }.radius → { center := p, radius := r } = s.circumsphere<GOAL>r = s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : Set.range s.points ⊆ Metric.sphere p r → p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>r = s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : (∀ p_1 ∈ Set.range s.points, p_1 ∈ { center := p, radius := r }) → p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>r = s.circumradius
<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>n : ℕ<VAR>s : Simplex ℝ P n<VAR>p : P<VAR>hp : p ∈ affineSpan ℝ (Set.range s.points)<VAR>r : ℝ<VAR>hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r<VAR>h : p = s.circumsphere.center ∧ r = s.circumsphere.radius<GOAL>r = s.circumradius
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroupWithOne G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x - ↑n) = f x - n • b
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg_mem : ∀ (x : X), g x ∈ Metric.closedBall 0 ‖f‖<VAR>hg : ContinuousMap.restrict s g = ↑f<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<GOAL>‖g'‖ = ‖f‖
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<GOAL>‖f‖ ≤ ‖g'‖
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<VAR>x : ↑s<GOAL>‖f x‖ ≤ ‖g'‖
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<VAR>x : ↑s<VAR>hx : f x = g' ↑x<GOAL>‖f x‖ ≤ ‖g'‖
<VAR>X : Type u<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : TietzeExtension 𝕜<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : ↑s →ᵇ E<VAR>hf : ¬‖f‖ = 0<VAR>this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)<VAR>hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖<VAR>g : C(X, E)<VAR>hg : ContinuousMap.restrict s g = ↑f<VAR>hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖<VAR>g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem<VAR>x : ↑s<VAR>hx : f x = g' ↑x<GOAL>‖g' ↑x‖ ≤ ‖g'‖
<VAR>X : TopCat<GOAL>⋯.functor = map (inclusionTopIso X).inv
<VAR>X : TopCat<GOAL>∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1
<VAR>X : TopCat<GOAL>∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y), ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯
<VAR>x : ℂ<GOAL>normSq x = abs x ^ 2
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<GOAL>𝟙 X ⊗ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : v ≠ w<GOAL>Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : v ≠ w<GOAL>(Set.univ.toFinset \ {v, w}.toFinset).card = Fintype.card V - 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : v ≠ w<GOAL>Set.univ.toFinset.card - {v, w}.toFinset.card = Fintype.card V - 2
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableEq V<VAR>v w : V<VAR>h : v ≠ w<GOAL>{v, w}.toFinset ⊆ Set.univ.toFinset
<VAR>m✝ n✝ n m : ℕ<VAR>hnm : n ≤ m<GOAL>n ! * n ^ (m - n) ≤ m !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁶ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝⁵ : TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : AddMonoid β<VAR>inst✝² : Monoid 𝕜<VAR>inst✝¹ : DistribMulAction 𝕜 β<VAR>inst✝ : ContinuousSMul 𝕜 β<VAR>hf : FinStronglyMeasurable f μ<VAR>c : 𝕜<GOAL>FinStronglyMeasurable (c • f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁶ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝⁵ : TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : AddMonoid β<VAR>inst✝² : Monoid 𝕜<VAR>inst✝¹ : DistribMulAction 𝕜 β<VAR>inst✝ : ContinuousSMul 𝕜 β<VAR>hf : FinStronglyMeasurable f μ<VAR>c : 𝕜<VAR>n : ℕ<GOAL>μ (support ↑((fun n => c • hf.approx n) n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁶ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝⁵ : TopologicalSpace β<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : AddMonoid β<VAR>inst✝² : Monoid 𝕜<VAR>inst✝¹ : DistribMulAction 𝕜 β<VAR>inst✝ : ContinuousSMul 𝕜 β<VAR>hf : FinStronglyMeasurable f μ<VAR>c : 𝕜<VAR>n : ℕ<GOAL>μ (support (c • ↑(hf.approx n))) < ⊤
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPushouts C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : Mono g<VAR>s : PushoutCocone f g<VAR>hs : IsColimit s<VAR>this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.left)<GOAL>Mono s.inl
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime (x ^ m) y
<VAR>R : Type u<VAR>I : Type v<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>s : I → R<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsCoprime x y<GOAL>IsCoprime (∏ _x ∈ range m, x) y
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<GOAL>(𝓝[>] 0)⁻¹ = atTop
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>x : ↑X<GOAL>(i.hom ≫ i.inv) x = x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>x : ↑X<GOAL>(𝟙 X) x = x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>x : ↑Y<GOAL>(i.inv ≫ i.hom) x = x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>X₁ X₂ : Type u<VAR>X Y : AlgebraCat R<VAR>i : X ≅ Y<VAR>x : ↑Y<GOAL>(𝟙 Y) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>v : Vector α (n + 1)<GOAL>a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a'✝ : α<VAR>v : Vector α (n + 1)<VAR>a' : α<VAR>v' : Vector α n<VAR>h : v = a' ::ᵥ v'<GOAL>a ∈ v.toList ↔ a = v.head ∨ a ∈ v.tail.toList
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>x y : M<VAR>H1 : (B x) y = 0<GOAL>(B y) x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I : R →+* R<VAR>B : M →ₛₗ[I] M →ₗ[R] R<VAR>H : B.IsSymm<VAR>x y : M<VAR>H1 : (B x) y = 0<GOAL>I ((B x) y) = 0
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : Function.Surjective ⇑f<GOAL>f.idealRange = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.range = ⊤<GOAL>f.idealRange = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.range = ⊤<GOAL>∃ N, ↑N = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : f.range = ⊤<GOAL>↑⊤ = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Preorder M<VAR>inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f g : ι → M<VAR>i : ι<VAR>l : List ι<VAR>ihl : (∀ i ∈ l, f i ≤ g i) → (∃ i ∈ l, f i < g i) → (map f l).prod < (map g l).prod<VAR>h₁ : ∀ i_1 ∈ i :: l, f i_1 ≤ g i_1<VAR>h₂ : ∃ i_1 ∈ i :: l, f i_1 < g i_1<GOAL>(map f (i :: l)).prod < (map g (i :: l)).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Preorder M<VAR>inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f g : ι → M<VAR>i : ι<VAR>l : List ι<VAR>ihl : (∀ i ∈ l, f i ≤ g i) → (∃ i ∈ l, f i < g i) → (map f l).prod < (map g l).prod<VAR>h₂ : ∃ i_1 ∈ i :: l, f i_1 < g i_1<VAR>h₁ : f i ≤ g i ∧ ∀ x ∈ l, f x ≤ g x<GOAL>f i * (map f l).prod < g i * (map g l).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>M₀ : Type u_6<VAR>G : Type u_7<VAR>R : Type u_8<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Preorder M<VAR>inst✝³ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝² : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>f g : ι → M<VAR>i : ι<VAR>l : List ι<VAR>ihl : (∀ i ∈ l, f i ≤ g i) → (∃ i ∈ l, f i < g i) → (map f l).prod < (map g l).prod<VAR>h₁ : f i ≤ g i ∧ ∀ x ∈ l, f x ≤ g x<VAR>h₂ : f i < g i ∨ ∃ a ∈ l, f a < g a<GOAL>f i * (map f l).prod < g i * (map g l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>γ : Type u_5<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : γ → α<GOAL>∏' (y : β), extend g f 1 y = ∏' (x : γ), f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>γ : Type u_5<VAR>g : γ → β<VAR>hg : Injective g<VAR>f : γ → α<VAR>this : mulSupport (extend g f 1) ⊆ Set.range g<GOAL>∏' (y : β), extend g f 1 y = ∏' (x : γ), f x
<VAR>θ : Angle<GOAL>Real.sin θ.toReal = θ.sin
<VAR>σ : Type u_1<VAR>f : σ → Option σ<VAR>a b c : σ<VAR>h : f a = f b<GOAL>(∃ b_1 ∈ f b, ReflTransGen (fun a b => b ∈ f a) b_1 c) ↔ ∃ b ∈ f a, ReflTransGen (fun a b => b ∈ f a) b c
<VAR>α : Type u<VAR>inst✝¹ : DecidableEq α<VAR>β : Type v<VAR>inst✝ : Fintype α<VAR>f g : Perm α<GOAL>sign (Equiv.trans f g) = sign g * sign f
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback f' (pullback.fst f g)<VAR>inst✝ : HasPullback (f' ≫ f) g<GOAL>(pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd f' (pullback.fst f g) ≫ pullback.fst f g = pullback.fst (f' ≫ f) g ≫ f'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>f' : W ⟶ X<VAR>inst✝² : HasPullback f g<VAR>inst✝¹ : HasPullback f' (pullback.fst f g)<VAR>inst✝ : HasPullback (f' ≫ f) g<GOAL>(pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) ≫ f' = pullback.fst (f' ≫ f) g ≫ f'
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>ℵ₀ ≤ o.cof ↔ o.IsLimit