ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<GOAL>|v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<GOAL>|v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<GOAL>|v - g.convs n| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<GOAL>|v - g.convs n| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<GOAL>|v - g.convs n| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<GOAL>|v - g.convs n| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<GOAL>|(-1) ^ n / den'| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<VAR>nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b<GOAL>|(-1) ^ n / den'| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<VAR>nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b<VAR>conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b<GOAL>|(-1) ^ n / den'| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<VAR>nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b<VAR>conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b<VAR>zero_lt_conts_b : 0 < conts.b<GOAL>|(-1) ^ n / den'| ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<VAR>nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b<VAR>conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b<VAR>zero_lt_conts_b : 0 < conts.b<GOAL>1 / den' ≤ 1 / den
<VAR>K : Type u_1<VAR>v : K<VAR>n : ℕ<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>not_terminatedAt_n : ¬(of v).TerminatedAt n<VAR>g : GenContFract K := of v<VAR>nextConts : Pair K := g.contsAux (n + 2)<VAR>conts : Pair K := g.contsAux (n + 1)<VAR>conts_eq : conts = g.contsAux (n + 1)<VAR>pred_conts : Pair K := g.contsAux n<VAR>pred_conts_eq : pred_conts = g.contsAux n<VAR>gp : Pair K<VAR>s_nth_eq : g.s.get? n = some gp<VAR>gp_a_eq_one : gp.a = 1<VAR>nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b<VAR>den : K := conts.b * (pred_conts.b + gp.b * conts.b)<VAR>ifp_succ_n : IntFractPair K<VAR>succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>ifp_succ_n_b_eq_gp_b : ↑ifp_succ_n.b = gp.b<VAR>ifp_n : IntFractPair K<VAR>stream_nth_eq : IntFractPair.stream v n = some ifp_n<VAR>stream_nth_fr_ne_zero : ifp_n.fr ≠ 0<VAR>if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)<VAR>nextConts_b_ineq : ↑(fib (n + 2)) ≤ pred_conts.b + gp.b * conts.b<VAR>conts_b_ineq : ↑(fib (n + 1)) ≤ conts.b<VAR>zero_lt_conts_b : 0 < conts.b<GOAL>0 < den ∧ den ≤ den'
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n e1 e2 t1 t2 : α<VAR>h1 : n * e1 = t1<VAR>h2 : n * e2 = t2<GOAL>n * (e1 - e2) = t1 - t2
<VAR>z : ℂ<GOAL>abs (cexp z) = Real.exp z.re
<VAR>α✝ : Type u_1<VAR>α' : Type u_2<VAR>β✝ : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>ι : Type u_14<VAR>α : ι → Type u_15<VAR>β : ι → Type u_16<VAR>γ : ι → Type u_17<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → DecidableEq (γ i)<VAR>f : (i : ι) → α i → β i → γ i<VAR>s : (i : ι) → Finset (α i)<VAR>t : (i : ι) → Finset (β i)<VAR>a✝ : (a : ι) → γ a<GOAL>(a✝ ∈ piFinset fun i => image₂ (f i) (s i) (t i)) ↔ a✝ ∈ image₂ (fun a b i => f i (a i) (b i)) (piFinset s) (piFinset t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulZeroOneClass α<VAR>inst✝² : MulZeroOneClass β<VAR>inst✝¹ : MulZeroOneClass γ<VAR>inst✝ : MulZeroOneClass δ<VAR>f✝ g✝ f g : α →*₀o β<VAR>h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom<GOAL>∀ (a : α), f a = g a
<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 : G → E<VAR>s : Set G<VAR>x : G<GOAL>DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s 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 : G → E<VAR>s : Set G<VAR>x : G<VAR>H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x<GOAL>DifferentiableWithinAt 𝕜 f s 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 : G → E<VAR>s : Set G<VAR>x : G<VAR>H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x<VAR>this : DifferentiableWithinAt 𝕜 (⇑iso.symm ∘ ⇑iso ∘ f) s x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>(a ::ₘ ⟦l⟧).antidiagonal = map (Prod.map id (cons a)) (antidiagonal ⟦l⟧) + map (Prod.map (cons a) id) (antidiagonal ⟦l⟧)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>(powersetAux' l ++ List.map (cons a) (powersetAux' l)).zip ((List.map (cons a) (powersetAux' l)).reverse ++ (powersetAux' l).reverse) ~ List.map (fun x => Prod.map id (cons a) x) ((powersetAux' l).zip (powersetAux' l).reverse) ++ List.map (fun x => Prod.map (cons a) id x) ((powersetAux' l).zip (powersetAux' l).reverse)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>(powersetAux' l).zip (List.map (cons a) (powersetAux' l)).reverse ++ (List.map (cons a) (powersetAux' l)).zip (powersetAux' l).reverse = (List.map id (powersetAux' l)).zip (List.map (cons a) (powersetAux' l).reverse) ++ (List.map (cons a) (powersetAux' l)).zip (List.map id (powersetAux' l).reverse)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>(powersetAux' l).length = (List.map (cons a) (powersetAux' l)).reverse.length
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.109587<VAR>inst✝ : MulAction R X<VAR>r₁ r₂ : R<VAR>s t : ↥S<GOAL>r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>inst✝ : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv = Scheme.Hom.app f U
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<GOAL>∃ i, ∀ j ≥ i, abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<GOAL>∃ i, ∀ j ≥ i, abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) i) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>hi₂ : |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>hi₂ : |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>sub_le : |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤ |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>hi₂ : |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>sub_le : |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤ |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|<VAR>this : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| + |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2 + ε / 2<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>hi₂ : |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>sub_le : |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤ |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|<VAR>this : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| + |(fun n => ∑ i ∈ range n, a i) i - ∑ k ∈ range (max n i), a k| < ε<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>hg : IsCauSeq abs fun n => ∑ i ∈ range n, a i<VAR>ε : α<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>j : ℕ<VAR>ji : j ≥ max n i<VAR>hi₁ : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>hi₂ : |(fun n => ∑ i ∈ range n, a i) (max n i) - (fun n => ∑ i ∈ range n, a i) i| < ε / 2<VAR>sub_le : |∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k| ≤ |∑ k ∈ range j, a k - ∑ k ∈ range i, a k| + |∑ k ∈ range i, a k - ∑ k ∈ range (max n i), a k|<VAR>this : |(fun n => ∑ i ∈ range n, a i) j - (fun n => ∑ i ∈ range n, a i) i| + |(fun n => ∑ i ∈ range n, a i) i - ∑ k ∈ range (max n i), a k| < ε<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) ≤ ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i j : ℕ<VAR>ji : j ≥ max n i<VAR>k : ℕ<VAR>hk : j - max n i = k<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) ≤ ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i j : ℕ<VAR>ji : j ≥ max n i<VAR>k : ℕ<VAR>hk : j = k + max n i<GOAL>abv ((fun n => ∑ i ∈ range n, f i) j - (fun n => ∑ i ∈ range n, f i) (max n i)) ≤ ∑ k ∈ range j, a k - ∑ k ∈ range (max n i), a k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a : ℕ → α<VAR>n : ℕ<VAR>hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m<VAR>i k' : ℕ<VAR>hi : abv (∑ i ∈ range (k' + max n i), f i - ∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + max n i), a k - ∑ k ∈ range (max n i), a k<GOAL>abv (∑ i ∈ range (k' + 1 + max n i), f i - ∑ i ∈ range (max n i), f i) ≤ ∑ k ∈ range (k' + 1 + max n i), a k - ∑ k ∈ range (max n i), a k