awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
h : Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast { a := 1, b := 0 })
⊢ ∃ (gp : Pair ℚ), Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast gp)

Tactic:
use Pair.mk 1 0

Premises used: OfNat.ofNat, GenContFract.Pair.mk
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ Eq.{u_1 + 1} (α := Pair K) { a := 1, b := 0 } (Pair.map Rat.cast { a := 1, b := 0 })

Tactic:
simp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
this : ∃ (conts : Pair ℚ), { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts

Tactic:
simpa [contsAux]

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
succ : ∃ (conts : Pair ℚ), { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (HAdd.hAdd (α := ℕ) 0 1) = Pair.map Rat.cast conts

Tactic:
suffices ∃ conts : Pair ℚ, Pair.mk g.h 1 = conts.map (↑) by simpa [contsAux]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
h : { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast { a := (↑⌊v⌋ : ℚ), b := 1 }
⊢ ∃ (conts : Pair ℚ), { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast conts

Tactic:
use Pair.mk ⌊v⌋ 1

Premises used: Int.floor, OfNat.ofNat, GenContFract.Pair.mk
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ { a := g.h, b := 1 : Pair K } = Pair.map Rat.cast { a := (↑⌊v⌋ : ℚ), b := 1 }

Tactic:
simp [g]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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
⊢ ∃ (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)

Premises used: lt_add_one, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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
⊢ ∃ (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

Premises used: GenContFract.s, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
h : (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast pred_conts
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast conts

Tactic:
use pred_conts
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ 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
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
this : g.contsAux (n + 2) = g.contsAux (n + 1)
⊢ (of v).contsAux (n + 1 + 1) = Pair.map Rat.cast pred_conts

Tactic:
simp only [g, this, pred_conts_eq]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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
⊢ ∃ (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

Premises used: lt_of_le_of_lt, lt_add_one, Nat.le_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
⊢ gp_n.a = 1 ∧ ∃ (z : ℤ), gp_n.b = (↑z : K)

Tactic:
of_partNum_eq_one_and_exists_int_partDen_eq s_ppred_nth_eq

Premises used: GenContFract.of_partNum_eq_one_and_exists_int_partDen_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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
⊢ ∃ (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

Premises used: GenContFract.Pair.b, GenContFract.Pair.a, GenContFract.of_partNum_eq_one_and_exists_int_partDen_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
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
⊢ ∃ (conts : Pair ℚ), (of v).contsAux (n + 1 + 1) = 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]

Premises used: GenContFract.contsAux_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
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)
⊢ ∃ (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:
use nextConts 1 (z : ℚ) ppred_conts pred_conts

Premises used: Int.cast, GenContFract.nextConts, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
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)
⊢ {
      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:
cases ppred_conts
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 ℚ }
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 ℚ })
⊢ {
      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 pred_conts
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
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_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:
simp [nextConts, nextNum, nextDen]

Premises used: GenContFract.nextDen, GenContFract.nextConts, GenContFract.nextNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
rw : ∃ (conts : Pair ℚ), (of v).contsAux (n + 1) = Pair.map Rat.cast conts
⊢ ∃ (conts : Pair ℚ), (of v).conts n = Pair.map Rat.cast conts

Tactic:
rw [nth_cont_eq_succ_nth_contAux]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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).contsAux (n + 1) = Pair.map Rat.cast conts

Tactic:
exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

Premises used: GenContFract.exists_gcf_pair_rat_eq_of_nth_contsAux, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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).contsAux (n + 1) = Pair.map Rat.cast conts

Tactic:
exact exists_gcf_pair_rat_eq_of_nth_contsAux v <| n + 1

Premises used: GenContFract.exists_gcf_pair_rat_eq_of_nth_contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
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)
⊢ ∃ (q : ℚ), (of v).nums n = (↑q : K)

Tactic:
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨a, _⟩, nth_cont_eq⟩

Premises used: GenContFract.exists_gcf_pair_rat_eq_nth_conts
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 ℚ }
h : (of v).nums n = (↑a : K)
⊢ ∃ (q : ℚ), (of v).nums n = (↑q : K)

Tactic:
use a
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 ℚ }
⊢ (of v).nums n = (↑a : K)

Tactic:
simp [num_eq_conts_a, nth_cont_eq]

Premises used: GenContFract.num_eq_conts_a
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
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)
⊢ ∃ (q : ℚ), (of v).dens n = (↑q : K)

Tactic:
rcases exists_gcf_pair_rat_eq_nth_conts v n with ⟨⟨_, b⟩, nth_cont_eq⟩

Premises used: GenContFract.exists_gcf_pair_rat_eq_nth_conts
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 ℚ }
h : (of v).dens n = (↑b : K)
⊢ ∃ (q : ℚ), (of v).dens n = (↑q : K)

Tactic:
use b
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 ℚ }
⊢ (of v).dens n = (↑b : K)

Tactic:
simp [den_eq_conts_b, nth_cont_eq]

Premises used: GenContFract.den_eq_conts_b
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
v : K
n : ℕ
rcases : ∀ (Aₙ : ℚ) (nth_num_eq : (of v).nums n = (↑Aₙ : K)), ∃ (q : ℚ), (of v).convs n = (↑q : K)
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)

Tactic:
rcases exists_rat_eq_nth_num v n with ⟨Aₙ, nth_num_eq⟩

Premises used: GenContFract.exists_rat_eq_nth_num
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
rcases : ∀ (Bₙ : ℚ) (nth_den_eq : (of v).dens n = (↑Bₙ : K)), ∃ (q : ℚ), (of v).convs n = (↑q : K)
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)

Tactic:
rcases exists_rat_eq_nth_den v n with ⟨Bₙ, nth_den_eq⟩

Premises used: GenContFract.exists_rat_eq_nth_den
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
h : (of v).convs n = (↑(Aₙ / Bₙ) : K)
⊢ ∃ (q : ℚ), (of v).convs n = (↑q : K)

Tactic:
use Aₙ / Bₙ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
⊢ (of v).convs n = (↑(Aₙ / Bₙ) : K)

Tactic:
simp [nth_num_eq, nth_den_eq, conv_eq_num_div_den]

Premises used: GenContFract.conv_eq_num_div_den
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 = (of v).convs n

Tactic:
of_correctness_of_terminates terminates

Premises used: GenContFract.of_correctness_of_terminates
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
obtain : ∀ (n : ℕ) (v_eq_conv : v = (of v).convs n), ∃ (q : ℚ), v = (↑q : K)
⊢ ∃ (q : ℚ), v = (↑q : K)

Tactic:
obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates

Premises used: GenContFract.of_correctness_of_terminates
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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 : ℚ), (of v).convs n = (↑q : K)

Tactic:
exists_rat_eq_nth_conv v n

Premises used: GenContFract.exists_rat_eq_nth_conv
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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
obtain : ∀ (q : ℚ) (conv_eq_q : (of v).convs n = (↑q : K)), ∃ (q : ℚ), v = (↑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

Premises used: GenContFract.convs, GenContFract.of, GenContFract.exists_rat_eq_nth_conv
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
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)
⊢ v = (↑q : K)

Tactic:
have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q