awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (↑⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹

Tactic:
floor_le ifp_n.fr⁻¹

Premises used: Inv.inv, GenContFract.IntFractPair.fr, Int.floor_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : FloorRing K
ifp_n ifp_succ_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (↑⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹

Tactic:
exact floor_le ifp_n.fr⁻¹

Premises used: Inv.inv, GenContFract.IntFractPair.fr, Int.floor_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ ∃ (gp_n : Pair K), (of v).s.get? n = some gp_n ∧ gp_n.b = b

Tactic:
exists_s_b_of_partDen nth_partDen_eq

Premises used: GenContFract.exists_s_b_of_partDen
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
obtain :
  ∀ (gp_n : Pair K) (nth_s_eq : (of v).s.get? n = some gp_n) (nth_partDen_eq : (of v).partDens.get? n = some gp_n.b),
    1 ≤ gp_n.b
⊢ 1 ≤ b

Tactic:
obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq

Premises used: GenContFract.s, GenContFract.of, GenContFract.exists_s_b_of_partDen, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp_n.b

Tactic:
IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Premises used: GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
obtain :
  ∀ (ifp_n : IntFractPair K) (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n)
    (ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b), 1 ≤ gp_n.b
⊢ 1 ≤ gp_n.b

Tactic:
obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Premises used: GenContFract.Pair.b, GenContFract.IntFractPair.stream, HAdd.hAdd, GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b
rw : LE.le.{u_1} (α := K) 1 (↑ifp_n.b : K)
⊢ 1 ≤ gp_n.b

Tactic:
rw [← ifp_n_b_eq_gp_n_b]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b
⊢ LE.le.{u_1} (α := K) 1 (↑ifp_n.b : K)

Tactic:
mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq

Premises used: Int.cast, congrArg, cast, LE.le, Int.cast_le._simp_1, GenContFract.IntFractPair.one_le_succ_nth_stream_b, GenContFract.IntFractPair.b, congrFun', Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b
⊢ LE.le.{u_1} (α := K) 1 (↑ifp_n.b : K)

Tactic:
exact mod_cast IntFractPair.one_le_succ_nth_stream_b succ_nth_stream_eq

Premises used: GenContFract.IntFractPair.one_le_succ_nth_stream_b
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
⊢ ∃ (ifp : IntFractPair K), IntFractPair.stream v (n + 1) = some ifp ∧ (↑ifp.b : K) = gp.b

Tactic:
IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Premises used: GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
obtain :
  ∀ (ifp : IntFractPair K) (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp),
    gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)
⊢ gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)

Tactic:
obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq

Premises used: GenContFract.IntFractPair.stream, HAdd.hAdd, GenContFract.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
⊢ (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }

Tactic:
have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : some gp = some { a := 1, b := (↑ifp.b : K) }), some gp = some { a := 1, b := (↑ifp.b : K) }
⊢ some gp = some { a := 1, b := (↑ifp.b : K) }

Tactic:
rwa [nth_s_eq] at this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
⊢ some gp = some { a := 1, b := (↑ifp.b : K) }

Tactic:
have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this_1 : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
this : some gp = some { a := 1, b := (↑ifp.b : K) }
⊢ gp = { a := 1, b := (↑ifp.b : K) }

Tactic:
injection this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
⊢ gp = { a := 1, b := (↑ifp.b : K) }

Tactic:
have : gp = ⟨1, ifp.b⟩ := by
    have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
    have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
    injection this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : gp = { a := 1, b := (↑ifp.b : K) }
⊢ gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
⊢ ∃ (gp : Pair K), (of v).s.get? n = some gp ∧ gp.a = a

Tactic:
exists_s_a_of_partNum nth_partNum_eq

Premises used: GenContFract.exists_s_a_of_partNum
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
obtain : ∀ (gp : Pair K) (nth_s_eq : (of v).s.get? n = some gp) (gp_a_eq_a_n : gp.a = a), a = 1
⊢ a = 1

Tactic:
obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
    exists_s_a_of_partNum nth_partNum_eq

Premises used: GenContFract.s, GenContFract.of, GenContFract.exists_s_a_of_partNum, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
⊢ gp.a = 1

Tactic:
have : gp.a = 1 := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).left
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : gp.a = 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a = 1), a = 1
⊢ a = 1

Tactic:
rwa [gp_a_eq_a_n] at this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ ∃ (gp : Pair K), (of v).s.get? n = some gp ∧ gp.b = b

Tactic:
exists_s_b_of_partDen nth_partDen_eq

Premises used: GenContFract.exists_s_b_of_partDen
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
obtain : ∀ (gp : Pair K) (nth_s_eq : (of v).s.get? n = some gp) (gp_b_eq_b_n : gp.b = b), ∃ (z : ℤ), b = (↑z : K)
⊢ ∃ (z : ℤ), b = (↑z : K)

