ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F✝ G✝ : C ⥤ D<VAR>X Y : C<VAR>F G : C ⥤ D<VAR>H I : D ⥤ E<VAR>α : F ≅ G<VAR>β : H ≅ I<VAR>x✝ : C<GOAL>((α.inv ≫ α.hom) ◫ (β.inv ≫ β.hom)).app x✝ = (𝟙 (G ⋙ I)).app x✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c✝ d✝ a b c d : α<GOAL>(a ⊔ b) \ c ≤ d ↔ a \ c ⊔ b \ c ≤ d
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d.degree ≠ n<GOAL>coeff d φ = 0
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : (weight 1) d ≠ n<GOAL>coeff d φ = 0
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝² : Monoid K<VAR>inst✝¹ : (i : ι) → Monoid (G i)<VAR>inst✝ : Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>motive : (con φ).Quotient → Prop<VAR>x : (con φ).Quotient<VAR>of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)<VAR>base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)<VAR>mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)<GOAL>motive x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → α<VAR>hf : Involutive f<VAR>a : α<VAR>l : List α<GOAL>a ∈ map f l ↔ f a ∈ l
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>|a * a| = a * a
<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 I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ↑(map f I) = ⇑f '' ↑I<GOAL>↑(map f I) = Submodule.map ↑f ↑I
<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 I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ↑(map f I) = ⇑f '' ↑I<GOAL>⇑f '' ↑I = ⇑↑f '' ↑↑I
<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>p q : R[X]<GOAL>(p * q).degree ≤ ↑(p.natDegree + 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>p q : R[X]<GOAL>p.degree + q.degree ≤ ↑(p.natDegree + 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>p q : R[X]<GOAL>p.degree + q.degree ≤ ↑p.natDegree + ↑q.natDegree
<VAR>s : Set Game<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddBelow s
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<GOAL>o.derivBFamily f = enumOrd (⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi))
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<GOAL>StrictMono (o.derivBFamily f) ∧ Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<GOAL>Set.range (o.derivBFamily f) = ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<GOAL>(∀ (a : Ordinal.{max u v}), o.derivBFamily f a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)) ∧ ∀ b ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi), ∃ a, o.derivBFamily f a = b
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<VAR>ha : a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)<GOAL>∃ a_1, o.derivBFamily f a_1 = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<VAR>ha : ∀ (i : Ordinal.{u}) (j : i < o), a ∈ fixedPoints (f i j)<GOAL>∃ a_1, o.derivBFamily f a_1 = a
<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>hg : Differentiable 𝕜 f<GOAL>(Differentiable 𝕜 fun y => f y - g y) ↔ Differentiable 𝕜 g
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : HeytingAlgebra α<VAR>inst✝¹ : HeytingAlgebra β<VAR>inst✝ : HeytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⇔ b) = f a ⇔ f b
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>huv : G.Adj u v<GOAL>(induce {u, v} G).Connected
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<GOAL>Function.Injective ⇑(coeHom E F)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<GOAL>Function.Injective DFunLike.coe
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : α<GOAL>Associates.mk a = 1 ↔ IsUnit a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>h : UniformInducing f<GOAL>Inducing f
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>G : SimpleGraph α<VAR>inst✝² : Fintype (Sym2 α)<VAR>inst✝¹ : NonAssocSemiring R<VAR>a b : α<VAR>e : Sym2 α<VAR>inst✝ : Fintype ↑(G.neighborSet a)<GOAL>(incMatrix R G * (incMatrix R G)ᵀ) a a = ↑(G.degree a)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>f : Π₀ (i : ι), Finset (α i)<GOAL>f.pi.card = f.prod fun i => ↑(f i).card
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (α i)<VAR>f : Π₀ (i : ι), Finset (α i)<GOAL>∏ i ∈ f.support, (f i).card = f.prod fun i => ↑(f i).card
<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 t : Set α<VAR>f✝ g f : α → ℝ≥0∞<GOAL>⨍⁻ (x : α), f x ∂μ = (∫⁻ (x : α), f x ∂μ) / μ univ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>hδ : 0 ≤ δ<VAR>t : ↑(Icc a b)<VAR>n : ℕ<VAR>ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))<GOAL>(fun a_1 => ↑a_1) t ≤ ↑(projIcc a b h ?m.54392)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>hδ : 0 ≤ δ<VAR>t : ↑(Icc a b)<VAR>n : ℕ<VAR>ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))<GOAL>|a + (n + 1) • δ - (a + n • δ)| ≤ δ
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>h : a ≤ b<VAR>δ : α<VAR>hδ : 0 ≤ δ<VAR>t : ↑(Icc a b)<VAR>n : ℕ<VAR>ht : t ∈ Icc (addNSMul h δ n) (addNSMul h δ (n + 1))<GOAL>|δ| ≤ δ
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>n : ℕ<VAR>y : F<GOAL>(X ^ q ^ n - C y).natSepDegree = 1
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<GOAL>e.symm ≫ₕ e' ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<GOAL>(e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<VAR>A : e.symm ≫ₕ f ∈ G<GOAL>(e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<VAR>A : e.symm ≫ₕ f ∈ G<VAR>B : f.symm ≫ₕ e' ∈ G<GOAL>(e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<VAR>A : e.symm ≫ₕ f ∈ G<VAR>B : f.symm ≫ₕ e' ∈ G<VAR>C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G<GOAL>(e.symm ≫ₕ e').restr s ∈ G
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝² : TopologicalSpace H<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>G : StructureGroupoid H<VAR>e e' : PartialHomeomorph M H<VAR>he : e ∈ maximalAtlas M G<VAR>he' : e' ∈ maximalAtlas M G<VAR>x : H<VAR>hx : x ∈ (e.symm ≫ₕ e').source<VAR>f : PartialHomeomorph M H := chartAt H (↑e.symm x)<VAR>s : Set H := e.target ∩ ↑e.symm ⁻¹' f.source<VAR>hs : IsOpen s<VAR>xs : x ∈ s<VAR>A : e.symm ≫ₕ f ∈ G<VAR>B : f.symm ≫ₕ e' ∈ G<VAR>C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G<VAR>D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s<GOAL>(e.symm ≫ₕ e').restr s ∈ G
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>eLpNormEssSup (c • f) μ = ↑‖c‖₊ * eLpNormEssSup f μ
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a b c : α<VAR>h₁ : a ≤ c<VAR>h₂ : b ≤ c<GOAL>max a b ≤ c
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ last n<GOAL>i.castPred hi < j ↔ i < j.castSucc
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p₁ p₂ : P<GOAL>g +ᵥ p₁ -ᵥ p₂ = g + (p₁ -ᵥ p₂)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>g : G<VAR>p₁ p₂ : P<GOAL>g +ᵥ p₁ -ᵥ p₂ +ᵥ p₂ = g + (p₁ -ᵥ p₂) +ᵥ p₂
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<GOAL>((hasseDeriv n) p).natDegree = p.natDegree - n
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : p.natDegree < n<GOAL>((hasseDeriv n) p).natDegree = p.natDegree - n
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>inst✝ : NoZeroSMulDivisors ℕ R<VAR>p : R[X]<VAR>n : ℕ<VAR>hn : n ≤ p.natDegree<GOAL>((hasseDeriv n) p).natDegree = p.natDegree - n
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>hfl : f.leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>hfd0 : 0 < f.degree<VAR>h0 : f.coeff 0 ∉ P ^ 2<VAR>hu : f.IsPrimitive<VAR>x✝ : f = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f : R[X]<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>hfl : f.leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P<VAR>hfd0✝ : 0 < f.degree<VAR>h0 : f.coeff 0 ∉ P ^ 2<VAR>hu : f.IsPrimitive<VAR>hf0 : f ≠ 0<VAR>hf : map (mk P) f = C ((mk P) f.leadingCoeff) * X ^ f.natDegree<VAR>hfd0 : 0 < f.natDegree<VAR>h : f.degree = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) (p * q) = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<VAR>hmp : m ≤ p.natDegree<GOAL>IsUnit p ∨ IsUnit q
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>p q : R[X]<VAR>hfl : (p * q).leadingCoeff ∉ P<VAR>hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P<VAR>hfd0✝ : 0 < (p * q).degree<VAR>h0 : (p * q).coeff 0 ∉ P ^ 2<VAR>hu : (p * q).IsPrimitive<VAR>hf0 : p * q ≠ 0<VAR>hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree<VAR>hfd0 : 0 < (p * q).natDegree<VAR>m n : ℕ<VAR>b c : (R ⧸ P)[X]<VAR>hmnd : m + n = (p * q).natDegree<VAR>hbc : C ((mk P) (p * q).leadingCoeff) = b * c<VAR>hp : map (mk P) p = b * X ^ m<VAR>hq : map (mk P) q = c * X ^ n<VAR>hmn : 0 < m → 0 < n → False<VAR>hpql0 : (mk P) (p * q).leadingCoeff ≠ 0<VAR>hp0 : p ≠ 0<VAR>hq0 : q ≠ 0<VAR>hbc0 : b.degree = 0 ∧ c.degree = 0<VAR>hmp : m ≤ p.natDegree<VAR>hnq : n ≤ q.natDegree<GOAL>IsUnit p ∨ IsUnit q