ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / c ≤ b ↔ a ≤ b * c
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝² : Fintype ι<VAR>F' : ι → Type u_7<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>((fun x' => Φ x' - Φ x - Φ' (x' - x)) =o[L] fun x' => x' - x) ↔ ∀ (i : ι), (fun x' => Φ x' i - Φ x i - ((proj i).comp Φ') (x' - x)) =o[L] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝¹ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<VAR>x : E<VAR>x✝ : E × E<GOAL>0 = (fun x => c) x✝.1 - (fun x => c) x✝.2 - 0 (x✝.1 - x✝.2)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => c * x) ⁻¹' Ioo a b = Ioo (b / c) (a / c)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f✝ f : R[X]<GOAL>(Polynomial.map (of f) f).IsRoot (root f)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>span R 0 = ⊥
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<VAR>this : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<VAR>this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<VAR>this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖<VAR>m : ℝ<VAR>xm : m ∈ Ioi x<VAR>hm : Ico x m ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}<GOAL>∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<VAR>this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖<VAR>m : ℝ<VAR>xm : m ∈ Ioi x<VAR>hm : Ico x m ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 (m - x)<GOAL>x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K : Set F<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>x : ℝ<VAR>hx : DifferentiableWithinAt ℝ f (Ici x) x<VAR>this✝ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖<VAR>m : ℝ<VAR>xm : m ∈ Ioi x<VAR>hm : Ico x m ⊆ {x_1 | (fun x_2 => ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 (m - x)<VAR>this : r ∈ Ioc (r / 2) r<GOAL>x ∈ A f (derivWithin f (Ici x) x) r ε
<VAR>n d : ℕ<VAR>n_coprime_d : n.Coprime d<GOAL>(↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
<VAR>n d : ℕ<VAR>n_coprime_d : n.Coprime d<VAR>this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋<GOAL>(↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
<VAR>n d : ℕ<VAR>n_coprime_d : n.Coprime d<VAR>this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋<GOAL>(↑n % ↑d).natAbs.Coprime d
<VAR>n d : ℕ<VAR>n_coprime_d : n.Coprime d<VAR>this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋<VAR>this : d.Coprime n<GOAL>(↑n % ↑d).natAbs.Coprime d
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : Quotient ↑H.toSubmonoid ↑K<GOAL>a ≠ b → Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : Quotient ↑H.toSubmonoid ↑K<GOAL>¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K) → a = b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : Quotient ↑H.toSubmonoid ↑K<VAR>h : ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)<GOAL>a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>a b x✝ : ℝ≥0<GOAL>nndist a b ≤ x✝ ↔ max (a - b) (b - a) ≤ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>a b x✝ : ℝ≥0<GOAL>nndist a b ≤ x✝ ↔ a ≤ x✝ + b ∧ b ≤ x✝ + a
<VAR>F : Type u_1<VAR>inst✝² : Norm F<VAR>inst✝¹ : One F<VAR>inst✝ : NormOneClass F<GOAL>(fun s => riemannZeta s - 1 / (s - 1)) =O[𝓝 1] fun x => 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>I J : FractionalIdeal A⁰ K<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<GOAL>I ≤ J⁻¹ ↔ J ≤ I⁻¹
<VAR>n✝ n : ℕ<GOAL>Fintype.card (Composition n) = 2 ^ (n - 1)
<VAR>n✝ n : ℕ<GOAL>Fintype.card (Composition n) = Fintype.card (CompositionAsSet n)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : TopologicalGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : OrderedCommGroup H<VAR>inst✝ : ContinuousInv H<VAR>a : H<GOAL>Tendsto (fun a => a⁻¹) (𝓟 (Iic a)) (𝓟 (Ici a⁻¹))
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.map A.comul ≫ F.δ A.X A.X) ≫ (F.map A.counit ≫ F.η) ▷ F.obj A.X = (λ_ (F.obj A.X)).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.map A.comul ≫ F.δ A.X A.X) ≫ F.obj A.X ◁ (F.map A.counit ≫ F.η) = (ρ_ (F.obj A.X)).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.map A.comul ≫ F.δ A.X A.X) ≫ F.obj A.X ◁ (F.map A.comul ≫ F.δ A.X A.X) = (F.map A.comul ≫ F.δ A.X A.X) ≫ (F.map A.comul ≫ F.δ A.X A.X) ▷ F.obj A.X ≫ (α_ (F.obj A.X) (F.obj A.X) (F.obj A.X)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.hom ≫ F.map Y✝.counit ≫ F.η = F.map X✝.counit ≫ F.η
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X✝ Y✝ : Comon_ C<VAR>f : X✝ ⟶ Y✝<GOAL>F.map f.hom ≫ F.map Y✝.comul ≫ F.δ Y✝.X Y✝.X = (F.map X✝.comul ≫ F.δ X✝.X X✝.X) ≫ (F.map f.hom ⊗ F.map f.hom)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>r : ℝ<VAR>hr₀ : 1 < r<VAR>hr₁ : r < l<GOAL>¬Summable f
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>r : ℝ<VAR>hr₀ : 1 < r<VAR>hr₁ : r < l<GOAL>∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>f : ℕ → α<VAR>l : ℝ<VAR>hl : 1 < l<VAR>h : Tendsto (fun n => ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)<VAR>key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0<VAR>r : ℝ<VAR>hr₀ : 1 < r<VAR>hr₁ : r < l<VAR>a✝¹ : ℕ<VAR>a✝ : r ≤ ‖f (a✝¹ + 1)‖ / ‖f a✝¹‖<VAR>h₁ : ‖f a✝¹‖ ≠ 0<GOAL>r * ‖f a✝¹‖ ≤ ‖f (a✝¹ + 1)‖
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a : α<GOAL>Unbounded r (s ∩ {b | ¬r b a}) ↔ Unbounded r s
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>x ∈ LinearMap.ker (dZero A) ↔ x ∈ A.ρ.invariants
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<GOAL>(∀ (a : G), (dZero A) x a = 0 a) ↔ ∀ (g : G), (A.ρ g) x - x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>b0 : b ≠ 0<GOAL>b * a / b = a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : MulZeroClass α<VAR>P Q : Prop<VAR>inst✝¹ : Decidable P<VAR>inst✝ : Decidable Q<VAR>a b : α<GOAL>((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>ha : DifferentiableWithinAt 𝕜 a s x<GOAL>DifferentiableWithinAt 𝕜 (fun x => a x ^ 0) s x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>ha : DifferentiableWithinAt 𝕜 a s x<VAR>n : ℕ<GOAL>DifferentiableWithinAt 𝕜 (fun x => a x ^ (n + 1)) s x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : P.Ring<GOAL>(f.toAlgHom.toLinearMap - g.toAlgHom.toLinearMap) x ∈ Submodule.restrictScalars R P'.ker
<VAR>α β : Type u<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n ≤ lift.{v, u} a ↔ ↑n ≤ a
<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>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<GOAL>IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x => f (x, b)
<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>inst✝ : DiscreteTopology β<VAR>f : α × β → γ<GOAL>(∀ (y : β) (x : α), 𝓝 (f (x, y)) ≤ map (f ∘ fun a => (a, y)) (𝓝 x)) ↔ ∀ (b : β) (x : α), 𝓝 (f (x, b)) ≤ map (fun x => f (x, b)) (𝓝 x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>B : FilterBasis α<GOAL>generate B.sets = B.filter
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>B : FilterBasis α<GOAL>generate B.sets ≤ B.filter
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>B : FilterBasis α<GOAL>B.filter ≤ generate B.sets
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>r : ℝ<VAR>z : K<GOAL>(starRingEnd K) (r • z) = r • (starRingEnd K) z
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q + r) = ↑q + ↑r
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.den ≠ 0<GOAL>↑(q.den * r.den) ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∈ s₁<GOAL>s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>(Scheme.ΓSpecIso Γ(X, U)).hom ≫ Scheme.Hom.app hU.fromSpec U = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) ⊤ ≫ (Spec (X.presheaf.obj (op (⋯.functor.obj ⊤)))).presheaf.map ((Opens.map (inv (ΓSpec.adjunction.unit.app ↑U)).val.base).map (eqToHom ⋯).op.unop).op ≫ Scheme.Hom.app (Spec.map (X.presheaf.map (eqToHom ⋯).op)) ((Opens.map (inv (ΓSpec.adjunction.unit.app ↑U)).val.base).obj ((Opens.map U.ι.val.base).obj U)) = (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if ↑a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>hq' : (fun t => F_nat 0 (1 - a) t - if 1 - a = 0 then 1 else 0) =O[atTop] fun t => rexp (-q * t)<VAR>ha' : ↑a = 0 ↔ a = 0<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>ha' : ↑a = 0 ↔ a = 0<VAR>hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)<GOAL>∃ p, 0 < p ∧ (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>ha' : ↑a = 0 ↔ a = 0<VAR>hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)<GOAL>(fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-min p q * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>ha' : ↑a = 0 ↔ a = 0<VAR>hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)<VAR>this : (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t => (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t<GOAL>(fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-min p q * t)
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>ha' : ↑a = 0 ↔ a = 0<VAR>hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)<VAR>this : (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t => (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t<GOAL>min p q ≤ p
<VAR>a : ℝ<VAR>ha : a ∈ Ico 0 1<VAR>p : ℝ<VAR>hp : 0 < p<VAR>hp' : (fun t => F_nat 0 a t - if a = 0 then 1 else 0) =O[atTop] fun t => rexp (-p * t)<VAR>q : ℝ<VAR>hq : 0 < q<VAR>ha' : ↑a = 0 ↔ a = 0<VAR>hq' : (fun t => F_nat 0 (1 - a) t) =O[atTop] fun t => rexp (-q * t)<VAR>this : (fun t => F_int 0 (↑a) t - if a = 0 then 1 else 0) =ᶠ[atTop] fun t => (F_nat 0 a t - if a = 0 then 1 else 0) + F_nat 0 (1 - a) t<GOAL>min p q ≤ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable α<VAR>inst✝ : Inhabited α<VAR>r : β → β → Prop<VAR>f : α → β<VAR>hf : Directed r f<VAR>a : α<GOAL>r (f a) (f (Directed.sequence f hf (encode a + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Encodable α<VAR>inst✝ : Inhabited α<VAR>r : β → β → Prop<VAR>f : α → β<VAR>hf : Directed r f<VAR>a : α<GOAL>r (f a) (f (Classical.choose ⋯))
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hy : 0 < y<GOAL>x ≤ logb b y ↔ y ≤ b ^ x
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S✝<VAR>inst✝ : Ring T<VAR>ι : Sort u_1<VAR>S : ι → Subring R<VAR>x : R<GOAL>x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝¹ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e<VAR>he : OrthogonalIdempotents e<GOAL>(1 - ∑ i : I, e i) * ∑ i : I, e i = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝¹ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e<VAR>he : OrthogonalIdempotents e<GOAL>(∑ i : I, e i) * (1 - ∑ i : I, e i) = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝¹ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e<VAR>he : OrthogonalIdempotents e<GOAL>∑ i : Option I, i.elim (1 - ∑ i : I, e i) e = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝¹ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e<VAR>he : OrthogonalIdempotents e<GOAL>none.elim (1 - ∑ i : I, e i) e + ∑ i : I, (some i).elim (1 - ∑ i : I, e i) e = 1
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>s : Set β<VAR>f : ↑s → α<VAR>θ : Cardinal.{u}<VAR>hθ : θ ≤ #↑s<VAR>h₁ : ℵ₀ ≤ θ<VAR>h₂ : #α < θ.ord.cof<GOAL>∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>s : Set β<VAR>f : ↑s → α<VAR>θ : Cardinal.{u}<VAR>hθ : θ ≤ #↑s<VAR>h₁ : ℵ₀ ≤ θ<VAR>h₂ : #α < θ.ord.cof<VAR>a : α<VAR>ha : θ ≤ #↑(f ⁻¹' {a})<GOAL>∃ a t, ∃ (h : t ⊆ s), θ ≤ #↑t ∧ ∀ ⦃x : β⦄ (hx : x ∈ t), f ⟨x, ⋯⟩ = a
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝ : IsDedekindDomain S<VAR>hp0 : map f p ≠ ⊥<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>ramificationIdx f p P = Multiset.count P (factors (map f p))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p✝ : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>p : ℝ≥0∞<VAR>c : F<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>eLpNorm (fun x => c) p μ < ⊤ ↔ c = 0 ∨ μ Set.univ < ⊤