ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>a✝ : Nontrivial β<VAR>inhabited_h : Inhabited β<VAR>S : Set (Set β)<VAR>hSc : S.Countable<VAR>hc : MeasurableSpace.CountablyGenerated β<VAR>h : NullMeasurable f μ<VAR>T : Set β → Set α<VAR>hTf : ∀ s ∈ S, T s ⊆ f ⁻¹' s<VAR>hTm : ∀ s ∈ S, MeasurableSet (T s)<VAR>hTeq : ∀ s ∈ S, T s =ᶠ[ae μ] f ⁻¹' s<VAR>U : Set β → Set α<VAR>hUf : ∀ s ∈ S, U s ⊇ f ⁻¹' s<VAR>hUm : ∀ s ∈ S, MeasurableSet (U s)<VAR>hUeq : ∀ s ∈ S, U s =ᶠ[ae μ] f ⁻¹' s<VAR>v : Set α := ⋃ s ∈ S, U s \ T s<VAR>hvm : MeasurableSet v<VAR>hvμ : μ v = 0<GOAL>Measurable (vᶜ.restrict (v.piecewise (fun x => default) f))
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension S A B<GOAL>IsCyclotomicExtension (S ∪ {n}) A B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension S A B<VAR>s : ℕ+<VAR>hs : s ∈ S ∪ {n}<GOAL>∃ r, IsPrimitiveRoot r ↑s
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : ∀ s ∈ S, n ∣ s<VAR>hS : S.Nonempty<VAR>H : IsCyclotomicExtension S A B<GOAL>adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1} = ⊤
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort u_1<VAR>inst✝ : Group G<VAR>ts' : ι → TopologicalSpace G<VAR>h' : ∀ (i : ι), TopologicalGroup G<GOAL>TopologicalGroup G
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<VAR>f : α →₀ M<GOAL>f.support.card = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Splits (j.comp i) f<VAR>lift : (a : F) → a ∈ (map (j.comp i) f).roots → L<VAR>lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a<GOAL>Splits i f
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Splits (j.comp i) f<VAR>lift : (a : F) → a ∈ (map (j.comp i) f).roots → L<VAR>lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a<GOAL>∃ s, map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Splits (j.comp i) f<VAR>lift : (a : F) → a ∈ (map (j.comp i) f).roots → L<VAR>lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a<GOAL>map j (map i f) = map j (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Splits (j.comp i) f<VAR>lift : (a : F) → a ∈ (map (j.comp i) f).roots → L<VAR>lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a<GOAL>C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod = map j (C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) (Multiset.pmap lift (map (j.comp i) f).roots ⋯)).prod)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>j : L →+* F<VAR>f : K[X]<VAR>h : Splits (j.comp i) f<VAR>lift : (a : F) → a ∈ (map (j.comp i) f).roots → L<VAR>lift_eq : ∀ (a : F) (a_1 : a ∈ (map (j.comp i) f).roots), j (lift a a_1) = a<GOAL>C ((j.comp i) f.leadingCoeff) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod = C (j (i f.leadingCoeff)) * (Multiset.map (fun a => X - C a) (map (j.comp i) f).roots).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<GOAL>¬ν ≤ μ ↔ ∃ s, μ s < ν s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>f : α →o β<VAR>g : β →o γ<VAR>x : β<VAR>c : Chain α<VAR>z : β<GOAL>((OrderHom.const α) x) (ωSup c) ≤ z ↔ ωSup (c.map ((OrderHom.const α) x)) ≤ z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>inst✝² : OmegaCompletePartialOrder α<VAR>inst✝¹ : OmegaCompletePartialOrder β<VAR>inst✝ : OmegaCompletePartialOrder γ<VAR>f : α →o β<VAR>g : β →o γ<VAR>x : β<VAR>c : Chain α<VAR>z : β<GOAL>Function.const α x (ωSup c) ≤ z ↔ ∀ (i : ℕ), (Function.const α x ∘ ⇑c) i ≤ z
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᶠ[ae μ] g<GOAL>μ.withDensity f = μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᶠ[ae μ] g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity f) s = (μ.withDensity g) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ≥0∞<VAR>h : f =ᶠ[ae μ] g<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
<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<GOAL>corootSpace 0 = ⊥
<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>x : ↥H<VAR>hx : x ∈ corootSpace 0<GOAL>x ∈ ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : ↥H<VAR>hx : x ∈ corootSpace 0<GOAL>{x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x} = {0}
<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>x : ↥H<VAR>hx : x ∈ corootSpace 0<GOAL>∀ x ∈ {x | ∃ y ∈ H, ∃ z ∈ H, ⁅y, z⁆ = x}, x = 0
<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>x : ↥H<VAR>hx : x ∈ corootSpace 0<VAR>y : L<VAR>hy : y ∈ H<VAR>z : L<VAR>hz : z ∈ H<GOAL>⁅y, z⁆ = 0
<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>x : ↥H<VAR>hx : x ∈ corootSpace 0<VAR>y : L<VAR>hy : y ∈ H<VAR>z : L<VAR>hz : z ∈ H<GOAL>⁅⟨y, hy⟩, ⟨z, hz⟩⁆ = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>p n : ℕ<VAR>inst✝² : ExpChar R p<VAR>f : R[X]<VAR>inst✝¹ : PerfectRing R p<VAR>inst✝ : DecidableEq R<GOAL>Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ lifts f ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>(∀ (n : ℕ), p.coeff n ∈ f.rangeS) ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f✝ g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>f : ↥(Lp E 1 μ)<GOAL>setToFun μ T hT ↑↑f = (setToL1 hT) f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>x ∈ ↑(torsion R M) ↔ x ∈ {x | (span R {x}).annihilator ≠ ⊥}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : DecidableEq R<GOAL>Finset.image (⇑(frobenius R p)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : DecidableEq R<GOAL>Finset.image (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots.toFinset ⊆ f.roots.toFinset
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : DecidableEq R<GOAL>p ^ 1 = p
<VAR>x : ℂ<GOAL>tan (↑π / 2 - x) = (tan x)⁻¹
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] M<GOAL>(trace R (Module.Dual R M)) (Module.Dual.transpose f) = (trace R M) f
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝¹ : IsIntegral Y<VAR>inst✝ : Nonempty ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<GOAL>IsDomain ↑Γ(X, U)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝¹ : IsIntegral Y<VAR>inst✝ : Nonempty ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : U = f ⁻¹ᵁ f ''ᵁ U<GOAL>IsDomain ↑Γ(X, U)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝¹ : IsIntegral Y<VAR>inst✝ : Nonempty ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this : U = f ⁻¹ᵁ f ''ᵁ U<GOAL>IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)
<VAR>X✝ : Scheme<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>inst✝¹ : IsIntegral Y<VAR>inst✝ : Nonempty ↑↑X.toPresheafedSpace<VAR>U : X.Opens<VAR>hU : Nonempty ↑↑(↑U).toPresheafedSpace<VAR>this✝ : U = f ⁻¹ᵁ f ''ᵁ U<VAR>this : IsDomain ↑Γ(Y, f ''ᵁ U)<GOAL>IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<GOAL>of V ⋙q (lift φ).toPrefunctor = φ
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<GOAL>Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ
<VAR>V : Type u<VAR>inst✝¹ : Quiver V<VAR>V' : Type u'<VAR>inst✝ : Groupoid V'<VAR>φ✝ φ : V ⥤q V'<GOAL>Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ Quotient.lift redStep (Paths.lift (Quiver.Symmetrify.lift φ)) ⋯).toPrefunctor) = φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S : WSeq (WSeq α)<GOAL>S.join.destruct = S.destruct.bind destruct_join.aux
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>S : WSeq (WSeq α)<GOAL>Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>g : G<GOAL>of' k G g %ᵒᶠ g = 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u_2<VAR>f : ι → Cardinal.{u_2}<VAR>c : Cardinal.{u_2}<VAR>hι : #ι < c.ord.cof<GOAL>Cardinal.lift.{?u.33596, u_2} #ι < c.ord.cof
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>g : β → γ<VAR>a : Filter α<VAR>c : Filter γ<VAR>h : Tendsto (g ∘ f) a c<GOAL>map g (map f a) ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<GOAL>EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : b < a<GOAL>EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>h : G.Colorable 0<VAR>v : V<VAR>i : ℕ<VAR>hi : i < 0<GOAL>False
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMul ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<GOAL>ConvexOn ℝ univ ⇑p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : NormedSpace ℝ 𝕜<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : SMul ℝ E<VAR>inst✝ : IsScalarTower ℝ 𝕜 E<VAR>p : Seminorm 𝕜 E<VAR>x : E<VAR>x✝² : x ∈ univ<VAR>y : E<VAR>x✝¹ : y ∈ univ<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>x✝ : a + b = 1<GOAL>p (a • x + b • y) ≤ a • p x + b • p y
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<GOAL>ConformalAt f z ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<GOAL>IsConformalMap (fderiv ℝ f z) ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<GOAL>((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ∧ fderiv ℝ f z ≠ 0 ↔ (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<GOAL>fderiv ℝ f z ≠ 0 → (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<GOAL>((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f z<GOAL>((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f z<GOAL>(∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f z<GOAL>(∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))<GOAL>(∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ DifferentiableAt ℂ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))<GOAL>(∃ map, restrictScalars ℝ map = (fderiv ℝ f z).comp ↑conjCLE) ↔ ∃ g', restrictScalars ℝ g' = fderiv ℝ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))<VAR>g : ℂ →L[ℂ] ℂ<GOAL>(fderiv ℝ f z).comp ↑conjCLE = fderiv ℝ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z✝ : ℂ<VAR>f✝ : ℂ → E<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>h : fderiv ℝ f z ≠ 0<VAR>h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ) ((starRingEnd ℂ) z))<VAR>g : ℂ →L[ℂ] ℂ<VAR>this : fderiv ℝ (⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z) = ↑conjCLE<GOAL>(fderiv ℝ f z).comp ↑conjCLE = fderiv ℝ (f ∘ ⇑(starRingEnd ℂ)) ((starRingEnd ℂ) z)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : Fintype ι<VAR>l : (i : ι) → G i<VAR>i : ι<VAR>v : G i<GOAL>⟪(V i) v, ∑ j : ι, (V j) (l j)⟫_𝕜 = ⟪v, l i⟫_𝕜
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c<GOAL>∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c<GOAL>∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x ∂ENNReal.ofReal |c| • Measure.map (fun x => x * c) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c<GOAL>∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume = c⁻¹ • |c| • (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume - ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c<VAR>h : c < 0<GOAL>∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume = c⁻¹ • |c| • (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume - ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<VAR>A : MeasurableEmbedding fun x => x * c<VAR>h : 0 < c<GOAL>∫ (x : ℝ) in Ioc a b, f (x * c) ∂volume - ∫ (x : ℝ) in Ioc b a, f (x * c) ∂volume = c⁻¹ • |c| • (∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (a * c) (b * c), f (x * c) ∂volume - ∫ (x : ℝ) in (fun x => x * c) ⁻¹' Ioc (b * c) (a * c), f (x * c) ∂volume)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<GOAL>IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<GOAL>P = C (eval 0 P) + X * (P /ₘ X)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<GOAL>P %ₘ X + X * (P /ₘ X) = C (eval 0 P) + X * (P /ₘ X)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹³ : Ring R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M'<VAR>inst✝⁹ : AddCommGroup M₁<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R M'<VAR>inst✝⁶ : Module R M₁<VAR>F : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : CommRing F<VAR>inst✝⁴ : Ring E<VAR>inst✝³ : Algebra F E<VAR>inst✝² : StrongRankCondition F<VAR>inst✝¹ : NoZeroSMulDivisors F E<VAR>inst✝ : Nontrivial E<GOAL>Module.rank F ↥(toSubmodule ⊥) = 1