ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : c * d ≠ 0<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>h1 : C c * C d * p = integerNormalization R⁰ a * integerNormalization R⁰ b<VAR>u : Rˣ<VAR>hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>u : Rˣ<VAR>h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p<VAR>hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>u : Rˣ<VAR>h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p<VAR>hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content<VAR>h0 : a ≠ 0 ∧ b ≠ 0<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>u : Rˣ<VAR>h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p<VAR>hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content<VAR>h0 : a ≠ 0 ∧ b ≠ 0<VAR>h : IsUnit (C ↑u * (integerNormalization R⁰ b).primPart)<GOAL>IsUnit a ∨ IsUnit b
<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✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<VAR>hp : p.IsPrimitive<VAR>hi : Irreducible p<VAR>a b : K[X]<VAR>hab : map (algebraMap R K) p = a * b<VAR>c : R<VAR>c0 : c ≠ 0<VAR>hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a<VAR>d : R<VAR>d0 : d ≠ 0<VAR>hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b<VAR>hcd0 : ¬C (c * d) = 0<VAR>u : Rˣ<VAR>h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p<VAR>hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content<VAR>h0 : a ≠ 0 ∧ b ≠ 0<VAR>h : IsUnit (integerNormalization R⁰ a).primPart<GOAL>IsUnit a ∨ IsUnit b
<VAR>l : Filter ℂ<VAR>hre : Tendsto re l atTop<VAR>r : ℝ<VAR>hr : im =O[l] fun z => z.re ^ r<VAR>n : ℕ<VAR>z : ℂ<VAR>hz : 0 ≤ z.re<GOAL>(fun z => (z.re ^ r) ^ n) z = (fun z => z.re ^ (r * ↑n)) z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<GOAL>Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α ∧ IsOpen U<GOAL>∃ i ∈ 𝓤 α, Prod.map mk mk ⁻¹' (Prod.map mk mk '' id i) ⊆ id U
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α ∧ IsOpen U<VAR>x✝¹ : α × α<VAR>x₁ x₂ : α<VAR>x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)<VAR>y₁ y₂ : α<VAR>hyU : (y₁, y₂) ∈ id U<VAR>hxy : Prod.map mk mk (y₁, y₂) = Prod.map mk mk (x₁, x₂)<GOAL>(x₁, x₂) ∈ id U
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α ∧ IsOpen U<VAR>x✝¹ : α × α<VAR>x₁ x₂ : α<VAR>x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)<VAR>y₁ y₂ : α<VAR>hyU : (y₁, y₂) ∈ id U<VAR>hxy : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂<GOAL>(x₁, x₂) ∈ id U
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.boundary ⟨c.length, ⋯⟩ = Fin.last n
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>Fin.last n = c.boundaries.max' ⋯
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A : Matrix ι ι R<VAR>j : ι<GOAL>((fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>A : Matrix ι ι R<VAR>j : ι<GOAL>∑ i : ι, (fun i => A i j * 1) i • b i = ∑ i : ι, A i j • b i
<VAR>x y : ℝ<GOAL>sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x
<VAR>x y : ℝ<GOAL>↑(sinh (3 * x)) = ↑(4 * sinh x ^ 3 + 3 * sinh x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<GOAL>∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<VAR>this : IsPathConnected univ<GOAL>∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>inst✝ : PathConnectedSpace X<VAR>n : ℕ<VAR>p : Fin (n + 1) → X<VAR>this : IsPathConnected univ<VAR>γ : Path (p 0) (p ↑n)<VAR>t : Fin (n + 1) → ↑I<VAR>h : ∀ (i : Fin (n + 1)), γ (t i) = p i<GOAL>∃ γ t, ∀ (i : Fin (n + 1)), γ (t i) = p i
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<GOAL>(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).symm = (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯).trans (LinearIsometryEquiv.neg ℝ)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<VAR>n : ℕ∞<GOAL>(∀ (i : ι), ContDiffOn 𝕜 n (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x => f x i) t
<VAR>A B : Grp<VAR>f : A ⟶ B<VAR>x : ↑B<GOAL>(((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(MonoidHom.range f), ⋯⟩) = fromCoset ⟨↑(MonoidHom.range f), ⋯⟩
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊆ ⋃ i, U i<GOAL>∃ t, s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥<GOAL>∃ t, s ⊆ ⋃ i ∈ t, U i
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅<VAR>ι✝ : Type u<VAR>U : ι✝ → Set X<VAR>hUo : ∀ (i : ι✝), IsOpen (U i)<VAR>hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥<VAR>t : Finset ι✝<VAR>ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅<GOAL>s ⊆ ⋃ i ∈ t, U i
<VAR>x✝ y x : ℝ<GOAL>arcsin ↑(projIcc (-1) 1 ⋯ x) = arcsin x
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s f : R<VAR>g : ↥(Submonoid.powers s)<GOAL>(toOpen R (PrimeSpectrum.basicOpen s)) f = (toOpen R (PrimeSpectrum.basicOpen s)) ↑g * const R f (↑g) (PrimeSpectrum.basicOpen s) ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>s f : R<VAR>g : ↥(Submonoid.powers s)<GOAL>const R f 1 (PrimeSpectrum.basicOpen s) ⋯ = const R (↑g) 1 (PrimeSpectrum.basicOpen s) ⋯ * const R f (↑g) (PrimeSpectrum.basicOpen s) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y✝ x y : α<VAR>h : x ≤ y<GOAL>leftLim f x ≤ leftLim f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y x : α<VAR>h : x ≤ x<GOAL>leftLim f x ≤ leftLim f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : ConditionallyCompleteLinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y✝ x y : α<VAR>h : x ≤ y<VAR>hxy : x < y<GOAL>leftLim f x ≤ leftLim f y
<VAR>R : Type u_1<VAR>inst✝ : Zero R<VAR>f : ArithmeticFunction R<VAR>n : ℕ<GOAL>(toArithmeticFunction ⇑f) n = f n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>Function.Surjective ⇑(Finsupp.total S (Ω[S⁄R]) S ⇑(D R S))
<VAR>n m✝ m : ℕ<VAR>a b : Fin n<GOAL>(fun x => x.addNat m) a = (fun x => x.addNat m) b → a = b
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>∃ S₁, S₁.multiplicity = S'.multiplicity
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>a b : 𝓞 K<VAR>H : a ^ 3 + b ^ 3 = ↑S'.u * S'.c ^ 3<VAR>coprime : IsCoprime a b<VAR>ha : ¬λ ∣ a<VAR>hb : ¬λ ∣ b<VAR>hab : λ ^ 2 ∣ a + b<GOAL>∃ S₁, S₁.multiplicity = S'.multiplicity
<VAR>V : Type u_1<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet<VAR>hn : ¬G.Adj s t<VAR>h : s ≠ t<VAR>this : DecidableEq V := Classical.decEq V<GOAL>(G ⊔ edge s t).edgeFinset = cons s(s, t) G.edgeFinset ⋯
<VAR>V : Type u_1<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet<VAR>hn : ¬G.Adj s t<VAR>h : s ≠ t<VAR>this : DecidableEq V := Classical.decEq V<GOAL>(edge s t).edgeFinset ∪ G.edgeFinset = {s(s, t)} ∪ G.edgeFinset
<VAR>V : Type u_1<VAR>inst✝³ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : Fintype ↑(G ⊔ edge s t).edgeSet<VAR>hn : ¬G.Adj s t<VAR>h : s ≠ t<VAR>this : DecidableEq V := Classical.decEq V<GOAL>{s(s, t)}.toFinset ∪ G.edgeSet.toFinset = {s(s, t)} ∪ G.edgeSet.toFinset
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁴ : (x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>inst✝³ : TopologicalSpace HB<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>chartAt (ModelProd HB F) x = (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝⁶ : TopologicalSpace F<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁴ : (x : B) → TopologicalSpace (E x)<VAR>HB : Type u_7<VAR>inst✝³ : TopologicalSpace HB<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>x : TotalSpace F E<GOAL>(trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB (↑(trivializationAt F E x.proj).toPartialHomeomorph x).1).prod (PartialHomeomorph.refl F) = (trivializationAt F E x.proj).toPartialHomeomorph ≫ₕ (chartAt HB x.proj).prod (PartialHomeomorph.refl F)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>g : B ⟶ op X<VAR>hg : Mono g<VAR>i : A ≅ B<VAR>hf : Mono (i.hom ≫ g)<GOAL>(fun A f x => Subobject.mk (kernel.ι f.unop)) A (i.hom ≫ g) hf = (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>g : B ⟶ op X<VAR>hg : Mono g<VAR>i : A ≅ B<VAR>hf : Mono (i.hom ≫ g)<GOAL>kernel (i.hom ≫ g).unop ≅ kernel g.unop
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>g : B ⟶ op X<VAR>hg : Mono g<VAR>i : A ≅ B<VAR>hf : Mono (i.hom ≫ g)<GOAL>?refine_1.hom ≫ kernel.ι g.unop = kernel.ι (i.hom ≫ g).unop
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f✝ : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f✝<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>f : A ⟶ op X<VAR>g : B ⟶ op X<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : Subobject.mk f ≤ Subobject.mk g<GOAL>Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤ Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f✝ : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f✝<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>f : A ⟶ op X<VAR>g : B ⟶ op X<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : Subobject.mk f ≤ Subobject.mk g<GOAL>Subobject.mk (kernel.ι f.unop) ≤ Subobject.mk (kernel.ι g.unop)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f✝ : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f✝<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>f : A ⟶ op X<VAR>g : B ⟶ op X<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : Subobject.mk f ≤ Subobject.mk g<GOAL>kernel.ι f.unop ≫ g.unop = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X✝ Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f✝ : X✝ ⟶ Y<VAR>inst✝¹ : HasKernel f✝<VAR>inst✝ : HasKernels C<VAR>X : C<VAR>A B : Cᵒᵖ<VAR>f : A ⟶ op X<VAR>g : B ⟶ op X<VAR>hf : Mono f<VAR>hg : Mono g<VAR>h : Subobject.mk f ≤ Subobject.mk g<GOAL>kernel.lift g.unop (kernel.ι f.unop) ?refine_1 ≫ kernel.ι g.unop = kernel.ι f.unop
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>i : ℕ<VAR>hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>i : ℕ<VAR>hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>i : ℕ<VAR>hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>𝓟 : Ideal R<VAR>f : R[X]<VAR>hf✝ : f.IsWeaklyEisensteinAt 𝓟<VAR>S : Type v<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>p : R<VAR>x : S<VAR>hx : (aeval x) f = 0<VAR>hmo : f.Monic<VAR>hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})<VAR>i : ℕ<VAR>hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i<VAR>k : ℕ<VAR>hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k<VAR>y : S<VAR>hy : y ∈ adjoin R {x}<VAR>H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree<GOAL>∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>α : Type u₂<VAR>F : J → α<VAR>h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂<VAR>j j' : J<GOAL>F j = F j'
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬r = 0<GOAL>∃ u, ↑u = (C r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬r = 0<GOAL>↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬C (normalize r) = 0<GOAL>↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬C (normalize r) = 0<GOAL>C (normalize r) * ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = C (normalize r) * (C r).primPart
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬C (normalize r) = 0<GOAL>C (normalize r) * ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = C r
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>r : R<VAR>h0 : ¬C (normalize r) = 0<GOAL>C r * C ↑(normUnit r) * C ↑(normUnit r)⁻¹ = C r
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ inst✝ : NumberField K<GOAL>finrank ℤ (Additive ((𝓞 K)ˣ ⧸ torsion K)) = rank K
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : OrderedAddCommGroup α<VAR>s t : NonemptyInterval α<VAR>a : α<GOAL>(s - t).length = s.length + t.length
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = -1 ↔ angle x y = π
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>cos (angle x y) = cos π ↔ angle x y = π