ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<GOAL>‖↑(let_fun h1 := ⋯; let z1 := ⟨↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) / ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)), h1⟩; let z' := ↑(newton_seq_aux hnorm n) - z1; ⟨z', ⋯⟩) - ↑(newton_seq_aux hnorm n)‖ = ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) F‖ / ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) (Polynomial.derivative F)‖
<VAR>X✝ X : LocallyRingedSpace<VAR>x : ↑↑X.toPresheafedSpace<GOAL>IsLocalRingHom (PresheafedSpace.Hom.stalkMap (𝟙 X.toSheafedSpace) x)
<VAR>X✝ X : LocallyRingedSpace<VAR>x : ↑↑X.toPresheafedSpace<GOAL>IsLocalRingHom (𝟙 (X.presheaf.stalk x))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atBot, p x<GOAL>∀ᶠ (n : ℚ) in atBot, p ↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atBot, p x<GOAL>∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<GOAL>‖lsmul 𝕜 𝕜'‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>x : 𝕜'<GOAL>‖(lsmul 𝕜 𝕜') x‖ ≤ 1 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x : 𝕜'), ‖(lsmul 𝕜 𝕜') x‖ ≤ N * ‖x‖<GOAL>1 ≤ N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x : 𝕜'), ‖(lsmul 𝕜 𝕜') x‖ ≤ N * ‖x‖<VAR>y : E<VAR>hy : y ≠ 0<GOAL>1 ≤ N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x : 𝕜'), ‖(lsmul 𝕜 𝕜') x‖ ≤ N * ‖x‖<VAR>y : E<VAR>hy : y ≠ 0<VAR>this : ‖((lsmul 𝕜 𝕜') 1) y‖ ≤ N * ‖1‖ * ‖y‖<GOAL>1 ≤ N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x : 𝕜'), ‖(lsmul 𝕜 𝕜') x‖ ≤ N * ‖x‖<VAR>y : E<VAR>hy : y ≠ 0<VAR>this : ‖y‖ ≤ N * ‖y‖<GOAL>1 ≤ N
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>𝕜' : Type u_3<VAR>inst✝⁴ : NormedField 𝕜'<VAR>inst✝³ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝² : NormedSpace 𝕜' E<VAR>inst✝¹ : IsScalarTower 𝕜 𝕜' E<VAR>inst✝ : Nontrivial E<VAR>N : ℝ<VAR>x✝ : N ≥ 0<VAR>h : ∀ (x : 𝕜'), ‖(lsmul 𝕜 𝕜') x‖ ≤ N * ‖x‖<VAR>y : E<VAR>hy : y ≠ 0<VAR>this : ‖y‖ ≤ N * ‖y‖<GOAL>1 * ‖y‖ ≤ N * ‖y‖
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>-b ≡ -a [PMOD p] ↔ a ≡ b [PMOD p]
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearIndependent R u
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearIndependent R (u ∘ Sum.inl) ∧ LinearIndependent R (u ∘ Sum.inr) ∧ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearIndependent R (u ∘ Sum.inl)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearIndependent R v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>hv : LinearIndependent R v<VAR>u : ι ⊕ ι' → ↑S.X₂<VAR>hw : LinearIndependent R (⇑S.g ∘ u ∘ Sum.inr)<VAR>hm : Mono S.f<VAR>huv : u ∘ Sum.inl = ⇑S.f ∘ v<GOAL>LinearMap.ker S.f = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<GOAL>s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>s t : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<GOAL>¬s.infsep < d ↔ ¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>x : α<VAR>inst : OrientedCmp cmp<VAR>t : RBNode α<GOAL>(ins cmp x t).reverse = ins (flip cmp) x t.reverse
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a b : α<VAR>hab : a < b<GOAL>∃ x, a ⋖ x ∧ x ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<GOAL>∃ x, a ⋖ x ∧ x ≤ sSup s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<VAR>hcon : ¬∃ x, a ⋖ x ∧ x ≤ sSup s<VAR>x : α<VAR>hx : x ∈ s<GOAL>x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<VAR>x : α<VAR>hx : x ∈ s<VAR>hcon : ∀ x ≤ sSup s, ¬a ⋖ x<GOAL>x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<VAR>x : α<VAR>hx : x ∈ s<VAR>hcon : ¬a ⋖ x ⊔ a<GOAL>x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<VAR>x : α<VAR>hx : x ∈ s<VAR>hcon : ¬a ⋖ x ⊔ a<VAR>hbot : x ⊓ a = ⊥<GOAL>x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsUpperModularLattice α<VAR>inst✝ : IsAtomistic α<VAR>a : α<VAR>s : Set α<VAR>h : ∀ a ∈ s, IsAtom a<VAR>hab : a < sSup s<VAR>x : α<VAR>hx : x ∈ s<VAR>hcon : ¬a ⋖ x ⊔ a<VAR>h_inf : x ⊓ a = x<GOAL>x ≤ a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsNoetherian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>∀ (a : Submodule R N), Submodule.map ((LinearMap.ker f).liftQ f ⋯) (Submodule.comap ((LinearMap.ker f).liftQ f ⋯) a) = a ⊓ LinearMap.range f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsNoetherian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>∀ (a : Submodule R N), Submodule.comap g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ LinearMap.range f
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z✝ : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A Z : C<VAR>f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>f = g
<VAR>I : Type u<VAR>inst✝¹⁰ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁹ : Category.{u_2, u_1} C<VAR>inst✝⁸ : MonoidalCategory C<VAR>Z✝ : C<VAR>X₁ X₂ X₃ : GradedObject I C<VAR>inst✝⁷ : X₁.HasTensor X₂<VAR>inst✝⁶ : X₂.HasTensor X₃<VAR>inst✝⁵ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝⁴ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>Y₁ Y₂ Y₃ : GradedObject I C<VAR>inst✝³ : Y₁.HasTensor Y₂<VAR>inst✝² : Y₂.HasTensor Y₃<VAR>inst✝¹ : (tensorObj Y₁ Y₂).HasTensor Y₃<VAR>inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)<VAR>j : I<VAR>A Z : C<VAR>f g : Z ⊗ tensorObj X₁ (tensorObj X₂ X₃) j ⟶ A<VAR>H : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>hZ : HasLeftTensor₃ObjExt Z X₁ X₂ X₃ j<VAR>h : ∀ (i₁ i₂ i₃ : I) (h : i₁ + i₂ + i₃ = j), Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f = Z ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g<GOAL>∀ (j_1 : Discrete ↑(r₁₂₃ ⁻¹' {j})), (((curriedTensor C).obj Z).mapCocone (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app j_1 ≫ f = (((curriedTensor C).obj Z).mapCocone (cofan₃MapBifunctorBifunctor₂₃MapObj (curriedTensor C) (curriedTensor C) ρ₂₃ X₁ X₂ X₃ j)).ι.app j_1 ≫ g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>∫ (x : X) in t \ k ∪ s \ k, f x ∂μ = ∫ (x : X) in s \ k, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>t \ k ∪ s \ k =ᶠ[ae μ] s \ k
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>μ ((t \ k) \ (s \ k)) = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>μ (t \ k) = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0<VAR>haux : StronglyMeasurable f<VAR>H : IntegrableOn f (s ∪ t) μ<VAR>k : Set X := f ⁻¹' {0}<VAR>hk : MeasurableSet k<VAR>h's : IntegrableOn f s μ<VAR>A : ∀ (u : Set X), ∫ (x : X) in u ∩ k, f x ∂μ = 0<GOAL>∀ᵐ (a : X) ∂μ, a ∉ t \ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I : Set β<GOAL>R.rightDual I ∈ R.leftFixedPoints
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I : Set β<GOAL>R.rightDual (R.leftDual (R.rightDual I)) ≤ R.rightDual I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>I : Set β<GOAL>R.rightDual I ≤ R.rightDual (R.leftDual (R.rightDual I))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>inst✝ : Nonempty ι<VAR>inhabited_h : Inhabited ι<GOAL>Function.Injective (col ι)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>σ.supportᶜ.card ≡ Fintype.card α [MOD p]
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>p ∣ σ.cycleType.sum
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>σ.supportᶜ.card ≤ Fintype.card α
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<GOAL>sInf (a • s) = a • sInf s
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>sInf (a • ∅) = a • sInf ∅
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : MulActionWithZero α ℝ<VAR>inst✝ : OrderedSMul α ℝ<VAR>a : α<VAR>ha : 0 ≤ a<VAR>s : Set ℝ<VAR>hs : s.Nonempty<GOAL>sInf (a • s) = a • sInf s
<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 : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>hf : Surjective ⇑f<VAR>p : MvPolynomial σ S₁<GOAL>∃ a, (map f) a = p
<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 : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>hf : Surjective ⇑f<VAR>i : σ →₀ ℕ<VAR>fr : S₁<GOAL>∃ a, (map f) a = (monomial i) fr
<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 : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>hf : Surjective ⇑f<VAR>a b : MvPolynomial σ S₁<VAR>ha : ∃ a_1, (map f) a_1 = a<VAR>hb : ∃ a, (map f) a = b<GOAL>∃ a_1, (map f) a_1 = a + b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>ν a[fun x => κ.densityProcess ν j a x s|↑(countableFiltration γ) i] =ᶠ[ae (ν a)] fun x => κ.densityProcess ν i a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Integrable (fun x => κ.densityProcess ν j a x s) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ (s_1 : Set γ), MeasurableSet s_1 → (ν a) s_1 < ⊤ → IntegrableOn (fun x => κ.densityProcess ν i a x s) s_1 (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ (s_1 : Set γ), MeasurableSet s_1 → (ν a) s_1 < ⊤ → ∫ (x : γ) in s_1, κ.densityProcess ν i a x s ∂ν a = ∫ (x : γ) in s_1, κ.densityProcess ν j a x s ∂ν a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>i j : ℕ<VAR>hij : i ≤ j<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>AEStronglyMeasurable' (↑(countableFiltration γ) i) (fun x => κ.densityProcess ν i a x s) (ν a)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>f : L ≃ₐ[K] L<GOAL>f ∈ ⊥.fixingSubgroup ↔ f ∈ ⊤
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>f : L ≃ₐ[K] L<VAR>x✝ : f ∈ ⊤<GOAL>f ∈ ⊥.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>f : L ≃ₐ[K] L<VAR>x✝ : f ∈ ⊤<VAR>x : L<VAR>hx : x ∈ ⊥<GOAL>f • ↑⟨x, hx⟩ = ↑⟨x, hx⟩
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>f : L ≃ₐ[K] L<VAR>x✝ : f ∈ ⊤<VAR>x : L<VAR>hx✝ : x ∈ ⊥<VAR>hx : x ∈ Set.range ⇑(algebraMap K L)<GOAL>f • ↑⟨x, hx✝⟩ = ↑⟨x, hx✝⟩
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>f : L ≃ₐ[K] L<VAR>x✝ : f ∈ ⊤<VAR>y : K<VAR>hx : (algebraMap K L) y ∈ ⊥<GOAL>f • ↑⟨(algebraMap K L) y, hx⟩ = ↑⟨(algebraMap K L) y, hx⟩
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>i : ι<VAR>a : α i<VAR>b : β i<VAR>x : γ i<GOAL>⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>i : ι<VAR>a : α i<VAR>b : β i<VAR>x : γ i<GOAL>(∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>x : α<VAR>y : Set α<VAR>hx : x ∈ s<VAR>hy : y ⊆ s<VAR>hxy : x ∉ y<GOAL>Disjoint x (sSup y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>x : α<VAR>y : Set α<VAR>hx : x ∈ s<VAR>hy : y ⊆ s<VAR>hxy : x ∉ y<VAR>this : Disjoint x (sSup (insert x y \ {x}))<GOAL>Disjoint x (sSup y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>x : α<VAR>y : Set α<VAR>hx : x ∈ s<VAR>hy : y ⊆ s<VAR>hxy : x ∉ y<VAR>this : Disjoint x (sSup y)<GOAL>Disjoint x (sSup y)
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : AddTorsor G P<VAR>v : G<VAR>p₁ p₂ : P<GOAL>v +ᵥ p₁ -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℕ<GOAL>derivative (C a * X ^ n) = C (a * ↑n) * X ^ (n - 1)
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : f.IsClosable<GOAL>∃! f', f.graph.topologicalClosure = f'.graph