Tactic:
obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b :=
    exists_s_b_of_partDen nth_partDen_eq

Premises used: GenContFract.s, GenContFract.of, GenContFract.exists_s_b_of_partDen, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
⊢ ∃ (z : ℤ), gp.b = (↑z : K)

Tactic:
have : ∃ z : ℤ, gp.b = (z : K) := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).right
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
this : ∃ (z : ℤ), gp.b = (↑z : K)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : ∃ (z : ℤ), b = (↑z : K)), ∃ (z : ℤ), b = (↑z : K)
⊢ ∃ (z : ℤ), b = (↑z : K)

Tactic:
rwa [gp_b_eq_b_n] at this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ (of v).IsSimpContFract

Tactic:
fun _ _ nth_partNum_eq =>
  of_partNum_eq_one nth_partNum_eq

Premises used: GenContFract.of_partNum_eq_one, GenContFract.IsSimpContFract
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
⊢ IsContFract (of v)

Tactic:
fun _ _ nth_partDen_eq =>
  lt_of_lt_of_le zero_lt_one (of_one_le_get?_partDen nth_partDen_eq)

Premises used: SimpContFract.IsContFract, zero_lt_one, GenContFract.of_one_le_get?_partDen, lt_of_lt_of_le
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
zero :
  ∀ (IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : LE.le (α := ℕ) 0 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 2)), (↑(fib 0) : K) ≤ ((of v).contsAux 0).b
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HAdd.hAdd (α := ℕ) 0 1 - 2)),
    (↑(fib (HAdd.hAdd (α := ℕ) 0 1)) : K) ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b
succ₁ :
  ∀ (n : ℕ) (IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)),
    (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
⊢ (↑(fib n) : K) ≤ ((of v).contsAux n).b

Tactic:
rcases n with (_ | _ | n)
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : LE.le (α := ℕ) 0 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 2)
⊢ (↑(fib 0) : K) ≤ ((of v).contsAux 0).b

Tactic:
simp [contsAux]

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HAdd.hAdd (α := ℕ) 0 1 - 2)
⊢ (↑(fib (HAdd.hAdd (α := ℕ) 0 1)) : K) ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b

Tactic:
simp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
⊢ ¬n + 2 ≤ 1

Tactic:
lia
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
⊢ ¬n + 2 ≤ 1

Tactic:
have : ¬n + 2 ≤ 1 := by lia
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
⊢ ¬g.TerminatedAt n

Tactic:
have not_terminatedAt_n : ¬g.TerminatedAt n := Or.resolve_left hyp this
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ ∃ (gp : Pair K), g.s.get? n = some gp

Tactic:
Option.ne_none_iff_exists'.mp not_terminatedAt_n

Premises used: Option.ne_none_iff_exists', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
succ :
  ∀ (gp : Pair K) (s_ppred_nth_eq : g.s.get? n = some gp), (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
obtain ⟨gp, s_ppred_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
          Option.ne_none_iff_exists'.mp not_terminatedAt_n

Premises used: GenContFract.s, Option.ne_none_iff_exists', Iff.mp, Stream'.Seq.get?
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
⊢ let pconts := g.contsAux (n + 1);
  pconts = g.contsAux (n + 1)

Tactic:
set pconts := g.contsAux (n + 1) with pconts_eq

Premises used: GenContFract.contsAux, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
⊢ let ppconts := g.contsAux n;
  ppconts = g.contsAux n

Tactic:
set ppconts := g.contsAux n with ppconts_eq

Premises used: GenContFract.contsAux
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
succ : (↑(fib (n + 2)) : K) ≤ ((of v).contsAux (n + 2)).b
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
simp only [Nat.add_assoc, Nat.reduceAdd]

Premises used: Nat.reduceAdd, Nat.add_assoc
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this_1 : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
this : HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ gp.a * ppconts.b + gp.b * pconts.b
⊢ (↑(fib (n + 2)) : K) ≤ ((of v).contsAux (n + 2)).b

Tactic:
simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]

Premises used: Nat.fib_add_two, add_comm, GenContFract.contsAux_recurrence
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
succ : HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ gp.a * ppconts.b + gp.b * pconts.b
⊢ (↑(fib (n + 2)) : K) ≤ ((of v).contsAux (n + 2)).b

Tactic:
suffices (fib n : K) + fib (n + 1) ≤ gp.a * ppconts.b + gp.b * pconts.b by
          simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this_1 : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
this : HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ ppconts.b + gp.b * pconts.b
⊢ HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ gp.a * ppconts.b + gp.b * pconts.b

Tactic:
simpa [of_partNum_eq_one <| partNum_eq_s_a s_ppred_nth_eq]

Premises used: GenContFract.of_partNum_eq_one, GenContFract.partNum_eq_s_a