awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
zero :
  ∀ (IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
    ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux n = Pair.map Rat.cast conts
have succ : ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
  ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
zero :
  ∀ (IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
    ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
    ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux n = Pair.map Rat.cast conts
have succ₁ : ∀ (n : ℕ) (IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts),
  ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux 0 = Pair.map Rat.cast conts
have zero : ∃ (gp : Pair ℚ), Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast gp)
Tactic: suffices ∃ gp : Pair ℚ, Pair.mk (1 : K) 0 = gp.map (↑) by simpa [contsAux]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < 0, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (gp : Pair ℚ), Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast gp)
have h : Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast { a := 1, b := 0 })
Tactic: use Pair.mk 1 0
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts
have succ : ∃ (conts : Pair ℚ), { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast conts
Tactic: suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast conts
have h : { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast { a := (↑⌊v⌋ : ℚ), b := 1 }
Tactic: use Pair.mk ⌊v⌋ 1
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ : ∀ (pred_conts : Pair ℚ) (pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts),
  ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: obtain ⟨pred_conts, pred_conts_eq⟩ := IH (n + 1) <| lt_add_one (n + 1)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ : ∀ (s_ppred_nth_eq : g.s.get? n = none), ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
succ : ∀ (s_ppred_nth_eq : g.s.get? n = none), ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ₁ : ∀ (gp_n : Pair K) (s_ppred_nth_eq : g.s.get? n = some gp_n),
  ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: rcases s_ppred_nth_eq : g.s.get? n with gp_n | gp_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have h : (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast pred_conts
Tactic: use pred_conts
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
s_ppred_nth_eq : g.s.get? n = none
⊢ (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast pred_conts
have this : g.contsAux (n + 2) = g.contsAux (n + 1)
Tactic: have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
            contsAux_stable_of_terminated (n + 1).le_succ s_ppred_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ : ∀ (ppred_conts : Pair ℚ) (ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts),
  ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: obtain ⟨ppred_conts, ppred_conts_eq⟩ :=
            IH n <| lt_of_le_of_lt n.le_succ <| lt_add_one <| n + 1
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ : ∀ (a_eq_one : gp_n.a = 1) (z : ℤ) (b_eq_z : gp_n.b = (↑z : K)),
  ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
Tactic: obtain ⟨a_eq_one, z, b_eq_z⟩ : gp_n.a = 1 ∧ ∃ z : ℤ, gp_n.b = (z : K) :=
            of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = (↑z : K)
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts
have succ : ∃ (conts : Pair ℚ),
  {
      a :=
        HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast ppred_conts)),
      b :=
        HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast ppred_conts)) :
      Pair K } =
    Pair.map Rat.cast conts
Tactic: simp only [g, a_eq_one, b_eq_z,
            contsAux_recurrence s_ppred_nth_eq ppred_conts_eq pred_conts_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = (↑z : K)
⊢ ∃ (conts : Pair ℚ),
    {
        a :=
          HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
            HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast ppred_conts)),
        b :=
          HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
            HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast ppred_conts)) :
        Pair K } =
      Pair.map Rat.cast conts
have h : {
    a :=
      HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
        HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast ppred_conts)),
    b :=
      HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
        HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast ppred_conts)) :
    Pair K } =
  Pair.map Rat.cast (nextConts 1 (↑z : ℚ) ppred_conts pred_conts)
Tactic: use nextConts 1 (z : ℚ) ppred_conts pred_conts
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
ppred_conts : Pair ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast ppred_conts
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = (↑z : K)
⊢ {
      a :=
        HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast ppred_conts)),
      b :=
        HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast ppred_conts)) :
      Pair K } =
    Pair.map Rat.cast (nextConts 1 (↑z : ℚ) ppred_conts pred_conts)
have h : ∀ (a b : ℚ) (ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }),
  {
      a :=
        HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast { a := a, b := b : Pair ℚ })),
      b :=
        HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast { a := a, b := b : Pair ℚ })) :
      Pair K } =
    Pair.map Rat.cast (nextConts 1 (↑z : ℚ) { a := a, b := b : Pair ℚ } pred_conts)
Tactic: cases ppred_conts
Cleared hypotheses: ppred_conts, ppred_conts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
g : GenContFract K := of v
n : ℕ
IH : ∀ m < n + 1 + 1, ∃ (conts : Pair ℚ), (of v).contsAux m = Pair.map Rat.cast conts
pred_conts : Pair ℚ
pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast pred_conts
gp_n : Pair K
s_ppred_nth_eq : g.s.get? n = some gp_n
a_eq_one : gp_n.a = 1
z : ℤ
b_eq_z : gp_n.b = (↑z : K)
a b : ℚ
ppred_conts_eq : (of v).contsAux n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }
⊢ {
      a :=
        HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast { a := a, b := b : Pair ℚ })),
      b :=
        HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast pred_conts)) +
          HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast { a := a, b := b : Pair ℚ })) :
      Pair K } =
    Pair.map Rat.cast (nextConts 1 (↑z : ℚ) { a := a, b := b : Pair ℚ } pred_conts)
