ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N✝ : Type v'<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N✝<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N✝<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Module S N✝<VAR>inst✝⁷ : IsScalarTower R S N✝<VAR>p : Submonoid R<VAR>inst✝⁶ : IsLocalization p S<VAR>f✝ : M →ₗ[R] N✝<VAR>inst✝⁵ : IsLocalizedModule p f✝<VAR>hp : p ≤ R⁰<VAR>N : Type v<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>inst✝ : IsLocalizedModule p f<GOAL>Module.rank S N = Module.rank R M
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₁<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : (L₁ ⋙ L₂).IsLocalization W₃<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ = W₃.map L₁<GOAL>L₂.IsLocalization W₂
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₁<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : (L₁ ⋙ L₂).IsLocalization W₃<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ = W₃.map L₁<VAR>this : (L₁ ⋙ W₂.Q).IsLocalization W₃<GOAL>L₂.IsLocalization W₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : _root_.RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : InnerProductSpace ℝ F<VAR>K U V : Submodule 𝕜 E<VAR>inst✝¹ : HasOrthogonalProjection U<VAR>inst✝ : HasOrthogonalProjection V<VAR>h : U ≤ V<VAR>x : E<GOAL>(orthogonalProjection U) x = (orthogonalProjection U) ↑((orthogonalProjection V) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>c • closedBall x r = closedBall (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>0 • closedBall x r = closedBall (0 • x) (‖0‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>hc : c ≠ 0<GOAL>c • closedBall x r = closedBall (c • x) (‖c‖ * r)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<GOAL>D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<GOAL>b⁻¹ • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_2<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module A M<VAR>inst✝³ : Module R M<VAR>D✝ D1 D2 : Derivation R A M<VAR>r : R<VAR>a✝ b✝ : A<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Module K M<VAR>inst✝ : Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<GOAL>(b * b⁻¹ * b⁻¹) • D a + -((a * (b ^ 2)⁻¹) • D b) = ((b ^ 2)⁻¹ * b) • D a + -(((b ^ 2)⁻¹ * a) • D b)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v : V<VAR>H : G.Subgraph<GOAL>G.singletonSubgraph v ≤ H ↔ v ∈ H.verts
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>v : V<VAR>H : G.Subgraph<GOAL>v ∈ H.verts → G.singletonSubgraph v ≤ H
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M : Type w'<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : M ⊨ T<VAR>p : T.CompleteType α<GOAL>∃ M, p ∈ T.realizedTypes (↑M) α
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M✝ : Type w'<VAR>inst✝² : L.Structure M✝<VAR>inst✝¹ : Nonempty M✝<VAR>inst✝ : M✝ ⊨ T<VAR>p : T.CompleteType α<VAR>M : ModelType ↑p<GOAL>∃ M, p ∈ T.realizedTypes (↑M) α
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M✝ : Type w'<VAR>inst✝² : L.Structure M✝<VAR>inst✝¹ : Nonempty M✝<VAR>inst✝ : M✝ ⊨ T<VAR>p : T.CompleteType α<VAR>M : ModelType ↑p<GOAL>(T.typeOf fun a => ↑(L.con a)) = p
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M✝ : Type w'<VAR>inst✝² : L.Structure M✝<VAR>inst✝¹ : Nonempty M✝<VAR>inst✝ : M✝ ⊨ T<VAR>p : T.CompleteType α<VAR>M : ModelType ↑p<VAR>φ : L[[α]].Sentence<GOAL>(φ ∈ T.typeOf fun a => ↑(L.con a)) ↔ φ ∈ p
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M✝ : Type w'<VAR>inst✝² : L.Structure M✝<VAR>inst✝¹ : Nonempty M✝<VAR>inst✝ : M✝ ⊨ T<VAR>p : T.CompleteType α<VAR>M : ModelType ↑p<VAR>φ : L[[α]].Sentence<GOAL>((Formula.equivSentence.symm φ).Realize fun a => ↑(L.con a)) ↔ φ ∈ p
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M✝ : Type w'<VAR>inst✝² : L.Structure M✝<VAR>inst✝¹ : Nonempty M✝<VAR>inst✝ : M✝ ⊨ T<VAR>p : T.CompleteType α<VAR>M : ModelType ↑p<VAR>φ : L[[α]].Sentence<GOAL>↑(ModelType.reduct (L.lhomWithConstants α) (M.subtheoryModel ⋯)) ⊨ φ ↔ ↑M ⊨ φ
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha0 : ↑a ≠ 0<GOAL>legendreSym p ↑a = 1 ↔ IsSquare ↑a
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha0 : ↑a ≠ 0<GOAL>IsSquare ↑↑a ↔ IsSquare ↑a
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha0 : ↑a ≠ 0<GOAL>↑↑a ≠ 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>m n : ℕ<VAR>inst✝ : NoZeroDivisors M₀<VAR>hn : n ≠ 0<GOAL>0 ^ n = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x<VAR>a_lt_b : a < b<VAR>s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x<VAR>a_lt_b : a < b<VAR>s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b<VAR>s_closed : IsClosed s<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x<VAR>a_lt_b : a < b<VAR>s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b<VAR>s_closed : IsClosed s<VAR>A : closure (Ioc a b) ⊆ s<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Icc a b)<VAR>hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x<VAR>φint : IntegrableOn φ (Icc a b) volume<VAR>hφg : ∀ x ∈ Ioo a b, g' x ≤ φ x<VAR>a_lt_b : a < b<VAR>s : Set ℝ := {t | g b - g t ≤ ∫ (u : ℝ) in t..b, φ u} ∩ Icc a b<VAR>s_closed : IsClosed s<VAR>A : Icc a b ⊆ s<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝ : TopologicalSpace Y<VAR>f : OnePoint X → Y<GOAL>Continuous f ↔ Tendsto (fun x => f ↑x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous fun x => f ↑x
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>g : ι' → Cardinal.{v}<VAR>hg : BddAbove (range g)<GOAL>(⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<VAR>h : Disjoint π₁.iUnion π₂.iUnion<VAR>this : ∀ J₁ ∈ π₁, ∀ J₂ ∈ π₂, J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂<GOAL>(↑(π₁.boxes ∪ π₂.boxes)).Pairwise (Disjoint on Box.toSet)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' (Iio y) y<GOAL>f' < slope f x y
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>f : α → α<VAR>hf : Involutive f<VAR>m : ℕ<GOAL>f^[2 * m + 1] = f
<VAR>p n : ℕ<GOAL>max (log 2 n) (padicValNat 2 (n + 1)) = log 2 (n + 1)
<VAR>p n : ℕ<GOAL>log 2 (n + 1) ≤ max (log 2 n) (padicValNat 2 (n + 1))
<VAR>p n : ℕ<GOAL>log 2 n < log 2 (n + 1) → log 2 (n + 1) ≤ padicValNat 2 (n + 1)
<VAR>p n : ℕ<VAR>h : log 2 n < log 2 (n + 1)<GOAL>log 2 (n + 1) ≤ padicValNat 2 (n + 1)
<VAR>p n : ℕ<VAR>h : n + 1 = 2 ^ log 2 (n + 1)<GOAL>log 2 (n + 1) ≤ padicValNat 2 (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<GOAL>∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>F_le_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)<GOAL>∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)<GOAL>∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>F_le_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)<GOAL>∀ (x : α), Tendsto (fun n => ENNReal.ofReal ‖F n x‖) atTop (𝓝 (ENNReal.ofReal ‖f x‖)) → (∀ (i : ℕ), ENNReal.ofReal ‖F i x‖ ≤ ENNReal.ofReal (bound x)) → ENNReal.ofReal ‖f x‖ ≤ ENNReal.ofReal (bound x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>F : ℕ → α → β<VAR>f : α → β<VAR>bound : α → ℝ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) atTop (𝓝 (f a))<VAR>F_le_bound✝ : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)<VAR>a : α<VAR>tendsto_norm : Tendsto (fun n => ENNReal.ofReal ‖F n a‖) atTop (𝓝 (ENNReal.ofReal ‖f a‖))<VAR>F_le_bound : ∀ (i : ℕ), ENNReal.ofReal ‖F i a‖ ≤ ENNReal.ofReal (bound a)<GOAL>ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
<VAR>q a b c : ℚ<GOAL>0 ≤ q → 0 ≤ -q → q = 0
<VAR>q a b c : ℚ<GOAL>0 ≤ q.num → q.num ≤ 0 → q.num ≤ 0 ∧ 0 ≤ q.num
<VAR>ψ θ : Angle<VAR>this : Int.natAbs 2 = 2<GOAL>2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑π
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = hammingDist y x
<VAR>L : Language<VAR>κ : Cardinal.{w}<VAR>T✝ : L.Theory<VAR>T : Language.empty.Theory<VAR>M N : T.ModelType<VAR>hM : #↑M = κ<VAR>hN : #↑N = κ<GOAL>Nonempty (↑M ≃[Language.empty] ↑N)
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → ℕ<GOAL>(Matrix.of fun i j => Polynomial.eval (↑(v i)) (descPochhammer ℤ ↑j)).det = ↑(∏ i : Fin n, (↑i)!) * (Matrix.of fun i j => ↑((v i).choose ↑j)).det
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → ℕ<VAR>x✝¹ x✝ : Fin n<GOAL>Polynomial.eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝)! * Matrix.of (fun i j => ↑((v i).choose ↑j)) x✝¹ x✝
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → ℕ<GOAL>↑(∏ i : Fin n, (↑i)!) = ∏ i : Fin n, ↑(↑i)!
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLUB s x<VAR>hx : ¬IsSuccLimit x<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>x : α<VAR>hx : ¬IsSuccLimit x<VAR>hs : IsLUB ∅ x<GOAL>x ∈ ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLUB s x<VAR>hx : ¬IsSuccLimit x<VAR>hs' : s.Nonempty<GOAL>x ∈ s
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>x✝ : IsUnit X<VAR>g : R[X]<VAR>_hfg : (monomial 1) 1 * g = 1<VAR>hgf : g * (monomial 1) 1 = 1<GOAL>0 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<VAR>x✝ : IsUnit X<VAR>g : R[X]<VAR>_hfg : (monomial 1) 1 * g = 1<VAR>hgf : g * (monomial 1) 1 = 1<GOAL>0 = (g * (monomial 1) 1).coeff 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a✝ a : α<VAR>h : a ∈ s<GOAL>(dirac a) s = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a✝ a : α<VAR>h : a ∈ s<VAR>this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1<GOAL>(dirac a) s = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a✝ a : α<VAR>h : a ∈ s<VAR>this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1<GOAL>(dirac a) s ≤ univ.indicator 1 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>a✝ a : α<VAR>h : a ∈ s<VAR>this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1<GOAL>(dirac a) s ≤ (dirac a) univ
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Ici a) = n - ↑a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ℕ → R<VAR>n : ℕ<GOAL>(f ⍟ g) n = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ℕ → R<VAR>n : ℕ<GOAL>(∑ x ∈ n.divisorsAntidiagonal, if x.2 = 0 then 0 else if x.1 = 0 then 0 else f x.1 * g x.2) = ∑ p ∈ n.divisorsAntidiagonal, f p.1 * g p.2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ℕ → R<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>(if p.2 = 0 then 0 else if p.1 = 0 then 0 else f p.1 * g p.2) = f p.1 * g p.2
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f g : ℕ → R<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<VAR>h₁ : p.1 ≠ 0<VAR>h₂ : p.2 ≠ 0<GOAL>(if p.2 = 0 then 0 else if p.1 = 0 then 0 else f p.1 * g p.2) = f p.1 * g p.2
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝² : S.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>homologyMap φ ≫ S₂.homologyι = S₁.homologyι ≫ opcyclesMap φ
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝² : S.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>S₁.rightHomologyι ≫ opcyclesMap φ = S₁.rightHomologyIso.hom ≫ S₁.homologyι ≫ opcyclesMap φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o₁ : Ordinal.{u_4}<VAR>o₂ : Ordinal.{u_5}<VAR>op : {a : Ordinal.{u_4}} → a < o₁ → {b : Ordinal.{u_5}} → b < o₂ → Ordinal.{max (max u_4 u_5) u_6}<VAR>a : Ordinal.{u_4}<VAR>b : Ordinal.{u_5}<VAR>ha : a < o₁<VAR>hb : b < o₂<GOAL>op ha hb = (fun {a} => op) ⋯ ⋯
<VAR>a : Ordinal.{u_1}<VAR>a0 : 0 < a<VAR>ha : a < ω<VAR>b : Ordinal.{u_1}<GOAL>a * (ω * b) = ω * b
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<VAR>t : ι → Set α<VAR>hst : ∀ (i : ι), s ⊆ t i<VAR>ht : ∀ (i : ι), MeasurableSet (t i)<VAR>hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<VAR>t : ι → Set α<VAR>ht : ∀ (i : ι), MeasurableSet (t i)<VAR>hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s<VAR>hst : s ⊆ ⋂ i, t i<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<VAR>t : ι → Set α<VAR>hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s<VAR>hst : s ⊆ ⋂ i, t i<VAR>ht : MeasurableSet (⋂ b, t b)<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<VAR>t : ι → Set α<VAR>hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s<VAR>hst : s ⊆ ⋂ i, t i<VAR>ht : MeasurableSet (⋂ b, t b)<VAR>i : ι<GOAL>(μ i) (⋂ i, t i) ≤ (μ i).trim s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>ι : Sort u_2<VAR>inst✝ : Countable ι<VAR>μ : ι → OuterMeasure α<VAR>s : Set α<VAR>t : ι → Set α<VAR>hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s<VAR>hst : s ⊆ ⋂ i, t i<VAR>ht : MeasurableSet (⋂ b, t b)<VAR>i : ι<GOAL>(μ i).trim s ≤ (μ i) (⋂ i, t i)
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : Commute f g<GOAL>τ (f * g) = τ f + τ g
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : Commute f g<GOAL>Tendsto (fun x => f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : Commute f g<GOAL>Tendsto (fun x => ((f ^ 2 ^ x) 0 + (g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : Commute f g<VAR>n : ℕ<GOAL>dist (((f * g) ^ n) 0) ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ≤ 1
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : Commute f g<VAR>n : ℕ<GOAL>dist ((fun n => (f ^ n) 0 + (g ^ n) 0) n) ((f ^ n * g ^ n) 0) ≤ 1
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : TopologicalSpace L<VAR>inst✝³ : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝² : SemilatticeInf L<VAR>inst✝¹ : OrderTop L<VAR>inst✝ : ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.inf f) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : CompleteSpace E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : NeZero μ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>s : Set α<VAR>inst✝ : UniformSpace α<GOAL>map (Prod.map Subtype.val Subtype.val) (𝓤 ↑s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype m<VAR>v : m → α<VAR>A : Matrix m n α<VAR>x✝ : n<GOAL>(v ᵥ* -A) x✝ = (-(v ᵥ* A)) x✝
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<GOAL>∀ (a : α), (∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)) → Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>x : α<VAR>hx : ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)<GOAL>Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>g : R[X]<VAR>inst✝ : Field K<VAR>f : K[X]<VAR>hf : f ≠ 0<GOAL>minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<GOAL>(laurent r) ((laurent s) f) = (laurent (r + s)) f