awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) 0) (↑a : K)

Tactic:
simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]

Premises used: Int.floor_intCast, GenContFract.zeroth_conv'_eq_h, GenContFract.of_h_eq_floor
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
n_1 : ℕ
h : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n_1) (↑a : K)
succ : Eq.{u_1 + 1} (α := K) (convs'Aux (s (of (↑a : K))) (n_1 + 1)) 0
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) (n_1 + 1)) (↑a : K)

Tactic:
rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]

Premises used: Int.floor_intCast, GenContFract.convs', add_eq_left, GenContFract.of_h_eq_floor
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
n_1 : ℕ
h : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n_1) (↑a : K)
⊢ Eq.{u_1 + 1} (α := K) (convs'Aux (s (of (↑a : K))) (n_1 + 1)) 0

Tactic:
convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

Premises used: GenContFract.convs'Aux_succ_none
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
n_1 : ℕ
h : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n_1) (↑a : K)
⊢ Eq.{u_1 + 1} (α := K) (convs'Aux (s (of (↑a : K))) (n_1 + 1)) 0

Tactic:
exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

Premises used: GenContFract.convs'Aux_succ_none
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
zero : Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) 0) (↑a : K)
succ :
  ∀ (n : ℕ),
    Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n) (↑a : K) →
      Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) (n + 1)) (↑a : K)
⊢ Eq.{u_1 + 1} (α := K) (convs' (of (↑a : K)) n) (↑a : K)

Tactic:
induction n with
  | zero => simp only [zeroth_conv'_eq_h, of_h_eq_floor, floor_intCast]
  | succ =>
    rw [convs', of_h_eq_floor, floor_intCast, add_eq_left]
    exact convs'Aux_succ_none ((of_s_of_int K a).symm ▸ Stream'.Seq.get?_nil 0) _

Premises used: Int.floor_intCast, GenContFract.convs', GenContFract.zeroth_conv'_eq_h, add_eq_left, Int.succ, GenContFract.of_h_eq_floor, GenContFract.convs'Aux_succ_none
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
inl : ∀ (h : fract v = 0), (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
inr : ∀ (h : fract v ≠ 0), (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rcases eq_or_ne (fract v) 0 with h | h

Premises used: Int.fract, eq_or_ne, GenContFract.h, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v = 0
⊢ ∃ (a : ℤ), v = (↑a : K)

Tactic:
⟨⌊v⌋, eq_of_sub_eq_zero h⟩

Premises used: Int.floor, eq_of_sub_eq_zero, Exists.intro
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v = 0
inl :
  ∀ (a : ℤ) (h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0),
    convs' (of (↑a : K)) (n + 1) =
      (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n

Tactic:
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩

Premises used: rfl
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
n : ℕ
inst_3 : IsStrictOrderedRing K
a : ℤ
h : Eq.{u_1 + 1} (α := K) (fract (↑a : K)) 0
inl : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
inl₁ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0⁻¹) n)
inl₂ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of 0) n)
inl₃ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (↑0 : K)) n)
inl₄ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (↑0 : K)
inl₅ : (↑a : K) = (↑(floor.{u_1} (α := K) (↑a : K)) : K) + 1 / 0
inl₆ : (↑a : K) = HAdd.hAdd (α := K) (↑(floor.{u_1} (α := K) (↑a : K)) : K) 0
inl₇ : Eq.{u_1 + 1} (α := K) (↑a : K) (↑(floor.{u_1} (α := K) (↑a : K)) : K)
inl₈ inl₉ : Eq.{u_1 + 1} (α := K) (↑a : K) (↑a : K)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)

Tactic:
rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]

Premises used: Int.floor_intCast, Int.cast_zero, inv_zero, Int.fract_intCast, GenContFract.convs'_of_int, add_zero, div_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v ≠ 0
inr :
  Pair.a { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } /
      (Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n) =
    1 / (of (fract v)⁻¹).convs' n
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]

Premises used: GenContFract.convs', GenContFract.convs'Aux_succ_some, GenContFract.of_s_head, GenContFract.of_h_eq_floor, add_right_inj
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v ≠ 0
rw :
  Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n =
    (of (fract v)⁻¹).h + convs'Aux (of (fract v)⁻¹).s n
rw₁ :
  Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n =
    (↑⌊(fract v)⁻¹⌋ : K) + convs'Aux (of (fract v)⁻¹).s n
rw₂ : convs'Aux (of v).s.tail n = convs'Aux (of (fract v)⁻¹).s n
rw₃ rw₄ : convs'Aux (of (fract v)⁻¹).s n = convs'Aux (of (fract v)⁻¹).s n
⊢ Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n

Tactic:
rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]

Premises used: GenContFract.convs', GenContFract.of_s_tail, GenContFract.of_h_eq_floor, add_right_inj
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : LinearOrder K
inst_2 : FloorRing K
v : K
n : ℕ
inst_3 : IsStrictOrderedRing K
h : fract v ≠ 0
⊢ Pair.a { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } /
      (Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n) =
    1 / (of (fract v)⁻¹).convs' n

