awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ≤ 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:
suffices (fib n : K) + fib (n + 1) ≤ ppconts.b + gp.b * pconts.b by
          simpa [of_partNum_eq_one <| partNum_eq_s_a s_ppred_nth_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 : ¬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
⊢ ¬g.TerminatedAt (n - 1)

Tactic:
have not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1) :=
          mt (terminated_stable <| Nat.sub_le n 1) not_terminatedAt_n
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ ¬g.TerminatedAt (n - 2)

Tactic:
have not_terminatedAt_ppred_n : ¬TerminatedAt g (n - 2) :=
          mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
⊢ (↑(fib n) : K) ≤ ppconts.b

Tactic:
have ppred_nth_fib_le_ppconts_B : (fib n : K) ≤ ppconts.b :=
          IH n (lt_trans (Nat.lt_add_one n) <| Nat.lt_add_one <| n + 1)
            (Or.inr not_terminatedAt_ppred_n)
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
this : (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b
⊢ HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ ppconts.b + gp.b * pconts.b

Tactic:
gcongr
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
succ : (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b
⊢ HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ ppconts.b + gp.b * pconts.b

Tactic:
suffices (fib (n + 1) : K) ≤ gp.b * pconts.b by gcongr
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
this : HMul.hMul (α := K) 1 (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b), (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b
⊢ (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b

Tactic:
rwa [one_mul] at this

Premises used: one_mul
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
succ : HMul.hMul (α := K) 1 (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b
⊢ (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b

Tactic:
suffices 1 * (fib (n + 1) : K) ≤ gp.b * pconts.b by rwa [one_mul] at 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
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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
⊢ 1 ≤ gp.b

Tactic:
have one_le_gp_b : (1 : K) ≤ gp.b :=
          of_one_le_get?_partDen (partDen_eq_s_b s_ppred_nth_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 : ¬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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
succ : (↑(fib (n + 1)) : K) ≤ pconts.b
⊢ HMul.hMul (α := K) 1 (↑(fib (n + 1)) : K) ≤ gp.b * pconts.b

Tactic:
gcongr
-- 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
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : (↑(fib n) : K) ≤ ppconts.b
one_le_gp_b : 1 ≤ gp.b
⊢ (↑(fib (n + 1)) : K) ≤ pconts.b

Tactic:
grind
-- 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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
rw : (↑(fib (n + 1)) : K) ≤ ((of v).contsAux (n + 1)).b
⊢ (↑(fib (n + 1)) : K) ≤ (of v).dens n

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.den_eq_conts_b
-- 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
hyp : Eq (α := ℕ) 0 0 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)

Tactic:
Or.inl <| le_refl 1

Premises used: le_refl, Or.inl, OfNat.ofNat
-- 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
hyp : Eq (α := ℕ) 0 0 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)

Tactic:
exact Or.inl <| le_refl 1

Premises used: le_refl, Or.inl, OfNat.ofNat
-- 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
n : ℕ
hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)

Tactic:
Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Premises used: Or.resolve_left, Nat.succ_ne_zero, Or.inr
-- 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
n : ℕ
hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)

Tactic:
exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Premises used: Or.resolve_left, Nat.succ_ne_zero, Or.inr
-- 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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
zero :
  ∀ (hyp : Eq (α := ℕ) 0 0 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)),
    HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 1)
succ : ∀ (n : ℕ) (hyp : n + 1 = 0 ∨ ¬(of v).TerminatedAt (n + 1 - 1)), n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 - 1)
⊢ n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)

Tactic:
cases n with
    | zero => exact Or.inl <| le_refl 1
    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)

Premises used: le_refl, Nat.zero, Or.inl, 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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)

Tactic:
have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
    cases n with
    | zero => exact Or.inl <| le_refl 1
    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)
-- 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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ (↑(fib (n + 1)) : K) ≤ ((of v).contsAux (n + 1)).b

Tactic:
fib_le_of_contsAux_b this

Premises used: GenContFract.fib_le_of_contsAux_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
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
this : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ (↑(fib (n + 1)) : K) ≤ ((of v).contsAux (n + 1)).b

Tactic:
exact fib_le_of_contsAux_b this

Premises used: GenContFract.fib_le_of_contsAux_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
g : GenContFract K := of v
⊢ LE.le.{u_1} (α := K) 0 0

Tactic:
rfl
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
succ : ∀ (terminated : g.TerminatedAt (n - 1)), 0 ≤ ((of v).contsAux (n + 1)).b
succ₁ : ∀ (not_terminated : ¬g.TerminatedAt (n - 1)), 0 ≤ ((of v).contsAux (n + 1)).b
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated

Premises used: HSub.hSub, Decidable.em, OfNat.ofNat, GenContFract.TerminatedAt
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
terminated : g.TerminatedAt (n - 1)
succ :
  ∀ (IH : 0 ≤ ((of v).contsAux 0).b) (terminated : g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)),
    0 ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b
succ₁ :
  ∀ (n : ℕ) (IH : 0 ≤ ((of v).contsAux (n + 1)).b) (terminated : g.TerminatedAt (n + 1 - 1)),
    0 ≤ ((of v).contsAux (n + 1 + 1)).b
