ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : X → M'<VAR>e : PartialHomeomorph X H<VAR>x : X<VAR>s : Set X<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : X → M'<VAR>e : PartialHomeomorph X H<VAR>x : X<VAR>s : Set X<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g (↑e.symm (↑e x)) ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g (↑e.symm (↑e x)) ∈ f'.source<VAR>hgs : ContinuousWithinAt g s (↑e.symm (↑e x))<GOAL>P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e✝ e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g✝ g' : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : X → M'<VAR>e : PartialHomeomorph X H<VAR>x : X<VAR>s : Set X<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g (↑e.symm (↑e x)) ∈ f.source<VAR>hf' : f' ∈ maximalAtlas M' G'<VAR>xf' : g (↑e.symm (↑e x)) ∈ f'.source<VAR>hgs : ContinuousWithinAt g s (↑e.symm (↑e x))<GOAL>ContinuousWithinAt (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>R : Type u_1<VAR>k : ℕ<GOAL>(σ k).IsMultiplicative
<VAR>R : Type u_1<VAR>k : ℕ<GOAL>(ζ * pow k).IsMultiplicative
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_int : Integrable X μ<GOAL>centralMoment X 1 μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_int : Integrable X μ<GOAL>∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>h_int : Integrable X μ<GOAL>∫ (a : Ω), X a ∂μ - ∫ (a : Ω), ∫ (x : Ω), X x ∂μ ∂μ = (1 - (μ Set.univ).toReal) * ∫ (x : Ω), X x ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun x => f x - c) f' x L
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n k : ℕ<GOAL>choose (↑n) k = ↑(n.choose k)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n k : ℕ<GOAL>(fun x => k.factorial • x) (choose (↑n) k) = (fun x => k.factorial • x) ↑(n.choose k)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>n k : ℕ<GOAL>k.factorial • choose (↑n) k = k.factorial • ↑(n.choose k)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>Associates.mk J ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>Associates.mk (Ideal.span {choose ⋯}) ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>Associates.mk (choose ⋯) ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>a₁ : R := choose ⋯<VAR>J₁ : Ideal R := choose ⋯<VAR>h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})<VAR>h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁<VAR>h_a₁_ne_zero : a₁ ≠ 0<VAR>h_J₁_ne_zero : J₁ ≠ 0<VAR>h_a_ne_zero : Ideal.span {a} ≠ 0<VAR>h_J_ne_zero : J ≠ 0<VAR>h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0<VAR>h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>Associates.mk (Ideal.span {a}) ≠ 0
<VAR>m n : ℕ<VAR>i : Fin n.succ<GOAL>↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v s t : Finset α<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>↑((P.nonUniforms G ε).biUnion fun x => match x with | (U, V) => U ×ˢ V).card < 4 * ε * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<GOAL>∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = ∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<GOAL>(fun a => (μ {a_1 | a < f a_1}).toReal) =ᶠ[ae (volume.restrict (Ioi 0))] fun a => (μ {a_1 | a ≤ f a_1}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>t : ℝ<VAR>ht : μ {a | t ≤ f a} = μ {a | t < f a}<GOAL>(μ {a | t < f a}).toReal = (μ {a | t ≤ f a}).toReal
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>inst✝⁵ : HasBinaryCoproduct A B<VAR>inst✝⁴ : HasBinaryCoproduct A' B'<VAR>inst✝³ : HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>inst✝² : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>f : A ⟶ A'<VAR>g : B ⟶ B'<VAR>inst✝¹ : IsIso (coprodComparison F A B)<VAR>inst✝ : IsIso (coprodComparison F A' B')<GOAL>inv (coprodComparison F A B) ≫ coprod.map (F.map f) (F.map g) = F.map (coprod.map f g) ≫ inv (coprodComparison F A' B')
<VAR>X₁ : Type u₁<VAR>inst✝⁵ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝² : TopologicalSpace Y✝<VAR>inst✝¹ : TietzeExtension Y✝<VAR>Y : Type v<VAR>inst✝ : TopologicalSpace Y<VAR>f : C(↑s, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>ht : TietzeExtension ↑t<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ restrict s g = f
<VAR>X₁ : Type u₁<VAR>inst✝⁵ : TopologicalSpace X₁<VAR>X : Type u<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>e : X₁ → X<VAR>he : ClosedEmbedding e<VAR>Y✝ : Type v<VAR>inst✝² : TopologicalSpace Y✝<VAR>inst✝¹ : TietzeExtension Y✝<VAR>Y : Type v<VAR>inst✝ : TopologicalSpace Y<VAR>f : C(↑s, Y)<VAR>t : Set Y<VAR>hf : ∀ (x : ↑s), f x ∈ t<VAR>ht : TietzeExtension ↑t<VAR>g : C(X, ↑t)<VAR>hg : restrict s g = { toFun := Set.codRestrict (⇑f) t hf, continuous_toFun := ⋯ }<GOAL>∃ g, (∀ (x : X), g x ∈ t) ∧ restrict s g = f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>i : ℕ<GOAL>(take i []).prod * (drop i []).prod = [].prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a h : M<VAR>t : List M<VAR>n : ℕ<GOAL>(h :: take n t).prod * (drop n t).prod = (h :: t).prod
<VAR>cf cg : Code<GOAL>encode cf < encode (cf.pair cg) ∧ encode cg < encode (cf.pair cg)
<VAR>cf cg : Code<GOAL>cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧ cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
<VAR>cf cg : Code<VAR>this : 1 * Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * 2 * Nat.pair cf.encodeCode cg.encodeCode<GOAL>cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧ cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
<VAR>cf cg : Code<VAR>this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)<GOAL>cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧ cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
<VAR>cf cg : Code<VAR>this✝ : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)<VAR>this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4<GOAL>cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧ cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<VAR>x✝¹ x✝ : M<GOAL>(sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c : Con M<VAR>S : Set (Con M)<VAR>x✝¹ x✝ : M<GOAL>(sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s
<VAR>α : Type u_1<VAR>f : Perm α<VAR>s : Set α<GOAL>BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Add R<VAR>inst✝⁴ : Mul R<VAR>inst✝³ : Neg R<VAR>inst✝² : One R<VAR>inst✝¹ : Zero R<VAR>inst✝ : CompatibleRing R<VAR>v : α → R<GOAL>Term.realize v 0 = 0
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f)
<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>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>Integrable (f ⊓ g) μ
<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>β : Type u_5<VAR>inst✝ : NormedLatticeAddCommGroup β<VAR>f g : α → β<VAR>hf : Memℒp f 1 μ<VAR>hg : Memℒp g 1 μ<GOAL>Memℒp (f ⊓ g) 1 μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : {i : Fin2 n} → α i → α i → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)<GOAL>LiftR (fun {i} => r) x y
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : {i : Fin2 n} → α i → α i → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)<GOAL>(fun i t => (↑t).1) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = x ∧ (fun i t => (↑t).2) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : {i : Fin2 n} → α i → α i → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)<GOAL>(fun i t => (↑t).2) <$$> abs ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩ = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} n → Type u_1<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : {i : Fin2 n} → α i → α i → Prop<VAR>x y : F α<VAR>a : (P F).A<VAR>f₀ f₁ : (P F).B a ⟹ α<VAR>xeq : x = abs ⟨a, f₀⟩<VAR>yeq : y = abs ⟨a, f₁⟩<VAR>h : ∀ (i : Fin2 n) (j : (P F).B a i), r (f₀ i j) (f₁ i j)<GOAL>abs ((fun i t => (↑t).2) <$$> ⟨a, fun i j => ⟨(f₀ i j, f₁ i j), ⋯⟩⟩) = abs ⟨a, f₁⟩
<VAR>b : ℕ<GOAL>b ^ log b 0 ≤ 0 + 1
<VAR>α : Type u<VAR>n : ℕ<GOAL>(range n).Nodup
<VAR>G : Type u_1<VAR>inst✝ : AddCommGroup G<VAR>B : AddGroupFilterBasis G<VAR>F : Filter G<VAR>this : UniformSpace G := B.uniformSpace<GOAL>Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U