Tactic:
exact congr_arg (1 / ·) (by rw [convs', of_h_eq_floor, add_right_inj, of_s_tail])

Premises used: HDiv.hDiv, congr_arg, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.contsAux (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
simp [*, contsAux, nextConts, nextDen, nextNum]

Premises used: GenContFract.contsAux, GenContFract.nextDen, GenContFract.nextConts, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
nth_s_eq : g.s.get? n = some gp
nth_contsAux_eq : g.contsAux n = ppred
succ_nth_contsAux_eq : g.contsAux (n + 1) = pred
⊢ g.conts (n + 1) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
simp [nth_cont_eq_succ_nth_contAux,
    contsAux_recurrence nth_s_eq nth_contsAux_eq succ_nth_contsAux_eq]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.contsAux_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.conts n = ppred
succ_nth_conts_eq : g.conts (n + 1) = pred
⊢ g.contsAux (n + 1) = ppred

Tactic:
rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.conts n = ppred
succ_nth_conts_eq : g.conts (n + 1) = pred
nth_conts_eq₁ : g.contsAux (n + 1) = ppred
⊢ g.contsAux (n + 1 + 1) = pred

Tactic:
rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.contsAux (n + 1) = ppred
succ_nth_conts_eq : g.contsAux (n + 1 + 1) = pred
⊢ g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
conts_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq

Premises used: GenContFract.conts_recurrenceAux
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp ppred pred : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_conts_eq : g.contsAux (n + 1) = ppred
succ_nth_conts_eq : g.contsAux (n + 1 + 1) = pred
⊢ g.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }

Tactic:
exact conts_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq

Premises used: GenContFract.conts_recurrenceAux
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_num_eq : g.nums n = ppredA
succ_nth_num_eq : g.nums (n + 1) = predA
⊢ ∃ (conts : Pair K), g.conts n = conts ∧ conts.a = ppredA

Tactic:
exists_conts_a_of_num nth_num_eq

Premises used: GenContFract.exists_conts_a_of_num
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
ppredA predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_num_eq : g.nums n = ppredA
succ_nth_num_eq : g.nums (n + 1) = predA
obtain :
  ∀ (ppredConts : Pair K) (nth_conts_eq : g.conts n = ppredConts) (nth_num_eq : g.nums n = ppredConts.a),
    g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredA

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.a = ppredA :=
    exists_conts_a_of_num nth_num_eq

Premises used: GenContFract.conts, GenContFract.exists_conts_a_of_num, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_num_eq : g.nums (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
⊢ ∃ (conts : Pair K), g.conts (n + 1) = conts ∧ conts.a = predA

Tactic:
exists_conts_a_of_num succ_nth_num_eq

Premises used: GenContFract.exists_conts_a_of_num
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
predA : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_num_eq : g.nums (n + 1) = predA
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
obtain :
  ∀ (predConts : Pair K) (succ_nth_conts_eq : g.conts (n + 1) = predConts)
    (succ_nth_num_eq : g.nums (n + 1) = predConts.a), g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
      ∃ conts, g.conts (n + 1) = conts ∧ conts.a = predA :=
    exists_conts_a_of_num succ_nth_num_eq

Premises used: GenContFract.conts, GenContFract.exists_conts_a_of_num, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_num_eq : g.nums n = ppredConts.a
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_num_eq : g.nums (n + 1) = predConts.a
rw : (g.conts (n + 2)).a = gp.b * predConts.a + gp.a * ppredConts.a
rw₁ rw₂ :
  { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b : Pair K }.a =
    gp.b * predConts.a + gp.a * ppredConts.a
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a

Tactic:
rw [num_eq_conts_a, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]

Premises used: GenContFract.num_eq_conts_a, GenContFract.conts_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_den_eq : g.dens n = ppredB
succ_nth_den_eq : g.dens (n + 1) = predB
⊢ ∃ (conts : Pair K), g.conts n = conts ∧ conts.b = ppredB

Tactic:
exists_conts_b_of_den nth_den_eq

Premises used: GenContFract.exists_conts_b_of_den
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
ppredB predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
nth_den_eq : g.dens n = ppredB
succ_nth_den_eq : g.dens (n + 1) = predB
obtain :
  ∀ (ppredConts : Pair K) (nth_conts_eq : g.conts n = ppredConts) (nth_den_eq : g.dens n = ppredConts.b),
    g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredB

Tactic:
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.b = ppredB :=
    exists_conts_b_of_den nth_den_eq

Premises used: GenContFract.exists_conts_b_of_den, GenContFract.conts, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
⊢ ∃ (conts : Pair K), g.conts (n + 1) = conts ∧ conts.b = predB

Tactic:
exists_conts_b_of_den succ_nth_den_eq

Premises used: GenContFract.exists_conts_b_of_den
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
predB : K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
succ_nth_den_eq : g.dens (n + 1) = predB
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
obtain :
  ∀ (predConts : Pair K) (succ_nth_conts_eq : g.conts (n + 1) = predConts)
    (succ_nth_den_eq : g.dens (n + 1) = predConts.b), g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b

Tactic:
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ :
      ∃ conts, g.conts (n + 1) = conts ∧ conts.b = predB :=
    exists_conts_b_of_den succ_nth_den_eq

Premises used: GenContFract.exists_conts_b_of_den, GenContFract.conts, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
gp : Pair K
succ_nth_s_eq : g.s.get? (n + 1) = some gp
ppredConts : Pair K
nth_conts_eq : g.conts n = ppredConts
nth_den_eq : g.dens n = ppredConts.b
predConts : Pair K
succ_nth_conts_eq : g.conts (n + 1) = predConts
succ_nth_den_eq : g.dens (n + 1) = predConts.b
rw : (g.conts (n + 2)).b = gp.b * predConts.b + gp.a * ppredConts.b
rw₁ rw₂ :
  { a := gp.b * predConts.a + gp.a * ppredConts.a, b := gp.b * predConts.b + gp.a * ppredConts.b : Pair K }.b =
    gp.b * predConts.b + gp.a * ppredConts.b
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b

Tactic:
rw [den_eq_conts_b, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]

Premises used: GenContFract.den_eq_conts_b, GenContFract.conts_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.TerminatedAt (n + 1)
⊢ s.get? (n + 1) = none

Tactic:
change s.get? (n + 1) = none at terminatedAt_succ_n

Premises used: Option.none, HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = Option.none
none : ∀ (s_nth_eq : s.get? n = Option.none), squashSeq s n = s
some : ∀ (val : Pair K) (s_nth_eq : s.get? n = Option.some val), squashSeq s n = s
⊢ squashSeq s n = s

Tactic:
cases s_nth_eq : s.get? n

Premises used: Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
s_nth_eq : s.get? n = none
⊢ squashSeq s n = s

Tactic:
simp only [*, squashSeq]

Premises used: GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
val : Pair K
s_nth_eq : s.get? n = some val
⊢ squashSeq s n = s

Tactic:
simp only [*, squashSeq]

Premises used: GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
gp_n gp_succ_n : Pair K
s_nth_eq : s.get? n = some gp_n
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s n).get? n = some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }

Tactic:
simp [*, squashSeq]

Premises used: GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = Option.none
none none₁ : s.get? m = s.get? m
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]

