ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ<VAR>heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A<VAR>A : Set α<VAR>hA : MeasurableSet A<GOAL>s A = (μ.singularPart ν) A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν s : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f<VAR>this : μ.HaveLebesgueDecomposition ν<VAR>hmeas : Measurable (μ.rnDeriv ν)<VAR>hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : s S = 0<VAR>hS₃ : ν Sᶜ = 0<VAR>T : Set α<VAR>hT₁ : MeasurableSet T<VAR>hT₂ : (μ.singularPart ν) T = 0<VAR>hT₃ : ν Tᶜ = 0<VAR>hνinter : ν (S ∩ T)ᶜ = 0<VAR>heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ<VAR>heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>hμinter : (μ.singularPart ν) (A ∩ (S ∩ T)) = 0<GOAL>s A = (μ.singularPart ν) A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⋖ b<GOAL>Ioc a b = {b}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<VAR>h : a ≤ b<GOAL>1 / b ≤ 1 / a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>K : Type u_4<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>hM : M ≤ nonZeroDivisors R<GOAL>(algebraMap R S) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>K : Type u_4<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>hM : M ≤ nonZeroDivisors R<GOAL>(algebraMap R S) x = (algebraMap R S) 0 ↔ x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hμs : μ s = ⊤<VAR>x : G<GOAL>condexpIndL1 hm μ s x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>s t : Set α<GOAL>s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionCommMonoid α<VAR>a b✝ c d : α<VAR>h : IsUnit a<VAR>b : α<GOAL>a / (a * b) = 1 / b
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hp0 : ¬p = 0<VAR>hx : IsIntegral A x<GOAL>minpoly A x ∣ p
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hp0 : ¬p = 0<VAR>hx : IsIntegral A x<GOAL>p %ₘ minpoly A x = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hp0 : ¬p = 0<VAR>hx : IsIntegral A x<VAR>hnz : ¬p %ₘ minpoly A x = 0<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝² : Field A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra A B<VAR>x : B<VAR>p : A[X]<VAR>hp : (Polynomial.aeval x) p = 0<VAR>hp0 : ¬p = 0<VAR>hx : IsIntegral A x<VAR>hnz : ¬p %ₘ minpoly A x = 0<GOAL>(p %ₘ minpoly A x).degree < (minpoly A x).degree
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>(↑(hC.diffFinset hs ht)).PairwiseDisjoint id
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>f : α → β<VAR>h : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y<VAR>x y : α<VAR>hxy : x ≤ y<GOAL>f x ⊓ f y = f x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>(eval P) W.polynomialX / P z ^ 4 = Polynomial.evalEval (P x / P z ^ 2) (P y / P z ^ 3) W.toAffine.polynomialX
<VAR>n : ℕ<GOAL>0 ∈ preCantorSet n
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqRe f).lim = f.lim.re
<VAR>f : CauSeq ℂ ⇑abs'<GOAL>(cauSeqRe f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).re
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : T2Space X<VAR>f : Filter X<VAR>inst✝ : CompactSpace X<VAR>U : Set X<GOAL>IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : T2Space X<VAR>f : Filter X<VAR>inst✝ : CompactSpace X<VAR>U : Set X<GOAL>(∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l) ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : T2Space X<VAR>f : Filter X<VAR>inst✝ : CompactSpace X<VAR>U : Set X<GOAL>(∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F) → ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : T2Space X<VAR>f✝ : Filter X<VAR>inst✝ : CompactSpace X<VAR>U : Set X<VAR>cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F<VAR>x : X<VAR>hx : x ∈ U<VAR>f : Ultrafilter X<VAR>h : ↑f ≤ 𝓝 x<GOAL>U ∈ f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : FirstCountableTopology X<VAR>inst✝¹ : T2Space X<VAR>f✝ : Filter X<VAR>inst✝ : CompactSpace X<VAR>U : Set X<VAR>cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F<VAR>x : X<VAR>f : Ultrafilter X<VAR>hx : f.lim ∈ U<VAR>h : ↑f ≤ 𝓝 x<GOAL>U ∈ f
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(C a * X ^ n).rootSet S = {0}
<VAR>α : Type u<VAR>a : α<VAR>s t : Set α<VAR>x : α<VAR>hs : {x}.Nontrivial<VAR>H : s = {x}<GOAL>False
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<GOAL>∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<GOAL>x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>hx : (Polynomial.map (algebraMap R S) f).IsRoot x<VAR>hmo : f.Monic<GOAL>x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
<VAR>R✝ : Type u_1<VAR>inst✝⁹ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<GOAL>Function.Bijective ⇑(ofTensorProduct I M)
<VAR>R✝ : Type u_1<VAR>inst✝⁹ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁸ : AddCommGroup M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Module.Finite R M<VAR>n : ℕ<VAR>f : (Fin n → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Bijective ⇑(ofTensorProduct I M)
<VAR>x y : ℝ<VAR>h : 0 ≤ x<GOAL>√x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>s : Finset (LieIdeal R L)<VAR>hs : ↑s ⊆ {I | IsAtom I}<VAR>I : LieIdeal R L<VAR>hI✝ : I ≤ s.sup id<VAR>S : Set (LieIdeal R L) := {I | IsAtom I}<VAR>hI : I < s.sup id<GOAL>∃ t ⊆ s, I = t.sup id
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>s : Finset (LieIdeal R L)<VAR>hs : ↑s ⊆ {I | IsAtom I}<VAR>I : LieIdeal R L<VAR>hI✝ : I ≤ s.sup id<VAR>S : Set (LieIdeal R L) := {I | IsAtom I}<VAR>hI : I < s.sup id<VAR>J : LieIdeal R L<VAR>hJs : J ∈ s<VAR>hJI : ¬J ≤ I<GOAL>∃ t ⊆ s, I = t.sup id
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsSemisimple R L<VAR>x : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id<VAR>a✝⁶ : ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id), (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card) instWellFoundedRelationOfSizeOf).1 y x → ∃ t ⊆ y.1, y.2.2.1 = t.sup id<VAR>s : Finset (LieIdeal R L)<VAR>a✝⁵ : (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id<VAR>a✝⁴ : ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id), (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card) instWellFoundedRelationOfSizeOf).1 y ⟨s, a✝⁵⟩ → ∃ t ⊆ y.1, y.2.2.1 = t.sup id<VAR>a✝³ : ↑s ⊆ {I | IsAtom I}<VAR>I✝ : (I : LieIdeal R L) ×' I ≤ s.sup id<VAR>a✝² : ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id), (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card) instWellFoundedRelationOfSizeOf).1 y ⟨s, ⟨a✝³, I✝⟩⟩ → ∃ t ⊆ y.1, y.2.2.1 = t.sup id<VAR>I : LieIdeal R L<VAR>a✝¹ : I ≤ s.sup id<VAR>a✝ : ∀ (y : (s : Finset (LieIdeal R L)) ×' (_ : ↑s ⊆ {I | IsAtom I}) ×' (I : LieIdeal R L) ×' I ≤ s.sup id), (invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card) instWellFoundedRelationOfSizeOf).1 y ⟨s, ⟨a✝³, ⟨I, a✝¹⟩⟩⟩ → ∃ t ⊆ y.1, y.2.2.1 = t.sup id<VAR>S : Set (LieIdeal R L) := {I | IsAtom I}<VAR>hI : I < s.sup id<VAR>J : LieIdeal R L<VAR>h✝ : J ∈ s ∧ ¬J ≤ I<VAR>hJs : J ∈ s<VAR>hJI : ¬J ≤ I<VAR>s' : Finset (LieIdeal R L) := s.erase J<VAR>hs' : s' ⊂ s<VAR>hs'S : ↑s' ⊆ S<VAR>K : LieIdeal R L := s'.sup id<VAR>this : I ≤ K<GOAL>(invImage (fun x => PSigma.casesOn x fun s a => PSigma.casesOn a fun a I => PSigma.casesOn I fun I a => s.card) instWellFoundedRelationOfSizeOf).1 ⟨s', ⟨hs'S, ⟨I, this⟩⟩⟩ ⟨s, ⟨a✝³, ⟨I, a✝¹⟩⟩⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>1 / a ≤ b ↔ 1 / b ≤ a
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<GOAL>-Y - C (C (map W f).toAffine.a₁ * X + C (map W f).toAffine.a₃) = Polynomial.map (mapRingHom f) (-Y - C (C W.a₁ * X + C W.a₃))
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpab : p ∣ S.a + S.b<VAR>hpaηb : p ∣ S.a + ↑η * S.b<GOAL>Associated p λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpab : p ∣ S.a + S.b<VAR>hpaηb : p ∣ S.a + ↑η * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpab : p ∣ 1 * S.a + 1 * S.b<VAR>hpaηb : p ∣ S.a + ↑η * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpab : p ∣ 1 * S.a + 1 * S.b<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<GOAL>p ∣ λ
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>p : 𝓞 K<VAR>hp : Prime p<VAR>hpab : p ∣ 1 * S.a + 1 * S.b<VAR>hpaηb : p ∣ 1 * S.a + ↑η * S.b<VAR>this : p ∣ (1 * ↑η - 1 * 1) * gcd S.a S.b<GOAL>p ∣ λ
<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>a : α<VAR>ha : (Ioi a).Nonempty<GOAL>frontier (Ioi a) = {a}
<GOAL>max (lsub fun i => (moveLeft 1 i).birthday) (lsub fun i => (moveRight 1 i).birthday) = 1
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : NoMinOrder α<VAR>a : α<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto (fun x => f ↑x) atBot l ↔ Tendsto f atBot l
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>n.gcd (n - m) = n.gcd m
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x ^ 2 * cos x ^ 2 = (b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>(b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4<VAR>h2 : Continuous fun x => cos (2 * x) ^ 2<GOAL>(b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4<VAR>h2 : Continuous fun x => cos (2 * x) ^ 2<VAR>h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2<GOAL>(b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4<VAR>h2 : Continuous fun x => cos (2 * x) ^ 2<VAR>h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2<VAR>h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d<GOAL>(b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ 1 * ((1 + cos (2 * x)) / 2) ^ 1
<VAR>a b : ℝ<VAR>n : ℕ<VAR>h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4<VAR>h2 : Continuous fun x => cos (2 * x) ^ 2<VAR>h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2<VAR>h4 : ∀ (d : ℝ), 2 * (2 * d) = 4 * d<GOAL>(b - a) / 8 - (sin (4 * b) - sin (4 * a)) / 32 = (b - a - 2⁻¹ * ((sin (4 * b) / 2 - sin (4 * a) / 2 + 2 * b - 2 * a) / 2)) / 4
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>HasFiniteIntegral (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>this : ∀ (x : α), ↑‖(f x).toReal‖₊ = ↑⟨(f x).toReal, ⋯⟩<GOAL>HasFiniteIntegral (fun x => (f x).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>this : ∀ (x : α), ↑‖(f x).toReal‖₊ = ↑⟨(f x).toReal, ⋯⟩<GOAL>∫⁻ (a : α), ↑⟨(f a).toReal, ⋯⟩ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0∞<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>this : ∀ (x : α), ↑‖(f x).toReal‖₊ = ↑⟨(f x).toReal, ⋯⟩<VAR>x : α<GOAL>↑⟨(f x).toReal, ⋯⟩ ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : Field K<VAR>a b : K<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a⁻¹ - b⁻¹ = (b - a) / (a * b)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategoryᵒᵖ<GOAL>(f.right.app (unop x)).unop ≫ (X✝.hom.app (unop x)).unop = (Y✝.hom.app (unop x)).unop ≫ f.left.unop
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategoryᵒᵖ<GOAL>(X✝.hom.app (unop x) ≫ f.right.app (unop x)).unop = (f.left ≫ Y✝.hom.app (unop x)).unop
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategoryᵒᵖ<GOAL>X✝.hom.app (unop x) ≫ f.right.app (unop x) = f.left ≫ Y✝.hom.app (unop x)
<VAR>m n : ℕ<GOAL>m < n.size ↔ 2 ^ m ≤ n
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<VAR>hne : ∀ z ∈ sphere c R, z ≠ w<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<VAR>hne : ∀ z ∈ sphere c R, z ≠ w<VAR>hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<VAR>hne : ∀ z ∈ sphere c R, z ≠ w<VAR>hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)<VAR>hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)<GOAL>(∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w