chore: remove stream-of-conciousness syntax for obtain (#11045)

This covers many instances, but is not exhaustive.

Independently of whether that syntax should be avoided (similar to #10534), I think all these changes are small improvements.

Archive/Sensitivity.lean

@@ -436,8 +436,8 @@ theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) :
     rw [Finsupp.mem_support_iff] at p_in
     rw [Set.mem_toFinset]
     exact (dualBases_e_ε _).mem_of_mem_span y_mem_H p p_in
-  obtain ⟨q, H_max⟩ : ∃ q : Q m.succ, ∀ q' : Q m.succ, |(ε q' : _) y| ≤ |ε q y|
-  exact Finite.exists_max _
+  obtain ⟨q, H_max⟩ : ∃ q : Q m.succ, ∀ q' : Q m.succ, |(ε q' : _) y| ≤ |ε q y| :=
+    Finite.exists_max _
   have H_q_pos : 0 < |ε q y| := by
     contrapose! y_ne
     exact epsilon_total fun p => abs_nonpos_iff.mp (le_trans (H_max p) y_ne)

Counterexamples/SorgenfreyLine.lean

@@ -315,14 +315,14 @@ theorem not_separatedNhds_rat_irrational_antidiag :
   have Hd : Dense (⋃ n, interior (C n)) :=
     IsGδ.setOf_irrational.dense_iUnion_interior_of_closed dense_irrational
       (fun _ => isClosed_closure) H
-  obtain ⟨N, hN⟩ : ∃ n : ℕ+, (interior <| C n).Nonempty; exact nonempty_iUnion.mp Hd.nonempty
+  obtain ⟨N, hN⟩ : ∃ n : ℕ+, (interior <| C n).Nonempty := nonempty_iUnion.mp Hd.nonempty
   /- Choose a rational number `r` in the interior of the closure of `C N`, then choose `n ≥ N > 0`
     such that `Ico r (r + n⁻¹) × Ico (-r) (-r + n⁻¹) ⊆ U`. -/
   rcases Rat.denseRange_cast.exists_mem_open isOpen_interior hN with ⟨r, hr⟩
   have hrU : ((r, -r) : ℝₗ × ℝₗ) ∈ U := @SU (r, -r) ⟨add_neg_self _, r, rfl⟩
   obtain ⟨n, hnN, hn⟩ :
-    ∃ n, N ≤ n ∧ Ico (r : ℝₗ) (r + (n : ℝₗ)⁻¹) ×ˢ Ico (-r : ℝₗ) (-r + (n : ℝₗ)⁻¹) ⊆ U
-  exact ((nhds_prod_antitone_basis_inv_pnat _ _).hasBasis_ge N).mem_iff.1 (Uo.mem_nhds hrU)
+      ∃ n, N ≤ n ∧ Ico (r : ℝₗ) (r + (n : ℝₗ)⁻¹) ×ˢ Ico (-r : ℝₗ) (-r + (n : ℝₗ)⁻¹) ⊆ U :=
+    ((nhds_prod_antitone_basis_inv_pnat _ _).hasBasis_ge N).mem_iff.1 (Uo.mem_nhds hrU)
   /- Finally, choose `x ∈ Ioo (r : ℝ) (r + n⁻¹) ∩ C N`. Then `(x, -r)` belongs both to `U` and `V`,
     so they are not disjoint. This contradiction completes the proof. -/
   obtain ⟨x, hxn, hx_irr, rfl⟩ :

Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -137,11 +137,11 @@ fraction `GeneralizedContinuedFraction.of`.
 /-- Shows that the integer parts of the continued fraction are at least one. -/
 theorem of_one_le_get?_part_denom {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) : 1 ≤ b := by
-  obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b;
-  exact exists_s_b_of_part_denom nth_part_denom_eq
+  obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
+    exists_s_b_of_part_denom nth_part_denom_eq
   obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
-    ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b
-  exact IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
+      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
+    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
   rw [← ifp_n_b_eq_gp_n_b]
   exact mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq
 #align generalized_continued_fraction.of_one_le_nth_part_denom GeneralizedContinuedFraction.of_one_le_get?_part_denom
@@ -152,8 +152,8 @@ denominators `bᵢ` correspond to integers.
 -/
 theorem of_part_num_eq_one_and_exists_int_part_denom_eq {gp : GeneralizedContinuedFraction.Pair K}
     (nth_s_eq : (of v).s.get? n = some gp) : gp.a = 1 ∧ ∃ z : ℤ, gp.b = (z : K) := by
