awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K} (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b),
    g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
b : K
nth_partDen_eq : g.partDens.get? n = some b
⊢ b ≠ 0
have obtain : ∀ (gp : Pair K) (s_nth_eq : g.s.get? n = some gp) (nth_partDen_eq : g.partDens.get? n = some gp.b), gp.b ≠ 0
Tactic: obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b :=
          exists_s_b_of_partDen nth_partDen_eq
Cleared hypotheses: b, nth_partDen_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K} (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b),
    g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = g'.convs n
have this : ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0
Tactic: have : ∀ ⦃b⦄, g.partDens.get? n = some b → b ≠ 0 := by
        intro b nth_partDen_eq
        obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b :=
          exists_s_b_of_partDen nth_partDen_eq
        exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ g.convs n = g.convs' n
have zero : ∀ {g : GenContFract K} (s_pos : ∀ {gp : Pair K} {m : ℕ}, m < 0 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b),
  g.convs 0 = g.convs' 0
Tactic: induction n generalizing g with
  | zero => simp
  | succ n IH =>
    let g' := squashGCF g n
    -- first replace the rhs with the squashed computation
    suffices g.convs (n + 1) = g'.convs' n by
      rwa [succ_nth_conv'_eq_squashGCF_nth_conv']
    rcases Decidable.em (TerminatedAt g n) with terminatedAt_n | not_terminatedAt_n
    · have g'_eq_g : g' = g := squashGCF_eq_self_of_terminated terminatedAt_n
      rw [convs_stable_of_terminated n.le_succ terminatedAt_n, g'_eq_g, IH _]
      intro _ _ m_lt_n s_mth_eq
      exact s_pos (Nat.lt_succ_of_lt m_lt_n) s_mth_eq
    · suffices g.convs (n + 1) = g'.convs n by
        -- invoke the IH for the squashed gcf
        rwa [← IH]
        intro gp' m m_lt_n s_mth_eq'
        -- case distinction on m + 1 = n or m + 1 < n
        rcases m_lt_n with n | succ_m_lt_n
        · -- the difficult case at the squashed position: we first obtain the values from
          -- the sequence
          obtain ⟨gp_succ_m, s_succ_mth_eq⟩ : ∃ gp_succ_m, g.s.get? (m + 1) = some gp_succ_m :=
            Option.ne_none_iff_exists'.mp not_terminatedAt_n
          obtain ⟨gp_m, mth_s_eq⟩ : ∃ gp_m, g.s.get? m = some gp_m :=
            g.s.ge_stable m.le_succ s_succ_mth_eq
          -- we then plug them into the recurrence
          suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
            have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
              squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
            grind
          have m_lt_n : m < m.succ := Nat.lt_succ_self m
          refine ⟨(s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).left, ?_⟩
          refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_
          have : 0 < gp_succ_m.a ∧ 0 < gp_succ_m.b := s_pos (lt_add_one <| m + 1) s_succ_mth_eq
          exact div_pos this.left this.right
        · -- the easy case: before the squashed position, nothing changes
          refine s_pos (Nat.lt_succ_of_lt <| Nat.lt_succ_of_lt succ_m_lt_n) ?_
          exact Eq.trans (squashGCF_nth_of_lt succ_m_lt_n).symm s_mth_eq'
      -- now the result follows from the fact that the convergents coincide at the squashed position
      -- as established in `succ_nth_conv_eq_squashGCF_nth_conv`.
      have : ∀ ⦃b⦄, g.partDens.get? n = some b → b ≠ 0 := by
        intro b nth_partDen_eq
        obtain ⟨gp, s_nth_eq, ⟨refl⟩⟩ : ∃ gp, g.s.get? n = some gp ∧ gp.b = b :=
          exists_s_b_of_partDen nth_partDen_eq
        exact (ne_of_lt (s_pos (lt_add_one n) s_nth_eq).right).symm
      exact succ_nth_conv_eq_squashGCF_nth_conv @this
Cleared hypotheses: n, g, s_pos
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
⊢ (↑(↑c : SimpContFract K) : GenContFract K).convs = (↑(↑c : SimpContFract K) : GenContFract K).convs'
have a : ∀ (n : ℕ),
  (↑(↑c : SimpContFract K) : GenContFract K).convs.get n =
    Stream'.get (↑(↑c : SimpContFract K) : GenContFract K).convs' n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
n : ℕ
⊢ (↑(↑c : SimpContFract K) : GenContFract K).convs.get n =
    Stream'.get (↑(↑c : SimpContFract K) : GenContFract K).convs' n
have a : ∀ {gp : Pair K} {m : ℕ}, m < n → (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
Tactic: apply GenContFract.convs_eq_convs'
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
⊢ (g.contsAux (n + 1)).a * (g.contsAux (n + 1 + 1)).b - (g.contsAux (n + 1)).b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have succ : let pred_conts := g.contsAux (n + 1);
∀
  (IH :
    ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
      (g.contsAux n).a * pred_conts.b - (g.contsAux n).b * pred_conts.a =
        ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0)
  (pred_conts_eq : pred_conts = g.contsAux (n + 1)),
  pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Tactic: set pred_conts := contsAux g (n + 1) with pred_conts_eq
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (hypothesis)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    (g.contsAux n).a * pred_conts.b - (g.contsAux n).b * pred_conts.a =
      ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
pred_conts_eq : pred_conts = g.contsAux (n + 1)
IH₁ :
  let ppred_conts := g.contsAux n;
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pred_conts.a * (g.contsAux (n + 1 + 1)).b - pred_conts.b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have ppred_conts_eq : let ppred_conts := g.contsAux n;
ppred_conts = g.contsAux n
Tactic: set ppred_conts := contsAux g n with ppred_conts_eq
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (hypothesis)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have not_terminated_at_n : ¬g.TerminatedAt n
Tactic: have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have succ : ∀ (gp : Pair K) (s_nth_eq : g.s.get? n = some gp),
  pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Tactic: obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
      Option.ne_none_iff_exists'.1 not_terminated_at_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have rw : pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a
Tactic: rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * (g.contsAux (n + 2)).b - pB * (g.contsAux (n + 2)).a = (ppA * pB - ppB * pA) * -gp.a
have rw : pA *
      { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
          b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b : Pair K }.b -
    pB *
      { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
          b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b : Pair K }.a =
  (ppA * pB - ppB * pA) * -gp.a
Tactic: rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n_1 n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have succ : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
Tactic: suffices ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, - (g.partNums.get? i).getD 0 by
      rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
      subst conts
      rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
      ring
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
    ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
have zero : ∀ (hyp : Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)),
  (g.contsAux 0).a * (g.contsAux (HAdd.hAdd (α := ℕ) 0 1)).b -
      (g.contsAux 0).b * (g.contsAux (HAdd.hAdd (α := ℕ) 0 1)).a =
    ∏ i ∈ Finset.range 0, -(g.partNums.get? i).getD 0
Tactic: induction n with
  | zero => simp [contsAux]
  | succ n IH =>
    -- set up some shorthand notation
    let conts := contsAux g (n + 2)
    set pred_conts := contsAux g (n + 1) with pred_conts_eq
    set ppred_conts := contsAux g n with ppred_conts_eq
    let pA := pred_conts.a
    let pB := pred_conts.b
    let ppA := ppred_conts.a
    let ppB := ppred_conts.b
    -- let's change the goal to something more readable
    change pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
    have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
    obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
      Option.ne_none_iff_exists'.1 not_terminated_at_n
    -- unfold the recurrence relation for `conts` once and simplify to derive the following
    suffices ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, - (g.partNums.get? i).getD 0 by
      rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
      subst conts
      rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
      ring
    exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)
