ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<VAR>h : n ∈ (derivative p).support<VAR>h1 : p.coeff (n + 1) = 0<GOAL>(derivative p).coeff n = 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>c : E<GOAL>∫ (x : ℝ) in a..b, c = (b - a) • c
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : GroupWithZero α<VAR>inst✝³ : GroupWithZero β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : SMulCommClass α β β<VAR>inst✝ : IsScalarTower α β β<VAR>c : α<VAR>x : β<GOAL>(c • x)⁻¹ = c⁻¹ • x⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : GroupWithZero α<VAR>inst✝³ : GroupWithZero β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : SMulCommClass α β β<VAR>inst✝ : IsScalarTower α β β<VAR>x : β<GOAL>(0 • x)⁻¹ = 0⁻¹ • x⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : GroupWithZero α<VAR>inst✝³ : GroupWithZero β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : SMulCommClass α β β<VAR>inst✝ : IsScalarTower α β β<VAR>c : α<VAR>x : β<VAR>hc : c ≠ 0<GOAL>(c • x)⁻¹ = c⁻¹ • x⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : GroupWithZero α<VAR>inst✝³ : GroupWithZero β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : SMulCommClass α β β<VAR>inst✝ : IsScalarTower α β β<VAR>c : α<VAR>hc : c ≠ 0<GOAL>(c • 0)⁻¹ = c⁻¹ • 0⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : GroupWithZero α<VAR>inst✝³ : GroupWithZero β<VAR>inst✝² : MulActionWithZero α β<VAR>inst✝¹ : SMulCommClass α β β<VAR>inst✝ : IsScalarTower α β β<VAR>c : α<VAR>x : β<VAR>hc : c ≠ 0<VAR>hx : x ≠ 0<GOAL>(c • x)⁻¹ = c⁻¹ • x⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>b : β<VAR>c : γ<VAR>f : δ ≃. β<VAR>h : f.symm b = none<VAR>x✝ : δ<VAR>a✝ : γ<GOAL>a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>b : β<VAR>c : γ<VAR>f : δ ≃. β<VAR>x✝ : δ<VAR>a✝ : γ<VAR>h : ∀ (a : δ), ¬f a = some b<GOAL>a✝ ∈ (f.trans (single b c)) x✝ ↔ a✝ ∈ ⊥ x✝
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>b : β<VAR>c : γ<VAR>f : δ ≃. β<VAR>x✝ : δ<VAR>a✝ : γ<VAR>h : ∀ (a : δ), ¬f a = some b<GOAL>(a✝ ∈ (f x✝).bind fun x => if x = b then some c else none) ↔ a✝ ∈ none
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq γ<VAR>b : β<VAR>c : γ<VAR>f : δ ≃. β<VAR>x✝ : δ<VAR>a✝ : γ<VAR>h : ∀ (a : δ), ¬f a = some b<GOAL>∀ (x : β), f x✝ = some x → ¬(if x = b then some c else none) = some a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι → Set α<VAR>h : ¬∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ t ≤ f i, t ≤ f j → t ≤ ⊥<GOAL>∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι → Set α<VAR>h : ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : x ≠ x_1), ∃ x_2, ∃ (_ : x_2 ≤ f x) (_ : x_2 ≤ f x_1), ¬x_2 ≤ ⊥<GOAL>∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t✝ : Set ι'<VAR>f : ι → Set α<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>h_ne : i ≠ j<VAR>t : Set α<VAR>hfi : t ≤ f i<VAR>hfj : t ≤ f j<VAR>ht : ¬t ≤ ⊥<GOAL>∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t✝ : Set ι'<VAR>f : ι → Set α<VAR>i : ι<VAR>hi : i ∈ s<VAR>j : ι<VAR>hj : j ∈ s<VAR>h_ne : i ≠ j<VAR>t : Set α<VAR>hfi : t ≤ f i<VAR>hfj : t ≤ f j<VAR>ht : t.Nonempty<GOAL>∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<GOAL>IsIntegrallyClosed A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>x : FractionRing A<VAR>hx : IsIntegral A x<GOAL>∃ y, (algebraMap A (FractionRing A)) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>x : FractionRing A<VAR>hx : IsIntegral A x<GOAL>x ∈ ↑(adjoinIntegral A⁰ x hx)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>h : IsDedekindDomainInv A<VAR>x : FractionRing A<VAR>hx : IsIntegral A x<GOAL>adjoinIntegral A⁰ x hx ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<GOAL>CotangentSpace.map f - CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<GOAL>∀ (i : P.vars), (CotangentSpace.map f - CotangentSpace.map g) (P.cotangentSpaceBasis i) = (↑S P'.cotangentComplex ∘ₗ f.sub g) (P.cotangentSpaceBasis i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>i : P.vars<GOAL>(CotangentSpace.map f - CotangentSpace.map g) (P.cotangentSpaceBasis i) = (↑S P'.cotangentComplex ∘ₗ f.sub g) (P.cotangentSpaceBasis i)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace V<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : TopologicalAddGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : SeparatingDual R V<VAR>W : Type u_3<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module R W<VAR>inst✝ : FiniteDimensional R W<VAR>f : W →ₗ[R] V<VAR>hf : Injective ⇑f<GOAL>Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace V<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : TopologicalAddGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : SeparatingDual R V<VAR>W : Type u_3<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module R W<VAR>inst✝ : FiniteDimensional R W<VAR>f : W →ₗ[R] V<VAR>hf : Injective ⇑f<VAR>this : Injective (⇑(ContinuousLinearMap.coeLM R).flip ∘ ⇑f)<GOAL>Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>inst✝¹⁰ : Field R<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : TopologicalSpace R<VAR>inst✝⁷ : TopologicalSpace V<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : TopologicalAddGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : SeparatingDual R V<VAR>W : Type u_3<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module R W<VAR>inst✝ : FiniteDimensional R W<VAR>f : W →ₗ[R] V<VAR>hf : Injective ⇑f<VAR>this : Injective ⇑((ContinuousLinearMap.coeLM R).flip ∘ₗ f)<GOAL>Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<GOAL>IsCompactElement F⟮x⟯
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<GOAL>∀ (s : Set (IntermediateField F E)), s.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) s → x ∈ ⨆ a, ↑a → ∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<VAR>s : Set (IntermediateField F E)<VAR>hne : s.Nonempty<VAR>hs : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hx : x ∈ ⨆ a, ↑a<GOAL>∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α x : E<VAR>s : Set (IntermediateField F E)<VAR>hne : s.Nonempty<VAR>hs : DirectedOn (fun x x_1 => x ≤ x_1) s<VAR>hx : x ∈ ⨆ a, ↑a<VAR>this : Nonempty ↑s<GOAL>∃ x_1, ∃ (_ : x_1 ∈ s), x ∈ x_1
<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✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<GOAL>sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊
<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✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊<GOAL>sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊
<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✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊<GOAL>‖f‖₊ ≤ sSup ((fun x => ‖f x‖₊) '' closedBall 0 1)
<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✝²⁴ : SeminormedAddCommGroup E✝<VAR>inst✝²³ : SeminormedAddCommGroup Eₗ<VAR>inst✝²² : SeminormedAddCommGroup F✝<VAR>inst✝²¹ : SeminormedAddCommGroup Fₗ<VAR>inst✝²⁰ : SeminormedAddCommGroup G<VAR>inst✝¹⁹ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜✝<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜₂✝<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜₃<VAR>inst✝¹⁵ : NormedSpace 𝕜✝ E✝<VAR>inst✝¹⁴ : NormedSpace 𝕜✝ Eₗ<VAR>inst✝¹³ : NormedSpace 𝕜₂✝ F✝<VAR>inst✝¹² : NormedSpace 𝕜✝ Fₗ<VAR>inst✝¹¹ : NormedSpace 𝕜₃ G<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ Gₗ<VAR>σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝<VAR>σ₂₃ : 𝕜₂✝ →+* 𝕜₃<VAR>σ₁₃ : 𝕜✝ →+* 𝕜₃<VAR>inst✝⁹ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃<VAR>inst✝⁸ : FunLike 𝓕 E✝ F✝<VAR>inst✝⁷ : RingHomIsometric σ₁₂✝<VAR>𝕜 : Type u_11<VAR>𝕜₂ : Type u_12<VAR>E : Type u_13<VAR>F : Type u_14<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : DenselyNormedField 𝕜<VAR>inst✝³ : NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜₂ F<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊<GOAL>sSup ((fun x => ‖f x‖₊) '' ball 0 1) ≤ sSup ((fun x => ‖f x‖₊) '' closedBall 0 1)
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₁.LeftHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<GOAL>φ.τ₁ ≫ (ofEpiOfIsIsoOfMono φ h).f' = h.f'
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>d : D<GOAL>L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d) = ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>F : Type u₄<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : Category.{v₄, u₄} F<VAR>G : C ⥤ E<VAR>H : D ⥤ F<VAR>L₁ : C ⥤ D<VAR>R₁ : D ⥤ C<VAR>L₂ : E ⥤ F<VAR>R₂ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : R₁ ⋙ G ⟶ H ⋙ R₂<VAR>d : D<GOAL>L₂.map (((mateEquiv adj₁ adj₂).toFun ((mateEquiv adj₁ adj₂).invFun α)).app d) ≫ adj₂.counit.app (H.obj d) = ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝¹ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f✝ : X → (i : ι) → π i<VAR>inst✝ : DecidableEq ι<VAR>l : Filter Y<VAR>f : Y → (i : ι) → π i<VAR>x : (i : ι) → π i<VAR>hf : Tendsto f l (𝓝 x)<VAR>i : ι<VAR>g : Y → π i<VAR>xi : π i<VAR>hg : Tendsto g l (𝓝 xi)<VAR>j : ι<GOAL>Tendsto (fun i_1 => Function.update (f i_1) i (g i_1) j) l (𝓝 (Function.update x i xi j))
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>padicValNat p p = 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>(multiplicity p p).get ⋯ = 1
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : MulPosReflectLT α<VAR>b0 : 0 < b<GOAL>a * b < b ↔ a * b < 1 * b
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>pn : (ι →₀ R) ⊗[R] N<VAR>i : ι<GOAL>((finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((rTensor N (Finsupp.lapply i)) pn)
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>hb : head s₁ = head s₂<VAR>ht : last s₁ = last s₂<GOAL>¬0 < s₂.length → ¬0 < s₁.length
<VAR>α : Type u<VAR>inst✝ : CanonicallyLinearOrderedCommMonoid α<VAR>a b c : α<GOAL>min (a * b) c = min (min a c * min b c) c
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>A : Matrix n n α<VAR>B : Matrix n m α<VAR>inst✝ : Invertible A<GOAL>⅟A * (A * B) = B
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsCyclotomicExtension {n} A B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : NeZero ↑↑n<GOAL>(aeval (zeta n A B)) (cyclotomic (↑n) A) = 0
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsCyclotomicExtension {n} A B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : NeZero ↑↑n<GOAL>IsPrimitiveRoot (zeta n A B) ↑n
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u_2<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<GOAL>Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u_2<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : ℵ₀ ≤ Module.rank K V<VAR>ι : Type u_2<VAR>b : Basis ι K V<GOAL>Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u_2<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_2<VAR>h : Infinite ι<VAR>b : Basis ι K V<GOAL>Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u_2<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_2<VAR>h : Infinite ι<VAR>b : Basis ι K V<VAR>e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ<GOAL>Module.rank Kᵐᵒᵖ (V →ₗ[K] K) = #(V →ₗ[K] K)
<VAR>K R : Type u<VAR>V✝ V₁ V₂ V₃ : Type v<VAR>V' V'₁ : Type v'<VAR>V'' : Type v''<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝² : DivisionRing K<VAR>V : Type u_2<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>ι : Type u_2<VAR>h : Infinite ι<VAR>b : Basis ι K V<VAR>e : (V →ₗ[K] K) ≃ₗ[Kᵐᵒᵖ] ι → Kᵐᵒᵖ<GOAL>Module.rank Kᵐᵒᵖ (ι → Kᵐᵒᵖ) = #(ι → Kᵐᵒᵖ)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : α → β<VAR>ι : Sort u_2<VAR>tα : TopologicalSpace α<VAR>tβ : TopologicalSpace β<VAR>f : β → α<GOAL>tβ = induced f tα ↔ ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>spectralRadius ℂ a = ↑‖a‖₊
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)<GOAL>spectralRadius ℂ a = ↑‖a‖₊
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)<GOAL>Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)<GOAL>(fun _n => ↑‖a‖₊) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)<VAR>n : ℕ<GOAL>↑‖a‖₊ = ((fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n) n
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<VAR>hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)<VAR>n : ℕ<GOAL>↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>x : L<GOAL>x ∈ K ⊓ K' ↔ x ∈ K ∧ x ∈ K'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : CompleteLattice α<VAR>f✝ g s✝ t : ι → α<VAR>a b : α<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<VAR>s : Set α<GOAL>f (sInf s) = sInf (⇑f.symm ⁻¹' s)