have h : ∀ (a_1 b_1 : ℚ) (pred_conts_eq : (of v).contsAux (n + 1) = Pair.map Rat.cast { a := a_1, b := b_1 : Pair ℚ }),
  {
      a :=
        HMul.hMul (α := K) (↑z : K) (Pair.a (Pair.map Rat.cast { a := a_1, b := b_1 : Pair ℚ })) +
          HMul.hMul (α := K) 1 (Pair.a (Pair.map Rat.cast { a := a, b := b : Pair ℚ })),
      b :=
        HMul.hMul (α := K) (↑z : K) (Pair.b (Pair.map Rat.cast { a := a_1, b := b_1 : Pair ℚ })) +
          HMul.hMul (α := K) 1 (Pair.b (Pair.map Rat.cast { a := a, b := b : Pair ℚ })) :
      Pair K } =
    Pair.map Rat.cast (nextConts 1 (↑z : ℚ) { a := a, b := b : Pair ℚ } { a := a_1, b := b_1 : Pair ℚ })
Tactic: cases pred_conts
Cleared hypotheses: pred_conts, pred_conts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
⊢ ∃ (conts : Pair ℚ), (of v).conts n = Pair.map Rat.cast conts
have rw : ∃ (conts : Pair ℚ), (of v).contsAux (n + 1) = Pair.map Rat.cast conts
Tactic: rw [nth_cont_eq_succ_nth_contAux]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
⊢ ∃ (q : ℚ), (of v).nums n = (↑q : K)
have rcases : ∀ (a b : ℚ) (nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }),
  ∃ (q : ℚ), (of v).nums n = (↑q : K)
Tactic: rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
a b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }
⊢ ∃ (q : ℚ), (of v).nums n = (↑q : K)
have h : (of v).nums n = (↑a : K)
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
⊢ ∃ (q : ℚ), (of v).dens n = (↑q : K)
have rcases : ∀ (a b : ℚ) (nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }),
  ∃ (q : ℚ), (of v).dens n = (↑q : K)
Tactic: rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
a b : ℚ
nth_cont_eq : (of v).conts n = Pair.map Rat.cast { a := a, b := b : Pair ℚ }
⊢ ∃ (q : ℚ), (of v).dens n = (↑q : K)
have h : (of v).dens n = (↑b : K)
Tactic: use b
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)
have rcases : ∀ (Aₙ : ℚ) (nth_num_eq : (of v).nums n = (↑Aₙ : K)), ∃ (q : ℚ), (of v).convs n = (↑q : K)
Tactic: rcases exists_rat_eq_nth_num v n with ⟨Aₙ, nth_num_eq⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = (↑Aₙ : K)
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)
have rcases : ∀ (Bₙ : ℚ) (nth_den_eq : (of v).dens n = (↑Bₙ : K)), ∃ (q : ℚ), (of v).convs n = (↑q : K)
Tactic: rcases exists_rat_eq_nth_den v n with ⟨Bₙ, nth_den_eq⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
Aₙ : ℚ
nth_num_eq : (of v).nums n = (↑Aₙ : K)
Bₙ : ℚ
nth_den_eq : (of v).dens n = (↑Bₙ : K)
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)
have h : (of v).convs n = (↑(Aₙ / Bₙ) : K)
Tactic: use Aₙ / Bₙ
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
terminates : (of v).Terminates
⊢ ∃ (q : ℚ), v = (↑q : K)
have obtain : ∀ (n : ℕ) (v_eq_conv : v = (of v).convs n), ∃ (q : ℚ), v = (↑q : K)
Tactic: obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
⊢ ∃ (q : ℚ), v = (↑q : K)
have obtain : ∀ (q : ℚ) (conv_eq_q : (of v).convs n = (↑q : K)), ∃ (q : ℚ), v = (↑q : K)
Tactic: obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convs n = (↑q : K) := exists_rat_eq_nth_conv v n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
terminates : (of v).Terminates
n : ℕ
v_eq_conv : v = (of v).convs n
q : ℚ
conv_eq_q : (of v).convs n = (↑q : K)
⊢ ∃ (q : ℚ), v = (↑q : K)
have this : v = (↑q : K)
Tactic: have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH : Option.map (mapFr Rat.cast) (IntFractPair.stream q n) = IntFractPair.stream v n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have IH₁ : Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
  (IntFractPair.stream (↑q : K) n)
Tactic: rw [v_eq_q] at IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
ifp_n : IntFractPair ℚ
stream_q_nth_eq : IntFractPair.stream q n = some ifp_n
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have succ : ∀ (b : ℤ) (fr : ℚ) (stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }),
  Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Tactic: obtain ⟨b, fr⟩ := ifp_n
Cleared hypotheses: ifp_n, stream_q_nth_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have succ : ∀ (fr_zero : fr = 0), Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Tactic: rcases Decidable.em (fr = 0) with fr_zero | fr_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
q : ℚ
v_eq_q : v = (↑q : K)
n : ℕ
IH :
  Eq.{u_1 + 1} (α := Option (IntFractPair K)) (Option.map (mapFr Rat.cast) (IntFractPair.stream q n))
    (IntFractPair.stream (↑q : K) n)
b : ℤ
fr : ℚ
stream_q_nth_eq : IntFractPair.stream q n = some { b := b, fr := fr }
succ : ∀ (fr_zero : fr = 0), Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
⊢ Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
have succ₁ : ∀ (fr_ne_zero : ¬fr = 0), Option.map (mapFr Rat.cast) (IntFractPair.stream q (n + 1)) = IntFractPair.stream v (n + 1)
Tactic: rcases Decidable.em (fr = 0) with fr_zero | fr_ne_zero