zero :
  ∀ (hyp : Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)),
    (g.contsAux 0).a * (g.contsAux (HAdd.hAdd (α := ℕ) 0 1)).b -
        (g.contsAux 0).b * (g.contsAux (HAdd.hAdd (α := ℕ) 0 1)).a =
      ∏ i ∈ Finset.range 0, -(g.partNums.get? i).getD 0
⊢ (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
    ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
have succ : ∀ (n : ℕ)
  (IH :
    ∀ (hyp : n = 0 ∨ ¬g.TerminatedAt (n - 1)),
      (g.contsAux n).a * (g.contsAux (n + 1)).b - (g.contsAux n).b * (g.contsAux (n + 1)).a =
        ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0)
  (hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)),
  (g.contsAux (n + 1)).a * (g.contsAux (n + 1 + 1)).b - (g.contsAux (n + 1)).b * (g.contsAux (n + 1 + 1)).a =
    ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Tactic: induction n with
  | zero => simp [contsAux]
  | succ n IH =>
    -- set up some shorthand notation
    let conts := contsAux g (n + 2)
    set pred_conts := contsAux g (n + 1) with pred_conts_eq
    set ppred_conts := contsAux g n with ppred_conts_eq
    let pA := pred_conts.a
    let pB := pred_conts.b
    let ppA := ppred_conts.a
    let ppB := ppred_conts.b
    -- let's change the goal to something more readable
    change pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
    have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
    obtain ⟨gp, s_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
      Option.ne_none_iff_exists'.1 not_terminated_at_n
    -- unfold the recurrence relation for `conts` once and simplify to derive the following
    suffices ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, - (g.partNums.get? i).getD 0 by
      rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]
      subst conts
      rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]
      ring
    exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n
