bump to nightly-2023-03-30-02

mathlib commit leanprover-community/mathlib@b685f50

Mathbin/Algebra/ContinuedFractions/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.basic
-! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -60,6 +60,7 @@ protected structure GeneralizedContinuedFraction.Pair where
 
 open GeneralizedContinuedFraction
 
+/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
 /-! Interlude: define some expected coercions and instances. -/
 
 
@@ -114,7 +115,7 @@ For convenience, one often writes `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),
 -/
 structure GeneralizedContinuedFraction where
   h : α
-  s : SeqCat <| Pair α
+  s : Seq <| Pair α
 #align generalized_continued_fraction GeneralizedContinuedFraction
 
 variable {α}
@@ -123,19 +124,19 @@ namespace GeneralizedContinuedFraction
 
 /-- Constructs a generalized continued fraction without fractional part. -/
 def ofInteger (a : α) : GeneralizedContinuedFraction α :=
-  ⟨a, SeqCat.nil⟩
+  ⟨a, Seq.nil⟩
 #align generalized_continued_fraction.of_integer GeneralizedContinuedFraction.ofInteger
 
 instance [Inhabited α] : Inhabited (GeneralizedContinuedFraction α) :=
   ⟨ofInteger default⟩
 
 /-- Returns the sequence of partial numerators `aᵢ` of `g`. -/
-def partialNumerators (g : GeneralizedContinuedFraction α) : SeqCat α :=
+def partialNumerators (g : GeneralizedContinuedFraction α) : Seq α :=
   g.s.map Pair.a
 #align generalized_continued_fraction.partial_numerators GeneralizedContinuedFraction.partialNumerators
 
 /-- Returns the sequence of partial denominators `bᵢ` of `g`. -/
-def partialDenominators (g : GeneralizedContinuedFraction α) : SeqCat α :=
+def partialDenominators (g : GeneralizedContinuedFraction α) : Seq α :=
   g.s.map Pair.b
 #align generalized_continued_fraction.partial_denominators GeneralizedContinuedFraction.partialDenominators
 
@@ -167,13 +168,13 @@ variable {β : Type _} [Coe α β]
 /-- Coerce a gcf by elementwise coercion. -/
 instance hasCoeToGeneralizedContinuedFraction :
     Coe (GeneralizedContinuedFraction α) (GeneralizedContinuedFraction β) :=
-  ⟨fun g => ⟨(g.h : β), (g.s.map coe : SeqCat <| Pair β)⟩⟩
+  ⟨fun g => ⟨(g.h : β), (g.s.map coe : Seq <| Pair β)⟩⟩
 #align generalized_continued_fraction.has_coe_to_generalized_continued_fraction GeneralizedContinuedFraction.hasCoeToGeneralizedContinuedFraction
 
 @[simp, norm_cast]
 theorem coe_to_generalizedContinuedFraction {g : GeneralizedContinuedFraction α} :
     (↑(g : GeneralizedContinuedFraction α) : GeneralizedContinuedFraction β) =
-      ⟨(g.h : β), (g.s.map coe : SeqCat <| Pair β)⟩ :=
+      ⟨(g.h : β), (g.s.map coe : Seq <| Pair β)⟩ :=
   rfl
 #align generalized_continued_fraction.coe_to_generalized_continued_fraction GeneralizedContinuedFraction.coe_to_generalizedContinuedFraction
 
@@ -389,7 +390,7 @@ Returns the approximation of the fraction described by the given sequence up to
 For example, `convergents'_aux [(1, 2), (3, 4), (5, 6)] 2 = 1 / (2 + 3 / 4)` and
 `convergents'_aux [(1, 2), (3, 4), (5, 6)] 0 = 0`.
 -/
-def convergents'Aux : SeqCat (Pair K) → ℕ → K
+def convergents'Aux : Seq (Pair K) → ℕ → K
   | s, 0 => 0
   | s, n + 1 =>
     match s.headI with

Mathbin/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.approximations
-! leanprover-community/mathlib commit c85b4d15cfdac3abffce2f449e228a0cf0326912
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -324,9 +324,9 @@ theorem of_denom_mono : (of v).denominators n ≤ (of v).denominators (n + 1) :=
   by
   let g := of v
   cases' Decidable.em <| g.partial_denominators.terminated_at n with terminated not_terminated