-  obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _
-  exact IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
+  obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
+    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
   have : gp = ⟨1, ifp.b⟩ := by
     have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
       get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
@@ -165,17 +165,17 @@ theorem of_part_num_eq_one_and_exists_int_part_denom_eq {gp : GeneralizedContinu
 /-- Shows that the partial numerators `aᵢ` are equal to one. -/
 theorem of_part_num_eq_one {a : K} (nth_part_num_eq : (of v).partialNumerators.get? n = some a) :
     a = 1 := by
-  obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a;
-  exact exists_s_a_of_part_num nth_part_num_eq
+  obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
+    exists_s_a_of_part_num nth_part_num_eq
   have : gp.a = 1 := (of_part_num_eq_one_and_exists_int_part_denom_eq nth_s_eq).left
   rwa [gp_a_eq_a_n] at this
 #align generalized_continued_fraction.of_part_num_eq_one GeneralizedContinuedFraction.of_part_num_eq_one
 
 /-- Shows that the partial denominators `bᵢ` correspond to an integer. -/
 theorem exists_int_eq_of_part_denom {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) : ∃ z : ℤ, b = (z : K) := by
-  obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b;
-  exact exists_s_b_of_part_denom nth_part_denom_eq
+  obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b :=
+    exists_s_b_of_part_denom nth_part_denom_eq
   have : ∃ z : ℤ, gp.b = (z : K) := (of_part_num_eq_one_and_exists_int_part_denom_eq nth_s_eq).right
   rwa [gp_b_eq_b_n] at this
 #align generalized_continued_fraction.exists_int_eq_of_part_denom GeneralizedContinuedFraction.exists_int_eq_of_part_denom
@@ -201,8 +201,8 @@ theorem fib_le_of_continuantsAux_b :
       · let g := of v -- case 2 ≤ n
         have : ¬n + 2 ≤ 1 := by linarith
         have not_terminated_at_n : ¬g.TerminatedAt n := Or.resolve_left hyp this
-        obtain ⟨gp, s_ppred_nth_eq⟩ : ∃ gp, g.s.get? n = some gp
-        exact Option.ne_none_iff_exists'.mp not_terminated_at_n
+        obtain ⟨gp, s_ppred_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
+          Option.ne_none_iff_exists'.mp not_terminated_at_n
         set pconts := g.continuantsAux (n + 1) with pconts_eq
         set ppconts := g.continuantsAux n with ppconts_eq
         -- use the recurrence of `continuantsAux`
@@ -273,8 +273,8 @@ theorem zero_le_of_denom : 0 ≤ (of v).denominators n := by
 theorem le_of_succ_succ_get?_continuantsAux_b {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) :
     b * ((of v).continuantsAux <| n + 1).b ≤ ((of v).continuantsAux <| n + 2).b := by
-  obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b
-  exact exists_s_b_of_part_denom nth_part_denom_eq
+  obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
+    exists_s_b_of_part_denom nth_part_denom_eq
   simp [of_part_num_eq_one (part_num_eq_s_a nth_s_eq), zero_le_of_continuantsAux_b,
     GeneralizedContinuedFraction.continuantsAux_recurrence nth_s_eq rfl rfl]
 #align generalized_continued_fraction.le_of_succ_succ_nth_continuants_aux_b GeneralizedContinuedFraction.le_of_succ_succ_get?_continuantsAux_b
@@ -298,8 +298,8 @@ theorem of_denom_mono : (of v).denominators n ≤ (of v).denominators (n + 1) :=
     have : g.denominators (n + 1) = g.denominators n :=
       denominators_stable_of_terminated n.le_succ this
     rw [this]
-  · obtain ⟨b, nth_part_denom_eq⟩ : ∃ b, g.partialDenominators.get? n = some b
-    exact Option.ne_none_iff_exists'.mp not_terminated
+  · obtain ⟨b, nth_part_denom_eq⟩ : ∃ b, g.partialDenominators.get? n = some b :=
+      Option.ne_none_iff_exists'.mp not_terminated
     have : 1 ≤ b := of_one_le_get?_part_denom nth_part_denom_eq
     calc
       g.denominators n ≤ b * g.denominators n := by
@@ -335,8 +335,8 @@ theorem determinant_aux (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)) :
     -- let's change the goal to something more readable
     change pA * conts.b - pB * conts.a = (-1) ^ (n + 1)
     have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
