ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ s t : Set X<VAR>hs : IsClosed s<VAR>h : s ⊆ t<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcov : ⋃ n, K n = t<GOAL>IsSigmaCompact s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ s t : Set X<VAR>hs : IsClosed s<VAR>h : s ⊆ t<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcov : ⋃ n, K n = t<GOAL>⋃ n, (fun n => s ∩ K n) n = s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t✝ s t : Set X<VAR>hs : IsClosed s<VAR>h : s ⊆ t<VAR>K : ℕ → Set X<VAR>hcompact : ∀ (n : ℕ), IsCompact (K n)<VAR>hcov : ⋃ n, K n = t<GOAL>s ∩ t = s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>s : ℕ → Set α<VAR>hs : f.HasAntitoneBasis s<VAR>r : ℕ → ℕ → Prop<VAR>hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n<GOAL>∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>s : ℕ → Set α<VAR>hs : f.HasAntitoneBasis s<VAR>r : ℕ → ℕ → Prop<VAR>hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n<VAR>this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n<GOAL>∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>s : ℕ → Set α<VAR>hs : f.HasAntitoneBasis s<VAR>r : ℕ → ℕ → Prop<VAR>hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n<VAR>this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n<VAR>φ : ℕ → ℕ<VAR>hφ : ∀ (n m : ℕ), m ∈ φ '' Iio n → m < φ n ∧ r m (φ n)<GOAL>∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>s : ℕ → Set α<VAR>hs : f.HasAntitoneBasis s<VAR>r : ℕ → ℕ → Prop<VAR>hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n<VAR>this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n<VAR>φ : ℕ → ℕ<VAR>hφ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)<GOAL>∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)
<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>x : X<VAR>f : Filter X<VAR>hf : f.NeBot<VAR>x✝ : CountableInterFilter f<VAR>hfa : f ≤ 𝓟 {x}<GOAL>𝓟 {x} ≤ 𝓝 x
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>hs : Splits i f<VAR>hf0 : (map i f).degree ≠ 0<VAR>this : DecidableEq L := Classical.decEq L<VAR>hf0' : map i f = 0<GOAL>∃ x, eval₂ i x f = 0
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>f : K[X]<VAR>hs : Splits i✝ f<VAR>hf0 : (map i✝ f).degree ≠ 0<VAR>this : DecidableEq L := Classical.decEq L<VAR>hf0' : ¬map i✝ f = 0<VAR>g : L[X]<VAR>hg : Irreducible g ∧ g ∣ map i✝ f<VAR>x : L<VAR>hx : g.IsRoot x<VAR>i : L[X]<VAR>hi : map i✝ f = g * i<GOAL>eval₂ i✝ x f = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>f : StructuredArrow S T<GOAL>(f.homMk' (𝟙 f.right)).right = (eqToHom ⋯).right
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>m : Ordnode α<VAR>y : α<VAR>r : Ordnode α<VAR>hm : m.Sized<GOAL>(l.node4L x m y r).size = l.size + m.size + r.size + 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b✝ c d : G<VAR>n : ℤ<VAR>a b : G<GOAL>a * b / b = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>h : cfcₙ f a = cfcₙ g a<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<GOAL>Set.EqOn f g (σₙ R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>h : (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } = (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }<GOAL>Set.EqOn f g (σₙ R a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf✝ : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0✝ : autoParam (f✝ 0 = 0) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0✝ : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>h : (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } = (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }<VAR>this : { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } = { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }<GOAL>Set.EqOn f g (σₙ R a)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<GOAL>s.Disjoint (ndinsert a t) ↔ a ∉ s ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<GOAL>a ∉ s ∧ t.Disjoint s ↔ a ∉ s ∧ s.Disjoint t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ : ℝ≥0<VAR>hf : ∀ (b : β), AntilipschitzWith K₁ fun a => f a b<VAR>s : Set α<VAR>t : Set β<VAR>hst : IsBounded (image2 f s t)<GOAL>IsBounded s ∨ IsBounded t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ : ℝ≥0<VAR>hf : ∀ (b : β), AntilipschitzWith K₁ fun a => f a b<VAR>s : Set α<VAR>t : Set β<VAR>hst : ¬IsBounded s ∧ ¬IsBounded t<GOAL>¬IsBounded (image2 f s t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ : ℝ≥0<VAR>hf : ∀ (b : β), AntilipschitzWith K₁ fun a => f a b<VAR>s : Set α<VAR>t : Set β<VAR>hst : ¬IsBounded s ∧ ¬IsBounded t<VAR>b : β<VAR>hb : b ∈ t<GOAL>¬IsBounded (image2 f s t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f✝ : α → β<VAR>f : α → β → γ<VAR>K₁ : ℝ≥0<VAR>hf : ∀ (b : β), AntilipschitzWith K₁ fun a => f a b<VAR>s : Set α<VAR>t : Set β<VAR>hst : ¬IsBounded s ∧ ¬IsBounded t<VAR>b : β<VAR>hb : b ∈ t<VAR>this : ¬IsBounded (image2 f s {b})<GOAL>¬IsBounded (image2 f s t)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>p : Prop<GOAL>IsAtom p ↔ p
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ≅ Y<VAR>Z : C<GOAL>f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>inst✝ : IsIso f<VAR>H : P (f ≫ g)<GOAL>P g
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S T : CommRingCat<VAR>f : R ⟶ S<VAR>g : S ⟶ T<VAR>inst✝ : IsIso f<VAR>H : P (f ≫ g)<GOAL>g = comp (f ≫ g) (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom
<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>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>f : ι → α<GOAL>(type r).brange (bfamilyOfFamily' r f) = range 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>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>f : ι → α<VAR>a : α<GOAL>a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range 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>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>f : ι → α<VAR>a : α<GOAL>a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u✝ v✝ : α → 𝕜<VAR>u v φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<GOAL>IsBigOWith c l u v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u✝ v✝ : α → 𝕜<VAR>u v φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<GOAL>∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u✝ v✝ : α → 𝕜<VAR>u v φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<VAR>x : α<VAR>hx : ‖φ x‖ ≤ c<GOAL>(fun x a => ‖a‖ ≤ c * ‖v x‖) x ((φ * v) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u✝ v✝ : α → 𝕜<VAR>u v φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<VAR>x : α<VAR>hx : ‖φ x‖ ≤ c<GOAL>‖φ x * v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>u✝ v✝ : α → 𝕜<VAR>u v φ : α → R<VAR>hφ : ∀ᶠ (x : α) in l, ‖φ x‖ ≤ c<VAR>h : u =ᶠ[l] φ * v<VAR>x : α<VAR>hx : ‖φ x‖ ≤ c<GOAL>‖φ x‖ * ‖v x‖ ≤ c * ‖v x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k✝ : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>k : β → α<VAR>l : Filter β<GOAL>f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)
<VAR>x : ℝ<GOAL>cos (π / 2 - x) = sin x
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<GOAL>min x.orderTop y.orderTop ≤ (x - y).orderTop
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddGroup R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<GOAL>min x.orderTop (-y).orderTop ≤ (x + -y).orderTop
<VAR>x : ℝ<GOAL>tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)
<VAR>x : ℝ<VAR>this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)<GOAL>tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>(unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) Y✝)).one ≫ f.hom.op = (unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) X✝)).one
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>((unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) Y✝)).one ≫ f.hom.op).unop = (unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) X✝)).one.unop
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>(unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) Y✝)).mul ≫ f.hom.op = (f.hom.op ⊗ f.hom.op) ≫ (unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) X✝)).mul
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>((unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) Y✝)).mul ≫ f.hom.op).unop = ((f.hom.op ⊗ f.hom.op) ≫ (unop ((fun A => op (Comon_ToMon_OpOp_obj' C A)) X✝)).mul).unop
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<GOAL>Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<GOAL>Integrable (fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<GOAL>Integrable ((fun v => cexp (-b * ↑‖v‖ ^ 2 + c * ↑⟪w, v⟫_ℝ)) ∘ ⇑(EuclideanSpace.measurableEquiv ι).symm) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<GOAL>Integrable (fun x => cexp (-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm x‖ ^ 2) + c * ↑⟪w, (EuclideanSpace.measurableEquiv ι).symm x⟫_ℝ)) volume
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<VAR>v : ι → ℝ<GOAL>-(b * ↑‖(EuclideanSpace.measurableEquiv ι).symm v‖ ^ 2) + c * ↑⟪w, (EuclideanSpace.measurableEquiv ι).symm v⟫_ℝ = -b * ∑ i : ι, ↑(v i) ^ 2 + ∑ i : ι, c * ↑(w i) * ↑(v i)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<VAR>v : ι → ℝ<GOAL>b * ↑√(∑ x : ι, v x ^ 2) ^ 2 = ∑ x : ι, b * ↑(v x) ^ 2
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<VAR>v : ι → ℝ<GOAL>b * ↑(√(∑ x : ι, v x ^ 2) ^ 2) = ∑ x : ι, b * ↑(v x ^ 2)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<VAR>v : ι → ℝ<GOAL>b * ↑(∑ x : ι, v x ^ 2) = ∑ x : ι, b * ↑(v x ^ 2)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>inst✝³ : FiniteDimensional ℝ V<VAR>inst✝² : MeasurableSpace V<VAR>inst✝¹ : BorelSpace V<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>hb : 0 < b.re<VAR>c : ℂ<VAR>w : EuclideanSpace ℝ ι<VAR>this : MeasurePreserving (⇑(EuclideanSpace.measurableEquiv ι)) volume volume<VAR>v : ι → ℝ<GOAL>0 ≤ ∑ x : ι, v x ^ 2
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<GOAL>Antitone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Antitone f
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>min a b = if a ≤ b then a else b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ blimsup u l p<GOAL>∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : x ∈ ⨅ s ∈ l, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b<GOAL>∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p✝ : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<VAR>l : Filter β<VAR>b : ι → Set β<VAR>q : ι → Prop<VAR>hl : l.HasBasis q b<VAR>u : β → Set α<VAR>p : β → Prop<VAR>x : α<VAR>hx : ∀ i ∈ l, ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2<GOAL>∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i