-  · have : g.partial_denominators.nth n = none := by rwa [SeqCat.TerminatedAt] at terminated
+  · have : g.partial_denominators.nth n = none := by rwa [Stream'.Seq.TerminatedAt] at terminated
     have : g.terminated_at n :=
-      terminated_at_iff_part_denom_none.elim_right (by rwa [SeqCat.TerminatedAt] at terminated)
+      terminated_at_iff_part_denom_none.elim_right (by rwa [Stream'.Seq.TerminatedAt] at terminated)
     have : g.denominators (n + 1) = g.denominators n :=
       denominators_stable_of_terminated n.le_succ this
     rw [this]

Mathbin/Algebra/ContinuedFractions/Computation/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.basic
-! leanprover-community/mathlib commit 10d887272d1a72b99da88bcb301d1da9d9d33696
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -168,10 +168,11 @@ This is just an intermediate representation and users should not (need to) direc
 it. The setup of rewriting/simplification lemmas that make the definitions easy to use is done in
 `algebra.continued_fractions.computation.translations`.
 -/
-protected def seq1 (v : K) : Seq1 <| IntFractPair K :=
+protected def seq1 (v : K) : Stream'.Seq1 <| IntFractPair K :=
   ⟨IntFractPair.of v,--the head
-      SeqCat.tail-- take the tail of `int_fract_pair.stream` since the first element is already in the
-      -- head create a sequence from `int_fract_pair.stream`
+      Stream'.Seq.tail-- take the tail of `int_fract_pair.stream` since the first element is already in
+      -- the head
+      -- create a sequence from `int_fract_pair.stream`
       ⟨IntFractPair.stream v,-- the underlying stream
           @stream_isSeq
           _ _ _ v⟩⟩

Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.terminates_iff_rat
-! leanprover-community/mathlib commit 134625f523e737f650a6ea7f0c82a6177e45e622
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -36,6 +36,7 @@ rational, continued fraction, termination
 
 namespace GeneralizedContinuedFraction
 
+/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
 open GeneralizedContinuedFraction (of)
 
 variable {K : Type _} [LinearOrderedField K] [FloorRing K]
@@ -227,14 +228,14 @@ theorem coe_of_h_rat_eq : (↑((of q).h : ℚ) : K) = (of v).h :=
 theorem coe_of_s_nth_rat_eq :
     (((of q).s.get? n).map (Pair.map coe) : Option <| Pair K) = (of v).s.get? n :=
   by
-  simp only [of, int_fract_pair.seq1, SeqCat.map_nth, SeqCat.nth_tail]
-  simp only [SeqCat.nth]
+  simp only [of, int_fract_pair.seq1, seq.map_nth, seq.nth_tail]
+  simp only [seq.nth]
   rw [← int_fract_pair.coe_stream_rat_eq v_eq_q]
   rcases succ_nth_stream_eq : int_fract_pair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
     simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
 #align generalized_continued_fraction.coe_of_s_nth_rat_eq GeneralizedContinuedFraction.coe_of_s_nth_rat_eq
 
-theorem coe_of_s_rat_eq : ((of q).s.map (Pair.map coe) : SeqCat <| Pair K) = (of v).s :=
+theorem coe_of_s_rat_eq : ((of q).s.map (Pair.map coe) : Seq <| Pair K) = (of v).s :=
   by
   ext n
   rw [← coe_of_s_nth_rat_eq v_eq_q]
@@ -254,7 +255,7 @@ theorem coe_of_rat_eq :
 theorem of_terminates_iff_of_rat_terminates {v : K} {q : ℚ} (v_eq_q : v = (q : K)) :
     (of v).Terminates ↔ (of q).Terminates := by
   constructor <;> intro h <;> cases' h with n h <;> use n <;>
-        simp only [SeqCat.TerminatedAt, (coe_of_s_nth_rat_eq v_eq_q n).symm] at h⊢ <;>
+        simp only [seq.terminated_at, (coe_of_s_nth_rat_eq v_eq_q n).symm] at h⊢ <;>
       cases (of q).s.get? n <;>
     trivial
 #align generalized_continued_fraction.of_terminates_iff_of_rat_terminates GeneralizedContinuedFraction.of_terminates_iff_of_rat_terminates

Mathbin/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.computation.translations
-! leanprover-community/mathlib commit 10d887272d1a72b99da88bcb301d1da9d9d33696
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -47,6 +47,7 @@ namespace GeneralizedContinuedFraction
 
 open GeneralizedContinuedFraction (of)
 
+/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
 -- Fix a discrete linear ordered floor field and a value `v`.
 variable {K : Type _} [LinearOrderedField K] [FloorRing K] {v : K}
 
@@ -217,7 +218,7 @@ theorem of_terminatedAt_iff_intFractPair_seq1_terminatedAt :
 
 theorem of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none :
     (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none := by
-  rw [of_terminated_at_iff_int_fract_pair_seq1_terminated_at, SeqCat.TerminatedAt,
+  rw [of_terminated_at_iff_int_fract_pair_seq1_terminated_at, Stream'.Seq.TerminatedAt,
     int_fract_pair.nth_seq1_eq_succ_nth_stream]
 #align generalized_continued_fraction.of_terminated_at_n_iff_succ_nth_int_fract_pair_stream_eq_none GeneralizedContinuedFraction.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none
 
@@ -240,7 +241,7 @@ theorem IntFractPair.exists_succ_nth_stream_of_gcf_of_nth_eq_some {gp_n : Pair K
     ∃ ifp, int_fract_pair.stream v (n + 1) = some ifp ∧ pair.mk 1 (ifp.b : K) = gp_n :=
     by
     unfold of int_fract_pair.seq1 at s_nth_eq
-    rwa [SeqCat.map_tail, SeqCat.nth_tail, SeqCat.map_nth, Option.map_eq_some'] at s_nth_eq
+    rwa [seq.map_tail, seq.nth_tail, seq.map_nth, Option.map_eq_some'] at s_nth_eq
   cases gp_n_eq
   injection gp_n_eq with _ ifp_b_eq_gp_n_b
   exists ifp
@@ -255,8 +256,8 @@ theorem nth_of_eq_some_of_succ_nth_intFractPair_stream {ifp_succ_n : IntFractPai
     (of v).s.get? n = some ⟨1, ifp_succ_n.b⟩ :=
   by
   unfold of int_fract_pair.seq1
-  rw [SeqCat.map_tail, SeqCat.nth_tail, SeqCat.map_nth]
-  simp [SeqCat.nth, stream_succ_nth_eq]
+  rw [seq.map_tail, seq.nth_tail, seq.map_nth]
+  simp [seq.nth, stream_succ_nth_eq]
 #align generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream GeneralizedContinuedFraction.nth_of_eq_some_of_succ_nth_intFractPair_stream
 
 /-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
@@ -282,7 +283,7 @@ theorem of_s_head_aux (v : K) :
             b := p.b }) :=
   by
   rw [of, int_fract_pair.seq1, of._match_1]
-  simp only [SeqCat.map_tail, SeqCat.map, SeqCat.tail, SeqCat.head, SeqCat.nth, Stream'.map]
+  simp only [seq.map_tail, seq.map, seq.tail, seq.head, seq.nth, Stream'.map]
   rw [← Stream'.nth_succ, Stream'.nth, Option.map]
 #align generalized_continued_fraction.of_s_head_aux GeneralizedContinuedFraction.of_s_head_aux
 
@@ -299,14 +300,14 @@ variable (K)
 
 /-- If `a` is an integer, then the coefficient sequence of its continued fraction is empty.
 -/
-theorem of_s_of_int (a : ℤ) : (of (a : K)).s = SeqCat.nil :=
+theorem of_s_of_int (a : ℤ) : (of (a : K)).s = Seq.nil :=
   haveI h : ∀ n, (of (a : K)).s.get? n = none :=
     by
     intro n
     induction' n with n ih
     · rw [of_s_head_aux, stream_succ_of_int, Option.bind]
     · exact (of (a : K)).s.Prop ih
-  SeqCat.ext fun n => (h n).trans (SeqCat.nth_nil n).symm
+  seq.ext fun n => (h n).trans (seq.nth_nil n).symm
 #align generalized_continued_fraction.of_s_of_int GeneralizedContinuedFraction.of_s_of_int
 
 variable {K} (v)
@@ -318,8 +319,7 @@ theorem of_s_succ (n : ℕ) : (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get?
   by
   cases' eq_or_ne (fract v) 0 with h h
   · obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩
-    rw [fract_int_cast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int, SeqCat.nth_nil,
-      SeqCat.nth_nil]
+    rw [fract_int_cast, inv_zero, of_s_of_int, ← cast_zero, of_s_of_int, seq.nth_nil, seq.nth_nil]
   cases' eq_or_ne ((of (fract v)⁻¹).s.get? n) none with h₁ h₁
   ·
     rwa [h₁, ← terminated_at_iff_s_none,
@@ -337,7 +337,7 @@ an element `v` of `K` as the coefficient sequence of that of the inverse of the
 fractional part of `v`.
 -/
 theorem of_s_tail : (of v).s.tail = (of (fract v)⁻¹).s :=
-  SeqCat.ext fun n => SeqCat.nth_tail (of v).s n ▸ of_s_succ v n
+  Seq.ext fun n => Seq.nth_tail (of v).s n ▸ of_s_succ v n
 #align generalized_continued_fraction.of_s_tail GeneralizedContinuedFraction.of_s_tail
 
 variable (K) (n)
@@ -350,7 +350,7 @@ theorem convergents'_of_int (a : ℤ) : (of (a : K)).convergents' n = a :=
   induction' n with n ih
   · simp only [zeroth_convergent'_eq_h, of_h_eq_floor, floor_int_cast]
   · rw [convergents', of_h_eq_floor, floor_int_cast, add_right_eq_self]
-    exact convergents'_aux_succ_none ((of_s_of_int K a).symm ▸ SeqCat.nth_nil 0) _
+    exact convergents'_aux_succ_none ((of_s_of_int K a).symm ▸ seq.nth_nil 0) _
 #align generalized_continued_fraction.convergents'_of_int GeneralizedContinuedFraction.convergents'_of_int
 
 variable {K} (v)

Mathbin/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Kappelmann
 
 ! This file was ported from Lean 3 source module algebra.continued_fractions.convergents_equiv
-! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
+! leanprover-community/mathlib commit a7e36e48519ab281320c4d192da6a7b348ce40ad
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -73,7 +73,8 @@ variable {K : Type _} {n : ℕ}
 
 namespace GeneralizedContinuedFraction
 
-variable {g : GeneralizedContinuedFraction K} {s : SeqCat <| Pair K}
+/- ./././Mathport/Syntax/Translate/Command.lean:224:11: unsupported: unusual advanced open style -/
+variable {g : GeneralizedContinuedFraction K} {s : Seq <| Pair K}
 
 section Squash
 
@@ -93,10 +94,10 @@ combines `⟨aₙ, bₙ⟩` and `⟨aₙ₊₁, bₙ₊₁⟩` at position `n` t
 `squash_seq s 0 = [(a₀, bₒ + a₁ / b₁), (a₁, b₁),...]`.
 If `s.terminated_at (n + 1)`, then `squash_seq s n = s`.
 -/
-def squashSeq (s : SeqCat <| Pair K) (n : ℕ) : SeqCat (Pair K) :=
+def squashSeq (s : Seq <| Pair K) (n : ℕ) : Seq (Pair K) :=
   match Prod.mk (s.get? n) (s.get? (n + 1)) with
   | ⟨some gp_n, some gp_succ_n⟩ =>
-    SeqCat.nats.zipWith
+    Seq.nats.zipWith
       (-- return the squashed value at position `n`; otherwise, do nothing.
       fun n' gp => if n' = n then ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ else gp)
       s
@@ -144,7 +145,7 @@ theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n :
     none =>
     have : squash_seq s (n + 1) = s := squash_seq_eq_self_of_terminated s_succ_succ_nth_eq
     cases s_succ_nth_eq : s.nth (n + 1) <;>
-      simp only [squash_seq, SeqCat.nth_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
+      simp only [squash_seq, seq.nth_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
   case
     some =>
     obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.nth (n + 1) = some gp_succ_n;
@@ -157,7 +158,7 @@ theorem squashSeq_succ_n_tail_eq_squashSeq_tail_n :
     · have : s.tail.nth m = s.nth (m + 1) := s.nth_tail m
       cases s_succ_mth_eq : s.nth (m + 1)
       all_goals have s_tail_mth_eq := this.trans s_succ_mth_eq
-      · simp only [*, squash_seq, SeqCat.nth_tail, SeqCat.nth_zipWith, Option.map₂_none_right]
+      · simp only [*, squash_seq, seq.nth_tail, seq.nth_zip_with, Option.map₂_none_right]
       · simp [*, squash_seq]
 #align generalized_continued_fraction.squash_seq_succ_n_tail_eq_squash_seq_tail_n GeneralizedContinuedFraction.squashSeq_succ_n_tail_eq_squashSeq_tail_n
 
@@ -177,7 +178,7 @@ theorem succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq :
       exact s.ge_stable zero_le_one s_succ_nth_eq
       have : (squash_seq s 0).headI = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
         squash_seq_nth_of_not_terminated s_head_eq s_succ_nth_eq
-      simp [*, convergents'_aux, SeqCat.head, SeqCat.nth_tail]
+      simp [*, convergents'_aux, seq.head, seq.nth_tail]
     case succ =>
       obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head
       exact s.ge_stable (m + 2).zero_le s_succ_nth_eq
@@ -188,7 +189,7 @@ theorem succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq :
       have : convergents'_aux s.tail (m + 2) = convergents'_aux (squash_seq s.tail m) (m + 1) :=
         by
         refine' IH gp_succ_n _
-        simpa [SeqCat.nth_tail] using s_succ_nth_eq
+        simpa [seq.nth_tail] using s_succ_nth_eq
       have : (squash_seq s (m + 1)).headI = some gp_head :=
         (squash_seq_nth_of_lt m.succ_pos).trans s_head_eq
       simp only [*, convergents'_aux, squash_seq_succ_n_tail_eq_squash_seq_tail_n]
@@ -237,7 +238,7 @@ theorem succ_nth_convergent'_eq_squashGcf_nth_convergent' :
   cases n
   case zero =>
     cases g_s_head_eq : g.s.nth 0 <;>
-      simp [g_s_head_eq, squash_gcf, convergents', convergents'_aux, SeqCat.head]
+      simp [g_s_head_eq, squash_gcf, convergents', convergents'_aux, seq.head]
   case succ =>
     simp only [succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squash_seq, convergents',
       squash_gcf]