awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₇ : Eq.{u_1 + 1} (α := K) (↑a : K) (↑(floor.{u_1} (α := K) (↑a : K)) : K)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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)
⊢ convs' (of (↑a : K)) (n + 1) =
    (↑(floor.{u_1} (α := K) (↑a : K)) : K) + HDiv.hDiv (α := K) 1 (convs' (of (fract (↑a : K))⁻¹) n)
have inl₈ : Eq.{u_1 + 1} (α := K) (↑a : K) (↑a : K)
Tactic: rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
      div_zero, add_zero, floor_intCast]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (fract v)⁻¹).convs' n
have 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
Tactic: rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n
have 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
Tactic: rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n
have 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
Tactic: rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n
have rw₂ : convs'Aux (of v).s.tail n = convs'Aux (of (fract v)⁻¹).s n
Tactic: rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Translations (goal)
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
⊢ Pair.b { a := 1, b := (↑⌊(fract v)⁻¹⌋ : K) : Pair K } + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n
have rw₃ : convs'Aux (of (fract v)⁻¹).s n = convs'Aux (of (fract v)⁻¹).s n
Tactic: rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (hypothesis)
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.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
have nth_conts_eq₁ : g.contsAux (n + 1) = ppred
Tactic: rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq
Cleared hypotheses: nth_conts_eq, succ_nth_conts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (hypothesis)
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.conts (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
have succ_nth_conts_eq₁ : g.contsAux (n + 1 + 1) = pred
Tactic: rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq
Cleared hypotheses: nth_conts_eq, succ_nth_conts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredA
have 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
Tactic: obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.a = ppredA :=
    exists_conts_a_of_num nth_num_eq
Cleared hypotheses: ppredA, nth_num_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.nums (n + 2) = gp.b * predA + gp.a * ppredConts.a
have 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
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
Cleared hypotheses: predA, succ_nth_num_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
have rw : (g.conts (n + 2)).a = 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.nums (n + 2) = gp.b * predConts.a + gp.a * ppredConts.a
have 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
Tactic: rw [num_eq_conts_a, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredB
have 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
Tactic: obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.b = ppredB :=
    exists_conts_b_of_den nth_den_eq
Cleared hypotheses: ppredB, nth_den_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.dens (n + 2) = gp.b * predB + gp.a * ppredConts.b
have 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
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
Cleared hypotheses: predB, succ_nth_den_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
have rw : (g.conts (n + 2)).b = 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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence (goal)
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
⊢ g.dens (n + 2) = gp.b * predConts.b + gp.a * ppredConts.b
have 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
Tactic: rw [den_eq_conts_b, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.TerminatedAt (n + 1)
⊢ squashSeq s n = s
have terminatedAt_succ_n₁ : s.get? (n + 1) = none
Tactic: change s.get? (n + 1) = none at terminatedAt_succ_n
Cleared hypotheses: terminatedAt_succ_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
terminatedAt_succ_n : s.get? (n + 1) = none
⊢ squashSeq s n = s
have none : ∀ (s_nth_eq : s.get? n = none), squashSeq s n = s
Tactic: cases s_nth_eq : s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
⊢ squashSeq s n = s
have some : ∀ (val : Pair K) (s_nth_eq : s.get? n = some val), squashSeq s n = s
Tactic: cases s_nth_eq : s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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) = none
⊢ (squashSeq s n).get? m = s.get? m
have none : s.get? m = s.get? m
Tactic: rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
⊢ (squashSeq s n).get? m = s.get? m
have some : ∀ (gp_n : Pair K) (s_nth_eq : s.get? n = some gp_n), (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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
m : ℕ
m_lt_n : m < n
⊢ (squashSeq s n).get? m = s.get? m
have cases : ∀ (x : Option (Pair K)) (s_succ_nth_eq : s.get? (n + 1) = x), (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]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_succ_nth_eq : s.get? (n + 2) = none
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
have none : ∀ (s_succ_nth_eq : s.get? (n + 1) = none), (squashSeq s (n + 1)).tail = squashSeq s.tail n
Tactic: cases s_succ_nth_eq : s.get? (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
have none₁ : ∀ (val : Pair K) (s_succ_nth_eq : s.get? (n + 1) = some val), (squashSeq s (n + 1)).tail = squashSeq s.tail n
Tactic: cases s_succ_nth_eq : s.get? (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
have some : ∀ (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
have some : ∀ (m : ℕ), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Tactic: ext1 m
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
have some : ∀ (m_eq_n : m = n), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Tactic: rcases Decidable.em (m = n) with m_eq_n | m_ne_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
m : ℕ
some : ∀ (m_eq_n : m = n), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
have some₁ : ∀ (m_ne_n : ¬m = n), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Tactic: rcases Decidable.em (m = n) with m_eq_n | m_ne_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
have some : ∀ (s_succ_mth_eq : s.get? (m + 1) = none), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Tactic: cases s_succ_mth_eq : s.get? (m + 1)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
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
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
m : ℕ
m_ne_n : ¬m = n
some : ∀ (s_succ_mth_eq : s.get? (m + 1) = none), (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
⊢ (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
have some₁ : ∀ (val : Pair K) (s_succ_mth_eq : s.get? (m + 1) = Option.some val),
  (squashSeq s (n + 1)).tail.get? m = (squashSeq s.tail n).get? m
Tactic: cases s_succ_mth_eq : s.get? (m + 1)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
⊢ (squashSeq s (n + 1)).tail = squashSeq s.tail n
have cases : ∀ (x : Option (Pair K)) (s_succ_succ_nth_eq : s.get? (n + 2) = x), (squashSeq s (n + 1)).tail = squashSeq s.tail n
Tactic: cases s_succ_succ_nth_eq : s.get? (n + 2) with
  | none =>
    cases s_succ_nth_eq : s.get? (n + 1) <;>
      simp only [squashSeq, Stream'.Seq.get?_tail, s_succ_nth_eq, s_succ_succ_nth_eq]
  | some gp_succ_succ_n =>
    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
    -- apply extensionality with `m` and continue by cases `m = n`.
    ext1 m
    rcases Decidable.em (m = n) with m_eq_n | m_ne_n
    · simp [*, squashSeq]
    · cases s_succ_mth_eq : s.get? (m + 1)
      · simp only [*, squashSeq, Stream'.Seq.get?_tail, Stream'.Seq.get?_zipWith,
          Option.map₂_none_right]
      · simp [*, squashSeq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = none
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
have none : convs'Aux s (n + 2) = convs'Aux s (n + 1)
Tactic: rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
      convs'Aux_stable_step_of_terminated s_succ_nth_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = Option.none
none : convs'Aux s (n + 2) = convs'Aux s (n + 1)
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
have none₁ : convs'Aux s (n + 1) = convs'Aux s (n + 1)
Tactic: rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
      convs'Aux_stable_step_of_terminated s_succ_nth_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = some gp_succ_n
⊢ convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
have some : ∀ (gp_head : Pair K) (s_head_eq : s.head = some gp_head),
  convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
Tactic: obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
inst : DivisionRing K
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
have this : (squashSeq s 0).head = some { a := gp_head.a, b := gp_head.b + gp_succ_n.a / gp_succ_n.b }
Tactic: have : (squashSeq s 0).head = some ⟨gp_head.a, gp_head.b + gp_succ_n.a / gp_succ_n.b⟩ :=
        squashSeq_nth_of_not_terminated s_head_eq s_succ_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = some gp_succ_n),
    convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
have some : ∀ (gp_head : Pair K) (s_head_eq : s.head = some gp_head),
  convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
Tactic: obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq