ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>s t : Set β<VAR>hs : Disjoint s t<VAR>ha : HasProd (s.mulIndicator f) a<VAR>hb : HasProd (t.mulIndicator f) b<GOAL>HasProd (fun a => s.mulIndicator f a * t.mulIndicator f a) (a * b)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝ : NonUnitalNonAssocCommSemiring α<VAR>a : α<GOAL>a ∈ NonUnitalSubsemiring.center α ↔ ∀ (b : α), Commute (L b) (L a)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝ : NonUnitalNonAssocCommSemiring α<VAR>a : α<GOAL>(L a = L a ∧ ∀ g ∈ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<GOAL>⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : Weight K (↥H) L<VAR>e f : L<VAR>heα : e ∈ rootSpace H ⇑α<VAR>hfα : f ∈ rootSpace H (-⇑α)<GOAL>∀ (h : ↥H), ⁅h, e⁆ = α h • e
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.75564, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<GOAL>s.r ≫ S.f = 𝟙 S.X₂ - S.g ≫ s.s
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A✝<VAR>inst✝⁷ : Ring B✝<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R A✝<VAR>inst✝⁴ : Algebra R B✝<VAR>f✝ : R →+* S<VAR>A : Type u_5<VAR>B : Type u_6<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>x : A<GOAL>IsIntegral R (f x) ↔ IsIntegral R x
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A✝<VAR>inst✝⁷ : Ring B✝<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R A✝<VAR>inst✝⁴ : Algebra R B✝<VAR>f✝ : R →+* S<VAR>A : Type u_5<VAR>B : Type u_6<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>x : A<VAR>x✝ : IsIntegral R (f x)<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hx : eval₂ (algebraMap R B) (f x) p = 0<GOAL>eval₂ (algebraMap R A) x p = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>f : E →L[𝕜] E<VAR>hf : ‖f‖ ≤ 1<VAR>x : E<GOAL>Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 ↑((orthogonalProjection (LinearMap.eqLocus f 1)) x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>f : E →L[𝕜] E<VAR>hf : ‖f‖ ≤ 1<VAR>x : E<GOAL>∀ (x : ↥(LinearMap.eqLocus (↑f) 1)), (orthogonalProjection (LinearMap.eqLocus f 1)) ↑x = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : CompleteSpace E<VAR>f : E →L[𝕜] E<VAR>hf : ‖f‖ ≤ 1<VAR>x : E<GOAL>↑(LinearMap.ker (orthogonalProjection (LinearMap.eqLocus f 1))) ⊆ closure ↑(LinearMap.range (↑f - 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>carrier : Set α<VAR>sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier<VAR>sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier<VAR>x : α<VAR>hx : x ∈ carrier<VAR>y : α<VAR>hy : y ∈ carrier<GOAL>x ⊔ y = sSup {x, y}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>carrier : Set α<VAR>sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier<VAR>sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier<VAR>x : α<VAR>hx : x ∈ carrier<VAR>y : α<VAR>hy : y ∈ carrier<GOAL>x ⊓ y = sInf {x, y}
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι✝ : Sort uι<VAR>s t u : Set α<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace β✝<VAR>inst✝⁴ : MeasurableSpace γ<VAR>inst✝³ : MeasurableSpace δ<VAR>π : δ' → Type u_6<VAR>π' : δ' → Type u_7<VAR>inst✝² : (x : δ') → MeasurableSpace (π x)<VAR>inst✝¹ : (x : δ') → MeasurableSpace (π' x)<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>e : ι ≃ ι'<VAR>β : ι' → Type u_10<VAR>inst✝ : (i' : ι') → MeasurableSpace (β i')<VAR>x : (i : ι) → β (e i)<VAR>i : ι<GOAL>(piCongrLeft (fun i' => β i') e) x (e i) = x i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w₁ w₂ : ι → k<VAR>p : ι → P<GOAL>(s.weightedVSub p) w₁ +ᵥ (affineCombination k s p) w₂ = (affineCombination k s p) (w₁ + w₂)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>f : ι → R⟦X⟧<VAR>d : ℕ<VAR>s : Finset ι<GOAL>(MvPowerSeries.coeff R (single () d)) (∏ j ∈ s, f j) = ∑ x ∈ s.finsuppAntidiag d, ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>f : ι → R⟦X⟧<VAR>d : ℕ<VAR>s : Finset ι<GOAL>∀ x ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) = ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>f : ι → R⟦X⟧<VAR>d : ℕ<VAR>s : Finset ι<VAR>x : ι →₀ ℕ<VAR>a✝ : x ∈ s.finsuppAntidiag d<GOAL>∏ i ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i)) (f i) = ∏ x_1 ∈ s, (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>f : ι → R⟦X⟧<VAR>d : ℕ<VAR>s : Finset ι<VAR>x : ι →₀ ℕ<VAR>a✝ : x ∈ s.finsuppAntidiag d<GOAL>∀ x_1 ∈ s, (MvPowerSeries.coeff R (((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) x_1)) (f x_1) = (MvPowerSeries.coeff R (single () (x x_1))) (f x_1)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>f : ι → R⟦X⟧<VAR>d : ℕ<VAR>s : Finset ι<VAR>x : ι →₀ ℕ<VAR>a✝¹ : x ∈ s.finsuppAntidiag d<VAR>i : ι<VAR>a✝ : i ∈ s<GOAL>((Finsupp.mapRange.addEquiv AddEquiv.finsuppUnique.symm).toEmbedding x) i = single () (x i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>i : ι<VAR>hi : i ∈ s<GOAL>eval (v i) (nodal s v) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>i : ι<VAR>hi : i ∈ s<GOAL>∏ i_1 ∈ s, (v i - v i_1) = 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>hG : IsSeparator G<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g<VAR>H : C<VAR>hH : H ∈ {G}<VAR>h : H ⟶ X<GOAL>h ≫ f = h ≫ g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>H : C<VAR>h : H ⟶ X<VAR>hG : IsSeparator H<VAR>hfg : ∀ (h : H ⟶ X), h ≫ f = h ≫ g<VAR>hH : H ∈ {H}<GOAL>h ≫ f = h ≫ g
<VAR>d✝ d : ℤ<VAR>hd : d ≤ 0<VAR>x : ℤ√d<VAR>u : (ℤ√d)ˣ<GOAL>x.norm = (x * ↑u).norm
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, f y = f c
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : StrictConvexSpace ℝ F<VAR>f : E → F<VAR>c : E<VAR>hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z<VAR>hc : IsLocalMax (norm ∘ f) c<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c<GOAL>∀ᶠ (y : E) in 𝓝 c, f y = f c
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>Prime X
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>(Ideal.span {X}).IsPrime
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>X ≠ 0
<VAR>A B C D B' D' : SemiNormedGrp<VAR>fab : A ⟶ B<VAR>fbd : B ⟶ D<VAR>fac : A ⟶ C<VAR>fcd : C ⟶ D<VAR>h : fab ≫ fbd = fac ≫ fcd<VAR>fbb' : B ⟶ B'<VAR>fdd' : D ⟶ D'<VAR>condb : fab ≫ fbb' = 0<VAR>condd : fcd ≫ fdd' = 0<VAR>g : B' ⟶ D'<VAR>h' : fbb' ≫ g = fbd ≫ fdd'<GOAL>explicitCokernelDesc condb ≫ g = explicitCokernelDesc ⋯ ≫ explicitCokernelDesc condd
<VAR>L : Language<VAR>L' : Language<GOAL>(L.sum L').card = lift.{max u' v', max u v} L.card + lift.{max u v, max u' v'} L'.card
<VAR>L : Language<VAR>L' : Language<GOAL>((sum fun i => lift.{max u' v v', u} #(L.Functions i)) + sum fun i => lift.{max u v v', u'} #(L'.Functions i)) + ((sum fun i => lift.{max v' u u', v} #(L.Relations i)) + sum fun i => lift.{max v u u', v'} #(L'.Relations i)) = ((sum fun i => lift.{max v u' v', u} #(L.Functions i)) + sum fun i => lift.{max u u' v', v} #(L.Relations i)) + ((sum fun i => lift.{max v' u v, u'} #(L'.Functions i)) + sum fun i => lift.{max u' u v, v'} #(L'.Relations i))
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M✝ N✝ P Q : Submodule R A<VAR>m n : A<VAR>M N : Submodule R Aᵐᵒᵖ<GOAL>comap (↑(opLinearEquiv R)) (M * N) = comap (↑(opLinearEquiv R)) N * comap (↑(opLinearEquiv R)) M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>Injective fun a => a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>Injective fun a => a * b⁻¹
<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>inst✝ : CompactSpace X<VAR>F : Ultrafilter X<GOAL>↑F ≤ 𝓝 F.lim
<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>inst✝ : CompactSpace X<VAR>F : Ultrafilter X<VAR>x : X<VAR>h : ↑F ≤ 𝓝 x<GOAL>↑F ≤ 𝓝 F.lim
<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>d m : ℕ<GOAL>((fun a => a + d) ∘ fun x => n • id x) m ≡ d [MOD n]
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : SuccOrder α<VAR>h : IsSuccLimit (succ a)<GOAL>IsMax a
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : SuccOrder α<VAR>h : IsSuccLimit (succ a)<VAR>H : ¬IsMax a<GOAL>False
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l<VAR>this : Tendsto ((fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x<VAR>hg' : ∀ x ∈ Iio a, g' x ≠ 0<VAR>hfbot : Tendsto f atBot (𝓝 0)<VAR>hgbot : Tendsto g atBot (𝓝 0)<VAR>hdiv : Tendsto (fun x => f' x / g' x) atBot l<VAR>hdnf : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x<VAR>hdng : ∀ x ∈ Ioi (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x<VAR>this✝ : Tendsto (fun x => (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) atTop l<VAR>this : Tendsto (fun x => (fun x => f (-x) / g (-x)) (-x)) atBot l<GOAL>Tendsto (fun x => f x / g x) atBot l
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).IsEisensteinAt (Submodule.span ℤ {↑p})
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).Monic
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>∀ {n_1 : ℕ}, n_1 < ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).natDegree → ((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff n_1 ∈ Submodule.span ℤ {↑p}
<VAR>R : Type u<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>((cyclotomic (p ^ (n + 1)) ℤ).comp (X + 1)).coeff 0 ∉ Submodule.span ℤ {↑p} ^ 2
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<GOAL>p w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>p w
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>p' 1 ⋯
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>∀ (x : W) (hx : x ∈ Submonoid.closure (Set.range cs.simple)) (y : W) (hy : y ∈ Set.range cs.simple), p' x hx → p' (x * y) ⋯
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>p : W → Prop<VAR>w : W<VAR>one : p 1<VAR>mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)<VAR>p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x => p w<VAR>this : w ∈ Submonoid.closure (Set.range cs.simple)<GOAL>w ∈ Submonoid.closure (Set.range cs.simple)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedField R<VAR>a b : ℍ[R]<VAR>q : ℚ<GOAL>↑(normSq ↑q) = ↑q ^ 2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : ι<VAR>hi : i ∉ range ⇑snf.f<VAR>m : M<VAR>hm : m ∈ N<GOAL>(snf.bM.repr ↑⟨m, hm⟩) i = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : ι<VAR>hi : i ∉ range ⇑snf.f<VAR>c : Fin n →₀ R<VAR>hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N<GOAL>(snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>i : ι<VAR>c : Fin n →₀ R<VAR>hm : (c.sum fun i x => x • ↑(snf.bN i)) ∈ N<VAR>hi : ∀ (j : Fin n), snf.f j ≠ i<GOAL>(snf.bM.repr ↑⟨c.sum fun i x => x • ↑(snf.bN i), hm⟩) i = 0
<VAR>x✝ y z x a : ℝ<GOAL>a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p r : α<VAR>h : ∀ {m : α}, m ∈ normalizedFactors r → m = p<VAR>hr : r ≠ 0<GOAL>∃ i, p ^ i ~ᵤ r
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p r : α<VAR>h : ∀ {m : α}, m ∈ normalizedFactors r → m = p<VAR>hr : r ≠ 0<GOAL>p ^ (↑Multiset.card).toFun (normalizedFactors r) ~ᵤ r
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p r : α<VAR>h : ∀ {m : α}, m ∈ normalizedFactors r → m = p<VAR>hr : r ≠ 0<VAR>this : (normalizedFactors r).prod ~ᵤ r<GOAL>p ^ (↑Multiset.card).toFun (normalizedFactors r) ~ᵤ r
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>b : β<GOAL>LipschitzWith 1 fun a => (a, b)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)<GOAL>↑(fib (n + 1)) ≤ (of v).dens n
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)<GOAL>↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)<VAR>this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)<GOAL>↑(fib (n + 1)) ≤ ((of v).contsAux (n + 1)).b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M✝ : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P✝ : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>a : Subtype P<VAR>m : M<VAR>a' : α<GOAL>(single a m).extendDomain a' = (single (↑a) m) a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M✝ : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P✝ : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>a : Subtype P<VAR>m : M<VAR>a' : α<GOAL>(if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M✝ : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P✝ : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>a : Subtype P<VAR>m : M<GOAL>(if h : P ↑a then (single a m) ⟨↑a, h⟩ else 0) = (single (↑a) m) ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M✝ : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P✝ : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>M : Type u_13<VAR>inst✝¹ : Zero M<VAR>P : α → Prop<VAR>inst✝ : DecidablePred P<VAR>a : Subtype P<VAR>m : M<VAR>a' : α<VAR>ha : ↑a ≠ a'<GOAL>(if h : P a' then (single a m) ⟨a', h⟩ else 0) = (single (↑a) m) a'
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<VAR>heq : dist p1 p2 = 0<GOAL>False
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : ∠ p1 p2 p3 = π<VAR>heq : p1 = p2<GOAL>False
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 : P<VAR>h : π / 2 = π<VAR>heq : p1 = p2<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a b : α<GOAL>↑s ⊆ {a} ↔ s ⊆ {a}