awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
have some : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
Tactic: suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
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
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
have this : (squashSeq s (m + 1)).head = some gp_head
Tactic: have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_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_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
have some : ∀ {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)
Tactic: induction n generalizing s gp_succ_n with
    | zero =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
      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
      simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
    | succ m IH =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq
      suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
      have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
      simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
Cleared hypotheses: n, s, gp_succ_n, 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
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (n + 1) = Option.some gp_succ_n
some :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K)
    (s_succ_nth_eq : s.get? (HAdd.hAdd (α := ℕ) 0 1) = Option.some gp_succ_n),
    convs'Aux s (HAdd.hAdd (α := ℕ) 0 2) = convs'Aux (squashSeq s 0) (HAdd.hAdd (α := ℕ) 0 1)
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
have some₁ : ∀ (m : ℕ)
  (IH :
    ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K) (s_succ_nth_eq : s.get? (m + 1) = Option.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) = Option.some gp_succ_n),
  convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)
Tactic: induction n generalizing s gp_succ_n with
    | zero =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
      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
      simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
    | succ m IH =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq
      suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
      have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
      simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
Cleared hypotheses: n, s, gp_succ_n, 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
⊢ convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
have cases : ∀ (x : Option (Pair K)) (s_succ_nth_eq : s.get? (n + 1) = x), convs'Aux s (n + 2) = convs'Aux (squashSeq s n) (n + 1)
Tactic: cases s_succ_nth_eq : s.get? <| n + 1 with
  | none =>
    rw [squashSeq_eq_self_of_terminated s_succ_nth_eq,
      convs'Aux_stable_step_of_terminated s_succ_nth_eq]
  | some gp_succ_n =>
    induction n generalizing s gp_succ_n with
    | zero =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable zero_le_one s_succ_nth_eq
      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
      simp_all [convs'Aux, Stream'.Seq.head, Stream'.Seq.get?_tail]
    | succ m IH =>
      obtain ⟨gp_head, s_head_eq⟩ : ∃ gp_head, s.head = some gp_head :=
        s.ge_stable (m + 2).zero_le s_succ_nth_eq
      suffices
        gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) =
          convs'Aux (squashSeq s (m + 1)) (m + 2)
        by simpa only [convs'Aux, s_head_eq]
      have : (squashSeq s (m + 1)).head = some gp_head :=
        (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq
      simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt 0
⊢ g.squashGCF 0 = g
have terminatedAt_n₁ : g.s.get? 0 = none
Tactic: change g.s.get? 0 = none at terminatedAt_n
Cleared hypotheses: terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n : ℕ
terminatedAt_n : g.TerminatedAt (n + 1)
⊢ g.squashGCF (n + 1) = g
have succ : ∀ (h : K) (s : Stream'.Seq (Pair K)) (terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)),
  { h := h, s := s : GenContFract K }.squashGCF (n + 1) = { h := h, s := s }
Tactic: cases g
Cleared hypotheses: g, terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
inst : DivisionRing K
n : ℕ
h : K
s : Stream'.Seq (Pair K)
terminatedAt_n : { h := h, s := s : GenContFract K }.TerminatedAt (n + 1)
⊢ { h := h, s := s : GenContFract K }.squashGCF (n + 1) = { h := h, s := s }
have succ : squashSeq s n = s
Tactic: simp only [squashGCF, mk.injEq, true_and]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt n
⊢ g.squashGCF n = g
have zero : ∀ (terminatedAt_n : g.TerminatedAt 0), g.squashGCF 0 = g
Tactic: cases n with
  | zero =>
    change g.s.get? 0 = none at terminatedAt_n
    simp only [squashGCF, terminatedAt_n]
  | succ =>
    cases g
    simp only [squashGCF, mk.injEq, true_and]
    exact squashSeq_eq_self_of_terminated terminatedAt_n
Cleared hypotheses: n, terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
terminatedAt_n : g.TerminatedAt n
zero : ∀ (terminatedAt_n : g.TerminatedAt 0), g.squashGCF 0 = g
⊢ g.squashGCF n = g
have succ : ∀ (n : ℕ) (terminatedAt_n : g.TerminatedAt (n + 1)), g.squashGCF (n + 1) = g
Tactic: cases n with
  | zero =>
    change g.s.get? 0 = none at terminatedAt_n
    simp only [squashGCF, terminatedAt_n]
  | succ =>
    cases g
    simp only [squashGCF, mk.injEq, true_and]
    exact squashSeq_eq_self_of_terminated terminatedAt_n
Cleared hypotheses: n, terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
⊢ g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
have zero : ∀ (g_s_head_eq : g.s.get? 0 = none), g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
Tactic: cases g_s_head_eq : g.s.get? 0
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
zero : ∀ (g_s_head_eq : g.s.get? 0 = none), g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
⊢ g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
have zero₁ : ∀ (val : Pair K) (g_s_head_eq : g.s.get? 0 = some val), g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
Tactic: cases g_s_head_eq : g.s.get? 0
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
⊢ g.convs' (n + 1) = (g.squashGCF n).convs' n
have zero : g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
Tactic: cases n with
  | zero =>
    cases g_s_head_eq : g.s.get? 0 <;>
      simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
  | succ =>
    simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
      squashGCF]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
zero : g.convs' (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs' 0
⊢ g.convs' (n + 1) = (g.squashGCF n).convs' n
have succ : ∀ (n : ℕ), g.convs' (n + 1 + 1) = (g.squashGCF (n + 1)).convs' (n + 1)
Tactic: cases n with
  | zero =>
    cases g_s_head_eq : g.s.get? 0 <;>
      simp [g_s_head_eq, squashGCF, convs', convs'Aux, Stream'.Seq.head]
  | succ =>
    simp only [succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq, convs',
      squashGCF]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
m_le_n : m ≤ n
⊢ g.contsAux m = (g.squashGCF n).contsAux m
have zero : ∀ (IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) (m_le_n : 0 ≤ n),
  g.contsAux 0 = (g.squashGCF n).contsAux 0
Tactic: rcases m with - | m'
Cleared hypotheses: m, IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
m : ℕ
IH : ∀ m_1 < m, m_1 ≤ n → g.contsAux m_1 = (g.squashGCF n).contsAux m_1
m_le_n : m ≤ n
zero :
  ∀ (IH : ∀ m < 0, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) (m_le_n : 0 ≤ n),
    g.contsAux 0 = (g.squashGCF n).contsAux 0
⊢ g.contsAux m = (g.squashGCF n).contsAux m
have succ : ∀ (m' : ℕ) (IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m) (m_le_n : m' + 1 ≤ n),
  g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)
Tactic: rcases m with - | m'
Cleared hypotheses: m, IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)
have succ : ∀ (IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m) (m_le_n : m' + 1 ≤ 0),
  g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)
Tactic: rcases n with - | n'
Cleared hypotheses: n, IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : DivisionRing K
m' : ℕ
IH : ∀ m < m' + 1, m ≤ n → g.contsAux m = (g.squashGCF n).contsAux m
m_le_n : m' + 1 ≤ n
succ :
  ∀ (IH : ∀ m < m' + 1, m ≤ 0 → g.contsAux m = (g.squashGCF 0).contsAux m) (m_le_n : m' + 1 ≤ 0),
    g.contsAux (m' + 1) = (g.squashGCF 0).contsAux (m' + 1)
⊢ g.contsAux (m' + 1) = (g.squashGCF n).contsAux (m' + 1)
have succ₁ : ∀ (n' : ℕ) (IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m)
  (m_le_n : m' + 1 ≤ n' + 1), g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)
Tactic: rcases n with - | n'
Cleared hypotheses: n, IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)
have succ : ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m)
  (m_le_n : HAdd.hAdd (α := ℕ) 0 1 ≤ n' + 1),
  g.contsAux (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF (n' + 1)).contsAux (HAdd.hAdd (α := ℕ) 0 1)
Tactic: rcases m' with - | m''
Cleared hypotheses: m', IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
m' n' : ℕ
IH : ∀ m < m' + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m' + 1 ≤ n' + 1
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m)
    (m_le_n : HAdd.hAdd (α := ℕ) 0 1 ≤ n' + 1),
    g.contsAux (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF (n' + 1)).contsAux (HAdd.hAdd (α := ℕ) 0 1)
⊢ g.contsAux (m' + 1) = (g.squashGCF (n' + 1)).contsAux (m' + 1)
have succ₁ : ∀ (m'' : ℕ) (IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m)
  (m_le_n : m'' + 1 + 1 ≤ n' + 1), g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
Tactic: rcases m' with - | m''
Cleared hypotheses: m', IH, m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
have m'_lt_n : m'' + 1 < n' + 1
Tactic: have m'_lt_n : m'' + 1 < n' + 1 := m_le_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
have succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
Tactic: have succ_m''th_contsAux_eq := IH (m'' + 1) (lt_add_one (m'' + 1)) m'_lt_n.le
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
have this : m'' < m'' + 2
Tactic: have : m'' < m'' + 2 := lt_add_of_pos_right m'' zero_lt_two
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
this : m'' < m'' + 2
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
have m''th_contsAux_eq : g.contsAux m'' = (g.squashGCF (n' + 1)).contsAux m''
Tactic: have m''th_contsAux_eq := IH m'' this (le_trans this.le m_le_n)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : DivisionRing K
n' m'' : ℕ
IH : ∀ m < m'' + 1 + 1, m ≤ n' + 1 → g.contsAux m = (g.squashGCF (n' + 1)).contsAux m
m_le_n : m'' + 1 + 1 ≤ n' + 1
m'_lt_n : m'' + 1 < n' + 1
succ_m''th_contsAux_eq : g.contsAux (m'' + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1)
this : m'' < m'' + 2
m''th_contsAux_eq : g.contsAux m'' = (g.squashGCF (n' + 1)).contsAux m''
⊢ g.contsAux (m'' + 1 + 1) = (g.squashGCF (n' + 1)).contsAux (m'' + 1 + 1)
have this₁ : (g.squashGCF (n' + 1)).s.get? m'' = g.s.get? m''
Tactic: have : (squashGCF g (n' + 1)).s.get? m'' = g.s.get? m'' :=
              squashGCF_nth_of_lt (Nat.succ_lt_succ_iff.mp m'_lt_n)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
have inl : ∀ (terminatedAt_n : g.TerminatedAt n), g.convs (n + 1) = (g.squashGCF n).convs n
Tactic: rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
inl : ∀ (terminatedAt_n : g.TerminatedAt n), g.convs (n + 1) = (g.squashGCF n).convs n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
have inr : ∀ (not_terminatedAt_n : ¬g.TerminatedAt n), g.convs (n + 1) = (g.squashGCF n).convs n
Tactic: rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
terminatedAt_n : g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
have this : g.squashGCF n = g
Tactic: have : squashGCF g n = g := squashGCF_eq_self_of_terminated terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
have inr : ∀ (a b : K) (s_nth_eq : g.s.get? n = some { a := a, b := b }), g.convs (n + 1) = (g.squashGCF n).convs n
Tactic: obtain ⟨⟨a, b⟩, s_nth_eq⟩ : ∃ gp_n, g.s.get? n = some gp_n :=
      Option.ne_none_iff_exists'.mp not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
n : ℕ
g : GenContFract K
inst : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
a b : K
s_nth_eq : g.s.get? n = some { a := a, b := b }
⊢ g.convs (n + 1) = (g.squashGCF n).convs n
have b_ne_zero : b ≠ 0
Tactic: have b_ne_zero : b ≠ 0 := nth_partDen_ne_zero (partDen_eq_s_b s_nth_eq)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : Field K
a b : K
b_ne_zero : b ≠ 0
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? 0 = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt 0
s_nth_eq : g.s.get? 0 = some { a := a, b := b }
⊢ g.convs (HAdd.hAdd (α := ℕ) 0 1) = (g.squashGCF 0).convs 0
have inr : (b * g.h + a) / b = g.h + a / b
Tactic: suffices (b * g.h + a) / b = g.h + a / b by
        simpa [squashGCF, s_nth_eq, conv_eq_conts_a_div_conts_b,
          conts_recurrenceAux s_nth_eq zeroth_contAux_eq_one_zero first_contAux_eq_h_one]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (goal)
Goal:
K : Type u_1
g : GenContFract K
inst : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
have inr : ∀ (pa pb : K) (s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }),
  g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
Tactic: obtain ⟨⟨pa, pb⟩, s_n'th_eq⟩ : ∃ gp_n', g.s.get? n' = some gp_n' :=
        g.s.ge_stable n'.le_succ s_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
have succ_n'th_contsAux_eq : let pred_conts := g.contsAux (n' + 1);
pred_conts = g.contsAux (n' + 1)
Tactic: set pred_conts := g.contsAux (n' + 1) with succ_n'th_contsAux_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
⊢ g.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
have n'th_contsAux_eq : let ppred_conts := g.contsAux n';
ppred_conts = g.contsAux n'
Tactic: set ppred_conts := g.contsAux n' with n'th_contsAux_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv (hypothesis)
Goal:
K : Type u_1
g : GenContFract K
inst : Field K
a b : K
b_ne_zero : b ≠ 0
n' : ℕ
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? (n' + 1) = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt (n' + 1)
s_nth_eq : g.s.get? (n' + 1) = some { a := a, b := b }
pa pb : K
s_n'th_eq : g.s.get? n' = some { a := pa, b := pb }
g' : GenContFract K := g.squashGCF (n' + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
succ_n'th_contsAux_eq : pred_conts = g.contsAux (n' + 1)
ppred_conts : Pair K := g.contsAux n'
n'th_contsAux_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.convs (n' + 1 + 1) = (g.squashGCF (n' + 1)).convs (n' + 1)
have succ_n'th_contsAux_eq' : let pred_conts' := g'.contsAux (n' + 1);
pred_conts' = g'.contsAux (n' + 1)
Tactic: set pred_conts' := g'.contsAux (n' + 1) with succ_n'th_contsAux_eq'