ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>h : Int.fract v ≠ 0<VAR>n : ℕ<GOAL>GenContFract.IntFractPair.stream v (n + 1) = GenContFract.IntFractPair.stream (Int.fract v)⁻¹ n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.IntFractPair.seq1 v).1 = GenContFract.IntFractPair.of v
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.of v).h = ↑(GenContFract.IntFractPair.seq1 v).1.b
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.of v).h = ↑⌊v⌋
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(GenContFract.IntFractPair.seq1 v).2.get? n = GenContFract.IntFractPair.stream v (n + 1)
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(GenContFract.of v).TerminatedAt n ↔ (GenContFract.IntFractPair.seq1 v).2.TerminatedAt n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(GenContFract.of v).TerminatedAt n ↔ GenContFract.IntFractPair.stream v (n + 1) = none
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>gp_n : GenContFract.Pair K<VAR>s_nth_eq : (GenContFract.of v).s.get? n = some gp_n<GOAL>∃ ifp, GenContFract.IntFractPair.stream v (n + 1) = some ifp ∧ ↑ifp.b = gp_n.b
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : GenContFract.IntFractPair K<VAR>stream_succ_nth_eq : GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n<GOAL>(GenContFract.of v).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_n : GenContFract.IntFractPair K<VAR>stream_nth_eq : GenContFract.IntFractPair.stream v n = some ifp_n<VAR>nth_fr_ne_zero : ifp_n.fr ≠ 0<GOAL>(GenContFract.of v).s.get? n = some { a := 1, b := ↑(GenContFract.IntFractPair.of ifp_n.fr⁻¹).b }
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.of v).s.get? 0 = (GenContFract.IntFractPair.stream v 1).bind (some ∘ fun p => { a := 1, b := ↑p.b })
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>h : Int.fract v ≠ 0<GOAL>(GenContFract.of v).s.head = some { a := 1, b := ↑⌊(Int.fract v)⁻¹⌋ }
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>a : ℤ<GOAL>(GenContFract.of ↑a).s = Stream'.Seq.nil
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(GenContFract.of v).s.get? (n + 1) = (GenContFract.of (Int.fract v)⁻¹).s.get? n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.of v).s.tail = (GenContFract.of (Int.fract v)⁻¹).s
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>n : ℕ<VAR>a : ℤ<GOAL>(GenContFract.of ↑a).convs' n = ↑a
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>(GenContFract.of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs' n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>gp ppred pred : GenContFract.Pair K<VAR>nth_s_eq : g.s.get? n = some gp<VAR>nth_contsAux_eq : g.contsAux n = ppred<VAR>succ_nth_contsAux_eq : g.contsAux (n + 1) = pred<GOAL>g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>gp ppred pred : GenContFract.Pair K<VAR>nth_s_eq : g.s.get? n = some gp<VAR>nth_contsAux_eq : g.contsAux n = ppred<VAR>succ_nth_contsAux_eq : g.contsAux (n + 1) = pred<GOAL>g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>gp ppred pred : GenContFract.Pair K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_conts_eq : g.conts n = ppred<VAR>succ_nth_conts_eq : g.conts (n + 1) = pred<GOAL>g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>ppredA predA : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_num_eq : g.nums n = ppredA<VAR>succ_nth_num_eq : g.nums (n + 1) = predA<GOAL>g.nums (n + 2) = gp.b * predA + gp.a * ppredA
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>ppredB predB : K<VAR>succ_nth_s_eq : g.s.get? (n + 1) = some gp<VAR>nth_den_eq : g.dens n = ppredB<VAR>succ_nth_den_eq : g.dens (n + 1) = predB<GOAL>g.dens (n + 2) = gp.b * predB + gp.a * ppredB
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.TerminatedAt m
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.contsAux (n + 2) = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_lt_m : n < m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.contsAux m = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>n : ℕ<VAR>DivisionRing K<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>terminatedAt_n : s.TerminatedAt n<GOAL>GenContFract.convs'Aux s (n + 1) = GenContFract.convs'Aux s n
<VAR>K : Type u_1<VAR>n m : ℕ<VAR>DivisionRing K<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : s.TerminatedAt n<GOAL>GenContFract.convs'Aux s m = GenContFract.convs'Aux s n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.conts m = g.conts n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.nums m = g.nums n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.dens m = g.dens n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.convs m = g.convs n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n m : ℕ<VAR>DivisionRing K<VAR>n_le_m : n ≤ m<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.convs' m = g.convs' n
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.partNums.get? n = none ↔ g.s.get? n = none
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<GOAL>g.partDens.get? n = none ↔ g.s.get? n = none
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<VAR>gp : GenContFract.Pair α<VAR>s_nth_eq : g.s.get? n = some gp<GOAL>g.partNums.get? n = some gp.a
<VAR>α : Type u_1<VAR>g : GenContFract α<VAR>n : ℕ<VAR>gp : GenContFract.Pair α<VAR>s_nth_eq : g.s.get? n = some gp<GOAL>g.partDens.get? n = some gp.b
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<GOAL>g.conts n = g.contsAux (n + 1)
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<GOAL>g.nums n = (g.conts n).a
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<GOAL>g.dens n = (g.conts n).b
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<GOAL>g.convs n = g.nums n / g.dens n
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<GOAL>g.convs n = (g.conts n).a / (g.conts n).b
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>A : K<VAR>nth_num_eq : g.nums n = A<GOAL>∃ conts, g.conts n = conts ∧ conts.a = A
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>n : ℕ<VAR>DivisionRing K<VAR>B : K<VAR>nth_denom_eq : g.dens n = B<GOAL>∃ conts, g.conts n = conts ∧ conts.b = B
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.contsAux 0 = { a := 1, b := 0 }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.contsAux 1 = { a := g.h, b := 1 }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.conts 0 = { a := g.h, b := 1 }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.nums 0 = g.h
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.dens 0 = 1
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.convs 0 = g.h
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.contsAux 2 = { a := gp.b * g.h + gp.a, b := gp.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.nums 1 = gp.b * g.h + gp.a
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<VAR>gp : GenContFract.Pair K<VAR>zeroth_s_eq : g.s.get? 0 = some gp<GOAL>g.dens 1 = gp.b
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>s : Stream'.Seq (GenContFract.Pair K)<GOAL>GenContFract.convs'Aux s 0 = 0
<VAR>K : Type u_1<VAR>g : GenContFract K<VAR>DivisionRing K<GOAL>g.convs' 0 = g.h
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>h : s.head = none<VAR>n : ℕ<GOAL>GenContFract.convs'Aux s (n + 1) = 0
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>s : Stream'.Seq (GenContFract.Pair K)<VAR>p : GenContFract.Pair K<VAR>h : s.head = some p<VAR>n : ℕ<GOAL>GenContFract.convs'Aux s (n + 1) = p.a / (p.b + GenContFract.convs'Aux s.tail n)
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>self : DirectSum.Decomposition ℳ<GOAL>Function.LeftInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>self : DirectSum.Decomposition ℳ<GOAL>Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<GOAL>DirectSum.IsInternal ℳ
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>p : M → Prop<VAR>h_zero : p 0<VAR>h_homogeneous : ∀ {i : ι} (m : ↥(ℳ i)), p ↑m<VAR>h_add : ∀ (m m' : M), p m → p m' → p (m + m')<VAR>m : M<GOAL>p m
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<GOAL>DirectSum.Decomposition.decompose' = ⇑(DirectSum.decompose ℳ)
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>i : ι<VAR>x : ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ).symm ((DirectSum.of (fun i => ↥(ℳ i)) i) x) = ↑x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>i : ι<VAR>x : ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ) ↑x = (DirectSum.of (fun i => ↥(ℳ i)) i) x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : M<VAR>i : ι<VAR>hx : x ∈ ℳ i<GOAL>(DirectSum.decompose ℳ) x = (DirectSum.of (fun i => ↥(ℳ i)) i) ⟨x, hx⟩
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : M<VAR>i : ι<VAR>hx : x ∈ ℳ i<GOAL>↑(((DirectSum.decompose ℳ) x) i) = x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : M<VAR>i j : ι<VAR>hx : x ∈ ℳ i<VAR>hij : i ≠ j<GOAL>↑(((DirectSum.decompose ℳ) x) j) = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : M<VAR>i j : ι<VAR>hxi : x ∈ ℳ i<VAR>hxj : x ∈ ℳ j<VAR>hx : x ≠ 0<GOAL>i = j
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>a : M<GOAL>(DirectSum.decomposeAddEquiv ℳ) a = (DirectSum.decompose ℳ) a
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>a : ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decomposeAddEquiv ℳ).symm a = (DirectSum.decompose ℳ).symm a
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<GOAL>(DirectSum.decompose ℳ) 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<GOAL>(DirectSum.decompose ℳ).symm 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x y : M<GOAL>(DirectSum.decompose ℳ) (x + y) = (DirectSum.decompose ℳ) x + (DirectSum.decompose ℳ) y
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x y : ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ).symm (x + y) = (DirectSum.decompose ℳ).symm x + (DirectSum.decompose ℳ).symm y
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>ι' : Type u_5<VAR>s : Finset ι'<VAR>f : ι' → M<GOAL>(DirectSum.decompose ℳ) (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ) (f i)
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>ι' : Type u_5<VAR>s : Finset ι'<VAR>f : ι' → ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ).symm (∑ i ∈ s, f i) = ∑ i ∈ s, (DirectSum.decompose ℳ).symm (f i)
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>SetLike σ M<VAR>AddSubmonoidClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>(i : ι) → (x : ↥(ℳ i)) → Decidable (x ≠ 0)<VAR>r : M<GOAL>∑ i ∈ DFinsupp.support ((DirectSum.decompose ℳ) r), ↑(((DirectSum.decompose ℳ) r) i) = r
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommGroup M<VAR>SetLike σ M<VAR>AddSubgroupClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : M<GOAL>(DirectSum.decompose ℳ) (-x) = -(DirectSum.decompose ℳ) x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommGroup M<VAR>SetLike σ M<VAR>AddSubgroupClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x : ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ).symm (-x) = -(DirectSum.decompose ℳ).symm x
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommGroup M<VAR>SetLike σ M<VAR>AddSubgroupClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x y : M<GOAL>(DirectSum.decompose ℳ) (x - y) = (DirectSum.decompose ℳ) x - (DirectSum.decompose ℳ) y
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddCommGroup M<VAR>SetLike σ M<VAR>AddSubgroupClass σ M<VAR>ℳ : ι → σ<VAR>DirectSum.Decomposition ℳ<VAR>x y : ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decompose ℳ).symm (x - y) = (DirectSum.decompose ℳ).symm x - (DirectSum.decompose ℳ).symm y
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ℳ : ι → Submodule R M<VAR>DirectSum.Decomposition ℳ<VAR>m : M<GOAL>(DirectSum.decomposeLinearEquiv ℳ) m = (DirectSum.decompose ℳ) m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ℳ : ι → Submodule R M<VAR>DirectSum.Decomposition ℳ<VAR>m : ⨁ (i : ι), ↥(ℳ i)<GOAL>(DirectSum.decomposeLinearEquiv ℳ).symm m = (DirectSum.decompose ℳ).symm m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ℳ : ι → Submodule R M<VAR>DirectSum.Decomposition ℳ<VAR>r : R<VAR>x : M<GOAL>(DirectSum.decompose ℳ) (r • x) = r • (DirectSum.decompose ℳ) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ℳ : ι → Submodule R M<VAR>DirectSum.Decomposition ℳ<VAR>i : ι<GOAL>↑(DirectSum.decomposeLinearEquiv ℳ).symm ∘ₗ DirectSum.lof R ι (fun x => ↥(ℳ x)) i = (ℳ i).subtype
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ℳ : ι → Submodule R M<VAR>DirectSum.Decomposition ℳ<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module R N<VAR>f g : M →ₗ[R] N<VAR>h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype<GOAL>f = g
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ conts, (GenContFract.of v).contsAux n = GenContFract.Pair.map Rat.cast conts
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ conts, (GenContFract.of v).conts n = GenContFract.Pair.map Rat.cast conts
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (GenContFract.of v).nums n = ↑q
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (GenContFract.of v).dens n = ↑q
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ q, (GenContFract.of v).convs n = ↑q
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>terminates : (GenContFract.of v).Terminates<GOAL>∃ q, v = ↑q
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>GenContFract.IntFractPair.mapFr Rat.cast (GenContFract.IntFractPair.of q) = GenContFract.IntFractPair.of v
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (GenContFract.IntFractPair.mapFr Rat.cast) (GenContFract.IntFractPair.stream q n) = GenContFract.IntFractPair.stream v n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>Stream'.map (Option.map (GenContFract.IntFractPair.mapFr Rat.cast)) (GenContFract.IntFractPair.stream q) = GenContFract.IntFractPair.stream v
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>↑(GenContFract.of q).h = (GenContFract.of v).h
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<VAR>n : ℕ<GOAL>Option.map (GenContFract.Pair.map Rat.cast) ((GenContFract.of q).s.get? n) = (GenContFract.of v).s.get? n
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>Stream'.Seq.map (GenContFract.Pair.map Rat.cast) (GenContFract.of q).s = (GenContFract.of v).s
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>{ h := ↑(GenContFract.of q).h, s := Stream'.Seq.map (GenContFract.Pair.map Rat.cast) (GenContFract.of q).s } = GenContFract.of v
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<VAR>q : ℚ<VAR>v_eq_q : v = ↑q<GOAL>(GenContFract.of v).Terminates ↔ (GenContFract.of q).Terminates
<VAR>q : ℚ<VAR>q_pos : 0 < q<GOAL>(GenContFract.IntFractPair.of q⁻¹).fr.num < q.num
<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : GenContFract.IntFractPair ℚ<VAR>stream_nth_eq : GenContFract.IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : GenContFract.IntFractPair.stream q (n + 1) = some ifp_succ_n<GOAL>ifp_succ_n.fr.num < ifp_n.fr.num
<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n : GenContFract.IntFractPair ℚ<GOAL>GenContFract.IntFractPair.stream q n = some ifp_n → ifp_n.fr.num ≤ (GenContFract.IntFractPair.of q).fr.num - ↑n
<VAR>q : ℚ<GOAL>∃ n, GenContFract.IntFractPair.stream q n = none
<VAR>q : ℚ<GOAL>(GenContFract.of q).Terminates
<VAR>K : Type u_1<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>v : K<GOAL>(GenContFract.of v).Terminates ↔ ∃ q, v = ↑q
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<GOAL>(GenContFract.of v).convs = (GenContFract.of v).convs'
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>n : ℕ<GOAL>(GenContFract.of v).convs (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs n
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>Archimedean K<VAR>ε : K<GOAL>ε > 0 → ∃ N, ∀ n ≥ N, |v - (GenContFract.of v).convs n| < ε
<VAR>K : Type u_1<VAR>v : K<VAR>LinearOrderedField K<VAR>FloorRing K<VAR>Archimedean K<VAR>TopologicalSpace K<VAR>OrderTopology K<GOAL>Filter.Tendsto (GenContFract.of v).convs Filter.atTop (𝓝 v)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Add M<VAR>S : ι → AddSubsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Add M<VAR>S : ι → AddSubsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>M : Type u_2<VAR>Add M<VAR>S : Set (AddSubsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>M : Type u_2<VAR>Mul M<VAR>S : Set (Subsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>M : Type u_2<VAR>Add M<VAR>S : Set (AddSubsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>M : Type u_2<VAR>Mul M<VAR>S : Set (Subsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>M : Type u_2<VAR>Add M<VAR>S T : AddSubsemigroup M<VAR>x : M<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>M : Type u_2<VAR>Mul M<VAR>S T : Subsemigroup M<VAR>x : M<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>M : Type u_2<VAR>Mul M<VAR>S T : Subsemigroup M<VAR>x : M<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>M : Type u_2<VAR>Add M<VAR>S T : AddSubsemigroup M<VAR>x : M<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>M : Type u_2<VAR>Mul M<VAR>S T : Subsemigroup M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x * y ∈ S ⊔ T
<VAR>M : Type u_2<VAR>Add M<VAR>S T : AddSubsemigroup M<VAR>x y : M<VAR>hx : x ∈ S<VAR>hy : y ∈ T<GOAL>x + y ∈ S ⊔ T
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Mul M<VAR>S : ι → Subsemigroup M<VAR>i : ι<VAR>x : M<GOAL>x ∈ S i → x ∈ iSup S
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Add M<VAR>S : ι → AddSubsemigroup M<VAR>i : ι<VAR>x : M<GOAL>x ∈ S i → x ∈ iSup S
<VAR>M : Type u_2<VAR>Mul M<VAR>S : Set (Subsemigroup M)<VAR>s : Subsemigroup M<VAR>hs : s ∈ S<VAR>x : M<GOAL>x ∈ s → x ∈ sSup S
<VAR>M : Type u_2<VAR>Add M<VAR>S : Set (AddSubsemigroup M)<VAR>s : AddSubsemigroup M<VAR>hs : s ∈ S<VAR>x : M<GOAL>x ∈ s → x ∈ sSup S
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Mul M<VAR>S : ι → Subsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x₁
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Add M<VAR>S : ι → AddSubsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C x₁
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>Mul M<VAR>S : ι → Subsemigroup M<VAR>C : (x : M) → x ∈ ⨆ i, S i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯<VAR>mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<GOAL>C x₁ hx₁