awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
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⦄, 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
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
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
this : ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = g'.convs n

Tactic:
succ_nth_conv_eq_squashGCF_nth_conv @this

Premises used: GenContFract.succ_nth_conv_eq_squashGCF_nth_conv
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
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
this : ∀ ⦃b : K⦄, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = g'.convs n

Tactic:
exact succ_nth_conv_eq_squashGCF_nth_conv @this

Premises used: GenContFract.succ_nth_conv_eq_squashGCF_nth_conv
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
a :
  ∀ (n : ℕ),
    (↑(↑c : SimpContFract K) : GenContFract K).convs.get n =
      Stream'.get (↑(↑c : SimpContFract K) : GenContFract K).convs' n
⊢ (↑(↑c : SimpContFract K) : GenContFract K).convs = (↑(↑c : SimpContFract K) : GenContFract K).convs'

Tactic:
ext n
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
n : ℕ
a : ∀ {gp : Pair K} {m : ℕ}, m < n → (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ (↑(↑c : SimpContFract K) : GenContFract K).convs.get n =
    Stream'.get (↑(↑c : SimpContFract K) : GenContFract K).convs' n

Tactic:
apply GenContFract.convs_eq_convs'

Premises used: GenContFract.convs_eq_convs'
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
a : m < n → (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
⊢ m < n → (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b

Tactic:
_
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
h : m < n
s_nth_eq : (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b

Tactic:
⟨zero_lt_one.trans_le ((c : SimpContFract K).property m gp.a
    (partNum_eq_s_a s_nth_eq)).symm.le, c.property m gp.b <| partDen_eq_s_b s_nth_eq⟩

Premises used: GenContFract.Pair.b, GenContFract.Pair.a, Eq.le, zero_lt_one, GenContFract.partNum_eq_s_a, LT.lt.trans_le, And.intro, GenContFract.partDen_eq_s_b, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : ContFract K
n : ℕ
gp : Pair K
m : ℕ
h : m < n
s_nth_eq : (↑(↑c : SimpContFract K) : GenContFract K).s.get? m = some gp
⊢ 0 < gp.a ∧ 0 < gp.b

Tactic:
exact ⟨zero_lt_one.trans_le ((c : SimpContFract K).property m gp.a
    (partNum_eq_s_a s_nth_eq)).symm.le, c.property m gp.b <| partDen_eq_s_b s_nth_eq⟩
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
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:
simp [contsAux]

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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)
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
⊢ (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:
set pred_conts := contsAux g (n + 1) with pred_conts_eq

Premises used: GenContFract.contsAux, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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)
⊢ 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

Tactic:
set ppred_conts := contsAux g n with ppred_conts_eq

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
⊢ let ppred_conts := g.contsAux n;
  ppred_conts = g.contsAux n

Tactic:
set ppred_conts := contsAux g n with ppred_conts_eq

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
succ : pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(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

Tactic:
change pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Premises used: GenContFract.Pair.b, GenContFract.Pair.a, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
⊢ ¬g.TerminatedAt n

Tactic:
have not_terminated_at_n : ¬TerminatedAt g n := Or.resolve_left hyp n.succ_ne_zero
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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), g.s.get? n = some gp

Tactic:
Option.ne_none_iff_exists'.1 not_terminated_at_n

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
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
⊢ 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

Premises used: GenContFract.s, Option.ne_none_iff_exists', Iff.mp, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
rw : pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]

Premises used: Option.getD_some, GenContFract.partNum_eq_s_a, Finset.prod_range_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
subst : pA * (g.contsAux (n + 2)).b - pB * (g.contsAux (n + 2)).a = (ppA * pB - ppB * pA) * -gp.a
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a

Tactic:
subst conts
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
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
⊢ pA * (g.contsAux (n + 2)).b - pB * (g.contsAux (n + 2)).a = (ppA * pB - ppB * pA) * -gp.a

Tactic:
rw [contsAux_recurrence s_nth_eq ppred_conts_eq pred_conts_eq]

Premises used: GenContFract.contsAux_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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 *
        { 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:
ring
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
succ : 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

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
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
⊢ ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0

Tactic:
IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n

Premises used: mt, Nat.sub_le, GenContFract.terminated_stable, OfNat.ofNat, Or.inr
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
⊢ ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0

Tactic:
exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n

Premises used: mt, Nat.sub_le, GenContFract.terminated_stable, OfNat.ofNat, Or.inr
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
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
⊢ (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

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

Premises used: GenContFract.s, GenContFract.contsAux, Finset.range, HAdd.hAdd, OfNat.ofNat, Or.inr, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
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
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
⊢ 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

Premises used: em, GenContFract.TerminatedAt
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
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)
⊢ 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:
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]

Premises used: GenContFract.nums_stable_of_terminated, Iff.mpr, GenContFract.dens_stable_of_terminated, Nat.le_succ, Finset.prod_range_succ, GenContFract.partNum_none_iff_s_none
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
terminatedAt_n : g.TerminatedAt n
⊢ 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:
grind
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
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:
determinant_aux <| Or.inr <| not_terminatedAt_n

Premises used: GenContFract.contsAux, GenContFract.dens, GenContFract.conts, _private.0.GenContFract.determinant_aux, GenContFract.nums, Stream'.get, Stream'.map, Stream'.tail, Or.inr
-- Module: Mathlib.Algebra.ContinuedFractions.Determinant
Goal:
K : Type u_1
inst : Field K
g : GenContFract K
n : ℕ
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:
exact determinant_aux <| Or.inr <| not_terminatedAt_n

Premises used: _private.0.GenContFract.determinant_aux, Or.inr