-- Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
theorem compExactValue_correctness_of_stream_eq_some :
    ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n →
      v = compExactValue ((of v).contsAux n) ((of v).contsAux <| n + 1) ifp_n.fr

Proof state:
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
have hA : (↑⌊1 / ifp_n.fr⌋ * pA + ppA) + pA * f = pA * (1 / ifp_n.fr) + ppA := by
  have := congrFun (congrArg HMul.hMul tmp_calc) f
  rwa [right_distrib, div_mul_cancel₀ (h := f_ne_zero),
    div_mul_cancel₀ (h := f_ne_zero)] at this

Result:
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) = compExactValue pconts conts (IntFractPair.of ifp_n.fr⁻¹).fr

Proof state:
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB) =
    compExactValue (g.contsAux (n + 1)) (g.contsAux (n + 2)) (IntFractPair.of ifp_n.fr⁻¹).fr

Tactic:
field_simp [compExactValue, contsAux_recurrence s_nth_eq ppconts_eq pconts_eq,
  nextConts, nextNum, nextDen]

Result:
case succ.intro.intro.intro.inr.intro.intro.intro.refl.refl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
⊢ (ppA * ifp_n.fr + pA) / (ppB * ifp_n.fr + pB) =
    if (IntFractPair.of (1 / ifp_n.fr)).fr = 0 then
      (↑⌊1 / ifp_n.fr⌋ * (g.contsAux (n + 1)).a + (g.contsAux n).a) /
        (↑⌊1 / ifp_n.fr⌋ * (g.contsAux (n + 1)).b + (g.contsAux n).b)
    else
      (↑⌊1 / ifp_n.fr⌋ * (g.contsAux (n + 1)).a + (g.contsAux n).a +
          (g.contsAux (n + 1)).a * (IntFractPair.of (1 / ifp_n.fr)).fr) /
        (↑⌊1 / ifp_n.fr⌋ * (g.contsAux (n + 1)).b + (g.contsAux n).b +
          (g.contsAux (n + 1)).b * (IntFractPair.of (1 / ifp_n.fr)).fr)