ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type u_1<VAR>a b n i : ℕ<VAR>x✝ : i ∈ range n<GOAL>a / b ^ (i + 1) * b ≤ a / b ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>a b n i : ℕ<VAR>x✝ : i ∈ range n<GOAL>a / (b ^ i * b) * b ≤ a / b ^ i
<VAR>α : Type u<VAR>β : Type u_1<VAR>a b n i : ℕ<VAR>x✝ : i ∈ range n<GOAL>a / b ^ i / b * b ≤ a / b ^ i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<GOAL>gauge s 0 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : normSq ↑z < 1<GOAL>z.im < (S • z).im
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : normSq ↑z < 1<VAR>this : z.im < z.im / normSq ↑z<GOAL>z.im < (S • z).im
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : normSq ↑z < 1<VAR>this : z.im < z.im / normSq ↑z<GOAL>(S • z).im = z.im / normSq ↑z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>h : normSq ↑z < 1<VAR>this : z.im < z.im / normSq ↑z<GOAL>z.im / normSq (denom (↑S) z) = z.im / normSq ↑z
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>inst✝ : Nonempty ι<VAR>inhabited_h : Inhabited ι<GOAL>Function.Injective (row ι)
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>HasEigenvector (↑T) (↑(⨅ x, T.rayleighQuotient ↑x)) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<GOAL>⨅ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>hx₀' : 0 < ‖x₀‖<VAR>hx₀'' : x₀ ∈ sphere 0 ‖x₀‖<GOAL>⨅ x, T.rayleighQuotient ↑x = T.rayleighQuotient x₀
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>T : E →L[𝕜] E<VAR>hT : IsSelfAdjoint T<VAR>x₀ : E<VAR>hx₀ : x₀ ≠ 0<VAR>hextr : IsMinOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>hx₀' : 0 < ‖x₀‖<VAR>hx₀'' : x₀ ∈ sphere 0 ‖x₀‖<GOAL>IsMinOn T.rayleighQuotient (sphere 0 ‖x₀‖) x₀
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : NFA α σ<VAR>M : DFA α σ<VAR>x : List α<GOAL>x ∈ M.toNFA.accepts ↔ x ∈ M.accepts
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M✝ : NFA α σ<VAR>M : DFA α σ<VAR>x : List α<GOAL>(∃ S ∈ M.toNFA.accept, S ∈ {M.evalFrom M.start x}) ↔ x ∈ M.accepts
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<GOAL>Submodule.span R (Set.range ⇑(ιMulti R n)) = ⋀[R]^n M
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<GOAL>⋀[R]^n M ≤ Submodule.span R (Set.range ⇑(ιMulti R n))
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<GOAL>↑(LinearMap.range (ι R)) ^ n ⊆ ↑(Submodule.span R (Set.range ⇑(ιMulti R n)))
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>u : ExteriorAlgebra R M<VAR>hu : u ∈ ↑(LinearMap.range (ι R)) ^ n<GOAL>u ∈ Set.range ⇑(ιMulti R n)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>f : Fin n → ↑↑(LinearMap.range (ι R))<VAR>hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n<GOAL>(List.ofFn fun i => ↑(f i)).prod ∈ Set.range ⇑(ιMulti R n)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>f : Fin n → ↑↑(LinearMap.range (ι R))<VAR>hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n<GOAL>((ιMulti R n) fun i => ιInv ↑(f i)) = (List.ofFn fun i => ↑(f i)).prod
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>f : Fin n → ↑↑(LinearMap.range (ι R))<VAR>hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n<GOAL>(List.ofFn fun i => (ι R) (ιInv ↑(f i))).prod = (List.ofFn fun i => ↑(f i)).prod
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>f : Fin n → ↑↑(LinearMap.range (ι R))<VAR>hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n<VAR>i : Fin n<GOAL>(ι R) (ιInv ↑(f i)) = ↑(f i)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>n : ℕ<VAR>f : Fin n → ↑↑(LinearMap.range (ι R))<VAR>hu : (List.ofFn fun i => ↑(f i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n<VAR>i : Fin n<VAR>v : M<VAR>hv : (ι R) v = ↑(f i)<GOAL>(ι R) (ιInv ↑(f i)) = ↑(f i)
<VAR>α : Type u_1<VAR>inst✝ : DivInvMonoid α<VAR>x y : α<GOAL>op (x / y) = (op y)⁻¹ * op x
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>x : ℕ<GOAL>bit a x % 2 = 0 ↔ (!a) = true
<VAR>f : Bool → Bool → Bool<VAR>a : Bool<VAR>x : ℕ<GOAL>(if a = true then 1 else 0) = 0 ↔ (!a) = true
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>h : b < a<GOAL>⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype (Sym2 V)<GOAL>Fintype.card G.Dart = 2 * G.edgeFinset.card
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>2 • o.oangle x (r • y) = 2 • o.oangle x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (_ : f a ≠ 1), f a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>a b d : α<VAR>x : WithBot α<GOAL>unbot' d x = d ↔ x = ↑d ∨ x = ⊥
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioo a b)<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioo a b)<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto f (𝓝[>] a) (𝓝 0)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hdf : DifferentiableOn ℝ f (Ioo a b)<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l<GOAL>Tendsto g (𝓝[>] a) (𝓝 0)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)<GOAL>M.LinearDisjoint N
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>κ : Type u_1<VAR>ι : Type u_2<VAR>m : Basis κ R ↥M<VAR>n : Basis ι R ↥N<VAR>H : Function.Injective ⇑(Finsupp.total (κ × ι) S R fun i => ↑(m i.1) * ↑(n i.2))<GOAL>M.LinearDisjoint N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : μ.WeaklyRegular<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>F : Set α<VAR>hFA : F ⊆ A<VAR>hFc : IsClosed F<VAR>hF : μ A < μ F + ε<GOAL>∃ F ⊆ A, IsClosed F ∧ μ (A \ F) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖adjointAux A‖ = ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖adjointAux A‖ ≤ ‖A‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<GOAL>‖A‖ ≤ ‖adjointAux A‖
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y z : R<GOAL>span {x, y + x * z} = span {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>h : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤<GOAL>Tendsto (fun p => p.1 - p.2) (𝓝 (⊤, ⊤)) (𝓝 (⊤ - ⊤))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>b : ℝ≥0<VAR>x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤<GOAL>Tendsto (fun p => p.1 - p.2) (𝓝 (⊤, ↑b)) (𝓝 (⊤ - ↑b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>b : ℝ≥0<VAR>x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤<GOAL>∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, ↑b), ↑x < a.1 - a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>b : ℝ≥0<VAR>x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤<VAR>x : ℝ≥0<VAR>y : ℝ≥0∞ × ℝ≥0∞<VAR>hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)<GOAL>↑x < y.1 - y.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝¹ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>b : ℝ≥0<VAR>x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤<VAR>x : ℝ≥0<VAR>y : ℝ≥0∞ × ℝ≥0∞<VAR>hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)<GOAL>y.2 + ↑x < y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0<VAR>x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤<GOAL>Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a - ⊤))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0<VAR>x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤<GOAL>Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ⊤)) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a : ℝ≥0<VAR>x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤<GOAL>∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ⊤), x.1 - x.2 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>a b : ℝ≥0<VAR>x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤<GOAL>Tendsto (fun a => a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>1 < card α ↔ Nontrivial α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>1 < card α ↔ 1 < #α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>1 < card α ↔ ↑1 < #α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>1 < card α ↔ ↑1 < toPartENat #α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - c ≤ a + (b - c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b ≤ a + (c + (b - c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<GOAL>(s ∪ t).card = s.card + t.card ↔ _root_.Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<GOAL>(s ∪ t).card = (s ∪ t).card + (s ∩ t).card ↔ _root_.Disjoint s t
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : Countable ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}<VAR>i : ι<GOAL>MeasurableSet (⋃ k, ⋃ (_ : k ≤ i), {ω | τ ω = k})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : Countable ι<VAR>f : Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}<VAR>i k : ι<VAR>hk : k ∈ fun k => Preorder.toLE.1 k i<GOAL>MeasurableSet {ω | τ ω = k}
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p : K[X]<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<GOAL>Irreducible p ↔ p.roots = 0
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p : K[X]<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<GOAL>Irreducible p ↔ p.roots = 0
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p : K[X]<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<GOAL>p.leadingCoeff⁻¹ ≠ 0
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p : K[X]<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<GOAL>2 ≤ (p * C p.leadingCoeff⁻¹).natDegree
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>p : K[X]<VAR>hp2 : 2 ≤ p.natDegree<VAR>hp3 : p.natDegree ≤ 3<VAR>hp0 : p ≠ 0<GOAL>(p * C p.leadingCoeff⁻¹).natDegree ≤ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<GOAL>ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>A : Type u_2<VAR>inst✝³ : AddGroup A<VAR>H✝ : Type u_3<VAR>inst✝² : Group H✝<VAR>inst✝¹ : IsSimpleGroup G<VAR>inst✝ : Nontrivial H✝<VAR>f : G →* H✝<VAR>hf : Function.Surjective ⇑f<VAR>H : Subgroup H✝<VAR>iH : H.Normal<GOAL>H = ⊥ ∨ H = ⊤
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>A : Type u_2<VAR>inst✝³ : AddGroup A<VAR>H✝ : Type u_3<VAR>inst✝² : Group H✝<VAR>inst✝¹ : IsSimpleGroup G<VAR>inst✝ : Nontrivial H✝<VAR>f : G →* H✝<VAR>hf : Function.Surjective ⇑f<VAR>H : Subgroup H✝<VAR>iH : H.Normal<VAR>h : comap f H = ⊥<GOAL>H = ⊥
<VAR>G : Type u_1<VAR>inst✝⁴ : Group G<VAR>A : Type u_2<VAR>inst✝³ : AddGroup A<VAR>H✝ : Type u_3<VAR>inst✝² : Group H✝<VAR>inst✝¹ : IsSimpleGroup G<VAR>inst✝ : Nontrivial H✝<VAR>f : G →* H✝<VAR>hf : Function.Surjective ⇑f<VAR>H : Subgroup H✝<VAR>iH : H.Normal<VAR>h : comap f H = ⊤<GOAL>H = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>x b : β<VAR>inst✝² : Fintype α<VAR>inst✝¹ : Fintype ↑(orbit α b)<VAR>inst✝ : Fintype ↥(stabilizer α b)<GOAL>Fintype.card ↑(orbit α b) * Fintype.card ↥(stabilizer α b) = Fintype.card α
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>x : M<VAR>hxf : x ∈ f.source<GOAL>x ∈ (f.extend I).source
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<VAR>this : Finite ↑s<GOAL>⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<VAR>this : Finite ↑s<GOAL>⋂ x, f ↑x ≤ᶠ[l] ⋂ x, g ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>b : α<VAR>inst✝ : NoMinOrder α<GOAL>pred b ⋖ b
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Finset P<GOAL>IsFractional S (span R ↑I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Finset P<VAR>s : R<VAR>hs1 : s ∈ S<VAR>hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)<GOAL>IsFractional S (span R ↑I)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Finset P<VAR>s : R<VAR>hs1 : s ∈ S<VAR>hs : ∀ a ∈ I, IsInteger R (↑⟨s, hs1⟩ • a)<GOAL>∃ a ∈ S, ∀ b ∈ ↑I, IsInteger R (a • b)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>⊤ ≤ normalClosure {⟨finRotate 5, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle<GOAL>⊤ ≤ normalClosure {⟨finRotate 5, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle<GOAL>normalClosure {⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ≤ normalClosure {⟨finRotate 5, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle<GOAL>{⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩} ⊆ ↑(normalClosure {⟨finRotate 5, ⋯⟩})
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle<GOAL>⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>h3 : (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹).IsThreeCycle<VAR>h : ⟨finRotate 5, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}<GOAL>⟨Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹, ⋯⟩ ∈ normalClosure {⟨finRotate 5, ⋯⟩}
<VAR>x y : ℝ*<VAR>hip : x.InfinitePos<VAR>hnin : ¬y.InfiniteNeg<VAR>r : ℝ<GOAL>↑r < x + y
<VAR>x y : ℝ*<VAR>hip : x.InfinitePos<VAR>hnin : ¬y.InfiniteNeg<VAR>r r₂ : ℝ<VAR>hr₂ : ¬y < ↑r₂<GOAL>↑r < x + y
<VAR>x y : ℝ*<VAR>hip : x.InfinitePos<VAR>hnin : ¬y.InfiniteNeg<VAR>r r₂ : ℝ<VAR>hr₂ : ¬y < ↑r₂<GOAL>↑r = ↑(r + -r₂) + ↑r₂
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>f.valuation = g.valuation ↔ f.norm = g.norm
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>0 < ↑p
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : PadicSeq p<VAR>hf : ¬f ≈ 0<VAR>hg : ¬g ≈ 0<GOAL>↑p ≠ 1
<VAR>M : Type u_1<VAR>inst✝ : Mul M<VAR>c d : Con M<GOAL>{ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c ≤ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d ↔ c ≤ d
<VAR>M : Type u_1<VAR>inst✝ : Mul M<VAR>c d : Con M<GOAL>(∀ {x y : Mᵐᵒᵖ}, ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y → ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔ ∀ {x y : M}, c x y → d x y
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f.degree < ↑s.card<VAR>eval_f : ∀ x ∈ s, eval x f = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>eval_f : ∀ x ∈ s, eval x f = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>eval_f : ∀ x ∈ s, ∑ i : Fin s.card, (degreeLTEquiv R s.card) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>f g : R[X]<VAR>s : Finset R<VAR>degree_f_lt : f ∈ degreeLT R s.card<VAR>eval_f : ∀ x ∈ s, ∑ i : Fin s.card, (degreeLTEquiv R s.card) ⟨f, degree_f_lt⟩ i * x ^ ↑i = 0<GOAL>(degreeLTEquiv R s.card) ⟨f, degree_f_lt⟩ = 0