ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁸ : CommRing A<VAR>inst✝³⁷ : CommRing B<VAR>inst✝³⁶ : Algebra A B<VAR>inst✝³⁵ : Field K✝<VAR>inst✝³⁴ : Field L✝<VAR>inst✝³³ : Algebra A K✝<VAR>inst✝³² : IsFractionRing A K✝<VAR>inst✝³¹ : Algebra B L✝<VAR>inst✝³⁰ : Algebra K✝ L✝<VAR>inst✝²⁹ : Algebra A L✝<VAR>inst✝²⁸ : IsScalarTower A B L✝<VAR>inst✝²⁷ : IsScalarTower A K✝ L✝<VAR>inst✝²⁶ : IsIntegralClosure B A L✝<VAR>inst✝²⁵ : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²⁴ : CommRing Aₘ<VAR>inst✝²³ : CommRing Bₘ<VAR>inst✝²² : Algebra Aₘ Bₘ<VAR>inst✝²¹ : Algebra A Aₘ<VAR>inst✝²⁰ : Algebra B Bₘ<VAR>inst✝¹⁹ : Algebra A Bₘ<VAR>inst✝¹⁸ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁷ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁶ : IsLocalization M Aₘ<VAR>inst✝¹⁵ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹⁴ : IsIntegrallyClosed A<VAR>inst✝¹³ : IsDomain A<VAR>inst✝¹² : IsIntegrallyClosed A<VAR>inst✝¹¹ : IsDomain B<VAR>inst✝¹⁰ : IsIntegrallyClosed B<VAR>inst✝⁹ : Module.Finite A B<VAR>inst✝⁸ : NoZeroSMulDivisors A B<VAR>inst✝⁷ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁹ : IsIntegralClosure B A L<VAR>this✝⁸ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁷ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁶ : IsScalarTower A Aₘ K<VAR>this✝⁵ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁴ : Algebra Bₘ L := g.toAlgebra<VAR>this✝³ : IsScalarTower B Bₘ L<VAR>this✝² : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝¹ : IsScalarTower Aₘ K L<VAR>this✝ : IsScalarTower Aₘ Bₘ L<VAR>this : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁸ : CommRing A<VAR>inst✝³⁷ : CommRing B<VAR>inst✝³⁶ : Algebra A B<VAR>inst✝³⁵ : Field K✝<VAR>inst✝³⁴ : Field L✝<VAR>inst✝³³ : Algebra A K✝<VAR>inst✝³² : IsFractionRing A K✝<VAR>inst✝³¹ : Algebra B L✝<VAR>inst✝³⁰ : Algebra K✝ L✝<VAR>inst✝²⁹ : Algebra A L✝<VAR>inst✝²⁸ : IsScalarTower A B L✝<VAR>inst✝²⁷ : IsScalarTower A K✝ L✝<VAR>inst✝²⁶ : IsIntegralClosure B A L✝<VAR>inst✝²⁵ : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²⁴ : CommRing Aₘ<VAR>inst✝²³ : CommRing Bₘ<VAR>inst✝²² : Algebra Aₘ Bₘ<VAR>inst✝²¹ : Algebra A Aₘ<VAR>inst✝²⁰ : Algebra B Bₘ<VAR>inst✝¹⁹ : Algebra A Bₘ<VAR>inst✝¹⁸ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁷ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁶ : IsLocalization M Aₘ<VAR>inst✝¹⁵ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹⁴ : IsIntegrallyClosed A<VAR>inst✝¹³ : IsDomain A<VAR>inst✝¹² : IsIntegrallyClosed A<VAR>inst✝¹¹ : IsDomain B<VAR>inst✝¹⁰ : IsIntegrallyClosed B<VAR>inst✝⁹ : Module.Finite A B<VAR>inst✝⁸ : NoZeroSMulDivisors A B<VAR>inst✝⁷ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹⁰ : IsIntegralClosure B A L<VAR>this✝⁹ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁸ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁷ : IsScalarTower A Aₘ K<VAR>this✝⁶ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁵ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁴ : IsScalarTower B Bₘ L<VAR>this✝³ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝² : IsScalarTower Aₘ K L<VAR>this✝¹ : IsScalarTower Aₘ Bₘ L<VAR>this✝ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this : FiniteDimensional K L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁸ : CommRing A<VAR>inst✝³⁷ : CommRing B<VAR>inst✝³⁶ : Algebra A B<VAR>inst✝³⁵ : Field K✝<VAR>inst✝³⁴ : Field L✝<VAR>inst✝³³ : Algebra A K✝<VAR>inst✝³² : IsFractionRing A K✝<VAR>inst✝³¹ : Algebra B L✝<VAR>inst✝³⁰ : Algebra K✝ L✝<VAR>inst✝²⁹ : Algebra A L✝<VAR>inst✝²⁸ : IsScalarTower A B L✝<VAR>inst✝²⁷ : IsScalarTower A K✝ L✝<VAR>inst✝²⁶ : IsIntegralClosure B A L✝<VAR>inst✝²⁵ : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²⁴ : CommRing Aₘ<VAR>inst✝²³ : CommRing Bₘ<VAR>inst✝²² : Algebra Aₘ Bₘ<VAR>inst✝²¹ : Algebra A Aₘ<VAR>inst✝²⁰ : Algebra B Bₘ<VAR>inst✝¹⁹ : Algebra A Bₘ<VAR>inst✝¹⁸ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁷ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁶ : IsLocalization M Aₘ<VAR>inst✝¹⁵ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹⁴ : IsIntegrallyClosed A<VAR>inst✝¹³ : IsDomain A<VAR>inst✝¹² : IsIntegrallyClosed A<VAR>inst✝¹¹ : IsDomain B<VAR>inst✝¹⁰ : IsIntegrallyClosed B<VAR>inst✝⁹ : Module.Finite A B<VAR>inst✝⁸ : NoZeroSMulDivisors A B<VAR>inst✝⁷ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹¹ : IsIntegralClosure B A L<VAR>this✝¹⁰ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁸ : IsScalarTower A Aₘ K<VAR>this✝⁷ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁶ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁵ : IsScalarTower B Bₘ L<VAR>this✝⁴ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝³ : IsScalarTower Aₘ K L<VAR>this✝² : IsScalarTower Aₘ Bₘ L<VAR>this✝¹ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this✝ : FiniteDimensional K L<VAR>this : IsIntegralClosure Bₘ Aₘ L<GOAL>(algebraMap A Aₘ) ((intNorm A B) x) = (intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁸ : CommRing A<VAR>inst✝³⁷ : CommRing B<VAR>inst✝³⁶ : Algebra A B<VAR>inst✝³⁵ : Field K✝<VAR>inst✝³⁴ : Field L✝<VAR>inst✝³³ : Algebra A K✝<VAR>inst✝³² : IsFractionRing A K✝<VAR>inst✝³¹ : Algebra B L✝<VAR>inst✝³⁰ : Algebra K✝ L✝<VAR>inst✝²⁹ : Algebra A L✝<VAR>inst✝²⁸ : IsScalarTower A B L✝<VAR>inst✝²⁷ : IsScalarTower A K✝ L✝<VAR>inst✝²⁶ : IsIntegralClosure B A L✝<VAR>inst✝²⁵ : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²⁴ : CommRing Aₘ<VAR>inst✝²³ : CommRing Bₘ<VAR>inst✝²² : Algebra Aₘ Bₘ<VAR>inst✝²¹ : Algebra A Aₘ<VAR>inst✝²⁰ : Algebra B Bₘ<VAR>inst✝¹⁹ : Algebra A Bₘ<VAR>inst✝¹⁸ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁷ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁶ : IsLocalization M Aₘ<VAR>inst✝¹⁵ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹⁴ : IsIntegrallyClosed A<VAR>inst✝¹³ : IsDomain A<VAR>inst✝¹² : IsIntegrallyClosed A<VAR>inst✝¹¹ : IsDomain B<VAR>inst✝¹⁰ : IsIntegrallyClosed B<VAR>inst✝⁹ : Module.Finite A B<VAR>inst✝⁸ : NoZeroSMulDivisors A B<VAR>inst✝⁷ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝⁶ : IsDomain Aₘ<VAR>inst✝⁵ : IsIntegrallyClosed Aₘ<VAR>inst✝⁴ : IsDomain Bₘ<VAR>inst✝³ : IsIntegrallyClosed Bₘ<VAR>inst✝² : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝¹ : Module.Finite Aₘ Bₘ<VAR>inst✝ : Algebra.IsSeparable (FractionRing Aₘ) (FractionRing Bₘ)<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹¹ : IsIntegralClosure B A L<VAR>this✝¹⁰ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁸ : IsScalarTower A Aₘ K<VAR>this✝⁷ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁶ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁵ : IsScalarTower B Bₘ L<VAR>this✝⁴ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝³ : IsScalarTower Aₘ K L<VAR>this✝² : IsScalarTower Aₘ Bₘ L<VAR>this✝¹ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this✝ : FiniteDimensional K L<VAR>this : IsIntegralClosure Bₘ Aₘ L<GOAL>(algebraMap Aₘ K) ((algebraMap A Aₘ) ((intNorm A B) x)) = (algebraMap Aₘ K) ((intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x))
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a✝ b c a : G<GOAL>a * a⁻¹ = 1
<VAR>Fq F : Type<VAR>inst✝⁴ : Field Fq<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra Fq[X] F<VAR>inst✝¹ : Algebra (RatFunc Fq) F<VAR>inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F<GOAL>¬IsField ↥(ringOfIntegers Fq F)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v✝ v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, a ∈ f x<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∃ a ∈ v.setsAt x ∩ f x, a ⊆ closedBall x ε
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v✝ v : VitaliFamily μ<VAR>f : α → Set (Set α)<VAR>s : Set α<VAR>h : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, a ∈ f x<VAR>x : α<VAR>hx : x ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>a : Set α<VAR>av : a ∈ v.setsAt x<VAR>ha : a ⊆ closedBall x ε<VAR>af : a ∈ f x<GOAL>∃ a ∈ v.setsAt x ∩ f x, a ⊆ closedBall x ε
<VAR>α : Type u<VAR>l✝ l' : List α<VAR>x : α<VAR>l : List α<GOAL>(x :: l).cyclicPermutations.length = l.length + 1
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : ConcreteCategory C<VAR>inst✝⁵ : HasForget₂ C Ab<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : (forget₂ C Ab).Additive<VAR>inst✝² : (forget₂ C Ab).PreservesHomology<VAR>inst✝¹ : HasZeroObject C<VAR>S : ShortComplex C<VAR>inst✝ : S.HasHomology<VAR>x₂ : ↑((forget₂ C Ab).obj S.X₂)<VAR>hx₂ : ((forget₂ C Ab).map S.g) x₂ = 0<GOAL>((forget₂ C Ab).map S.iCycles) ((S.mapCyclesIso (forget₂ C Ab)).hom ((S.map (forget₂ C Ab)).abCyclesIso.inv ⟨x₂, hx₂⟩)) = x₂
<VAR>α : Type u<VAR>hα : Nonempty α<VAR>a : α<VAR>l : List α<VAR>h : ∀ (n : ℕ), (a :: l).rotate n = a :: l<VAR>n : ℕ<VAR>h₁ : n < (a :: l).length<VAR>h₂ : n < (replicate (a :: l).length a).length<GOAL>(a :: l)[n] = (replicate (a :: l).length a)[n]
<VAR>α : Type u<VAR>hα : Nonempty α<VAR>a : α<VAR>l : List α<VAR>x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1<VAR>n : ℕ<VAR>b : α<VAR>hb : a :: l = replicate (a :: l).length b<GOAL>(a :: l).rotate n = a :: l
<VAR>m n k : ℕ<GOAL>(m + n).choose k = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : IsFilteredOrEmpty C<VAR>j₁ j₂ : C<VAR>f g h : j₁ ⟶ j₂<GOAL>f ≫ coeq₃Hom f g h = g ≫ coeq₃Hom f g h
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<GOAL>(a.wronskian b).natDegree < a.natDegree + b.natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<GOAL>(a.wronskian b).natDegree < a.natDegree + b.natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.wronskian b).natDegree < a.natDegree + b.natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>↑(a.wronskian b).natDegree < ↑a.natDegree + ↑b.natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>(a.wronskian b).degree = ↑(a.wronskian b).natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a.degree = ↑a.natDegree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a b : R[X]<VAR>hw : a.wronskian b ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>b.degree = ↑b.natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>x : ℚ<GOAL>Integrable (fun a => (preCDF ρ x a).toReal) ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>x : ℚ<GOAL>AEStronglyMeasurable (fun a => (preCDF ρ x a).toReal) ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>x : ℚ<VAR>t : Set α<VAR>x✝¹ : MeasurableSet t<VAR>x✝ : ρ.fst t ≠ ⊤<GOAL>∫⁻ (x_1 : α) in t, ↑‖(preCDF ρ x x_1).toReal‖₊ ∂ρ.fst ≤ ρ.fst univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Filter α<VAR>G : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>m : α → β<GOAL>SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<GOAL>HasDerivWithinAt f^[n] (f' ^ n) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : 𝕜 → 𝕜<VAR>f' : 𝕜<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : MapsTo f s s<VAR>n : ℕ<VAR>this : HasFDerivWithinAt f^[n] (smulRight 1 f' ^ n) s x<GOAL>HasDerivWithinAt f^[n] (f' ^ n) s x
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>x : ℤ<GOAL>x ∈ filter (fun x => r ∣ x) (Ico a b) ↔ x ∈ map { toFun := fun x => x * r, inj' := ⋯ } (Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)
<VAR>a b r : ℤ<VAR>hr : 0 < r<VAR>x : ℤ<GOAL>((a ≤ x ∧ x < b) ∧ ∃ c, x = c * r) ↔ ∃ a_1, (a ≤ a_1 * r ∧ a_1 * r < b) ∧ { toFun := fun x => x * r, inj' := ⋯ } a_1 = x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A✝ : Type u_4<VAR>inst✝¹ : AddGroup A✝<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>A A' B : Subgroup G<VAR>hA : A ≤ B<VAR>hA' : A' ≤ B<GOAL>(A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A✝ : Type u_4<VAR>inst✝¹ : AddGroup A✝<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>A A' B : Subgroup G<VAR>hA : A ≤ B<VAR>hA' : A' ≤ B<GOAL>map B.subtype ((A ⊔ A').subgroupOf B) = map B.subtype (A.subgroupOf B ⊔ A'.subgroupOf B)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A✝ : Type u_4<VAR>inst✝¹ : AddGroup A✝<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>A A' B : Subgroup G<VAR>hA : A ≤ B<VAR>hA' : A' ≤ B<GOAL>B ⊓ (A ⊔ A') = B ⊓ A ⊔ B ⊓ A'
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<GOAL>absNorm I = 1 ↔ I = ⊤
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : DecidableEq p<VAR>inst✝⁶ : DecidableEq q<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Fintype p<VAR>inst✝² : Fintype q<VAR>inst✝¹ : Fintype l<VAR>inst✝ : Invertible 2<GOAL>PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>q : Type u_3<VAR>l : Type u_4<VAR>R : Type u₂<VAR>inst✝⁸ : DecidableEq n<VAR>inst✝⁷ : DecidableEq p<VAR>inst✝⁶ : DecidableEq q<VAR>inst✝⁵ : DecidableEq l<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Fintype p<VAR>inst✝² : Fintype q<VAR>inst✝¹ : Fintype l<VAR>inst✝ : Invertible 2<GOAL>fromBlocks (1 * 1 + 0 * 0) (1 * 0 + 0 * ⅟(PD l R)) (0 * 1 + PD l R * 0) (0 * 0 + 1) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : ChartedSpace H H'<VAR>x : M'<VAR>y : E<VAR>hy : y ∈ (extChartAt I x).target<VAR>this : ChartedSpace H M' := ChartedSpace.comp H H' M'<GOAL>writtenInExtChartAt I I x (↑(chartAt H' x)) y = y
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<VAR>H : denom g z = 0<GOAL>False
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<VAR>H : denom g z = 0<VAR>DET : 0 < ↑(GeneralLinearGroup.det ↑g)<GOAL>False
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<VAR>H : denom g z = 0<VAR>DET : 0 < ↑(GeneralLinearGroup.det ↑g)<VAR>hz : 0 < (↑z).im<GOAL>False
<VAR>g : ↥GL(2, ℝ)⁺<VAR>z : ℍ<VAR>H : denom g z = 0<VAR>DET : 0 < (↑↑g).det<VAR>hz : 0 < (↑z).im<GOAL>False
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>f : X ⟶ Y<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>(s.cofan Δ).inj A ≫ f.app Δ = s.φ f (unop A.fst).len ≫ Y.map A.e.op
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>f : X ⟶ Y<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<GOAL>s.ι (unop A.fst).len ≫ X.map A.e.op ≫ f.app Δ = s.ι (unop A.fst).len ≫ f.app (op [(unop A.fst).len]) ≫ Y.map A.e.op
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>x y : Quotient G α<VAR>h : x.orbit = y.orbit<GOAL>x = y
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>x y : Quotient G α<VAR>h : Setoid.r (Quotient.out' x) (Quotient.out' y)<GOAL>x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : 1 ≤ f<GOAL>1 < ∏ i : ι, f i ↔ 1 < f
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>x y : γ<GOAL>0 < dist x y ↔ x ≠ y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α ↪ β<VAR>s : Finset α<GOAL>↑((map f s).preimage ⇑f ⋯) = ↑s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>cg : KernelFork S.g<VAR>hg : IsLimit cg<VAR>cf : CokernelCofork S.f<VAR>hf : IsColimit cf<GOAL>S.Exact ↔ Fork.ι cg ≫ Cofork.π cf = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>cg : KernelFork S.g<VAR>hg : IsLimit cg<VAR>cf : CokernelCofork S.f<VAR>hf : IsColimit cf<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>cg : KernelFork S.g<VAR>hg : IsLimit cg<VAR>cf : CokernelCofork S.f<VAR>hf : IsColimit cf<VAR>e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg<VAR>e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>cg : KernelFork S.g<VAR>hg : IsLimit cg<VAR>cf : CokernelCofork S.f<VAR>hf : IsColimit cf<VAR>e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg<VAR>e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf<VAR>this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<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>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Subsingleton R<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<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>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Subsingleton R<VAR>this : Subsingleton M<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<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>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Subsingleton R<VAR>this✝ : Subsingleton M<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>Module.rank R M = 1
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<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>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Subsingleton R<VAR>this✝ : Subsingleton M<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>∀ (i : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }), #↑↑i ≤ 1
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : Ring R'<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>inst✝² : Module R' M'<VAR>inst✝¹ : Module R' M₁<VAR>inst✝ : Subsingleton R<VAR>this✝ : Subsingleton M<VAR>this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }<GOAL>∀ w < 1, ∃ i, w < #↑↑i