ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>ε n ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 < (2 * ε n) ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 ≤ ε n
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>s : Set (ι → ℝ)<VAR>x y : ι → ℝ<VAR>δ : ℝ<VAR>f : (δ : ℝ) → 0 < δ → ι → ℝ<VAR>hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ<VAR>hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s<VAR>H : Tendsto (fun r => volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)<VAR>ε : ℕ → ℝ<VAR>hε' : ∀ (n : ℕ), 0 < ε n<VAR>hε₀ : Tendsto ε atTop (𝓝[>] 0)<VAR>n : ℕ<VAR>this : 0 < ε n<GOAL>0 ≤ ε n / 4
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : TopologicalSpace F<VAR>κ : ι → Type u_10<VAR>inst✝² : Nonempty ((i : ι) × κ i)<VAR>inst✝¹ : ∀ (i : ι), Nonempty (κ i)<VAR>p : (i : ι) → SeminormFamily 𝕜 E (κ i)<VAR>t : ι → TopologicalSpace E<VAR>inst✝ : ∀ (i : ι), TopologicalAddGroup E<VAR>hp : ∀ (i : ι), WithSeminorms (p i)<GOAL>WithSeminorms (SeminormFamily.sigma p)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : TopologicalSpace F<VAR>κ : ι → Type u_10<VAR>inst✝² : Nonempty ((i : ι) × κ i)<VAR>inst✝¹ : ∀ (i : ι), Nonempty (κ i)<VAR>p : (i : ι) → SeminormFamily 𝕜 E (κ i)<VAR>t : ι → TopologicalSpace E<VAR>inst✝ : ∀ (i : ι), TopologicalAddGroup E<VAR>hp : ∀ (i : ι), WithSeminorms (p i)<VAR>this : TopologicalAddGroup E<GOAL>WithSeminorms (SeminormFamily.sigma p)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : TopologicalSpace F<VAR>κ : ι → Type u_10<VAR>inst✝² : Nonempty ((i : ι) × κ i)<VAR>inst✝¹ : ∀ (i : ι), Nonempty (κ i)<VAR>p : (i : ι) → SeminormFamily 𝕜 E (κ i)<VAR>t : ι → TopologicalSpace E<VAR>inst✝ : ∀ (i : ι), TopologicalAddGroup E<VAR>this : TopologicalAddGroup E<VAR>hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace<GOAL>⨅ i, t i = ⨅ i, UniformSpace.toTopologicalSpace
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup E<VAR>inst✝⁸ : Module 𝕜 E<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : TopologicalSpace F<VAR>κ : ι → Type u_10<VAR>inst✝² : Nonempty ((i : ι) × κ i)<VAR>inst✝¹ : ∀ (i : ι), Nonempty (κ i)<VAR>p : (i : ι) → SeminormFamily 𝕜 E (κ i)<VAR>t : ι → TopologicalSpace E<VAR>inst✝ : ∀ (i : ι), TopologicalAddGroup E<VAR>this : TopologicalAddGroup E<VAR>hp : ∀ (i : ι), t i = ⨅ i_1, UniformSpace.toTopologicalSpace<GOAL>⨅ i, t i = ⨅ i, ⨅ j, UniformSpace.toTopologicalSpace
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<GOAL>Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}
<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✝⁴ : NormedRing R<VAR>inst✝³ : NormedAlgebra 𝕜 R<VAR>𝕜' : Type u_4<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff 𝕜 n fun x => (f 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✝⁴ : NormedRing R<VAR>inst✝³ : NormedAlgebra 𝕜 R<VAR>𝕜' : Type u_4<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝕜'<VAR>inst✝ : CompleteSpace 𝕜'<VAR>f : E → 𝕜'<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>∀ (x : E), ContDiffAt 𝕜 n (fun x => (f x)⁻¹) x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g : G<VAR>a : α<GOAL>orbit G a = orbit G (g⁻¹ • g • a)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! x, b - (Equiv.neg ℤ) x • a ∈ Ioc c (c + a)
<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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<GOAL>count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<GOAL>count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<GOAL>count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<GOAL>count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hw' : Irreducible (Associates.mk w.asIdeal)<GOAL>count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hw' : Irreducible (Associates.mk w.asIdeal)<GOAL>¬⟨Associates.mk v.asIdeal, hv⟩ = ⟨Associates.mk w.asIdeal, hw'⟩
<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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hw' : Irreducible (Associates.mk w.asIdeal)<GOAL>¬Associates.mk v.asIdeal = Associates.mk w.asIdeal
<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 w : HeightOneSpectrum R<VAR>hw : w ≠ v<VAR>hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal<VAR>hw_ne_zero : ↑w.asIdeal ≠ 0<VAR>hv : Irreducible (Associates.mk v.asIdeal)<VAR>hw' : Irreducible (Associates.mk w.asIdeal)<GOAL>¬v = w
<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 → R<VAR>hP : W'.Equation P<GOAL>W'.addY P P = 0
<VAR>X : TopCat<VAR>U : Opens ↑X<VAR>V : Opens ↥U<GOAL>⋯.functor.obj ((map U.inclusion).obj (⋯.functor.obj V)) = ⋯.functor.obj V
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : CanonicallyOrderedAddCommMonoid α<VAR>inst✝ : LocallyFiniteOrder α<VAR>f : ι →₀ α<GOAL>(Iic f).card = ∏ i ∈ f.support, (Iic (f i)).card
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(f ^ n).natSepDegree = f.natSepDegree
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>m : M<VAR>hm : m ∈ ↑N<GOAL>((toEnd R L M) x ∘ₗ (↑N).subtype) ⟨m, hm⟩ ∈ ↑N
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Precoherent C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<GOAL>IsSheaf (coherentTopology C) F ↔ IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Precoherent C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)<GOAL>IsSheaf (coherentTopology C) F
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Precoherent C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)<GOAL>IsSheaf (coherentTopology C) (e.functor.op ⋙ e.inverse.op ⋙ F)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>inst✝¹ : Precoherent C<VAR>A : Type u_3<VAR>inst✝ : Category.{u_5, u_3} A<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : IsSheaf (coherentTopology D) (e.inverse.op ⋙ F)<GOAL>F ≅ e.functor.op ⋙ e.inverse.op ⋙ F
<VAR>α : Type u<VAR>β : Type v<VAR>f✝ f : α → β<VAR>hf : Bijective f<VAR>s : Set β<VAR>t : Set α<GOAL>f ⁻¹' s = t ↔ s = f '' t
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : ¬Nat.Prime k<VAR>h : MinFacHelper n k<GOAL>MinFacHelper n k'
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : ¬Nat.Prime k<VAR>h : MinFacHelper n k<VAR>h2 : n.minFac = k<GOAL>False
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : ¬Nat.Prime n.minFac<VAR>h : MinFacHelper n k<VAR>h2 : n.minFac = k<GOAL>False
<VAR>n : ℕ<VAR>h : n ≠ 1<GOAL>Prime n ↔ ↑(n - 1)! = -1
<VAR>n : ℕ<VAR>h : n ≠ 1<VAR>h1 : Prime n<GOAL>↑(n - 1)! = -1
<VAR>n : ℕ<VAR>h : n ≠ 1<VAR>h1 : Prime n<VAR>this : Fact (Prime n)<GOAL>↑(n - 1)! = -1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : IsNoetherian K V<GOAL>Set.range ⇑(finsetBasis K V) = Basis.ofVectorSpaceIndex K V
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>j : F<VAR>inst✝ : DecidableEq F<VAR>h3 : 3 = 0<GOAL>ofJ 0 = ofJ1728 F
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hn : 1 < n<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1<VAR>hn : 1 < n<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1<VAR>hn : 1 < n<VAR>hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1<VAR>hn : 1 < n<VAR>hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1<VAR>heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1<VAR>hn : 1 < n<VAR>hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1<VAR>heq : (X ^ n - 1).coeff 0 = -(cyclotomic n R).coeff 0<VAR>hzero : (X ^ n - 1).coeff 0 = -1<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hi : ∀ m < n, 1 < m → (cyclotomic m R).coeff 0 = 1<VAR>hn : 1 < n<VAR>hprod : ∏ i ∈ n.properDivisors, (cyclotomic i R).coeff 0 = -1<VAR>heq : -1 = -(cyclotomic n R).coeff 0<VAR>hzero : (X ^ n - 1).coeff 0 = -1<GOAL>(cyclotomic n R).coeff 0 = 1
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<GOAL>s.toList.length = card s
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>g : G<VAR>hB : IsBlock G B<GOAL>IsBlock G (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>g : G<VAR>hB : IsBlock (↥⊤) B<GOAL>IsBlock (↥⊤) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>g : G<VAR>hB : IsBlock (↥⊤) B<GOAL>IsBlock (↥(Subgroup.map (↑(MulAut.conj g)) (Subgroup.comap ↑(MulAut.conj g) ⊤))) (g • B)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>g : G<VAR>hB : IsBlock (↥⊤) B<GOAL>IsBlock (↥(Subgroup.comap ↑(MulAut.conj g) ⊤)) B
<VAR>A B : AddGrp<VAR>f : A ⟶ B<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>A B : AddGrp<VAR>f : A ⟶ B<VAR>i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>1 - x ∣ 1 - x ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>1 - x ∣ 1 ^ n - x ^ n
<VAR>x y : ℝ<GOAL>1 * 1 = x ↔ x = 1
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>t : Finset L[[α]].Sentence<GOAL>List.foldr (fun x x_1 => x ⊓ x_1) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>t : Finset L[[α]].Sentence<GOAL>(∀ (M : ModelType ↑p), ∀ φ ∈ t, φ.Realize default default) ↔ ∀ x ∈ ↑t, ∀ (M : ModelType ↑p), BoundedFormula.Realize x default default
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>f g : ℕ → α<VAR>h : partialSups f = partialSups g<GOAL>⨆ n, f n = ⨆ n, g n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<GOAL>↑s = ∅ ↔ s = ⊥
<VAR>x y : ℂ<GOAL>cos (2 * x) = 2 * cos x ^ 2 - 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>r' : ENNReal<VAR>hzr' : edist c z < r'<VAR>hr' : r' < r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>r' : NNReal<VAR>hzr' : edist c z < ↑r'<VAR>hr' : ↑r' < r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>r' : NNReal<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hr' : ↑r' < r<GOAL>HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>r' : NNReal<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hr' : ↑r' < r<GOAL>DifferentiableOn ℂ f (Metric.ball c ↑r')
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>r : ENNReal<VAR>hf : DifferentiableOn ℂ f (EMetric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ EMetric.ball c r<VAR>r' : NNReal<VAR>hzr' : z ∈ Metric.ball c ↑r'<VAR>hr' : ↑r' < r<GOAL>DifferentiableOn ℂ f (EMetric.ball c ↑r')
<VAR>q : ℤ[X]<VAR>k m n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>u v w : ℤˣ<GOAL>(trinomial k m n ↑u ↑v ↑w).support.card = 3
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R<VAR>f : ℂ → ℂ<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z<GOAL>(∮ (z : ℂ) in C(c, R), f z / (z - w)) = 2 * ↑π * I * f w
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h : ∅ ∉ 𝒜<GOAL>Set.Sized r ↑(∂ 𝒜) ↔ Set.Sized (r + 1) ↑𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>h : ∅ ∉ 𝒜<VAR>h𝒜 : Set.Sized r ↑(∂ 𝒜)<VAR>s : Finset α<VAR>hs : s ∈ ↑𝒜<GOAL>s.card = r + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>k r : ℕ<VAR>h : ∅ ∉ 𝒜<VAR>h𝒜 : Set.Sized r ↑(∂ 𝒜)<VAR>s : Finset α<VAR>hs : s ∈ ↑𝒜<VAR>a : α<VAR>ha : a ∈ s<GOAL>s.card = r + 1
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>inst✝ : IsEmpty α<VAR>M : Matroid α<GOAL>M = emptyOn α
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>E B I X R J : Set α<VAR>inst✝ : IsEmpty α<VAR>M : Matroid α<GOAL>M.E = ∅
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>G : D ⥤ C<VAR>F : C ⥤ D<VAR>adj : F ⊣ G<VAR>A : adj.toMonad.Algebra<VAR>inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))<GOAL>G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) = G.map (adj.counit.app (F.obj A.A)) ≫ G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
<VAR>l r : List Char<GOAL>{ s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.remainingBytes = utf8Len r
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>↑⌊τ f⌋ ≤ τ f
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>t₁ t₂ : TopologicalSpace E<VAR>h₁ : LocallyConvexSpace 𝕜 E<VAR>h₂ : LocallyConvexSpace 𝕜 E<GOAL>LocallyConvexSpace 𝕜 E
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>t₁ t₂ : TopologicalSpace E<VAR>h₁ : LocallyConvexSpace 𝕜 E<VAR>h₂ : LocallyConvexSpace 𝕜 E<VAR>b : Bool<GOAL>LocallyConvexSpace 𝕜 E
<VAR>n : ℕ<GOAL>Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2
<VAR>n : ℕ<GOAL>Monoid.exponent (QuaternionGroup n) = lcm (2 * n) (2 * 2)
<VAR>n : ℕ<GOAL>Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
<VAR>n : ℕ<VAR>hn : n = 0<GOAL>Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
<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<GOAL>count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk (choose ⋯)).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<GOAL>s ∩ (t ∪ s) = s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<GOAL>IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>this : (WellFounded fun x x_1 => x > x_1) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k<GOAL>IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>this : (WellFounded fun x x_1 => x > x_1) ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k<GOAL>IsNoetherian R M ↔ ∀ (k : Submodule R M), CompleteLattice.IsCompactElement k
<VAR>α : Type u_1<VAR>f : Char → α → α<VAR>s : String<VAR>a : α<GOAL>foldr f a s = List.foldr f a s.data