Premises used: GenContFract.squashSeq_eq_self_of_terminated
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
val : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val
⊢ ∃ (gp_n : Pair K), s.get? n = some gp_n

Tactic:
s.ge_stable n.le_succ s_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Nat.le_succ
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
val : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some val
some : ∀ (gp_n : Pair K) (s_nth_eq : s.get? n = Option.some gp_n), (squashSeq s n).get? m = s.get? m
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Nat.le_succ, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
val : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val
gp_n : Pair K
s_nth_eq : s.get? n = some gp_n
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
simp [*, squashSeq, m_lt_n.ne]

Premises used: GenContFract.squashSeq, LT.lt.ne
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
cases : ∀ (x : Option (Pair K)) (s_succ_nth_eq : s.get? (n + 1) = x), (squashSeq s n).get? m = s.get? m
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
cases s_succ_nth_eq : s.get? (n + 1) with
  | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
  | some =>
    obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n :=
      s.ge_stable n.le_succ s_succ_nth_eq
    simp [*, squashSeq, m_lt_n.ne]

Premises used: GenContFract.squashSeq, Option.some, Option.none, HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?, LT.lt.ne
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = Option.none
none : ∀ (s_succ_nth_eq : s.get? (n + 1) = Option.none), (squashSeq s (n + 1)).tail = squashSeq s.tail n
none₁ : ∀ (val : Pair K) (s_succ_nth_eq : s.get? (n + 1) = some val), (squashSeq s (n + 1)).tail = squashSeq s.tail n
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
cases s_succ_nth_eq : s.get? (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]

Premises used: Stream'.Seq.get?_tail, GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
val : Pair K
s_succ_nth_eq : s.get? (n + 1) = some val
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]

Premises used: Stream'.Seq.get?_tail, GenContFract.squashSeq
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = some gp_succ_succ_n
⊢ ∃ (gp_succ_n : Pair K), s.get? (n + 1) = some gp_succ_n

Tactic:
s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Nat.le_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
gp_succ_succ_n : Pair K
s_succ_succ_nth_eq : s.get? (n + 2) = Option.some gp_succ_succ_n
some :
  ∀ (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n),
    (squashSeq s (n + 1)).tail = squashSeq s.tail n
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n

Tactic:
obtain ⟨gp_succ_n, s_succ_nth_eq⟩ : ∃ gp_succ_n, s.get? (n + 1) = some gp_succ_n :=
      s.ge_stable (n + 1).le_succ s_succ_succ_nth_eq

Premises used: Stream'.Seq.ge_stable, Nat.le_succ, HAdd.hAdd, OfNat.ofNat, Stream'.Seq.get?