ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : Div α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x / (equivShrink α).symm y)) = (equivShrink α).symm x / (equivShrink α).symm y
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosMono α<VAR>hb : 0 ≤ b<VAR>h : 1 ≤ a<GOAL>b ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>r : List α<GOAL>l₁ ++ drop l₁.length (l₁ ++ r) = l₁ ++ r
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J J' : FractionalIdeal R₁⁰ K<VAR>hJ' : J' ≠ 0<GOAL>I ≤ J / J' ↔ I * J' ≤ J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J J' : FractionalIdeal R₁⁰ K<VAR>hJ' : J' ≠ 0<GOAL>I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ I * J' ≤ J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J J' : FractionalIdeal R₁⁰ K<VAR>hJ' : J' ≠ 0<GOAL>I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ ↑I * ↑J' ≤ ↑J
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<GOAL>ContDiff ℝ n ↑univUnitBall
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<GOAL>ContDiff ℝ n fun x => (√(1 + ‖x‖ ^ 2))⁻¹
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2<GOAL>ContDiff ℝ n fun x => (√(1 + ‖x‖ ^ 2))⁻¹
<VAR>n : ℕ∞<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2<GOAL>ContDiff ℝ n fun x => √(1 + ‖x‖ ^ 2)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle x y = ↑π ↔ x ≠ 0 ∧ y ≠ 0 ∧ o.oangle x (-y) = 0
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∑ i ∈ Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∑ x ∈ Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
<VAR>x₀ : ℝ<VAR>a b : ℕ<VAR>f : ℝ → ℝ<VAR>hab : a ≤ b<VAR>hf : AntitoneOn f (Icc ↑a ↑b)<GOAL>∑ x ∈ Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring K<VAR>inst✝ : Algebra F K<VAR>x : K<VAR>h : IsSeparable F x<GOAL>IsIntegral F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring K<VAR>inst✝ : Algebra F K<VAR>x : K<VAR>h : IsSeparable F x<VAR>h✝ : Subsingleton F<GOAL>IsIntegral F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring K<VAR>inst✝ : Algebra F K<VAR>x : K<VAR>h : IsSeparable F x<VAR>h✝ : Nontrivial F<GOAL>IsIntegral F x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.134154, u_2} D<VAR>L : C ⥤ D<VAR>W✝ : MorphismProperty C<VAR>inst✝ : L.IsLocalization W✝<VAR>W : MorphismProperty Cᵒᵖ<VAR>X Y : Cᵒᵖ<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>Z : Cᵒᵖ<VAR>t₁ : z₁.Y' ⟶ Z<VAR>t₂ : z₂.Y' ⟶ Z<VAR>hs : z₁.s ≫ t₁ = z₂.s ≫ t₂<VAR>hf : z₁.f ≫ t₁ = z₂.f ≫ t₂<VAR>ht : W (z₁.s ≫ t₁)<GOAL>RightFractionRel z₁.unop z₂.unop
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>inst✝¹ : IsFractionRing R₁ K<VAR>I : FractionalIdeal S P<VAR>inst✝ : (↑I).IsPrincipal<GOAL>I = spanSingleton S (generator ↑I)
<VAR>α : Type u_1<VAR>l : List α<GOAL>map Prod.fst l.enum = range l.length
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<GOAL>W.ΨSq 2 = W.Ψ₂Sq
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l r : List α<VAR>h1 : (a :: l).length - 1 - 0 < ((a :: l).reverseAux r).length<VAR>x✝ : 0 < (a :: l).length<GOAL>((a :: l).reverseAux r)[(a :: l).length - 1 - 0] = (a :: l)[0]
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l r : List α<VAR>h1 : (a :: l).length - 1 - 0 < ((a :: l).reverseAux r).length<VAR>x✝ : 0 < (a :: l).length<VAR>aux : ∀ (h1 : 0 + l.length < (l.reverseAux (a :: r)).length) (h2 : 0 < (a :: r).length), (l.reverseAux (a :: r)).get ⟨0 + l.length, h1⟩ = (a :: r).get ⟨0, h2⟩<GOAL>((a :: l).reverseAux r)[(a :: l).length - 1 - 0] = (a :: l)[0]
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>a : α<VAR>l r : List α<VAR>h1 : (a :: l).length - 1 - 0 < ((a :: l).reverseAux r).length<VAR>x✝ : 0 < (a :: l).length<VAR>aux : ∀ (h1 : l.length < (l.reverseAux (a :: r)).length) (h2 : 0 < (a :: r).length), (l.reverseAux (a :: r)).get ⟨l.length, h1⟩ = (a :: r).get ⟨0, h2⟩<GOAL>((a :: l).reverseAux r)[(a :: l).length - 1 - 0] = (a :: l)[0]
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>u : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>u : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>u : UniformSpace E<VAR>inst✝ : UniformAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : ι<GOAL>comap (⇑(p i)) (𝓝 0) = 𝓝 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>b : ℤ<GOAL>b ≤ ⌊↑(b + 1)⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>b : ℤ<GOAL>b ≤ b + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>a : α<VAR>f : F<VAR>neZero : NeZero (f a)<VAR>h : a = 0<GOAL>f 0 = 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'<GOAL>f.ker = ⊥ ↔ Function.Injective ⇑f
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x y z : α<VAR>h : x ∈ y :: z :: l<VAR>hx : x = y<GOAL>(y :: z :: l).next x h = z
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>a : α<VAR>this : (a :: const a).tail = const a<GOAL>(const a).tail = const a
<VAR>R : Type u_1<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>a✝ a : R<GOAL>a + a = 0 ↔ a = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeInf γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Tendsto f F atBot<VAR>hg : Tendsto g G atBot<GOAL>Tendsto (Prod.map f g) (F ×ˢ G) atBot
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeInf γ<VAR>F : Filter α<VAR>G : Filter β<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Tendsto f F atBot<VAR>hg : Tendsto g G atBot<GOAL>Tendsto (Prod.map f g) (F ×ˢ G) (atBot ×ˢ atBot)
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<GOAL>clog b r = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>s : Finset ι<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>∫⁻ (a : α), f a ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫⁻ (a : α), f a ∂μ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>ι : Type u_5<VAR>m : MeasurableSpace α<VAR>s : Finset ι<VAR>f : α → ℝ≥0∞<VAR>μ : ι → Measure α<GOAL>∑' (i : { x // x ∈ s }), ∫⁻ (a : α), f a ∂μ ↑i = ∑' (x : ↑↑s), ∫⁻ (a : α), f a ∂μ ↑x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>inst✝ : DecidableEq τ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>((bind₁ f) φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>inst✝ : DecidableEq τ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(φ.support.biUnion fun d => (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars) ≤ φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>inst✝ : DecidableEq τ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(φ.support.biUnion fun d => d.support.biUnion fun i => (f i).vars) ≤ φ.vars.biUnion fun i => (f i).vars
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<VAR>this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<VAR>this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)<VAR>g : E →L[ℝ] ℝ<VAR>hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x<VAR>hnormeq : ‖g‖ = ‖fr‖<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<VAR>this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)<VAR>g : E →L[ℝ] ℝ<VAR>hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x<VAR>hnormeq : ‖g‖ = ‖fr‖<VAR>h : ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x<GOAL>(∀ (x : ↥p), g.extendTo𝕜 ↑x = f x) ∧ ‖g.extendTo𝕜‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<VAR>this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)<VAR>g : E →L[ℝ] ℝ<VAR>hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x<VAR>hnormeq : ‖g‖ = ‖fr‖<VAR>h : ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x<GOAL>‖g.extendTo𝕜‖ ≤ ‖f‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<VAR>this✝¹ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>this✝ : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower ℝ 𝕜 E<VAR>this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>fr : ↥p →L[ℝ] ℝ := reCLM.comp (ContinuousLinearMap.restrictScalars ℝ f)<VAR>g : E →L[ℝ] ℝ<VAR>hextends : ∀ (x : ↥(Submodule.restrictScalars ℝ p)), g ↑x = fr x<VAR>hnormeq : ‖g‖ = ‖fr‖<VAR>h : ∀ (x : ↥p), g.extendTo𝕜 ↑x = f x<GOAL>‖f‖ ≤ ‖g.extendTo𝕜‖
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<GOAL>f ↑n = f 1 + log ↑(n - 1)!
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<GOAL>f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<VAR>A : 0 < ↑m<GOAL>f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<VAR>A : 0 < ↑m<GOAL>f ↑m + log ↑m = f 1 + log ↑m !
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<VAR>A : 0 < ↑m<GOAL>f 1 + log ↑((m - 1)! * m) = f 1 + log ↑m !
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<VAR>A : 0 < ↑m<GOAL>f 1 + log ↑((m - 1)! * m) = f 1 + log ↑(m.pred ! * (m.pred + 1))
<VAR>f : ℝ → ℝ<VAR>x : ℝ<VAR>n : ℕ<VAR>hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y<VAR>hn : n ≠ 0<VAR>m : ℕ<VAR>hm : 1 ≤ m<VAR>IH : f ↑m = f 1 + log ↑(m - 1)!<VAR>A : 0 < ↑m<GOAL>m = m.pred + 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ {a}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>(∃ a ∉ s, a ∈ t ∧ s ⊆ t) ↔ ∃ a ∈ t, s ⊆ t ∧ a ∉ s
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x : ↥H<GOAL>((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x : ↥H<VAR>this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x<GOAL>((traceForm K (↥H) L) (coroot α)) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>x : ↥H<VAR>this : ((cartanEquivDual H) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = α x<GOAL>2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • ((traceForm K (↥H) L) ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))) x = 2 • (α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)))⁻¹ • α x
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>f : X →ᵇ ℝ<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) ⊥ ≤ ∫ (x : X), f x ∂μ<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) ⊥ (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (𝓝 (∫ (x : X), f x ∂μ))
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>∫ (x : X), f x ∂μ ≤ liminf (fun i => ∫ (x : X), f x ∂μs i) L
<VAR>X : Type u_1<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : OpensMeasurableSpace X<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>μ : Measure X<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ι → Measure X<VAR>inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)<VAR>h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ<VAR>f : X →ᵇ ℝ<VAR>hL : L.NeBot<VAR>obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)<VAR>bdd_above : IsBoundedUnder (fun x x_1 => x ≤ x_1) L fun i => ∫ (x : X), f x ∂μs i<VAR>bdd_below : IsBoundedUnder (fun x x_1 => x ≥ x_1) L fun i => ∫ (x : X), f x ∂μs i<GOAL>limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<GOAL>IsSatisfiable (⋃ i, T i) ↔ ∀ (i : ι), (T i).IsSatisfiable
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<VAR>h' : ∀ (i : ι), (T i).IsSatisfiable<GOAL>IsSatisfiable (⋃ i, T i)
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<VAR>h' : ∀ (i : ι), (T i).IsSatisfiable<GOAL>∀ (T0 : Finset L.Sentence), ↑T0 ⊆ ⋃ i, T i → IsSatisfiable ↑T0
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<VAR>h' : ∀ (i : ι), (T i).IsSatisfiable<VAR>T0 : Finset L.Sentence<VAR>hT0 : ↑T0 ⊆ ⋃ i, T i<GOAL>IsSatisfiable ↑T0
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>T : ι → L.Theory<VAR>h : Directed (fun x x_1 => x ⊆ x_1) T<VAR>h' : ∀ (i : ι), (T i).IsSatisfiable<VAR>T0 : Finset L.Sentence<VAR>hT0 : ↑T0 ⊆ ⋃ i, T i<VAR>i : ι<VAR>hi : ↑T0 ⊆ T i<GOAL>IsSatisfiable ↑T0