Cleared hypotheses: hyp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have inl : ∀ (terminatedAt_n : g.TerminatedAt n),
  g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Tactic: rcases em <| TerminatedAt g n with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
inl :
  ∀ (terminatedAt_n : g.TerminatedAt n),
    g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have inr : ∀ (not_terminatedAt_n : ¬g.TerminatedAt n),
  g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
Tactic: rcases em <| TerminatedAt g n with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
⊢ g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
have inl : g.nums n * g.dens n - g.dens n * g.nums n =
  HMul.hMul (α := K) (∏ x ∈ Finset.range n, -(g.partNums.get? x).getD 0) (-Option.getD none 0)
Tactic: rw [dens_stable_of_terminated n.le_succ terminatedAt_n,
      nums_stable_of_terminated n.le_succ terminatedAt_n, Finset.prod_range_succ,
      partNum_none_iff_s_none.mpr terminatedAt_n]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (hypothesis)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
have hi₁ : i < n + 1
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
have obtain : ∀ (gp : Pair K) (s_ith_eq : (↑s : GenContFract K).s.get? i = some gp),
  -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
Tactic: obtain ⟨gp, s_ith_eq⟩ : ∃ gp, (↑s : GenContFract K).s.get? i = some gp :=
      Option.ne_none_iff_exists'.1 <| mt (terminated_stable <| Nat.le_of_succ_le_succ hi) ‹_›
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s : GenContFract K).s.get? i = some gp
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
have rw : -(some gp.a).getD 0 = -1
Tactic: rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s : GenContFract K).s.get? i = some gp
rw : -(some gp.a).getD 0 = -1
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
have rw₁ : Eq.{u_1 + 1} (α := K) (-Option.getD (some 1) 0) (-1)
Tactic: rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
i : ℕ
hi : i < n + 1
gp : Pair K
s_ith_eq : (↑s : GenContFract K).s.get? i = some gp
rw : -(some gp.a).getD 0 = -1
rw₁ : Eq.{u_1 + 1} (α := K) (-Option.getD (some 1) 0) (-1)
⊢ -((↑s : GenContFract K).partNums.get? i).getD 0 = -1
have rw₂ : Eq.{u_1 + 1} (α := K) (-1) (-1)
Tactic: rw [partNum_eq_s_a s_ith_eq, s.property i gp.a <| partNum_eq_s_a s_ith_eq, Option.getD_some]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
⊢ ∏ i ∈ Finset.range (n + 1), -1 = HPow.hPow (α := K) (-1) (n + 1)
have rw : HPow.hPow (α := K) (-1) (Finset.range (n + 1)).card = HPow.hPow (α := K) (-1) (n + 1)
Tactic: rw [Finset.prod_const, Finset.card_range]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Determinant (goal)
Goal:
K : Type u_1
inst : Field K
s : SimpContFract K
n : ℕ
not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n
rw : HPow.hPow (α := K) (-1) (Finset.range (n + 1)).card = HPow.hPow (α := K) (-1) (n + 1)
⊢ ∏ i ∈ Finset.range (n + 1), -1 = HPow.hPow (α := K) (-1) (n + 1)
have rw₁ : HPow.hPow (α := K) (-1) (n + 1) = HPow.hPow (α := K) (-1) (n + 1)
Tactic: rw [Finset.prod_const, Finset.card_range]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
n : ℕ
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)
have terminatedAt_n₁ : g.s.get? n = none
Tactic: rw [terminatedAt_iff_s_none] at terminatedAt_n
Cleared hypotheses: terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
⊢ g.contsAux m = g.contsAux (n + 1)
have refine : ∀ (k : ℕ) (hnk : n.succ ≤ k) (hk : g.contsAux k = g.contsAux (n + 1)), g.contsAux (k + 1) = g.contsAux (n + 1)
Tactic: refine Nat.le_induction rfl (fun k hnk hk => ?_) _ n_lt_m
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ k
hk : g.contsAux k = g.contsAux (n + 1)
⊢ g.contsAux (k + 1) = g.contsAux (n + 1)
have rcases : ∀ (k : ℕ) (hnk : n.succ ≤ n + k + 1) (hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)),
  g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)
Tactic: rcases Nat.exists_eq_add_of_lt hnk with ⟨k, rfl⟩
Cleared hypotheses: k, hnk, hk