-    obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp
-    exact Option.ne_none_iff_exists'.1 not_terminated_at_n
+    obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
+      Option.ne_none_iff_exists'.1 not_terminated_at_n
     -- unfold the recurrence relation for `conts` once and simplify to derive the following
     suffices pA * (ppB + gp.b * pB) - pB * (ppA + gp.b * pA) = (-1) ^ (n + 1) by
       simp only [conts, continuantsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
@@ -459,8 +459,8 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
   set pred_conts := continuantsAux g n with pred_conts_eq
   -- change the goal to something more readable
   change |v - convergents g n| ≤ 1 / (conts.b * nextConts.b)
-  obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp
-  exact Option.ne_none_iff_exists'.1 not_terminated_at_n
+  obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
+    Option.ne_none_iff_exists'.1 not_terminated_at_n
   have gp_a_eq_one : gp.a = 1 := of_part_num_eq_one (part_num_eq_s_a s_nth_eq)
   -- unfold the recurrence relation for `nextConts.b`
   have nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b := by
@@ -469,8 +469,8 @@ theorem abs_sub_convergents_le (not_terminated_at_n : ¬(of v).TerminatedAt n) :
   let denom := conts.b * (pred_conts.b + gp.b * conts.b)
   suffices |v - g.convergents n| ≤ 1 / denom by rw [nextConts_b_eq]; congr 1
   obtain ⟨ifp_succ_n, succ_nth_stream_eq, ifp_succ_n_b_eq_gp_b⟩ :
-    ∃ ifp_succ_n, IntFractPair.stream v (n + 1) = some ifp_succ_n ∧ (ifp_succ_n.b : K) = gp.b
-  exact IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some s_nth_eq
+      ∃ ifp_succ_n, IntFractPair.stream v (n + 1) = some ifp_succ_n ∧ (ifp_succ_n.b : K) = gp.b :=
+    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some s_nth_eq
   obtain ⟨ifp_n, stream_nth_eq, stream_nth_fr_ne_zero, if_of_eq_ifp_succ_n⟩ :
     ∃ ifp_n,
       IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean

@@ -132,8 +132,8 @@ theorem compExactValue_correctness_of_stream_eq_some :
     -- Nat.succ
     obtain ⟨ifp_n, nth_stream_eq, nth_fract_ne_zero, -⟩ :
       ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
-        ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-    exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+        ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
+      IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
     -- introduce some notation
     set conts := g.continuantsAux (n + 2) with conts_eq
     set pconts := g.continuantsAux (n + 1) with pconts_eq
@@ -143,8 +143,8 @@ theorem compExactValue_correctness_of_stream_eq_some :
     · suffices v = conts.a / conts.b by simpa [compExactValue, ifp_succ_n_fr_eq_zero]
       -- use the IH and the fact that ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ to prove this case
       obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_inv_eq_floor⟩ :
-        ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋
-      exact IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero
+          ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ⌊ifp_n.fr⁻¹⌋ :=
+        IntFractPair.exists_succ_nth_stream_of_fr_zero succ_nth_stream_eq ifp_succ_n_fr_eq_zero
       have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
       cases this
       have s_nth_eq : g.s.get? n = some ⟨1, ⌊ifp_n.fr⁻¹⌋⟩ :=
@@ -163,8 +163,8 @@ theorem compExactValue_correctness_of_stream_eq_some :
       -- get the correspondence between ifp_n and ifp_succ_n
       obtain ⟨ifp_n', nth_stream_eq', ifp_n_fract_ne_zero, ⟨refl⟩⟩ :
         ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧
-          ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-      exact IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
+          ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
+        IntFractPair.succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
       have : ifp_n' = ifp_n := by injection Eq.trans nth_stream_eq'.symm nth_stream_eq
       cases this
       -- get the correspondence between ifp_n and g.s.nth n
@@ -270,8 +270,7 @@ be `v`.
 theorem of_correctness_atTop_of_terminates (terminates : (of v).Terminates) :
     ∀ᶠ n in atTop, v = (of v).convergents n := by
   rw [eventually_atTop]
-  obtain ⟨n, terminated_at_n⟩ : ∃ n, (of v).TerminatedAt n
-  exact terminates
+  obtain ⟨n, terminated_at_n⟩ : ∃ n, (of v).TerminatedAt n := terminates
   use n
   intro m m_geq_n
   rw [convergents_stable_of_terminated m_geq_n terminated_at_n]

Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -89,8 +89,8 @@ nonrec theorem exists_gcf_pair_rat_eq_of_nth_conts_aux :
         · -- invoke the IH a second time
           cases' IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1 with ppred_conts
             ppred_conts_eq
-          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K);
-          exact of_part_num_eq_one_and_exists_int_part_denom_eq s_ppred_nth_eq
+          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
+            of_part_num_eq_one_and_exists_int_part_denom_eq s_ppred_nth_eq
           -- finally, unfold the recurrence to obtain the required rational value.
           simp only [a_eq_one, b_eq_z,
             continuantsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
@@ -128,10 +128,10 @@ variable {v}
 
 /-- Every terminating continued fraction corresponds to a rational number. -/
 theorem exists_rat_eq_of_terminates (terminates : (of v).Terminates) : ∃ q : ℚ, v = ↑q := by
-  obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convergents n;
-  exact of_correctness_of_terminates terminates
-  obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K)
-  exact exists_rat_eq_nth_convergent v n
+  obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convergents n :=
+    of_correctness_of_terminates terminates
+  obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K) :=
+    exists_rat_eq_nth_convergent v n
   have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
   use q, this
 #align generalized_continued_fraction.exists_rat_eq_of_terminates GeneralizedContinuedFraction.exists_rat_eq_of_terminates
