ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = coeff d p ⊗ₜ[R] n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p * ((IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))).comp Algebra.TensorProduct.includeRight) n) = coeff d p ⊗ₜ[R] n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p * (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) = coeff d p ⊗ₜ[R] n
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : CommSemiring N<VAR>inst✝ : Algebra R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<VAR>g : S →+* 𝕎 R<VAR>k₁✝ k₂✝ : ℕ<VAR>h : k₁✝ ≤ k₂✝<GOAL>(TruncatedWittVector.truncate h).comp ((fun k => (truncate k).comp g) k₂✝) = (fun k => (truncate k).comp g) k₁✝
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>f✝ : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f✝ k₂) = f✝ k₁<VAR>f : (k : ℕ) → S →+* TruncatedWittVector p k R<VAR>hf : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁<GOAL>(fun g => ⟨fun k => (truncate k).comp g, ⋯⟩) ((fun f => lift ↑f ⋯) ⟨f, hf⟩) = ⟨f, hf⟩
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>inst✝ : Nontrivial R<VAR>h : IsCoprime x y<GOAL>x ≠ 0 ∨ y ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>inst✝ : Nontrivial R<VAR>h : IsCoprime x y<GOAL>x = 0 → y ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>z : R<VAR>inst✝ : Nontrivial R<VAR>h : IsCoprime 0 0<GOAL>False
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<GOAL>(shiftFunctorZero (OppositeShift C A) A).hom.app X = ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>X : OppositeShift C A<GOAL>𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) = 𝟙 (Opposite.op ((shiftFunctor C 0).obj (Opposite.unop X)))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>frontier (closedBall x r) = sphere x r
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>RTendsto r l₁ l₂ ↔ l₁ ≤ rcomap r l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>(∀ s ∈ l₂, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>r : Rel α β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>(∀ s ∈ l₂.sets, r.core s ∈ l₁) ↔ l₁ ≤ rcomap r l₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' S : Submodule R M<GOAL>Nat.card M = Nat.card ↥S * Nat.card (M ⧸ S)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝² : Ring R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>p p' S : Submodule R M<GOAL>Nat.card M = Nat.card ((M ⧸ S) × ↥S)
<VAR>m n : ZNum<GOAL>m ∣ n ↔ n % m = 0
<VAR>m n : ZNum<GOAL>↑n % ↑m = 0 ↔ ↑n % ↑m = ↑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>R : Type u_6<VAR>inst✝² : NormedDivisionRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>s : Set R<VAR>x : R<VAR>hx : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => x⁻¹) s x = -((mulLeftRight 𝕜 R) 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>R : Type u_6<VAR>inst✝² : NormedDivisionRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>s : Set R<VAR>x : R<VAR>hx : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderiv 𝕜 Inv.inv x = -((mulLeftRight 𝕜 R) x⁻¹) x⁻¹
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableRel r<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>xs : List α<VAR>hx : x ∉ xs<GOAL>(orderedInsert r x xs).erase x = xs
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>inst✝¹ : DecidableRel r<VAR>inst✝ : DecidableEq α<VAR>x : α<VAR>xs : List α<VAR>hx : x ∉ xs<GOAL>x ∉ takeWhile (fun b => decide ¬r x b) xs
<VAR>α : Type u<VAR>β : Type u_1<VAR>n : ℕ<VAR>x : α<VAR>inst✝ : LinearOrderedRing α<VAR>hn : n ≠ 0<GOAL>∑ i ∈ range n, x ^ i < 0 ↔ Even n ∧ x + 1 < 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : Nonempty α<GOAL>univ.dens = 1
<VAR>Γ✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ✝<VAR>inst✝¹ : AddMonoid R<VAR>Γ : Type u_3<VAR>inst✝ : LinearOrder Γ<VAR>x y : HahnSeries Γ R<VAR>hxy : y.orderTop < x.orderTop<GOAL>(x + y).leadingCoeff = y.leadingCoeff
<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>f : α → β<VAR>x : α<VAR>s : Set α<GOAL>ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>E : LinearRecurrence α<VAR>q : α<GOAL>(E.IsSolution fun n => q ^ n) ↔ E.charPoly.IsRoot q
<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>E : LinearRecurrence α<VAR>q : α<GOAL>(E.IsSolution fun n => q ^ n) ↔ eval₂ (RingHom.id α) q ((monomial E.order) 1 - ∑ i : Fin E.order, (monomial ↑i) (E.coeffs i)) = 0
<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>E : LinearRecurrence α<VAR>q : α<GOAL>(E.IsSolution fun n => q ^ n) ↔ q ^ E.order - ∑ x : Fin E.order, E.coeffs x * q ^ ↑x = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>ι : Type u_2<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>inst✝¹ : (i : ι) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite volume<VAR>hf : ∀ (i : ι), Integrable (f i) volume<VAR>e : Fin (card ι) ≃ ι := (equivFin ι).symm<GOAL>Integrable (fun x => ∏ i : ι, f i (x i)) volume
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>ι : Type u_2<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_3<VAR>f : (i : ι) → E i → 𝕜<VAR>inst✝¹ : (i : ι) → MeasureSpace (E i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite volume<VAR>hf : ∀ (i : ι), Integrable (f i) volume<VAR>e : Fin (card ι) ≃ ι := (equivFin ι).symm<GOAL>Integrable (fun x => ∏ x_1 : Fin (card ι), f (e x_1) (x x_1)) volume
<VAR>a b p q : ℝ≥0<VAR>h✝ h : p.IsConjExponent q<GOAL>1 < q
<VAR>a b p q : ℝ≥0<VAR>h✝ h : p.IsConjExponent q<GOAL>1 < p / (p - 1)
<VAR>a b p q : ℝ≥0<VAR>h✝ h : p.IsConjExponent q<GOAL>q⁻¹ + p⁻¹ = 1
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε + cgf X μ t)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : 0 ≤ t<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{?u.113036, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n : M<VAR>h₁ : m ⊗ n ≅ 𝟙_ M<VAR>h₂ : n ⊗ m ≅ 𝟙_ M<VAR>H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom<VAR>X : C<GOAL>(F.obj m).map ((unitOfTensorIsoUnit F m n h₁).inv.app X) ≫ (F.μ n m).app ((F.obj m).obj X) ≫ (F.map h₂.hom).app ((F.obj m).obj X) ≫ F.εIso.inv.app ((F.obj m).obj X) = 𝟙 ((F.obj m).obj X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{?u.113036, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>m n : M<VAR>h₁ : m ⊗ n ≅ 𝟙_ M<VAR>h₂ : n ⊗ m ≅ 𝟙_ M<VAR>H : h₁.hom ▷ m ≫ (λ_ m).hom = (α_ m n m).hom ≫ m ◁ h₂.hom ≫ (ρ_ m).hom<VAR>X : C<GOAL>(F.map (λ_ m).inv).app X ≫ (F.map (h₁.inv ▷ m)).app X ≫ (F.map (α_ m n m).hom).app X ≫ (F.map (m ◁ h₂.hom)).app X ≫ (F.map (ρ_ m).hom).app X = 𝟙 ((F.obj m).obj X)
<VAR>x : ℤ<VAR>r : ℝ<GOAL>closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋
<VAR>R S T : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>Function.Surjective ⇑(g.comp 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✝³ : MeasurableSpace E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>μ : Measure β<VAR>hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s<VAR>hi : HasFiniteIntegral (fun x => f x - y₀) μ<GOAL>Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ∂μ) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>v : α → β<VAR>l : β → γ<VAR>u : γ → β<VAR>gc : GaloisConnection l u<VAR>hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝<VAR>hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<GOAL>l (limsup v f) ≤ limsup (fun x => l (v x)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>v : α → β<VAR>l : β → γ<VAR>u : γ → β<VAR>gc : GaloisConnection l u<VAR>hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝<VAR>hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>c : γ<VAR>hc : ∀ᶠ (n : γ) in map (fun x => l (v x)) f, n ≤ c<GOAL>l (limsup v f) ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>v : α → β<VAR>l : β → γ<VAR>u : γ → β<VAR>gc : GaloisConnection l u<VAR>hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝<VAR>hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>c : γ<VAR>hc : ∀ᶠ (a : α) in f, l (v a) ≤ c<GOAL>l (limsup v f) ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>v : α → β<VAR>l : β → γ<VAR>u : γ → β<VAR>gc : GaloisConnection l u<VAR>hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝<VAR>hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>c : γ<VAR>hc : ∀ᶠ (a : α) in f, v a ≤ u c<GOAL>limsup v f ≤ u c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι✝ : Sort x<VAR>κ : ι✝ → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → β<GOAL>l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<GOAL>(haarMeasure K₀) ↑K₀ = 1
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<VAR>this : LocallyCompactSpace G<GOAL>(haarMeasure K₀) ↑K₀ = 1
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<VAR>this : LocallyCompactSpace G<GOAL>((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure ↑K₀ = 1
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<VAR>this : LocallyCompactSpace G<GOAL>(haarContent K₀).outerMeasure (closure ↑K₀) ≠ 0
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalGroup G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>K₀ : PositiveCompacts G<VAR>this : LocallyCompactSpace G<GOAL>(haarContent K₀).outerMeasure (closure ↑K₀) ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f : ↥(Lp E p μ)<GOAL>0 ≤ᶠ[ae μ] ↑↑f ↔ 0 ≤ f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f : ↥(Lp E p μ)<GOAL>0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f : ↥(Lp E p μ)<VAR>h0 : ↑↑0 =ᶠ[ae μ] 0<GOAL>0 ≤ᶠ[ae μ] ↑↑f ↔ ↑↑0 ≤ᶠ[ae μ] ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f : ↥(Lp E p μ)<VAR>h0 : ↑↑0 =ᶠ[ae μ] 0<VAR>h : 0 ≤ᶠ[ae μ] ↑↑f<VAR>a✝¹ : α<VAR>a✝ : 0 a✝¹ ≤ ↑↑f a✝¹<VAR>h2 : ↑↑0 a✝¹ = 0 a✝¹<GOAL>↑↑0 a✝¹ ≤ ↑↑f a✝¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝ : NormedLatticeAddCommGroup E<VAR>f : ↥(Lp E p μ)<VAR>h0 : ↑↑0 =ᶠ[ae μ] 0<VAR>h : ↑↑0 ≤ᶠ[ae μ] ↑↑f<VAR>a✝¹ : α<VAR>a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹<VAR>h2 : ↑↑0 a✝¹ = 0 a✝¹<GOAL>0 a✝¹ ≤ ↑↑f a✝¹
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i j : Fin (n + 2)<VAR>H : i ≤ j<GOAL>X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op = X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id F) f<GOAL>f.roots.Nodup ↔ f.Separable
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id F) f<VAR>hnsep : ¬f.Separable<GOAL>¬f.roots.Nodup
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id F) f<VAR>hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0<GOAL>¬f.roots.Nodup
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id F) f<VAR>hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0<VAR>x : F<VAR>hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0<GOAL>¬f.roots.Nodup
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (RingHom.id F) f<VAR>hnsep : ¬(GCDMonoid.gcd f (derivative f)).degree = 0<VAR>x : F<VAR>hx : eval₂ (RingHom.id F) x (GCDMonoid.gcd f (derivative f)) = 0<GOAL>∃ x, 1 < Multiset.count x f.roots
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Iic a) = ν (Iic a)<GOAL>μ = ν
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a b x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Iic a) = ν (Iic a)<GOAL>μ univ = ν univ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Iic a) = ν (Iic a)<VAR>a b : α<VAR>hlt : a < b<GOAL>μ (Ioc a b) = ν (Ioc a b)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Iic a) = ν (Iic a)<VAR>a b : α<VAR>hlt : a < b<GOAL>ν (Iic a) ≠ ⊤
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹¹ : TopologicalSpace α✝<VAR>inst✝¹⁰ : MeasurableSpace α✝<VAR>inst✝⁹ : OpensMeasurableSpace α✝<VAR>inst✝⁸ : MeasurableSpace δ<VAR>inst✝⁷ : LinearOrder α✝<VAR>inst✝⁶ : OrderClosedTopology α✝<VAR>a✝ b✝ x : α✝<VAR>α : Type u_5<VAR>inst✝⁵ : TopologicalSpace α<VAR>m : MeasurableSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : BorelSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>h : ∀ (a : α), μ (Iic a) = ν (Iic a)<VAR>a b : α<VAR>hlt : a < b<GOAL>μ (Iic a) ≠ ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<GOAL>p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑r < p.radius - ↑‖x‖₊<GOAL>↑r ≤ (p.changeOrigin x).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑‖x‖₊ + ↑r < p.radius<GOAL>↑r ≤ (p.changeOrigin x).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑‖x‖₊ + ↑r < p.radius<VAR>hr' : ↑‖x‖₊ < p.radius<GOAL>↑r ≤ (p.changeOrigin x).radius
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑‖x‖₊ + ↑r < p.radius<VAR>hr' : ↑‖x‖₊ < p.radius<GOAL>Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r : ℝ≥0<VAR>_h0 : 0 < r<VAR>hr : ↑‖x‖₊ + ↑r < p.radius<VAR>hr' : ↑‖x‖₊ < p.radius<VAR>this : ∀ (k : ℕ), ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k<GOAL>Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n