⊢ 0 ≤ ((of v).contsAux (n + 1)).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
g : GenContFract K := of v
IH : 0 ≤ ((of v).contsAux 0).b
terminated : g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)
⊢ 0 ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b

Tactic:
simp [zero_le_one]

Premises used: zero_le_one
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
⊢ g.contsAux (n + 2) = g.contsAux (n + 1)

Tactic:
have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux (n + 1)).b
terminated : g.TerminatedAt (n + 1 - 1)
this : g.contsAux (n + 2) = g.contsAux (n + 1)
⊢ 0 ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
simp only [g, this, IH]
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ LE.le.{u_1} (α := K) 0 (↑(fib (n + 1)) : K)

Tactic:
mod_cast (n + 1).fib.zero_le

Premises used: Nat.zero_le, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, HAdd.hAdd, Nat.fib, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq.trans
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ (↑(fib (n + 1)) : K) ≤ ((of v).contsAux (n + 1)).b

Tactic:
fib_le_of_contsAux_b (Or.inr not_terminated)

Premises used: GenContFract.fib_le_of_contsAux_b, Or.inr
-- 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
g : GenContFract K := of v
n : ℕ
IH : 0 ≤ ((of v).contsAux n).b
not_terminated : ¬g.TerminatedAt (n - 1)
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
calc
        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Premises used: GenContFract.contsAux, Nat.zero_le, GenContFract.Pair.b, GenContFract.of, HAdd.hAdd, Nat.fib, GenContFract.fib_le_of_contsAux_b, OfNat.ofNat, Or.inr
-- 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
g : GenContFract K := of v
zero : LE.le.{u_1} (α := K) 0 0
succ : ∀ (n : ℕ) (IH : 0 ≤ ((of v).contsAux n).b), 0 ≤ ((of v).contsAux (n + 1)).b
⊢ 0 ≤ ((of v).contsAux n).b

Tactic:
induction n with
  | zero => rfl
  | succ n IH =>
    rcases Decidable.em <| g.TerminatedAt (n - 1) with terminated | not_terminated
    · -- terminating case
      rcases n with - | n
      · simp [zero_le_one]
      · have : g.contsAux (n + 2) = g.contsAux (n + 1) :=
          contsAux_stable_step_of_terminated terminated
        simp only [g, this, IH]
    · -- non-terminating case
      calc
        (0 : K) ≤ fib (n + 1) := mod_cast (n + 1).fib.zero_le
        _ ≤ ((of v).contsAux (n + 1)).b := fib_le_of_contsAux_b (Or.inr not_terminated)

Premises used: GenContFract.contsAux, Nat.zero_le, GenContFract.Pair.b, HSub.hSub, GenContFract.of, zero_le_one, Decidable.em, HAdd.hAdd, Nat.fib, Nat.zero, OfNat.ofNat, GenContFract.TerminatedAt
-- 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
rw : 0 ≤ ((of v).contsAux (n + 1)).b
⊢ 0 ≤ (of v).dens n

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.den_eq_conts_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
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
zero_le_of_contsAux_b

Premises used: GenContFract.zero_le_of_contsAux_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
⊢ 0 ≤ ((of v).contsAux (n + 1)).b

Tactic:
exact zero_le_of_contsAux_b

Premises used: GenContFract.zero_le_of_contsAux_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
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),
    gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b
⊢ b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ 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, rfl, 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
⊢ gp_n.b * ((of v).contsAux (n + 1)).b ≤ ((of v).contsAux (n + 2)).b

Tactic:
simp [of_partNum_eq_one (partNum_eq_s_a nth_s_eq), zero_le_of_contsAux_b,
    GenContFract.contsAux_recurrence nth_s_eq rfl rfl]

Premises used: GenContFract.of_partNum_eq_one, GenContFract.partNum_eq_s_a, GenContFract.zero_le_of_contsAux_b, rfl, GenContFract.contsAux_recurrence
-- 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_partDenom_eq : (of v).partDens.get? n = some b
rw : b * ((of v).contsAux (n + 1)).b ≤ (of v).dens (n + 1)
⊢ b * (of v).dens n ≤ (of v).dens (n + 1)

Tactic:
rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]

Premises used: GenContFract.nth_cont_eq_succ_nth_contAux, GenContFract.den_eq_conts_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
b : K
nth_partDenom_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ (of v).dens (n + 1)

Tactic:
le_of_succ_succ_get?_contsAux_b nth_partDenom_eq

Premises used: GenContFract.contsAux, GenContFract.dens, GenContFract.conts, GenContFract.le_of_succ_succ_get?_contsAux_b, Stream'.get, Stream'.map, Stream'.tail
-- 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_partDenom_eq : (of v).partDens.get? n = some b
⊢ b * ((of v).contsAux (n + 1)).b ≤ (of v).dens (n + 1)

Tactic:
exact le_of_succ_succ_get?_contsAux_b nth_partDenom_eq

Premises used: GenContFract.le_of_succ_succ_get?_contsAux_b