ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>(sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op t)))).hom ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val = ((presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ (F.val.obj (op t)) U)).hom ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)) ⋙ U) ≫ (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.val.obj (op t)))).hom ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val = toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)) ⋙ U) ≫ ((presheafToSheaf J B ⋙ sheafToPresheaf J B).mapIso (constComp Cᵒᵖ (F.val.obj (op t)) U)).hom ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val = toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)) ⋙ U) ≫ ((presheafToSheaf J B).map (constComp Cᵒᵖ (F.val.obj (op t)) U).hom).val ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val = (constComp Cᵒᵖ (F.val.obj (op t)) U).hom ≫ (sheafificationAdjunction J B).unit.app ((const Cᵒᵖ).obj (U.obj (F.val.obj (op t)))) ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<GOAL>whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val = { app := fun x => 𝟙 (U.obj (F.val.obj (op t))), naturality := ⋯ } ≫ toSheafify J ((const Cᵒᵖ).obj (U.obj (F.val.obj (op t)))) ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>x✝ : Cᵒᵖ<GOAL>(whiskerRight (toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))) U ≫ ((sheafCompose J U).map ((constantSheafAdj J A ht).counit.app F)).val).app x✝ = ({ app := fun x => 𝟙 (U.obj (F.val.obj (op t))), naturality := ⋯ } ≫ toSheafify J ((const Cᵒᵖ).obj (U.obj (F.val.obj (op t)))) ≫ ((constantSheafAdj J B ht).counit.app ((sheafCompose J U).obj F)).val).app x✝
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>x✝ : Cᵒᵖ<GOAL>U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))).app x✝) ≫ U.map (𝟙 (((presheafToSheaf J A).obj ((const Cᵒᵖ).obj (F.val.obj (op t)))).val.obj x✝)) ≫ U.map (((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val.app x✝) ≫ U.map ((sheafifyLift J (𝟙 F.val) ⋯).app x✝) = (toSheafify J ((const Cᵒᵖ).obj (U.obj (F.val.obj (op t))))).app x✝ ≫ (sheafifyLift J ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ⋯).app x✝
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_5, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_6, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_4, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F : Sheaf J A<VAR>x✝ : Cᵒᵖ<GOAL>U.map ((toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op t)))).app x✝) ≫ U.map (((presheafToSheaf J A).map ((constantPresheafAdj A ht).counit.app F.val)).val.app x✝) ≫ U.map ((sheafifyLift J (𝟙 F.val) ⋯).app x✝) = (toSheafify J ((const Cᵒᵖ).obj (U.obj (F.val.obj (op t)))) ≫ sheafifyLift J ((constantPresheafAdj B ht).counit.app (F.val ⋙ U)) ⋯).app x✝
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<GOAL>∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>x : ↥(f.domain ⊔ g.domain) → E<VAR>hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain<VAR>y : ↥(f.domain ⊔ g.domain) → E<VAR>hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain<VAR>hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z<GOAL>∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>x : ↥(f.domain ⊔ g.domain) → E<VAR>hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain<VAR>y : ↥(f.domain ⊔ g.domain) → E<VAR>hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain<VAR>hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z<VAR>fg : ↥(f.domain ⊔ g.domain) → F := fun z => ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩<GOAL>∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>f g : E →ₗ.[R] F<VAR>h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y<VAR>x : ↥(f.domain ⊔ g.domain) → E<VAR>hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain<VAR>y : ↥(f.domain ⊔ g.domain) → E<VAR>hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain<VAR>hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z<VAR>fg : ↥(f.domain ⊔ g.domain) → F := fun z => ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩<VAR>fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'<GOAL>∃ fg, ∀ (x : ↥f.domain) (y : ↥g.domain) (z : ↥(f.domain ⊔ g.domain)), ↑x + ↑y = ↑z → fg z = ↑f x + ↑g y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>t 𝒰 f g i j ≫ pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) ≫ pullback.fst (𝒰.map j ≫ f) g = pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x - y) < π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x - y) < π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>angle x (x + -y) < π / 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>c : β<GOAL>Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun x => c) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>c : β<GOAL>Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p ⊤
<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>t : Triangle ℝ P<VAR>ho : t.orthocenter ∉ Set.range t.points<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hpi : Function.Injective p<GOAL>∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
<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>t : Triangle ℝ P<VAR>ho : t.orthocenter ∉ Set.range t.points<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hpi : Function.Injective p<VAR>i₁ i₂ i₃ j₂ j₃ : Fin 3<VAR>left✝² : i₁ ≠ i₂<VAR>left✝¹ : i₁ ≠ i₃<VAR>left✝ : i₂ ≠ i₃<VAR>h₁₂₃ : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>h₁ : p i₁ = t.orthocenter<VAR>hj₂₃ : j₂ ≠ j₃<VAR>h₂ : t.points j₂ = p i₂<VAR>h₃ : t.points j₃ = p i₃<GOAL>∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
<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>t : Triangle ℝ P<VAR>ho : t.orthocenter ∉ Set.range t.points<VAR>p : Fin 3 → P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hpi : Function.Injective p<VAR>hs : Set.range p = Set.range t.points<GOAL>∃ c ∈ affineSpan ℝ (Set.range t.points), ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>f : ℕ → α<VAR>a : α<VAR>d : ℕ → ℝ<VAR>hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n<VAR>hd : Summable d<VAR>ha : Tendsto f atTop (𝓝 a)<GOAL>dist (f 0) a ≤ tsum d
<VAR>z x✝ y x p : ℝ<VAR>hx : x ≠ 0 ∨ 1 ≤ p<GOAL>x ≠ 0 ∨ ↑One.one ≤ p
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>p : ι → Set (Set α)<VAR>hp_pi : ∀ (n : ι), IsPiSystem (p n)<VAR>hp_directed : Directed (fun x x_1 => x ≤ x_1) p<VAR>t1 : Set α<VAR>ht1 : t1 ∈ ⋃ n, p n<VAR>t2 : Set α<VAR>ht2 : t2 ∈ ⋃ n, p n<VAR>h : (t1 ∩ t2).Nonempty<GOAL>t1 ∩ t2 ∈ ⋃ n, p n
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>p : ι → Set (Set α)<VAR>hp_pi : ∀ (n : ι), IsPiSystem (p n)<VAR>hp_directed : Directed (fun x x_1 => x ≤ x_1) p<VAR>t1 : Set α<VAR>ht1 : ∃ i, t1 ∈ p i<VAR>t2 : Set α<VAR>ht2 : ∃ i, t2 ∈ p i<VAR>h : (t1 ∩ t2).Nonempty<GOAL>∃ i, t1 ∩ t2 ∈ p i
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : PartialOrder A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarOrderedRing A<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Module ℝ A<VAR>inst✝⁴ : IsScalarTower ℝ A A<VAR>inst✝³ : SMulCommClass ℝ A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus ℝ A<VAR>a : A<GOAL>0 ≤ a ↔ IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : PartialOrder A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarOrderedRing A<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Module ℝ A<VAR>inst✝⁴ : IsScalarTower ℝ A A<VAR>inst✝³ : SMulCommClass ℝ A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus ℝ A<VAR>a : A<GOAL>IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal → 0 ≤ a
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : PartialOrder A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarOrderedRing A<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Module ℝ A<VAR>inst✝⁴ : IsScalarTower ℝ A A<VAR>inst✝³ : SMulCommClass ℝ A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>0 ≤ a
<VAR>A : Type u_1<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : PartialOrder A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : StarOrderedRing A<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : Module ℝ A<VAR>inst✝⁴ : IsScalarTower ℝ A A<VAR>inst✝³ : SMulCommClass ℝ A A<VAR>inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueNonUnitalContinuousFunctionalCalculus ℝ A<VAR>x : A<VAR>hx : IsSelfAdjoint x<VAR>ha₁ : IsSelfAdjoint (x * x)<VAR>ha₂ : QuasispectrumRestricts (x * x) ⇑ContinuousMap.realToNNReal<GOAL>0 ≤ x * x
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : ↑((autToPow K hμ) f) = ↑((autToPow K hμ) g)<GOAL>f = g
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hfg : ↑⋯.choose = ↑⋯.choose<GOAL>f = g
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : ↑hf'.choose = ↑hg'.choose<GOAL>f = g
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : ↑hf'.choose = ↑hg'.choose<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<GOAL>f = g
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : ↑hf'.choose = ↑hg'.choose<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>f = g
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : ↑hf'.choose = ↑hg'.choose<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>f ↑↑hμ.toRootsOfUnity = g ↑↑hμ.toRootsOfUnity
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>f ↑↑hμ.toRootsOfUnity = g ↑↑hμ.toRootsOfUnity
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>↑↑hμ.toRootsOfUnity ^ hf'.choose = ↑↑hμ.toRootsOfUnity ^ hg'.choose
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>↑↑(hμ.toRootsOfUnity ^ hf'.choose) = ↑↑(hμ.toRootsOfUnity ^ hg'.choose)
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>hμ.toRootsOfUnity ^ hf'.choose = hμ.toRootsOfUnity ^ hg'.choose
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>hf'.choose ≡ hg'.choose [MOD orderOf hμ.toRootsOfUnity]
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>orderOf hμ.toRootsOfUnity = ↑n
<VAR>n : ℕ+<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>L : Type u_2<VAR>μ : L<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>f g : L ≃ₐ[K] L<VAR>hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m<VAR>hfg : hf'.choose ≡ hg'.choose [MOD ↑n]<VAR>hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose<VAR>hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose<GOAL>orderOf hμ.toRootsOfUnity = orderOf μ