ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<VAR>hF : LinearMap.ker F ≠ ⊥<VAR>y : L<VAR>hyα : y ∈ ↑(rootSpace H ⇑α)<VAR>hy₀ : ⟨y, hyα⟩ ≠ 0<VAR>hy : ⁅y, f⁆ = 0<VAR>P : ⋯.HasPrimitiveVectorWith y (-2)<GOAL>False
<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>hα : α.IsNonZero<VAR>contra : 1 < finrank K ↥↑(rootSpace H ⇑α)<VAR>h e f : L<VAR>ht : IsSl2Triple h e f<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<VAR>F : ↥↑(rootSpace H ⇑α) →ₗ[K] K := (killingForm K L) f ∘ₗ (↑(rootSpace H ⇑α)).subtype<VAR>hF : LinearMap.ker F ≠ ⊥<VAR>y : L<VAR>hyα : y ∈ ↑(rootSpace H ⇑α)<VAR>hy₀ : ⟨y, hyα⟩ ≠ 0<VAR>hy : ⁅y, f⁆ = 0<VAR>P : ⋯.HasPrimitiveVectorWith y (-2)<VAR>n : ℕ<VAR>hn : -2 = ↑n<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>coborder s = (frontier s)ᶜ ↔ IsOpen s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm f p μ = eLpNorm g p ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>(∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : β), ↑‖g a‖₊ ^ p.toReal ∂ν) ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ p.toReal ∂μ = ∫⁻ (a : β), ↑‖g a‖₊ ^ p.toReal ∂ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : OpensMeasurableSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>p : ℝ≥0∞<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>IdentDistrib (fun x => ↑‖f x‖₊ ^ p.toReal) (fun x => ↑‖g x‖₊ ^ p.toReal) μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>l : List α<VAR>l₁ l₂ : List β<VAR>h : Forall₂ R l (l₁ ++ l₂)<GOAL>Forall₂ R (take l₁.length l) l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>l : List α<VAR>l₁ l₂ : List β<VAR>h : Forall₂ R l (l₁ ++ l₂)<VAR>h' : Forall₂ R (take l₁.length l) (take l₁.length (l₁ ++ l₂))<GOAL>Forall₂ R (take l₁.length l) l₁
<VAR>M : Type u_1<VAR>inst✝⁴ : Zero M<VAR>l : List M<VAR>inst✝³ : DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : ℕ<VAR>R : Type u_2<VAR>inst✝² : AddZeroClass R<VAR>x : R<VAR>xs : List R<VAR>inst✝¹ : DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0<VAR>inst✝ : DecidablePred fun i => xs.getD i 0 ≠ 0<GOAL>(xs ++ [x]).toFinsupp = xs.toFinsupp + Finsupp.single xs.length x
<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>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>b : P<VAR>hb : b ∈ I * J<GOAL>IsInteger R ((aI * aJ) • b)
<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>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>b : P<VAR>hb : b ∈ I * J<GOAL>∀ m ∈ I, ∀ n ∈ J, IsInteger R ((aI * aJ) • (m * n))
<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>I J : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>aJ : R<VAR>haJ : aJ ∈ S<VAR>hJ : ∀ b ∈ J, IsInteger R (aJ • b)<VAR>b : P<VAR>hb : b ∈ I * J<GOAL>∀ (x y : P), IsInteger R ((aI * aJ) • x) → IsInteger R ((aI * aJ) • y) → IsInteger R ((aI * aJ) • (x + y))
<VAR>b : ℂ<VAR>hb : 0 < b.re<GOAL>∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>hb' : b ≠ 0<GOAL>∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>hb' : b ≠ 0<VAR>A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x<GOAL>∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>hb' : b ≠ 0<VAR>A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x<VAR>B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))<GOAL>∫ (r : ℝ) in Ioi 0, ↑r * cexp (-b * ↑r ^ 2) = (2 * b)⁻¹
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>hb' : b ≠ 0<VAR>A : ∀ (x : ℂ), HasDerivAt (fun x => -(2 * b)⁻¹ * cexp (-b * x ^ 2)) (x * cexp (-b * x ^ 2)) x<VAR>B : Tendsto (fun y => -(2 * b)⁻¹ * cexp (-b * ↑y ^ 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))<GOAL>(2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * ↑0 ^ 2)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>n : ℕ<GOAL>iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : ¬p = 1<GOAL>Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : ¬p = 1<GOAL>(∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b✝ : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hp1 : ¬p = 1<VAR>a b : R[X]<VAR>ha : a.Monic<VAR>hb : b.Monic<GOAL>a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : (i : ι) → Preorder (π i)<VAR>x y : (i : ι) → π i<GOAL>x < y ↔ x ≤ y ∧ ∃ i, x i < y i
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>K : Type u_6<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>N₃ : Type u_14<VAR>N₄ : Type u_15<VAR>ι : Type u_16<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Subsingleton M<VAR>inst✝ : Subsingleton M₂<VAR>x✝ : M<GOAL>(ofSubsingleton M M) x✝ = (refl R M) x✝
<VAR>f✝ g : CircleDeg1Lift<VAR>f : CircleDeg1Liftˣ<VAR>n : ℕ<GOAL>τ ↑(f ^ ↑n) = ↑↑n * τ ↑f
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : t ≤ 0<VAR>x : X<GOAL>(F.extend t) x = f₀ x
<VAR>F✝ : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>f₀ f₁ : C(X, Y)<VAR>F : f₀.Homotopy f₁<VAR>t : ℝ<VAR>ht : t ≤ 0<VAR>x : X<GOAL>(F.extend t) x = F (0, x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N n : ℕ<VAR>c : R<VAR>n✝ : ℕ<GOAL>(reflect N (C c * X ^ n)).coeff n✝ = (C c * X ^ (revAt N) n).coeff n✝
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N n : ℕ<VAR>c : R<VAR>n✝ : ℕ<GOAL>c * (X ^ n).coeff ((revAt N) n✝) = c * if n✝ = (revAt N) n then 1 else 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : Norm E<VAR>a : 𝕜<VAR>f : 𝕜 → E<VAR>h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[≠] a) (norm ∘ f)<GOAL>f =o[𝓝[≠] a] fun x => (x - a)⁻¹
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : Norm E<VAR>a : 𝕜<VAR>f : 𝕜 → E<VAR>h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[≠] a) (norm ∘ f)<GOAL>Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[≠] a) atTop
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : Norm E<VAR>a : 𝕜<VAR>f : 𝕜 → E<VAR>h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[≠] a) (norm ∘ f)<GOAL>Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[≠] a) atTop
<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>M' : Submodule R M<VAR>P : Type w<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>Q : Type w'<VAR>inst✝⁴ : AddCommGroup Q<VAR>inst✝³ : Module R Q<VAR>inst✝² : Module S Q<VAR>inst✝¹ : IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>inst✝ : IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<VAR>x : N<GOAL>x ∈ Submodule.localized' S p f (ker g) ↔ x ∈ ker (extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))
<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>M' : Submodule R M<VAR>P : Type w<VAR>inst✝⁶ : AddCommGroup P<VAR>inst✝⁵ : Module R P<VAR>Q : Type w'<VAR>inst✝⁴ : AddCommGroup Q<VAR>inst✝³ : Module R Q<VAR>inst✝² : Module S Q<VAR>inst✝¹ : IsScalarTower R S Q<VAR>f' : P →ₗ[R] Q<VAR>inst✝ : IsLocalizedModule p f'<VAR>g : M →ₗ[R] P<VAR>x : N<GOAL>(∃ m, g m = 0 ∧ ∃ s, IsLocalizedModule.mk' f m s = x) ↔ ((IsLocalizedModule.map p f f') g) x = 0
<VAR>a b : Ordinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ω<VAR>hb : ↑n < ω<GOAL>(fun x x_1 => x ^ x_1) ↑m ↑n < ω
<VAR>a b : Ordinal.{u_1}<VAR>m n : ℕ<VAR>ha : ↑m < ω<VAR>hb : ↑n < ω<GOAL>↑(m ^ n) < ω
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<GOAL>p ≠ 0 ↔ ∃ d, coeff d p ≠ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<GOAL>(¬∀ (d : σ →₀ ℕ), coeff d p = 0) ↔ ∃ d, coeff d p ≠ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<GOAL>(∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : LinearOrderedRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>h : AffineIndependent k p<VAR>w : ι → k<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>i₁ i₂ i₃ : ι<VAR>h₁ : i₁ ∈ s<VAR>h₂ : i₂ ∈ s<VAR>h₃ : i₃ ∈ s<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>c : k<VAR>hc0 : 0 < c<VAR>hc1 : c < 1<VAR>hs : (affineCombination k s p) w ∈ affineSpan k {p i₁, (AffineMap.lineMap (p i₂) (p i₃)) c}<GOAL>SignType.sign (w i₂) = SignType.sign (w i₃)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c : ℝ<VAR>hc : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ c<VAR>μ : Measure (ι → ℝ)<VAR>inst✝ : IsLocallyFiniteMeasure μ<GOAL>‖integral I l f μ.toBoxAdditive.toSMul‖ ≤ (μ ↑I).toReal * c
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>(∃ n, (coeff R n) φ ≠ 0) ↔ φ ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>(¬∃ n, (coeff R n) φ ≠ 0) ↔ ¬φ ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ : R⟦X⟧<GOAL>(∀ (n : ℕ), (coeff R n) φ = 0) ↔ φ = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Finset ι<VAR>S T : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>f : (i : ι) → α i<GOAL>f ∈ cylinder s S \ cylinder s T ↔ f ∈ cylinder s (S \ T)
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>P : α → Prop<GOAL>(∀ i ∈ ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>f' : C(X, ↑(Set.Icc (-‖↑f‖) ‖↑f‖)) := (↑f).attachBound<VAR>abs : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ) := { toFun := fun x => |↑x|, continuous_toFun := ⋯ }<GOAL>abs.comp f' ∈ A.topologicalClosure
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>x y : α<GOAL>swap x y = Equiv.refl α ↔ x = y
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>x y : α<VAR>h : swap x y = Equiv.refl α<GOAL>(Equiv.refl α) x = (Equiv.refl α) y
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace ℝ F<VAR>G : Type u_3<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : InnerProductSpace ℝ G<VAR>K : ProperCone ℝ E<GOAL>↑(map (ContinuousLinearMap.id ℝ E) K) = ↑K
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>B : C<GOAL>(initialIsInitial.uniqueUpToIso HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : DecidableEq β<VAR>inst✝³ : DecidableEq γ<VAR>inst✝² : SMul αᵐᵒᵖ β<VAR>inst✝¹ : SMul β γ<VAR>inst✝ : SMul α γ<VAR>a : α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c<VAR>a✝ : γ<GOAL>a✝ ∈ (op a • s) • t ↔ a✝ ∈ s • a • t
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>inst✝ : Invertible 3<GOAL>(ofJ0 R).j = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>inst✝ : Invertible 3<GOAL>↑(unitOfInvertible (-3 ^ 3))⁻¹ * 0 ^ 3 = 0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>s : Set G<GOAL>closure (⇑(closure s).subtype ⁻¹' s) = ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>s : Set G<GOAL>map (closure s).subtype (closure (⇑(closure s).subtype ⁻¹' s)) = map (closure s).subtype ⊤
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>s : Set G<GOAL>s ⊆ Set.range ⇑(closure s).subtype
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>s : Set G<GOAL>s ⊆ {x | x ∈ ↑(closure s)}
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>0 < star x ↔ 0 < x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E p μ)<GOAL>↑(toSimpleFunc (-f)) =ᶠ[ae μ] -↑(toSimpleFunc f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → ↑(toSimpleFunc (-f)) a✝ = (-↑(toSimpleFunc f)) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(toSimpleFunc (-f)) a✝ = -↑(toSimpleFunc f) a✝
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s✝ t✝ : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).dens + t.dens = (s ∪ t).dens
<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>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a✝ b✝ : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>a b : ℝ<VAR>N : ℕ<GOAL>Submartingale (fun n => ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a✝ b✝ : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>a b : ℝ<VAR>N : ℕ<GOAL>∀ (n : ℕ) (ω : Ω), (1 - upcrossingStrat a b f N n) ω ≤ 1
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a✝ b✝ : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N✝ n m : ℕ<VAR>ω : Ω<VAR>ℱ : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Submartingale f ℱ μ<VAR>a b : ℝ<VAR>N : ℕ<GOAL>∀ (n : ℕ) (ω : Ω), 0 ≤ (1 - upcrossingStrat a b f N n) ω
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.44267, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<VAR>p : ℤ<GOAL>(mapOfHomotopy H ≫ (triangle φ₂).mor₃).f p = ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a).f p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : TopCat<VAR>H₁ : X ≅ Y<VAR>ℱ : Presheaf C Y<VAR>𝒢 : Presheaf C X<VAR>H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢<VAR>U : (Opens ↑X)ᵒᵖ<GOAL>(Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U))) = U
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>(p * q).coeff (p * q).natDegree = p.coeff p.natDegree * q.coeff q.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff * q.leadingCoeff ≠ 0<GOAL>p.leadingCoeff * q.leadingCoeff = p.coeff p.natDegree * q.coeff q.natDegree
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : OrderTop α<VAR>s : Multiset α<VAR>a : α<GOAL>∀ (a_1 : α) (s : Multiset α), (a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b) → (a ≤ (a_1 ::ₘ s).inf ↔ ∀ b ∈ a_1 ::ₘ s, a ≤ b)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>this : DecidableEq α := Classical.decEq α<VAR>m n : ℕ<VAR>h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n<VAR>hmlen : m ≤ n<GOAL>m = n
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>this : DecidableEq α := Classical.decEq α<VAR>m n : ℕ<VAR>h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n<VAR>hmlen : m ≤ n<VAR>hmn : ¬m = n<GOAL>False
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>this : DecidableEq α := Classical.decEq α<VAR>m n : ℕ<VAR>h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n<VAR>hmlen : m ≤ n<VAR>hmn✝ : ¬m = n<VAR>hmn : m < n<GOAL>False
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>this : DecidableEq α := Classical.decEq α<VAR>m n : ℕ<VAR>h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n<VAR>hmlen : m ≤ n<VAR>hmn✝ : ¬m = n<VAR>hmn : m < n<GOAL>Classical.choose ⋯ ∈ (Multiset.pmap (fun m x => Infinite.natEmbeddingAux α m) (Multiset.range n) ⋯).toFinset
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>inst✝ : Infinite α<VAR>this : DecidableEq α := Classical.decEq α<VAR>m n : ℕ<VAR>h : Infinite.natEmbeddingAux α m = Infinite.natEmbeddingAux α n<VAR>hmlen : m ≤ n<VAR>hmn✝ : ¬m = n<VAR>hmn : m < n<GOAL>Infinite.natEmbeddingAux α m = Classical.choose ⋯