ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>R : Type u_2<VAR>inst✝³ : SMul R ℝ≥0<VAR>inst✝² : SMul R ℝ≥0∞<VAR>inst✝¹ : IsScalarTower R ℝ≥0 ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>μ : FiniteMeasure Ω<VAR>A s : Set Ω<VAR>s_mble : MeasurableSet s<GOAL>↑(μ.restrict A) s = ↑μ (s ∩ A)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>x : α<VAR>l₁ l₂ : List α<GOAL>x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : DecidableEq L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : IsFractionRing R K<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Fintype (ClassGroup R)<GOAL>Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : DecidableEq L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : IsFractionRing R K<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Fintype (ClassGroup R)<GOAL>(∃ x, ∀ (y : ClassGroup R), y = x) → IsPrincipalIdealRing R
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : DecidableEq L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : IsFractionRing R K<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Fintype (ClassGroup R)<VAR>I : ClassGroup R<VAR>hI : ∀ (y : ClassGroup R), y = I<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : Field K<VAR>inst✝¹⁰ : Field L<VAR>inst✝⁹ : DecidableEq L<VAR>inst✝⁸ : Algebra R K<VAR>inst✝⁷ : IsFractionRing R K<VAR>inst✝⁶ : Algebra K L<VAR>inst✝⁵ : FiniteDimensional K L<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsDedekindDomain R<VAR>inst✝ : Fintype (ClassGroup R)<VAR>I : ClassGroup R<VAR>hI : ∀ (y : ClassGroup R), y = I<VAR>eq_one : ∀ (J : ClassGroup R), J = 1<GOAL>IsPrincipalIdealRing R
<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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • proj i) 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>ι : Type u_6<VAR>𝔸 : Type u_7<VAR>𝔸' : Type u_8<VAR>inst✝⁵ : NormedRing 𝔸<VAR>inst✝⁴ : NormedCommRing 𝔸'<VAR>inst✝³ : NormedAlgebra 𝕜 𝔸<VAR>inst✝² : NormedAlgebra 𝕜 𝔸'<VAR>u : Finset ι<VAR>f : ι → E → 𝔸<VAR>f' : ι → E →L[𝕜] 𝔸<VAR>g : ι → E → 𝔸'<VAR>g' : ι → E →L[𝕜] 𝔸'<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>x : ι → 𝔸'<GOAL>HasStrictFDerivAt (fun x => (Multiset.map x u.val).prod) (Multiset.map (fun x_1 => (Multiset.map x (u.erase x_1).val).prod • proj x_1) u.val).sum x
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<GOAL>IsNilpotent ((LieAlgebra.ad R A) a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<GOAL>IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<VAR>hl : IsNilpotent (LinearMap.mulLeft R a)<GOAL>IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<VAR>hl : IsNilpotent (LinearMap.mulLeft R a)<VAR>hr : IsNilpotent (LinearMap.mulRight R a)<GOAL>IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>h : IsNilpotent a<VAR>hl : IsNilpotent (LinearMap.mulLeft R a)<VAR>hr : IsNilpotent (LinearMap.mulRight R a)<VAR>this : Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R a)<GOAL>IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝¹ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>inst✝ : (center G).FiniteIndex<VAR>g : G<VAR>k : ℕ<VAR>x✝ : G<VAR>hk : x✝⁻¹ * g ^ k * x✝ ∈ center G<GOAL>x✝⁻¹ * g ^ k * x✝ = g ^ k
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁸ : Ring k<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : AddCommGroup V₂<VAR>inst✝⁵ : Module k V₁<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AddTorsor V₁ P₁<VAR>inst✝² : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Injective ⇑φ<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>inst✝¹ : Nonempty ↥E<VAR>inst✝ : Nonempty ↥F<VAR>hEF : AffineSubspace.map φ E ≤ F<VAR>x y : ↥E<VAR>h : (φ.restrict hEF) x = (φ.restrict hEF) y<GOAL>x = y
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>inst✝⁸ : Ring k<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : AddCommGroup V₂<VAR>inst✝⁵ : Module k V₁<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AddTorsor V₁ P₁<VAR>inst✝² : AddTorsor V₂ P₂<VAR>φ : P₁ →ᵃ[k] P₂<VAR>hφ : Function.Injective ⇑φ<VAR>E : AffineSubspace k P₁<VAR>F : AffineSubspace k P₂<VAR>inst✝¹ : Nonempty ↥E<VAR>inst✝ : Nonempty ↥F<VAR>hEF : AffineSubspace.map φ E ≤ F<VAR>x y : ↥E<VAR>h : φ ↑x = φ ↑y<GOAL>↑x = ↑y
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>f : E → F<VAR>x : E<VAR>c : R<VAR>hf : ContDiffAt 𝕜 n f x<GOAL>ContDiffAt 𝕜 n (fun y => c • f y) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>f : E → F<VAR>x : E<VAR>c : R<VAR>hf : ContDiffWithinAt 𝕜 n f univ x<GOAL>ContDiffWithinAt 𝕜 n (fun y => c • f y) univ x
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X✝<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f✝ : X✝ → (i : ι) → π i<VAR>X : Type u_8<VAR>f : X → (i : ι) → π i<GOAL>induced f Pi.topologicalSpace = ⨅ i, induced (fun x => f x i) inferInstance
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>inst✝³ : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝² : (i : η) → Group (Gs i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<GOAL>Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>inst✝³ : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝² : (i : η) → Group (Gs i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<GOAL>∀ (c : ℕ), Group.nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)) ≤ c
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>H : Subgroup G<VAR>inst✝³ : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝² : (i : η) → Group (Gs i)<VAR>inst✝¹ : Fintype η<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>k : ℕ<GOAL>Group.nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)) ≤ k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>re ⟪0, x⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>e : E<VAR>f : E → F<VAR>g : E → G<VAR>s : Set E<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>q : FormalMultilinearSeries 𝕜 E G<VAR>w✝¹ : ℝ≥0∞<VAR>hf : HasFPowerSeriesWithinOnBall f p s e w✝¹<VAR>w✝ : ℝ≥0∞<VAR>hg : HasFPowerSeriesWithinOnBall g q s e w✝<GOAL>HasFPowerSeriesWithinAt (fun x => (f x, g x)) (p.prod q) s e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>q : ℚ<VAR>h✝ : q < 0<GOAL>0 ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>q : ℚ<VAR>h✝ : ¬q < 0<GOAL>0 ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>h₂ : PrimrecRel fun a b => f a = b<VAR>g : α → ℕ<VAR>pg : Primrec g<VAR>hg : ∀ (x : α), f x ≤ g x<GOAL>Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → ℕ<VAR>h₂ : PrimrecRel fun a b => f a = b<VAR>g : α → ℕ<VAR>pg : Primrec g<VAR>hg : ∀ (x : α), f x ≤ g x<VAR>n : α<GOAL>Nat.findGreatest (fun b => f n = b) (g n) = f n
<VAR>ι : Type u_1<VAR>I✝ J✝ : Box ι<VAR>x y : ι → ℝ<VAR>I J : WithBot (Box ι)<GOAL>↑I = ↑J ↔ I = J
<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 : Ideal R<VAR>hI : I ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : v.maxPowDividing I ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : v.maxPowDividing I ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I<VAR>h_not_dvd : ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors ∣ ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors<VAR>h_not_dvd : ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : Associates.mk (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ∣ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)<VAR>h_not_dvd : ¬Associates.mk (v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1)) ∣ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : Associates.mk (v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≤ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)<VAR>h_not_dvd : ¬Associates.mk (v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1)) ≤ Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : (Associates.mk v.asIdeal).count (Associates.mk I).factors ≤ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors<VAR>h_not_dvd : ¬(Associates.mk v.asIdeal).count (Associates.mk I).factors + 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).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 : Ideal R<VAR>hI : I ≠ 0<VAR>h_ne_zero : Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>h_dvd : (Associates.mk v.asIdeal).count (Associates.mk I).factors ≤ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors<VAR>h_not_dvd : (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors < (Associates.mk v.asIdeal).count (Associates.mk I).factors + 1<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).factors
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<GOAL>cons a f ∘ rev = snoc (f ∘ rev) a
<VAR>m n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>β : Type v<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>f : Fin n → α<VAR>i : Fin (n + 1)<GOAL>(cons a f ∘ rev) i = snoc (f ∘ rev) a i
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι✝ : Sort u_1<VAR>ι : Sort u_2<VAR>u : ι → UniformSpace α<VAR>a : α<GOAL>𝓝 a = 𝓝 a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>IsCompact ((convexHull ℝ) s)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>IsCompact (⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x) '' stdSimplex ℝ ↑s)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : s.Finite<GOAL>Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs : s.Finite<VAR>this : Fintype ↑s<GOAL>Continuous ⇑(∑ x : ↑s, (LinearMap.proj x).smulRight ↑x)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>map valEmbedding (Iio b) = Iio ↑b
<VAR>m s step : Nat<GOAL>m ∈ range' s 0 step ↔ ∃ i, i < 0 ∧ m = s + step * i
<VAR>m s step n : Nat<GOAL>m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i
<VAR>m s step n : Nat<VAR>h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n<GOAL>m ∈ range' s (n + 1) step ↔ ∃ i, i < n + 1 ∧ m = s + step * i
<VAR>m s step n : Nat<VAR>h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n<GOAL>(m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a, (∃ j, a = j + 1 ∧ j < n) ∧ m = s + step * a
<VAR>m s step n : Nat<VAR>h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n<GOAL>(m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ a x, a = x + 1 ∧ x < n ∧ m = s + step * a
<VAR>m s step n : Nat<VAR>h : ∀ (i : Nat), i ≤ n ↔ i = 0 ∨ ∃ j, i = j.succ ∧ j < n<GOAL>(m = s ∨ ∃ i, i < n ∧ m = s + step + step * i) ↔ m = s ∨ ∃ b a, a = b + 1 ∧ b < n ∧ m = s + step * a
<VAR>α : Type u<VAR>m n : ℕ<GOAL>take m (range n) = range (min m n)
<VAR>α : Type u<VAR>m n : ℕ<GOAL>(take m (range n)).length = (range (min m n)).length
<VAR>α : Type u<VAR>m n : ℕ<GOAL>∀ (n_1 : ℕ) (h₁ : n_1 < (take m (range n)).length) (h₂ : n_1 < (range (min m n)).length), (take m (range n))[n_1] = (range (min m n))[n_1]
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : Semiring R₃<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>e : M ≃ₛₗ[σ₁₂] M₂<VAR>h✝ : M₂ →ₛₗ[σ₂₃] M₃<VAR>p q : Submodule R M<VAR>inst✝¹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝ : RingHomInvPair σ₂₁ σ₁₂<VAR>h : Bijective ⇑f<VAR>x : M<GOAL>(ofBijective f h).symm (f x) = x
<VAR>x y : ℝ<GOAL>cosh x ^ 2 = sinh x ^ 2 + 1
<VAR>x y : ℝ<GOAL>↑(cosh x ^ 2) = ↑(sinh x ^ 2 + 1)
<GOAL>|log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
<VAR>t : |2⁻¹| = 2⁻¹<GOAL>|log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
<VAR>t : |2⁻¹| = 2⁻¹<VAR>z : |∑ i ∈ range 34, 2⁻¹ ^ (i + 1) / (↑i + 1) + log (1 - 2⁻¹)| ≤ |2⁻¹| ^ (34 + 1) / (1 - |2⁻¹|)<GOAL>|log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)