ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this : Algebra R' S' := f'.toAlgebra<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝ : Algebra R' S' := f'.toAlgebra<VAR>this : IsScalarTower R R' S'<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝³ : Algebra R S := f.toAlgebra<VAR>this✝² : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝¹ : Algebra R' S' := f'.toAlgebra<VAR>this✝ : IsScalarTower R R' S'<VAR>this : IsScalarTower R S S'<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝⁴ : Algebra R S := f.toAlgebra<VAR>this✝³ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝² : Algebra R' S' := f'.toAlgebra<VAR>this✝¹ : IsScalarTower R R' S'<VAR>this✝ : IsScalarTower R S S'<VAR>this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing S✝<VAR>M✝ : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R'✝ S'✝ : Type u<VAR>inst✝¹¹ : CommRing R'✝<VAR>inst✝¹⁰ : CommRing S'✝<VAR>f✝ : R✝ →+* S✝<VAR>inst✝⁹ : Algebra R✝ R'✝<VAR>inst✝⁸ : Algebra S✝ S'✝<VAR>R S : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>f : R →+* S<VAR>M : Submonoid R<VAR>R' S' : Type u_1<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>inst✝¹ : IsLocalization M R'<VAR>inst✝ : IsLocalization (Submonoid.map f M) S'<VAR>hf : f.Finite<VAR>this✝⁵ : Algebra R S := f.toAlgebra<VAR>this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra<VAR>f' : R' →+* S' := IsLocalization.map S' f ⋯<VAR>this✝³ : Algebra R' S' := f'.toAlgebra<VAR>this✝² : IsScalarTower R R' S'<VAR>this✝¹ : IsScalarTower R S S'<VAR>this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'<VAR>this : Module.Finite R S<GOAL>(IsLocalization.map S' f ⋯).Finite
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemigroup α<VAR>a b : α<GOAL>IsSquare (a * a * (b * b))
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>α : Type u_2<VAR>M : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>π : Prepartition I<VAR>f : Box ι → α<VAR>g : Box ι → M<GOAL>∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J = ∑ J ∈ π.boxes, g J
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>i : ℕ<VAR>x : ExteriorAlgebra R M<VAR>hx : x ∈ ⋀[R]^i M<GOAL>(liftι R M) ↑⟨x, hx⟩ = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>i : ℕ<VAR>x : ExteriorAlgebra R M<VAR>hx : x ∈ ⋀[R]^i M<GOAL>(liftι R M) x = (DirectSum.of (fun i => ↥(⋀[R]^i M)) i) ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - (c + d) ≤ a - c + (b - d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - d - c ≤ a - c + (b - d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + (b - d) - c ≤ a - c + (b - d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>b - d + a - c ≤ b - d + (a - c)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(memberSubfamily a 𝒜).card + (nonMemberSubfamily a 𝒜).card = 𝒜.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<GOAL>(filter (fun s => a ∈ s) 𝒜).card + (filter (fun s => a ∉ s) 𝒜).card = 𝒜.card
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝ a : α<VAR>𝒜 : Finset (Finset α)<GOAL>Set.InjOn (fun s => s.erase a) ↑(filter (fun s => a ∈ s) 𝒜)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l✝ l' : List α<VAR>a : α<VAR>l : List α<GOAL>l.toFinset.Nonempty ↔ l ≠ []
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>f f₁ f₂ : (i : ι) → Filter (α i)<VAR>s✝ : (i : ι) → Set (α i)<VAR>p : (i : ι) → α i → Prop<VAR>inst✝ : Finite ι<VAR>s : (i : ι) → Set (α i)<GOAL>(pi fun i => 𝓟 (s i)) = 𝓟 (univ.pi s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>h : pred a < b<GOAL>Ico (pred a) b = insert (pred a) (Ico a b)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s✝ t✝ u✝ : Set E<VAR>x y : E<VAR>s t u : Set E<GOAL>convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>ι : Type u_3<VAR>I : Set ι<VAR>hI : I.Finite<VAR>s : ι → Set α<GOAL>Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α × β → E<VAR>hf : Integrable f (μ.prod ν)<GOAL>∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f : α × β → E<VAR>hf : Integrable f (μ.prod ν)<GOAL>∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Lattice α<VAR>a b c d : α<GOAL>a ⊓ b < a ⊔ b ↔ a ≠ b
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<VAR>hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<VAR>hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)<VAR>H : (fun z => log (1 + z) - logTaylor (n + 1) z) z = z * ∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹<GOAL>‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<VAR>hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)<VAR>H : (fun z => log (1 + z) - logTaylor (n + 1) z) z = z * ∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹<GOAL>‖z‖ * ‖∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<VAR>hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)<VAR>H : (fun z => log (1 + z) - logTaylor (n + 1) z) z = z * ∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹<GOAL>‖z‖ ^ (n + 1) * ‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * ((1 - ‖z‖)⁻¹ / (↑n + 1))
<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<VAR>help : IntervalIntegrable (fun t => t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1<VAR>f : ℂ → ℂ := fun z => log (1 + z) - logTaylor (n + 1) z<VAR>f' : ℂ → ℂ := fun z => (-z) ^ n * (1 + z)⁻¹<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)<VAR>hcont : ContinuousOn (fun t => f' (0 + ↑t * z)) (Set.Icc 0 1)<VAR>H : (fun z => log (1 + z) - logTaylor (n + 1) z) z = z * ∫ (t : ℝ) in 0 ..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹<GOAL>‖∫ (x : ℝ) in 0 ..1, ↑x ^ n * (1 + ↑x * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹ / (↑n + 1)
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Type u_6<VAR>inst✝ : Monoid H<VAR>ψ : G →* H<VAR>x : G<GOAL>orderOf (ψ x) ∣ orderOf x
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Type u_6<VAR>inst✝ : Monoid H<VAR>ψ : G →* H<VAR>x : G<GOAL>ψ x ^ orderOf x = 1
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x✝ y : G<VAR>n m : ℕ<VAR>H : Type u_6<VAR>inst✝ : Monoid H<VAR>ψ : G →* H<VAR>x : G<GOAL>ψ 1 = 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝ q : R[X]<VAR>x✝ : A<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<VAR>x : S<GOAL>(aeval x) p = ∑ i ∈ range (p.natDegree + 1), p.coeff i • x ^ i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : CommSemiring A'<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R A'<VAR>inst✝² : Algebra R B<VAR>p✝ q : R[X]<VAR>x✝ : A<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Algebra R S<VAR>p : R[X]<VAR>x : S<GOAL>(aeval x) p = ∑ x_1 ∈ range (p.natDegree + 1), (algebraMap R S) (p.coeff x_1) * x ^ x_1
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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✝³ : Nontrivial R<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<GOAL>finrank R M = 0 ↔ ∀ (x : M), ∃ a, a ≠ 0 ∧ a • x = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<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✝³ : Nontrivial R<VAR>inst✝² : NoZeroSMulDivisors R M<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<GOAL>finrank R M = 0 ↔ ↑(finrank R M) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>hx : AlgebraicIndependent R x<VAR>i : ι<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin (X (some i)) = Polynomial.C (hx.aevalEquiv (X i))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsGreatest s b<GOAL>IsGreatest (insert a s) (max a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b✝ : α<VAR>inst✝ : LinearOrder γ<VAR>a b : γ<VAR>s : Set γ<VAR>hs : IsGreatest s b<GOAL>IsGreatest ({a} ∪ s) (max a b)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>(W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℤ<GOAL>((mapRingHom f) (W.preΨ n) ^ 2 * if Even n then (mapRingHom f) W.Ψ₂Sq else 1) = (mapRingHom f) (W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p1 p2 : P<GOAL>dist p1 (midpoint ℝ p1 p2) = dist p2 (midpoint ℝ p1 p2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s<GOAL>map Subtype.val atTop = 𝓝[<] b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s<VAR>hb' : Iio b = ∅<GOAL>map Subtype.val atTop = 𝓝[<] b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>hb : s ⊆ Iio b<VAR>hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s<VAR>a : α<VAR>ha : a ∈ Iio b<GOAL>map Subtype.val atTop = 𝓝[<] b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>(∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t) ∧ { ofColex := s } ≠ { ofColex := t } ↔ ∃ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (init m)) (m (last n))
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDerivWithin 𝕜 (n + 1) f univ x) m = ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ₁ ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (φ₁ ≫ b) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (a ≫ φ₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>(HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₁) ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr φ₂)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.68425, u_1} C<VAR>inst✝⁶ : Category.{?u.68429, u_2} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasBinaryBiproducts C<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasZeroObject D<VAR>inst✝ : HasBinaryBiproducts D<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ<VAR>φ₁ : K₁ ⟶ L₁<VAR>φ₂ : K₂ ⟶ L₂<VAR>a : K₁ ⟶ K₂<VAR>b : L₁ ⟶ L₂<VAR>H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)<GOAL>((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₁).mor₃ ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₁) ≫ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ₂).mor₃ ≫ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso 1).hom.app K₂