chore: format to avoid multiple goals (#10979)

As requested on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Help.20with.20.60nightly-testing.60/near/423307621)
leanprover-community · Feb 26, 2024 · 7eae15a · 7eae15a
1 parent fb56e88
commit 7eae15a
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean b/Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
@@ -206,9 +206,9 @@ theorem compExactValue_correctness_of_stream_eq_some :
         nextContinuants, nextNumerator, nextDenominator]
       have hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f := rfl
       rw [one_div, if_neg _, ← one_div, hfr]
-      field_simp [hA, hB]
-      ac_rfl
-      rwa [inv_eq_one_div, hfr]
+      · field_simp [hA, hB]
+        ac_rfl
+      · rwa [inv_eq_one_div, hfr]
 #align generalized_continued_fraction.comp_exact_value_correctness_of_stream_eq_some GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some
 
 open GeneralizedContinuedFraction (of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none)