ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<GOAL>|rexp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)
<GOAL>|rexp 1 - expNear 13 1 ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 - 1) * 10 - 1) * 11 - 1) * 12 - 1) * 13)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
<GOAL>|rexp 1 - expNear 13 1 (5 / 7)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (243243 / 390625)
<GOAL>|1 - 5 / 7| ≤ 243243 / 390625 - |1| / 14 * ((14 + 1) / 14)
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>a ⨳ 0 = 0
<VAR>a✝ b c d : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>∀ a' < a, ∀ b' < 0, a' ⨳ 0 ♯ a ⨳ b' < 0 ♯ a' ⨳ b'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>a✝ a : α<VAR>ha : a ≠ 0<VAR>x y : β<VAR>h : a⁻¹ • x = y<GOAL>x = a • y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : MulAction α β<VAR>a✝ a : α<VAR>ha : a ≠ 0<VAR>x y : β<VAR>h : x = a • y<GOAL>a⁻¹ • x = y
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<GOAL>HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) x<GOAL>HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<GOAL>HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<VAR>A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm<GOAL>HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<VAR>A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm<VAR>B : f' = (f'.comp ↑iso).comp ↑iso.symm<GOAL>HasFDerivWithinAt f f' s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<VAR>A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm<VAR>B : f' = (f'.comp ↑iso).comp ↑iso.symm<GOAL>HasFDerivWithinAt ((f ∘ ⇑iso) ∘ ⇑iso.symm) ((f'.comp ↑iso).comp ↑iso.symm) s (iso x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<VAR>A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm<VAR>B : f' = (f'.comp ↑iso).comp ↑iso.symm<GOAL>MapsTo (⇑iso.symm) s (⇑iso ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s✝ t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>s : Set F<VAR>x : E<VAR>f' : F →L[𝕜] G<VAR>H : HasFDerivWithinAt (f ∘ ⇑iso) (f'.comp ↑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))<VAR>A : f = (f ∘ ⇑iso) ∘ ⇑iso.symm<VAR>B : f' = (f'.comp ↑iso).comp ↑iso.symm<VAR>y : F<VAR>hy : y ∈ s<GOAL>iso.symm y ∈ ⇑iso ⁻¹' s
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<GOAL>u.r - 1 < u.bp
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<VAR>h₀ : u.r - 1 + 1 = u.r<GOAL>u.r - 1 < u.bp
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<VAR>h₀ : u.r - 1 + 1 = u.r<VAR>h₁ : u.r < u.bp + 1<GOAL>u.r - 1 < u.bp
<VAR>u : XgcdType<VAR>hr : u.r ≠ 0<VAR>h₀ : u.r - 1 + 1 = u.r<VAR>h₁ : u.r - 1 + 1 < u.bp + 1<GOAL>u.r - 1 < u.bp
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>IsBounded sᶜ ↔ IsCobounded s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>f✝ g✝ : α → ℝ<VAR>s✝ : Set α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>f_mble : AEMeasurable f μ<VAR>g_mble : AEMeasurable g μ<VAR>s : Set α<VAR>s_mble : NullMeasurableSet s μ<GOAL>NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)} (μ.prod volume)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace α✝<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : LinearOrder α✝<VAR>inst✝⁷ : LinearOrder β<VAR>inst✝⁶ : OrderTopology α✝<VAR>inst✝⁵ : OrderTopology β<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace α✝<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : LinearOrder α✝<VAR>inst✝⁷ : LinearOrder β<VAR>inst✝⁶ : OrderTopology α✝<VAR>inst✝⁵ : OrderTopology β<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<VAR>hx : x ∉ Ioo y x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace α✝<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : LinearOrder α✝<VAR>inst✝⁷ : LinearOrder β<VAR>inst✝⁶ : OrderTopology α✝<VAR>inst✝⁵ : OrderTopology β<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<VAR>hx : x ∉ Ioo y x<VAR>ht : (Ioo y x).Nonempty<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹⁰ : TopologicalSpace α✝<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : LinearOrder α✝<VAR>inst✝⁷ : LinearOrder β<VAR>inst✝⁶ : OrderTopology α✝<VAR>inst✝⁵ : OrderTopology β<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : FirstCountableTopology α<VAR>x y : α<VAR>hy : y < x<VAR>hx : x ∉ Ioo y x<VAR>ht : (Ioo y x).Nonempty<VAR>u : ℕ → α<VAR>hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x<GOAL>∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : Countable ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → F<VAR>f_lim : α → F<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>eLpNorm f_lim ⊤ μ ≤ liminf (fun n => eLpNorm (f n) ⊤ μ) atTop
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : Countable ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → F<VAR>f_lim : α → F<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>essSup (fun x => liminf (fun m => ↑‖f m x‖₊) atTop) μ ≤ liminf (fun n => eLpNorm (f n) ⊤ μ) atTop
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedAddCommGroup G<VAR>ι : Type u_5<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : Countable ι<VAR>inst✝ : LinearOrder ι<VAR>f : ι → α → F<VAR>f_lim : α → F<VAR>h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))<GOAL>essSup (fun x => liminf (fun m => ↑‖f m x‖₊) atTop) μ ≤ liminf (fun n => essSup (fun x => ↑‖f n x‖₊) μ) atTop
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁵ inst✝⁴ : Group α<VAR>inst✝³ : MulAction α β<VAR>x : β<VAR>inst✝² : Fintype α<VAR>inst✝¹ : (a : α) → Fintype ↑(fixedBy β a)<VAR>inst✝ : Fintype (Quotient (orbitRel α β))<GOAL>∑ a : α, Fintype.card ↑(fixedBy β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>(σ • w).IsComplex ↔ w.IsComplex
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>Function.Surjective ⇑(trace K L)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>range (trace K L) = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>¬range (trace K L) = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : CommRing T<VAR>inst✝¹² : Algebra R S<VAR>inst✝¹¹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : Field L<VAR>inst✝⁸ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁷ : Fintype ι<VAR>F : Type u_6<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra R L<VAR>inst✝⁴ : Algebra L F<VAR>inst✝³ : Algebra R F<VAR>inst✝² : IsScalarTower R L F<VAR>pb : PowerBasis K L<VAR>inst✝¹ : FiniteDimensional K L<VAR>inst✝ : Algebra.IsSeparable K L<GOAL>¬trace K L = 0
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f g : R[X] →+* S<VAR>h₁ : ∀ (a : R), f (C a) = g (C a)<VAR>h₂ : f X = g X<VAR>f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom<VAR>hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom<VAR>g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom<VAR>hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom<VAR>A : f' = g'<GOAL>f = g
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f g : R[X] →+* S<VAR>h₁ : ∀ (a : R), f (C a) = g (C a)<VAR>h₂ : f X = g X<VAR>f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom<VAR>hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom<VAR>g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom<VAR>hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom<VAR>A : f' = g'<VAR>B : f = f'.comp ↑(toFinsuppIso R)<GOAL>f = g
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Semiring S<VAR>f g : R[X] →+* S<VAR>h₁ : ∀ (a : R), f (C a) = g (C a)<VAR>h₂ : f X = g X<VAR>f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom<VAR>hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom<VAR>g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom<VAR>hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom<VAR>A : f' = g'<VAR>B : f = f'.comp ↑(toFinsuppIso R)<VAR>C' : g = g'.comp ↑(toFinsuppIso R)<GOAL>f = g
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.OfLocalizationSpan @RingHom.Finite
<VAR>R S : Type u<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>M : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝³ : CommRing R'<VAR>inst✝² : CommRing S'<VAR>f : R →+* S<VAR>inst✝¹ : Algebra R R'<VAR>inst✝ : Algebra S S'<GOAL>RingHom.OfLocalizationFiniteSpan @RingHom.Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).Finite<VAR>this✝ : Algebra R S := f.toAlgebra<VAR>this : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<GOAL>f.Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).Finite<VAR>this✝¹ : Algebra R S := f.toAlgebra<VAR>this✝ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<GOAL>f.Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).Finite<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<GOAL>f.Finite
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).Finite<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<GOAL>⊤.FG
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>H : ∀ (r : { x // x ∈ s }), ⊤.FG<GOAL>⊤.FG
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>⊤.FG
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>Submodule.span R ↑(s.attach.biUnion sf) = ⊤
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<GOAL>⊤ ≤ ⨆ x, Submodule.span R ↑(sf x)