ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : LinearOrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>f : E → 𝕜<VAR>hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y<VAR>hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x<VAR>B : 𝕜<GOAL>Convex 𝕜 {x | f x ≤ B}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : LinearOrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>f : E → 𝕜<VAR>hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y<VAR>hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x<VAR>B : 𝕜<GOAL>∀ ⦃x : E⦄, x ∈ {x | f x ≤ B} → ∀ ⦃y : E⦄, y ∈ {x | f x ≤ B} → [x-[𝕜]y] ⊆ {x | f x ≤ B}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝² : LinearOrderedRing 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : SMul 𝕜 E<VAR>f : E → 𝕜<VAR>hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y<VAR>hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x<VAR>B : 𝕜<VAR>x : E<VAR>hx : x ∈ {x | f x ≤ B}<VAR>y : E<VAR>hy : y ∈ {x | f x ≤ B}<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hs : a + b = 1<GOAL>a • x + b • y ∈ {x | f x ≤ B}
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>i : ι<VAR>x : G i<GOAL>hV.linearIsometry (lp.single 2 i x) = (V i) x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>i : ι<VAR>x : G i<GOAL>∑' (i_1 : ι), (V i_1) (↑(lp.single 2 i x) i_1) = ∑' (b' : ι), if b' = i then (V i) x else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>i : ι<VAR>x : G i<VAR>j : ι<GOAL>(V j) (↑(lp.single 2 i x) j) = if j = i then (V i) x else 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>i : ι<VAR>x : G i<VAR>j : ι<GOAL>(V j) (if h : j = i then ⋯ ▸ x else 0) = if j = i then (V i) x else 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : doset a ↑H ↑K = doset b ↑H ↑K<GOAL>mk H K a = mk H K b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H K : Subgroup G<VAR>a b : G<VAR>h : doset a ↑H ↑K = doset b ↑H ↑K<GOAL>∃ h ∈ H, ∃ k ∈ K, b = h * a * k
<VAR>α : Type u<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a b c : α<GOAL>a⁻¹ ≤ a ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>inst✝ : CircularOrder α<VAR>a b x✝ : α<GOAL>x✝ ∈ (cIcc a b)ᶜ ↔ x✝ ∈ cIoo b a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<GOAL>LipschitzWith 2 fun p => p.1 - p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<GOAL>LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>this : Isometry (Prod.map toReal toReal)<GOAL>LipschitzWith 2 (Subtype.val ∘ fun p => p.1 - p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>this : Isometry (Prod.map toReal toReal)<GOAL>2 = 1 * 1 + 1 * 1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, F⟮↑i.snd⟯
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>i : ι<GOAL>f i ≤ ⨆ i, F⟮↑i.snd⟯
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>s ∈ ∂ 𝒜ᶜˢ ↔ s ∈ (∂⁺ 𝒜)ᶜˢ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>(∃ s_1, s_1ᶜ ∈ 𝒜 ∧ ∃ a ∈ s_1, s_1.erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>s : Finset α<GOAL>(∃ b, ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b)ᶜ ∈ 𝒜 ∧ ∃ a ∈ (Equiv.symm (Function.Involutive.toPerm compl ⋯)) b, ((Equiv.symm (Function.Involutive.toPerm compl ⋯)) b).erase a = s) ↔ ∃ s_1 ∈ 𝒜, ∃ a ∉ s_1, insert a s_1 = sᶜ
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>x : E<VAR>s : Set E<GOAL>IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<GOAL>Metric.diam s = sSup s - sInf s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>s : Set ℝ<VAR>h : Bornology.IsBounded s<GOAL>0 ≤ sSup s - sInf s
<VAR>m n a b c : ℕ<GOAL>↑a = ↑b ↔ a ≡ b [MOD c]
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>s : Set Y<GOAL>map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>n₁ : ℤ<VAR>x a₁ : α<VAR>n₂ : ℤ<VAR>a₂ : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : n₁ + n₂ = n'<VAR>h₂ : a₁ + a₂ = a'<GOAL>termg n₁ x a₁ + termg n₂ x a₂ = termg n' x a'
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>n₁ : ℤ<VAR>x a₁ : α<VAR>n₂ : ℤ<VAR>a₂ : α<VAR>n' : ℤ<VAR>a' : α<VAR>h₁ : n₁ + n₂ = n'<VAR>h₂ : a₁ + a₂ = a'<GOAL>n₁ • x + a₁ + (n₂ • x + a₂) = n₁ • x + n₂ • x + (a₁ + a₂)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x₁ y₁ x₂ y₂ : α<GOAL>dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
<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✝ : H.FiniteIndex<VAR>g : G<VAR>key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k<GOAL>ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>a : Ordinal.{max u v}<GOAL>a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>M : Type uM<VAR>N : Type uN<VAR>P : Type uP<VAR>Q : Type uQ<VAR>P' : Type uP'<VAR>Q' : Type uQ'<VAR>inst✝³¹ : CommSemiring R<VAR>inst✝³⁰ : Semiring A<VAR>inst✝²⁹ : Semiring B<VAR>inst✝²⁸ : Algebra R A<VAR>inst✝²⁷ : Algebra R B<VAR>inst✝²⁶ : AddCommMonoid M<VAR>inst✝²⁵ : Module R M<VAR>inst✝²⁴ : Module A M<VAR>inst✝²³ : Module B M<VAR>inst✝²² : IsScalarTower R A M<VAR>inst✝²¹ : IsScalarTower R B M<VAR>inst✝²⁰ : SMulCommClass A B M<VAR>inst✝¹⁹ : AddCommMonoid N<VAR>inst✝¹⁸ : Module R N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : Module R P<VAR>inst✝¹⁵ : Module A P<VAR>inst✝¹⁴ : Module B P<VAR>inst✝¹³ : IsScalarTower R A P<VAR>inst✝¹² : IsScalarTower R B P<VAR>inst✝¹¹ : SMulCommClass A B P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : Module R Q<VAR>inst✝⁸ : AddCommMonoid P'<VAR>inst✝⁷ : Module R P'<VAR>inst✝⁶ : Module A P'<VAR>inst✝⁵ : Module B P'<VAR>inst✝⁴ : IsScalarTower R A P'<VAR>inst✝³ : IsScalarTower R B P'<VAR>inst✝² : SMulCommClass A B P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>f : M →ₗ[A] P<VAR>g₁ g₂ : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>((curry (map f (g₁ + g₂))) x✝¹) x✝ = ((curry (map f g₁ + map f g₂)) x✝¹) x✝
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>a : (forget TopCat).obj ↑(X.restrictFunctor.obj U).left.toPresheafedSpace<GOAL>(X.restrictFunctor.map i).left.val.base a = ((Opens.toTopCat ↑X.toPresheafedSpace).map i) a
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>a : (forget TopCat).obj ↑(X.restrictFunctor.obj U).left.toPresheafedSpace<GOAL>↑((X.restrictFunctor.map i).left.val.base a) = ↑(((Opens.toTopCat ↑X.toPresheafedSpace).map i) a)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : E<GOAL>‖(Lp.const p μ) c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : IsFiniteMeasure μ<VAR>c : E<GOAL>‖indicatorConstLp p ⋯ ⋯ c‖ ≤ ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<VAR>i : σ<GOAL>i ∈ (C a * φ).vars ↔ i ∈ φ.vars
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<VAR>i : σ<GOAL>(∃ d, coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<VAR>i : σ<GOAL>∀ (a_1 : σ →₀ ℕ), coeff a_1 (C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<VAR>i : σ<VAR>d : σ →₀ ℕ<GOAL>coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>A : Type u_3<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>a : A<VAR>ha : a ≠ 0<VAR>φ : MvPolynomial σ A<VAR>i : σ<VAR>d : σ →₀ ℕ<GOAL>coeff d (C a * φ) ≠ 0 ↔ coeff d φ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<GOAL>∫⁻ (x : α), 1 ∂μ = μ univ
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>Λ : Type u_2<VAR>σ : Type u_3<VAR>q : Stmt₁<GOAL>q ∈ stmts₁ q
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hp : p ≠ 0<GOAL>(erase p.natDegree p).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hp : p ≠ 0<GOAL>(erase p.natDegree p).degree ≠ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>hp : p ≠ 0<GOAL>(p.support.erase p.natDegree).max ≠ ↑p.natDegree
<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₁ s₂ s₃ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s₁ ∩ (s₂ ∩ s₃) ↔ x✝ ∈ s₂ ∩ (s₁ ∩ s₃)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<GOAL>iterate f (f a) = map f (iterate f a)
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → α<VAR>a : α<VAR>n : ℕ<GOAL>iterate f (f a) n = map f (iterate f a) n
<VAR>α : Type u_1<VAR>s : Set αᵒᵖ<VAR>a : αᵒᵖ<GOAL>unop a ∈ s.unop ↔ a ∈ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>n : ℕ<VAR>a : ℤ<GOAL>⌈↑n⌉ ≤ a ↔ ↑n ≤ a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc✝ gc : GaloisConnection l u<VAR>s : Set α<GOAL>l (sSup s) = ⨆ a ∈ s, l a
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iInf f).toNNReal = ⨅ i, (f i).toNNReal
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hf : ∀ (i : ι), f i ≠ ⊤<VAR>h✝ : IsEmpty ι<GOAL>(iInf f).toNNReal = ⨅ i, (f i).toNNReal
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hf : ∀ (i : ι), f i ≠ ⊤<VAR>h✝ : Nonempty ι<GOAL>(iInf f).toNNReal = ⨅ i, (f i).toNNReal
<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>inst✝³ : Semiring R<VAR>inst✝² : Semiring R₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e : M ≃ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<GOAL>↑(Submodule.map (↑e) p) = ↑(Submodule.comap (↑e.symm) p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n : ℕ<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ periodicPts f<GOAL>Cycle.Chain r (periodicOrbit f x) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n : ℕ<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ periodicPts f<GOAL>(∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)) ↔ ∀ (n : ℕ), r (f^[n] x) (f^[n + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n✝ : ℕ<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ periodicPts f<VAR>H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)<VAR>n : ℕ<GOAL>r (f^[n] x) (f^[n + 1] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ fa : α → α<VAR>fb : β → β<VAR>x✝ y : α<VAR>m n✝ : ℕ<VAR>r : α → α → Prop<VAR>f : α → α<VAR>x : α<VAR>hx : x ∈ periodicPts f<VAR>H : ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)<VAR>n : ℕ<GOAL>r (f^[n % minimalPeriod f x] x) (f^[(n % minimalPeriod f x).succ] x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 1<VAR>a✝ : Nontrivial R<GOAL>P.toPoly.Monic
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<GOAL>edist x y ≤ edist z x + edist z y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>a • s ⊆ t ↔ s ⊆ a⁻¹ • t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>↑(a • s) ⊆ ↑t ↔ ↑s ⊆ ↑(a⁻¹ • t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>b : β<GOAL>a • ↑s ⊆ ↑t ↔ ↑s ⊆ a⁻¹ • ↑t
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>n : ℕ<VAR>r : R<GOAL>((toZModPow n).comp (lift f_compat)) r = (f n) r
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>n : ℕ<VAR>r : R<GOAL>(lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>hs : s ∈ nonZeroDivisors R<VAR>i : ℕ<GOAL>i ∈ p.support → i ∈ (p.scaleRoots s).support
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>hs : s ∈ nonZeroDivisors R<VAR>i : ℕ<GOAL>p.coeff i ≠ 0 → p.coeff i * s ^ (p.natDegree - i) ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>hs : s ∈ nonZeroDivisors R<VAR>i : ℕ<VAR>p_ne_zero : p.coeff i ≠ 0<VAR>ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>p : R[X]<VAR>s : R<VAR>hs : s ∈ nonZeroDivisors R<VAR>i : ℕ<VAR>p_ne_zero : p.coeff i ≠ 0<VAR>ps_zero : p.coeff i * s ^ (p.natDegree - i) = 0<VAR>this : p.coeff i = 0<GOAL>False
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>A : Type u₃<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>f : L →ₗ⁅R⁆ A<VAR>x : L<GOAL>((lift R) f) ((mkAlgHom R L) (ιₜ x)) = f x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<GOAL>((algebraMap K (K_hat R K)) k).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<GOAL>{x | (algebraMap K (K_hat R K)) k x ∉ adicCompletionIntegers K x}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<GOAL>{x | 1 < Valued.v k}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<GOAL>{v | 1 < v.valuation k}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<GOAL>{v | 1 < v.valuation k}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>{v | 1 < v.valuation k}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>{v | v.valuation ((algebraMap R K) d) < 1}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>{v | v.intValuation d < 1}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>{v | v.intValuationDef d < 1}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>{v | v.asIdeal ∣ Ideal.span {d}}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>k : K<VAR>n d : R<VAR>hd : d ∈ nonZeroDivisors R<VAR>hk : k * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1<VAR>hd' : d ≠ 0<GOAL>Ideal.span {d} ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : PadicSeq p<VAR>ha : ¬a ≈ 0<GOAL>∃ z, a.norm = ↑p ^ (-z)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : PadicSeq p<VAR>ha : ¬a ≈ 0<VAR>k : ℚ<VAR>hk : a.norm = padicNorm p k<VAR>hk' : k ≠ 0<GOAL>∃ z, a.norm = ↑p ^ (-z)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<GOAL>P = span {x}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<GOAL>P = span {x}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<GOAL>P = span {x}
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>inst✝ : IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<VAR>this : DecidableEq (Ideal R) := Classical.decEq (Ideal R)<VAR>hx0 : x ≠ 0<VAR>hP0 : ¬P = ⊥<VAR>hspan0 : span {x} ≠ ⊥<GOAL>P = span {x}