ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<VAR>b : Γ<VAR>hr : ¬r = 0<GOAL>((of R).symm ((HahnSeries.single b) r • x)).coeff (b +ᵥ a) = r • ((of R).symm x).coeff a
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁶ : PartialOrder Γ<VAR>inst✝⁵ : PartialOrder Γ'<VAR>inst✝⁴ : VAdd Γ Γ'<VAR>inst✝³ : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<VAR>b : Γ<VAR>hr : ¬r = 0<GOAL>∑ x_1 ∈ VAddAntidiagonal ⋯ ⋯ (b +ᵥ a), ((HahnSeries.single b) r).coeff x_1.1 • ((of R).symm x).coeff x_1.2 = r • ((of R).symm x).coeff a
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>x y : FractionRing R[X]<GOAL>(liftMonoidWithZeroHom φ hφ') { toFractionRing := x } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } → { toFractionRing := x } = { toFractionRing := y }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>y : FractionRing R[X]<VAR>a : R[X] × ↥R[X]⁰<GOAL>(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := y } → { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := y }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<GOAL>(liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a.1 a.2 } = (liftMonoidWithZeroHom φ hφ') { toFractionRing := Localization.mk a'.1 a'.2 } → { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<GOAL>φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2 → { toFractionRing := Localization.mk a.1 a.2 } = { toFractionRing := Localization.mk a'.1 a'.2 }
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<VAR>h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2<GOAL>Localization.mk a.1 a.2 = Localization.mk a'.1 a'.2
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<VAR>h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2<GOAL>↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<VAR>h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2<VAR>this : φ a.1 * φ ↑a'.2 = φ a'.1 * φ ↑a.2<GOAL>↑(a'.1, a'.2).2 * (a.1, a.2).1 = ↑(a.1, a.2).2 * (a'.1, a'.2).1
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<VAR>h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2<GOAL>φ ↑a.2 ≠ 0
<VAR>K : Type u<VAR>inst✝⁶ : CommRing K<VAR>G₀ : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : CommGroupWithZero G₀<VAR>inst✝⁴ : Field L<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : Nontrivial R<VAR>φ : R[X] →*₀ G₀<VAR>hφ : Function.Injective ⇑φ<VAR>hφ' : optParam (R[X]⁰ ≤ Submonoid.comap φ G₀⁰) ⋯<VAR>a a' : R[X] × ↥R[X]⁰<VAR>h : φ a.1 / φ ↑a.2 = φ a'.1 / φ ↑a'.2<GOAL>φ ↑a'.2 ≠ 0
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<GOAL>IsCoprime I J ↔ I ⊔ J = ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasShift C ℤ<VAR>X : C<VAR>X✝ Y✝ : Triangle C<VAR>f : X✝ ⟶ Y✝<GOAL>(-(shiftFunctor C 1).map X✝.mor₁) ≫ (shiftFunctor C 1).map f.hom₂ = (shiftFunctor C 1).map f.hom₁ ≫ (-(shiftFunctor C 1).map Y✝.mor₁)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f✝ f : R →+* S<VAR>x : R<VAR>p : R[X]<VAR>h : p.IsRoot x<GOAL>(Polynomial.map f p).IsRoot (f x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>h : IsInitial X → False<VAR>hzero : Nat.card ↑(F.obj X) = 0<GOAL>False
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>h : IsInitial X → False<VAR>hzero : Nat.card ↑(F.obj X) = 0<GOAL>Nonempty (IsInitial X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>h : IsInitial X → False<VAR>hzero : Nat.card ↑(F.obj X) = 0<GOAL>IsEmpty ↑(F.obj X)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>r : ℝ≥0∞<GOAL>volume (EMetric.ball a r) = 2 * r
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<GOAL>volume (EMetric.ball a ⊤) = 2 * ⊤
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>r : ℝ≥0∞<VAR>hr : r ≠ ⊤<GOAL>volume (EMetric.ball a r) = 2 * r
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hT : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse<VAR>l : Λ<VAR>N : Stmt₂<GOAL>∃ b, TrCfg (TM2.stepAux N v S) b ∧ Reaches (TM1.step (tr M)) (TM1.stepAux (trNormal N) v (Tape.mk' ∅ (addBottom L))) b
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝¹⁰ : NormedField 𝕜<VAR>inst✝⁹ : AddCommGroup H<VAR>inst✝⁸ : Module 𝕜 H<VAR>inst✝⁷ : AddCommGroup E<VAR>inst✝⁶ : Module 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>hφ : Inducing (⇑(ofFun 𝔖) ∘ ⇑φ)<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<VAR>hφ : Inducing (⇑(ofFun 𝔖) ∘ ⇑φ)<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<VAR>s : Set α<VAR>hs : s ∈ 𝔖<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<VAR>s : Set α<VAR>hs : s ∈ 𝔖<VAR>this : TopologicalSpace H := TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<VAR>s : Set α<VAR>hs : s ∈ 𝔖<VAR>this : TopologicalSpace H := TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)<VAR>φ' : H →ₗ[𝕜] ↑s → E := { toFun := s.restrict ∘ ⇑φ, map_add' := ⋯, map_smul' := ⋯ }<GOAL>ContinuousSMul 𝕜 H
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>H : Type u_4<VAR>hom : Type u_5<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup H<VAR>inst✝⁷ : Module 𝕜 H<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : UniformSpace E<VAR>inst✝³ : UniformAddGroup E<VAR>inst✝² : ContinuousSMul 𝕜 E<VAR>𝔖 : Set (Set α)<VAR>inst✝¹ : FunLike hom H (α → E)<VAR>inst✝ : LinearMapClass hom 𝕜 H (α → E)<VAR>φ : hom<VAR>h : ∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)<VAR>s : Set α<VAR>hs : s ∈ 𝔖<VAR>this : TopologicalSpace H := TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑φ) (UniformFun.topologicalSpace (↑s) E)<VAR>φ' : H →ₗ[𝕜] ↑s → E := { toFun := s.restrict ∘ ⇑φ, map_add' := ⋯, map_smul' := ⋯ }<VAR>u : H<GOAL>Bornology.IsVonNBounded 𝕜 (Set.range (φ' u))
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝³ : BooleanAlgebra α<VAR>inst✝² : BooleanAlgebra β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : BoundedLatticeHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a \ b) = f a \ f b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)<VAR>K : ι → ℕ → Set X<VAR>hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)<VAR>hcov : ∀ (i : ι), ⋃ n, K i n = s i<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)<VAR>K : ι → ℕ → Set X<VAR>hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)<VAR>hcov : ∀ (i : ι), ⋃ n, K i n = s i<VAR>this : ⋃ i, s i = ⋃ x, Function.uncurry K x<GOAL>IsSigmaCompact (⋃ i, s i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)<VAR>K : ι → ℕ → Set X<VAR>hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)<VAR>hcov : ∀ (i : ι), ⋃ n, K i n = s i<VAR>this : ⋃ i, s i = ⋃ x, Function.uncurry K x<GOAL>IsSigmaCompact (⋃ x, Function.uncurry K x)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<GOAL>Tendsto f atTop (𝓝 g)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<VAR>b : ℕ → ℝ<VAR>hb₀ : ∀ (n : ℕ), 0 ≤ b n<VAR>hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N<VAR>hb_lim : Tendsto b atTop (𝓝 0)<GOAL>Tendsto f atTop (𝓝 g)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<VAR>b : ℕ → ℝ<VAR>hb₀ : ∀ (n : ℕ), 0 ≤ b n<VAR>hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N<VAR>hb_lim : Tendsto b atTop (𝓝 0)<GOAL>∀ (n : ℕ) (x : E'), ‖(f n) x - g x‖ ≤ b n * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<VAR>b : ℕ → ℝ<VAR>hb₀ : ∀ (n : ℕ), 0 ≤ b n<VAR>hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N<VAR>hb_lim : Tendsto b atTop (𝓝 0)<VAR>n : ℕ<VAR>x : E'<GOAL>‖(f n) x - g x‖ ≤ b n * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<VAR>b : ℕ → ℝ<VAR>hb₀ : ∀ (n : ℕ), 0 ≤ b n<VAR>hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N<VAR>hb_lim : Tendsto b atTop (𝓝 0)<VAR>n : ℕ<VAR>x : E'<VAR>this : Tendsto (fun m => ‖(f n) x - (f m) x‖) atTop (𝓝 ‖(f n) x - g x‖)<GOAL>‖(f n) x - g x‖ ≤ b n * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedAddCommGroup G<VAR>inst✝¹⁰ : NormedAddCommGroup Fₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜₂ F<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f✝ g✝ : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>E' : Type u_11<VAR>inst✝² : SeminormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace 𝕜 E'<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : ℕ → E' →SL[σ₁₂] F<VAR>g : E' →SL[σ₁₂] F<VAR>hg : Tendsto (fun n x => (f n) x) atTop (𝓝 ⇑g)<VAR>hf : CauchySeq f<VAR>b : ℕ → ℝ<VAR>hb₀ : ∀ (n : ℕ), 0 ≤ b n<VAR>hfb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N<VAR>hb_lim : Tendsto b atTop (𝓝 0)<VAR>n : ℕ<VAR>x : E'<VAR>this : Tendsto (fun m => ‖(f n) x - (f m) x‖) atTop (𝓝 ‖(f n) x - g x‖)<VAR>m : ℕ<VAR>hm : m ≥ n<GOAL>‖(f n) x - (f m) x‖ ≤ b n * ‖x‖
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : LinearOrderedField R<VAR>inst✝ : Archimedean R<VAR>r : R<VAR>n : ℕ<VAR>hn : -r ≤ ↑n<GOAL>↑(-↑n) ≤ r
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>l₁ ~ l₂ → List.kerase a l₁ ~ List.kerase a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>Pairwise (fun a_1 b => decide (a = a_1.fst) = true → decide (a = b.fst) = true → False) l₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>l l₁✝ l₂✝ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>nd : l₁.NodupKeys<GOAL>∀ {a_1 b : Sigma β}, a_1.fst ≠ b.fst → decide (a = a_1.fst) = true → decide (a = b.fst) = true → False
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>s : Set E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹² : CommSemiring R✝<VAR>inst✝¹¹ : NonUnitalRing A✝<VAR>inst✝¹⁰ : Module R✝ A✝<VAR>inst✝⁹ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁸ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁷ : Semifield R<VAR>inst✝⁶ : Field S<VAR>inst✝⁵ : NonUnitalRing A<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : Module S A<VAR>inst✝² : IsScalarTower S A A<VAR>inst✝¹ : SMulCommClass S A A<VAR>inst✝ : Algebra R S<VAR>a : A<VAR>f : S → R<VAR>h : QuasispectrumRestricts a f<GOAL>f 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b c d : Associates α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<VAR>x : Associates α<VAR>hx : b = a * x<VAR>y : Associates α<VAR>hy : d = c * y<GOAL>b * d = a * c * (x * y)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>c ⊔ d = ringConGen (⇑c ⊔ ⇑d)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>c d : RingCon R<GOAL>(ringConGen fun x y => c x y ∨ d x y) = ringConGen (⇑c ⊔ ⇑d)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>¬x ⤳ y ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(¬∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<GOAL>(∃ s, IsClosed s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ S, IsClosed S ∧ x ∈ S ∧ y ∉ S
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s : LowerSet α<VAR>a : α<GOAL>SupIrred (Iic a)
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : LowerSet α<VAR>a : α<VAR>s t : LowerSet α<VAR>hst : s ⊔ t = Iic a<GOAL>s = Iic a ∨ t = Iic a
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : LowerSet α<VAR>a : α<VAR>s t : LowerSet α<VAR>hst : s ⊔ t = Iic a<VAR>this : a ∈ Iic a<GOAL>s = Iic a ∨ t = Iic a