-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem exists_gcf_pair_rat_eq_of_nth_contsAux :
    ∃ conts : Pair ℚ, (of v).contsAux n = (conts.map (↑) : Pair K) :=
  Nat.strong_induction_on n
    (by
      clear n
      let g := of v
      intro n IH
      rcases n with (_ | _ | n)
      -- n = 0
      · suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]
        use Pair.mk 1 0
        simp
      -- n = 1
      · suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]
        use Pair.mk ⌊v⌋ 1
        simp [g]
      -- 2 ≤ n
      · obtain ⟨pred_conts, pred_conts_eq⟩ := IH (n + 1) <| lt_add_one (n + 1)
        -- invoke the IH
        rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
        -- option.none
        · use pred_conts
          have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
            contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
          simp only [g, this, pred_conts_eq]
        -- option.some
        · -- invoke the IH a second time
          obtain ⟨ppred_conts, ppred_conts_eq⟩ :=
            IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1
          obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
            of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq
          -- finally, unfold the recurrence to obtain the required rational value.
          simp only [g, a_eq_one, b_eq_z,
            contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
          use nextConts 1 (z : ℚ) ppred_conts pred_conts
          cases ppred_conts; cases pred_conts
          simp [nextConts, nextNum, nextDen])

Proof state:
case h.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝ b✝ : ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast pred_conts).a + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).a,
      b := ↑z * (Pair.map Rat.cast pred_conts).b + 1 * (Pair.map Rat.cast { a := a✝, b := b✝ }).b } =
    Pair.map Rat.cast (nextConts 1 ↑z { a := a✝, b := b✝ } pred_conts)

Tactic:
cases pred_conts

Result:
case h.mk.mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = ↑z
a✝¹ b✝¹ : ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a✝¹, b := b✝¹ }
a✝ b✝ : ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast { a := a✝, b := b✝ }
⊢ { a := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).a + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).a,
      b := ↑z * (Pair.map Rat.cast { a := a✝, b := b✝ }).b + 1 * (Pair.map Rat.cast { a := a✝¹, b := b✝¹ }).b } =
    Pair.map Rat.cast (nextConts 1 ↑z { a := a✝¹, b := b✝¹ } { a := a✝, b := b✝ })

Proof state:
case h
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
⊢ { a := g.h, b := 1 } = Pair.map Rat.cast { a := ↑⌊v⌋, b := 1 }

Tactic:
simp [g]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0 + 1, ∃ conts, (of v).contsAux m = Pair.map Rat.cast conts
this : ∃ conts, { a := g.h, b := 1 } = Pair.map Rat.cast conts
⊢ ∃ conts, (of v).contsAux (0 + 1) = Pair.map Rat.cast conts

Tactic:
simpa [contsAux]

Result:
no goals