ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>(∀ (x : α), (𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsConnected s) id) ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x✝ : α<GOAL>(𝓝 x✝).HasBasis (fun s => IsOpen s ∧ x✝ ∈ s ∧ IsConnected s) id ↔ ∀ U ∈ 𝓝 x✝, ∃ V ⊆ U, IsOpen V ∧ x✝ ∈ V ∧ IsConnected V
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).valuation = x.valuation + y.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h_norm : ‖x * y‖ = ‖x‖ * ‖y‖<GOAL>(x * y).valuation = x.valuation + y.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h_norm : ‖x * y‖ = ‖x‖ * ‖y‖<VAR>hp_ne_one : ↑p ≠ 1<GOAL>(x * y).valuation = x.valuation + y.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h_norm : ‖x * y‖ = ‖x‖ * ‖y‖<VAR>hp_ne_one : ↑p ≠ 1<VAR>hp_pos : 0 < ↑p<GOAL>(x * y).valuation = x.valuation + y.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ℚ_[p]<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h_norm : (x * y).valuation = x.valuation + y.valuation<VAR>hp_ne_one : ↑p ≠ 1<VAR>hp_pos : 0 < ↑p<GOAL>(x * y).valuation = x.valuation + y.valuation
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b✝ c a b : α<GOAL>|a * b| = |a| * |b|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b✝ c a b : α<GOAL>a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<GOAL>descSet hc {x} ∩ descSet hc {y} = ∅
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<GOAL>∀ (j : J) (x_1 : K.obj j), lc.ι.app j { down := x_1 } ∈ ∅ ↔ c.ι.app j x_1 ∈ descSet hc {x} ∩ descSet hc {y}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<VAR>j : J<VAR>z : K.obj j<GOAL>lc.ι.app j { down := z } ∈ ∅ ↔ c.ι.app j z ∈ descSet hc {x} ∩ descSet hc {y}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<VAR>j : J<VAR>z : K.obj j<GOAL>c.ι.app j z ∉ descSet hc {x} ∩ descSet hc {y}
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<VAR>j : J<VAR>z : K.obj j<VAR>hx : c.ι.app j z ∈ descSet hc {x}<VAR>hy : c.ι.app j z ∈ descSet hc {y}<GOAL>False
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<VAR>x y : lc.pt<VAR>hn : x ≠ y<VAR>j : J<VAR>z : K.obj j<VAR>hx : lc.ι.app j { down := z } = x<VAR>hy : lc.ι.app j { down := z } = y<GOAL>False
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin p.length<GOAL>(if H : ↑i < p.length then p.toFun ⟨↑i, ⋯⟩ else q.toFun ⟨↑i - p.length, ⋯⟩) = p.toFun i.castSucc
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>connect : p.last = q.head<VAR>i : Fin p.length<GOAL>p.toFun ⟨↑i, ⋯⟩ = p.toFun i.castSucc
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S T : NonUnitalSubalgebra R A<GOAL>∀ {x : A}, x ∈ T → x ∈ S ⊔ T
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S T : NonUnitalSubalgebra R A<GOAL>T ≤ S ⊔ T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E''<VAR>c' : F''<VAR>l : Filter α<VAR>inst✝ : l.NeBot<GOAL>((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E''<VAR>l : Filter α<VAR>inst✝ : l.NeBot<GOAL>((fun _x => c) =O[l] fun _x => 0) ↔ 0 = 0 → c = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁴ : Norm E<VAR>inst✝¹³ : Norm F<VAR>inst✝¹² : Norm G<VAR>inst✝¹¹ : SeminormedAddCommGroup E'<VAR>inst✝¹⁰ : SeminormedAddCommGroup F'<VAR>inst✝⁹ : SeminormedAddCommGroup G'<VAR>inst✝⁸ : NormedAddCommGroup E''<VAR>inst✝⁷ : NormedAddCommGroup F''<VAR>inst✝⁶ : NormedAddCommGroup G''<VAR>inst✝⁵ : SeminormedRing R<VAR>inst✝⁴ : SeminormedAddGroup E'''<VAR>inst✝³ : SeminormedRing R'<VAR>inst✝² : NormedDivisionRing 𝕜<VAR>inst✝¹ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l✝ l' : Filter α<VAR>c : E''<VAR>c' : F''<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>hc' : c' ≠ 0<GOAL>((fun _x => c) =O[l] fun _x => c') ↔ c' = 0 → c = 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b b' : β a<VAR>s✝ : Finmap β<VAR>s : AList β<GOAL>insert a b' (insert a b ⟦s⟧) = insert a b' ⟦s⟧
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>x : α 0<VAR>q : (i : Fin (n + 1)) → α i<VAR>p : (i : Fin n) → α i.succ<VAR>i : Fin n<VAR>y : α i.succ<VAR>z : α 0<VAR>j : Fin n<GOAL>tail (update q 0 z) j = tail q j
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set α<VAR>f : (x : α) → x ∈ S → Set X<VAR>ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)<VAR>hS : S.Countable<VAR>hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)<GOAL>Dense (⋂ s, ⋂ (h : s ∈ S), f s h)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set α<VAR>f : (x : α) → x ∈ S → Set X<VAR>ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)<VAR>hS : S.Countable<VAR>hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)<GOAL>Dense (⋂ x, f ↑x ⋯)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set α<VAR>f : (x : α) → x ∈ S → Set X<VAR>ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)<VAR>hS : S.Countable<VAR>hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)<VAR>this : Countable ↑S<GOAL>Dense (⋂ x, f ↑x ⋯)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : AddMonoid N<VAR>M' : Type u_3<VAR>inst✝ : Monoid M'<VAR>P : Submonoid M<VAR>h : P.FG<VAR>e : M →* M'<GOAL>(Submonoid.map e P).FG
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>whiskerRight (leftDerivedToHomotopyCategory (𝟙 F)) (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) = 𝟙 (F.leftDerived n)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>𝟙 (F.leftDerivedToHomotopyCategory ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) = 𝟙 (F.leftDerived n)
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>h : ContinuousMultilinearMap 𝕜 E' F<GOAL>((liftIsometry 𝕜 E' F) h).comp (mapL f) = (liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>h : ContinuousMultilinearMap 𝕜 E' F<GOAL>↑(((liftIsometry 𝕜 E' F) h).comp (mapL f)) = ↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>h : ContinuousMultilinearMap 𝕜 E' F<VAR>x✝ : (i : ι) → E i<GOAL>((↑(((liftIsometry 𝕜 E' F) h).comp (mapL f))).compMultilinearMap (tprod 𝕜)) x✝ = ((↑((liftIsometry 𝕜 E F) (h.compContinuousLinearMap f))).compMultilinearMap (tprod 𝕜)) x✝
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>x : α<GOAL>{y | (mkClasses c H).Rel x y} ∈ c
<VAR>α : Type u_1<VAR>c : Set (Set α)<VAR>H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b<VAR>x x✝ : α<GOAL>(mkClasses c H).Rel x x✝ ↔ (mkClasses c H).Rel x✝ x
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ ↑s.direction ↔ v ∈ (fun x => p -ᵥ x) '' ↑s
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>(∃ x ∈ ↑s, x -ᵥ p = -v) ↔ ∃ x ∈ ↑s, p -ᵥ x = v
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ι → ↥(lp E p)<VAR>hF : Bornology.IsBounded (Set.range F)<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ι → ↥(lp E p)<VAR>hF : Bornology.IsBounded (Set.range F)<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>C : ℝ<VAR>hCF : ∀ (k : ι), ‖F k‖ ≤ C<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>f : (a : α) → E a<VAR>C : ℝ<VAR>_i : Fact (1 ≤ ⊤)<VAR>F : ι → ↥(lp E ⊤)<VAR>hF : Bornology.IsBounded (Set.range F)<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>hCF : ∀ (k : ι), ‖F k‖ ≤ C<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>ι : Type u_3<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>_i : Fact (1 ≤ p)<VAR>F : ι → ↥(lp E p)<VAR>hF : Bornology.IsBounded (Set.range F)<VAR>f : (a : α) → E a<VAR>hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)<VAR>C : ℝ<VAR>hCF : ∀ (k : ι), ‖F k‖ ≤ C<VAR>hp : p < ⊤<GOAL>Memℓp f p
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<VAR>h : Squarefree (n ^ k)<GOAL>Squarefree n ∧ k = 1
<VAR>s : Finset ℕ<VAR>m n p k : ℕ<VAR>hk : k ≠ 0<VAR>hn : 0 ≠ 1<VAR>h : Squarefree (0 ^ k)<GOAL>Squarefree 0 ∧ k = 1
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<VAR>h : Squarefree (n ^ k)<VAR>h₁ : ¬k = 1<GOAL>False
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<VAR>h : Squarefree (n ^ k)<VAR>h₁ : ¬k = 1<VAR>this : 2 ≤ k<GOAL>False
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<VAR>h : Squarefree (n ^ k)<VAR>h₁ : ¬k = 1<VAR>this : 2 ≤ k<GOAL>n * n ∣ n ^ k
<VAR>s : Finset ℕ<VAR>m n✝ p n k : ℕ<VAR>hn : n ≠ 1<VAR>hk : k ≠ 0<VAR>h : Squarefree (n ^ k)<VAR>h₁ : ¬k = 1<VAR>this : 2 ≤ k<GOAL>n ^ 2 ∣ n ^ k
<VAR>m✝ n✝ a b c d n m : ℕ<GOAL>n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<GOAL>Squarefree n ∧ IsPrimePow n ↔ Prime n
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<GOAL>Squarefree n ∧ IsPrimePow n → Prime n
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<GOAL>(Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
<VAR>s : Finset ℕ<VAR>m n p✝ p k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>h : Squarefree (p ^ k)<GOAL>Prime (p ^ k)
<VAR>s : Finset ℕ<VAR>m n p✝ p k : ℕ<VAR>hp : Prime p<VAR>hk : 0 < k<VAR>h : Squarefree p ∧ k = 1<GOAL>Prime (p ^ k)
<VAR>p b : ℝ<VAR>hp : 0 < p<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = b ^ (-1 / p) * Gamma (1 / p + 1)
<VAR>p b : ℝ<VAR>hp : 0 < p<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in Ioi 0, rexp (-b * x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-b * x ^ p)
<VAR>p b : ℝ<VAR>hp : 0 < p<VAR>hb : 0 < b<GOAL>b ^ (-1 / p) * Gamma (1 / p + 1) = b ^ (-(0 + 1) / p) * (1 / p) * Gamma ((0 + 1) / p)
<VAR>n : ℕ<GOAL>↑n = 1 ↔ Odd n
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)) ⋯<GOAL>IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ) h)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)) ⋯<GOAL>LinearMap.restrict (f - (algebraMap R (End R M)) μ) h ^ k = 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k : ℕ<VAR>h : optParam (MapsTo ⇑(f - (algebraMap R (End R M)) μ) ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)) ⋯<VAR>x✝ : ↥((f.genEigenspace μ) k)<GOAL>↑((LinearMap.restrict (f - (algebraMap R (End R M)) μ) h ^ k) x✝) = ↑(0 x✝)
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p : K[X]<VAR>q : ↥K[X]⁰<GOAL>RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p q }
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<GOAL>∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : (fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖<VAR>hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2<GOAL>∀ (i : α), ↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn : ‖↑n / log ↑n ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖<VAR>hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2<VAR>i : α<GOAL>↑(r i n) ≤ c * ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c : ℝ := b (max_bi b) + (1 - b (max_bi b)) / 2<VAR>h_max_bi_pos : 0 < b (max_bi b)<VAR>h_max_bi_lt_one : 0 < 1 - b (max_bi b)<VAR>hc_pos : 0 < c<VAR>h₁ : 0 < (1 - b (max_bi b)) / 2<VAR>hc_lt_one : c < 1<VAR>hlo : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ c * ‖↑x‖<VAR>hlo' : ∀ᶠ (x : ℕ) in atTop, ‖↑x / log ↑x ^ 2‖ ≤ (1 - b (max_bi b)) / 2 * ‖↑x‖<VAR>n : ℕ<VAR>hn : ↑n / log ↑n ^ 2 ≤ (1 - b (max_bi b)) / 2 * ‖↑n‖<VAR>hn' : ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / log ↑n ^ 2<VAR>i : α<GOAL>↑(r i n) ≤ c * ↑n