@@ -283,8 +283,8 @@ theorem stream_succ_nth_fr_num_lt_nth_fr_num_rat {ifp_n ifp_succ_n : IntFractPai
   obtain ⟨ifp_n', stream_nth_eq', ifp_n_fract_ne_zero, IntFractPair.of_eq_ifp_succ_n⟩ :
     ∃ ifp_n',
       IntFractPair.stream q n = some ifp_n' ∧
-        ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n
-  exact succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
+        ifp_n'.fr ≠ 0 ∧ IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n :=
+    succ_nth_stream_eq_some_iff.mp stream_succ_nth_eq
   have : ifp_n = ifp_n' := by injection Eq.trans stream_nth_eq.symm stream_nth_eq'
   cases this
   rw [← IntFractPair.of_eq_ifp_succ_n]

Mathlib/Algebra/ContinuedFractions/ContinuantsRecurrence.lean

@@ -51,11 +51,11 @@ theorem numerators_recurrence {gp : Pair K} {ppredA predA : K}
     (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_num_eq : g.numerators n = ppredA)
     (succ_nth_num_eq : g.numerators (n + 1) = predA) :
     g.numerators (n + 2) = gp.b * predA + gp.a * ppredA := by
-  obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.a = ppredA
-  exact exists_conts_a_of_num nth_num_eq
+  obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.a = ppredA :=
+    exists_conts_a_of_num nth_num_eq
   obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
-    ∃ conts, g.continuants (n + 1) = conts ∧ conts.a = predA
-  exact exists_conts_a_of_num succ_nth_num_eq
+      ∃ conts, g.continuants (n + 1) = conts ∧ conts.a = predA :=
+    exists_conts_a_of_num succ_nth_num_eq
   rw [num_eq_conts_a, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
 #align generalized_continued_fraction.numerators_recurrence GeneralizedContinuedFraction.numerators_recurrence
 
@@ -64,11 +64,11 @@ theorem denominators_recurrence {gp : Pair K} {ppredB predB : K}
     (succ_nth_s_eq : g.s.get? (n + 1) = some gp) (nth_denom_eq : g.denominators n = ppredB)
     (succ_nth_denom_eq : g.denominators (n + 1) = predB) :
     g.denominators (n + 2) = gp.b * predB + gp.a * ppredB := by
-  obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.b = ppredB
-  exact exists_conts_b_of_denom nth_denom_eq
+  obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.continuants n = conts ∧ conts.b = ppredB :=
+    exists_conts_b_of_denom nth_denom_eq
   obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
-    ∃ conts, g.continuants (n + 1) = conts ∧ conts.b = predB
-  exact exists_conts_b_of_denom succ_nth_denom_eq
+      ∃ conts, g.continuants (n + 1) = conts ∧ conts.b = predB :=
+    exists_conts_b_of_denom succ_nth_denom_eq
   rw [denom_eq_conts_b, continuants_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
 #align generalized_continued_fraction.denominators_recurrence GeneralizedContinuedFraction.denominators_recurrence