ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<VAR>h : Pairwise (Disjoint on B)<VAR>h' : ⋃ j, B j = univ<GOAL>n = 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<VAR>h : Pairwise (Disjoint on B)<VAR>h' : ⋃ j, B j = univ<VAR>hδ : 0 ≤ δ / 2<GOAL>n = 0
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>A : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup A<VAR>inst✝⁴ : CompactSpace A<VAR>inst✝³ : ConnectedSpace A<VAR>inst✝² : MeasurableSpace A<VAR>inst✝¹ : BorelSpace A<VAR>μ : Measure A<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>this : IsFiniteMeasure μ<VAR>B : ↑(Icc 0 n) → Set A := fun j => closedBall (↑j • ξ) (δ / 2)<VAR>hB : ∀ (j : ↑(Icc 0 n)), IsClosed (B j)<VAR>h : Pairwise (Disjoint on B)<VAR>h' : ⋃ j, B j = univ<VAR>hδ : 0 ≤ δ / 2<VAR>h'' : ∀ (j : ↑(Icc 0 n)), (B j).Nonempty<GOAL>n = 0
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁ b₂ b₃ c✝ c₁ c₂ : R<VAR>c k : ℕ<GOAL>a ^ (c * k) = (a ^ c) ^ k
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f<GOAL>(o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>H : o.bsup f = o.blsub f<GOAL>(o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<VAR>H : o.bsup f = o.blsub f<GOAL>(o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
<VAR>x y : ℝ<GOAL>↑(sin x ^ 2 + cos x ^ 2) = ↑1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>ha : a ≠ 0<GOAL>(C a).degree = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module.Finite R M₁<VAR>inst✝⁴ : Module.Free R M₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module.Finite R M₂<VAR>inst✝ : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>f₁ : M₁ →ₗ[R] M₁<VAR>f₂ : M₂ →ₗ[R] M₂<VAR>b₁ : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁<VAR>b₂ : Basis (ChooseBasisIndex R M₂) R M₂ := chooseBasis R M₂<VAR>b : Basis (ChooseBasisIndex R M₁ ⊕ ChooseBasisIndex R M₂) R (M₁ × M₂) := b₁.prod b₂<GOAL>(f₁.prodMap f₂).charpoly = f₁.charpoly * f₂.charpoly
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>f : R[X]<VAR>inst✝² : Algebra R S<VAR>T : Type u_1<VAR>inst✝¹ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>inst✝ : Algebra R T<VAR>hx' : (aeval x) f = 0<VAR>h : IsAdjoinRoot S f<VAR>z : R[X]<GOAL>(liftHom x hx' h) (h.map z) = (aeval x) z
<VAR>n p : ℕ<VAR>hp : Prime p<GOAL>Even p ↔ p = 2
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<GOAL>cos x ≤ 1 / √(x ^ 2 + 1)
<VAR>x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ 0<VAR>hx2 : 0 ≤ 3 * π / 2<GOAL>cos 0 ≤ 1 / √(0 ^ 2 + 1)
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<VAR>hx3 : x ≠ 0<GOAL>cos x ≤ 1 / √(x ^ 2 + 1)
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>val✝² : List α<VAR>property✝ : val✝².length = n<VAR>val✝¹ : ℕ<VAR>isLt✝¹ : val✝¹ < n<VAR>val✝ : ℕ<VAR>isLt✝ : val✝ < n<VAR>h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩<GOAL>(set ⟨val✝², property✝⟩ ⟨val✝¹, isLt✝¹⟩ a).get ⟨val✝, isLt✝⟩ = get ⟨val✝², property✝⟩ ⟨val✝, isLt✝⟩
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>val✝² : List α<VAR>property✝ : val✝².length = n<VAR>val✝¹ : ℕ<VAR>isLt✝¹ : val✝¹ < n<VAR>val✝ : ℕ<VAR>isLt✝ : val✝ < n<VAR>h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩<GOAL>(val✝².set val✝¹ a)[val✝] = val✝²[val✝]
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>val✝² : List α<VAR>property✝ : val✝².length = n<VAR>val✝¹ : ℕ<VAR>isLt✝¹ : val✝¹ < n<VAR>val✝ : ℕ<VAR>isLt✝ : val✝ < n<VAR>h : ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩<GOAL>val✝¹ ≠ val✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.268023, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>IsZero (Opposite.op ((shiftFunctor C (-1)).obj 0))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.268023, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>𝟙 (Opposite.op ((shiftFunctor C (-1)).obj 0)) = 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{?u.268023, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>(𝟙 ((shiftFunctor C (-1)).obj 0)).op = 0
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>i : B<GOAL>cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(𝓝 ⊤).HasBasis (fun x => True) fun x => Ioi ↑x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : EReal<VAR>hx : x < ⊤<GOAL>∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : EReal<VAR>hx : x < ⊤<VAR>y : ℚ<VAR>hxy : x < ↑↑y<GOAL>∃ i', True ∧ Ioi ↑i' ⊆ Ioi x
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x < x + ↑⌊τ f⌋ + 1
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x < x + (↑⌊τ f⌋ + 1)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x < x + ↑(⌊τ f⌋ + 1)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>τ f < ↑(⌊τ f⌋ + 1)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>τ f < ↑⌊τ f⌋ + 1
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>n m : ℤ<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>n m : ℤ<VAR>hn : 0 ≤ n<VAR>hm : 0 ≤ m<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>n m : ℤ<VAR>hn : 0 ≤ n<VAR>hm : m < 0<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>n m : ℤ<VAR>hn : n < 0<VAR>hm : 0 ≤ m<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>n m : ℤ<VAR>hn : n < 0<VAR>hm : m < 0<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<GOAL>σ.cycleType.lcm = orderOf σ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictInitialObjects C<VAR>I : C<VAR>hI : IsInitial I<VAR>A : C<VAR>f g : A ⟶ I<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictInitialObjects C<VAR>I : C<VAR>hI : IsInitial I<VAR>A : C<VAR>f g : A ⟶ I<VAR>this : IsIso f<GOAL>f = g
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasStrictInitialObjects C<VAR>I : C<VAR>hI : IsInitial I<VAR>A : C<VAR>f g : A ⟶ I<VAR>this✝ : IsIso f<VAR>this : IsIso g<GOAL>f = g
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<GOAL>∃ p ∈ I.minimalPrimes, p ≤ J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<GOAL>∃ m ∈ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}, OrderDual.toDual J ≤ m ∧ ∀ z ∈ {p | IsPrime p ∧ I ≤ p}, m ≤ z → z = m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<GOAL>∀ c ⊆ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}, IsChain (fun x x_1 => x ≤ x_1) c → ∀ y ∈ c, ∃ ub ∈ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}, ∀ z ∈ c, z ≤ ub
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<GOAL>OrderDual.toDual J ∈ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<VAR>c : Set (Ideal R)<VAR>hc : c ⊆ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}<VAR>hc' : IsChain (fun x x_1 => x ≤ x_1) c<VAR>J' : (Ideal R)ᵒᵈ<VAR>hJ' : J' ∈ c<GOAL>∃ ub ∈ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}, ∀ z ∈ c, z ≤ ub
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<VAR>c : Set (Ideal R)<VAR>hc : c ⊆ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}<VAR>hc' : IsChain (fun x x_1 => x ≤ x_1) c<VAR>J' : (Ideal R)ᵒᵈ<VAR>hJ' : J' ∈ c<GOAL>I ≤ OrderDual.ofDual (OrderDual.toDual (sInf c))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>I J : Ideal R<VAR>inst✝ : J.IsPrime<VAR>e : I ≤ J<VAR>c : Set (Ideal R)<VAR>hc : c ⊆ {p | IsPrime p ∧ I ≤ OrderDual.ofDual p}<VAR>hc' : IsChain (fun x x_1 => x ≤ x_1) c<VAR>J' : (Ideal R)ᵒᵈ<VAR>hJ' : J' ∈ c<GOAL>∀ z ∈ c, z ≤ OrderDual.toDual (sInf c)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Monoid N<VAR>inst✝² : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List M<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<GOAL>(map (⇑f) l).prod = f l.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : Monoid N<VAR>inst✝² : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a : M<VAR>l : List M<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<GOAL>foldl (fun x y => x * f y) (f 1) l = f (foldl (fun x x_1 => x * x_1) 1 l)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<GOAL>IsClosed {f | IsCompactOperator ⇑f}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<GOAL>closure {f | IsCompactOperator ⇑f} ⊆ {f | IsCompactOperator ⇑f}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : u ∈ closure {f | IsCompactOperator ⇑f}<GOAL>u ∈ {f | IsCompactOperator ⇑f}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<GOAL>u ∈ {f | IsCompactOperator ⇑f}
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<GOAL>TotallyBounded (⇑u '' closedBall 0 1)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<GOAL>∀ U ∈ 𝓝 0, ∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv✝ : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>hTv : ⇑v '' closedBall 0 1 ⊆ ⋃ y ∈ T, y +ᵥ V<GOAL>∃ t, t.Finite ∧ ⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ t, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv✝ : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>hTv : ⇑v '' closedBall 0 1 ⊆ ⋃ y ∈ T, y +ᵥ V<GOAL>⇑u '' closedBall 0 1 ⊆ ⋃ y ∈ T, y +ᵥ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv✝ : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>hTv : closedBall 0 1 ⊆ ⋃ i ∈ T, ⇑v ⁻¹' (i +ᵥ V)<GOAL>closedBall 0 1 ⊆ ⋃ i ∈ T, ⇑u ⁻¹' (i +ᵥ U)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv✝ : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>hTv : x ∈ ⋃ i ∈ T, ⇑v ⁻¹' (i +ᵥ V)<GOAL>x ∈ ⋃ i ∈ T, ⇑u ⁻¹' (i +ᵥ U)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv✝ : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>hTv : ∃ i, ∃ (_ : i ∈ T), x ∈ ⇑v ⁻¹' (i +ᵥ V)<GOAL>∃ i, ∃ (_ : i ∈ T), x ∈ ⇑u ⁻¹' (i +ᵥ U)