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 : IsStrictOrderedRing K
inst_3 : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
stream_nth_eq : IntFractPair.stream v 0 = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)
hn : n = 0
subst :
  let conts := g.contsAux (HAdd.hAdd (α := ℕ) 0 1);
  let pred_conts := g.contsAux 0;
  let A := conts.a;
  let B := conts.b;
  let pA := pred_conts.a;
  let pB := pred_conts.b;
  ∀ (g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)),
    pA * B - pB * A = HPow.hPow (α := K) (β := ℕ) (-1) 0
⊢ pA * B - pB * A = HPow.hPow (α := K) (β := ℕ) (-1) 0

Tactic:
subst n
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
stream_nth_eq : IntFractPair.stream v 0 = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : Eq (α := ℕ) 0 0 ∨ ¬g.TerminatedAt (HSub.hSub (α := ℕ) 0 1)
conts : Pair K := g.contsAux (HAdd.hAdd (α := ℕ) 0 1)
pred_conts : Pair K := g.contsAux 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ pA * B - pB * A = HPow.hPow (α := K) (β := ℕ) (-1) 0

Tactic:
simp [pA, pB, A, B, pred_conts, conts]
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
hn : n = n'.succ
subst :
  let conts := g.contsAux (n'.succ + 1);
  let pred_conts := g.contsAux n'.succ;
  let A := conts.a;
  let B := conts.b;
  let pA := pred_conts.a;
  let pB := pred_conts.b;
  ∀ (g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)),
    pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)

Tactic:
subst n
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
n_eq_zero_or_not_terminatedAt_pred_n : n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n

Premises used: false_or, Nat.succ_ne_zero
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : ¬g.TerminatedAt (n' + 1 - 1)
⊢ ¬g.TerminatedAt n'

Tactic:
rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n

Premises used: add_tsub_cancel_right
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : ¬g.TerminatedAt n'
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)

Tactic:
(SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_n

Premises used: GenContFract.contsAux, GenContFract.dens, SimpContFract.determinant, GenContFract.conts, GenContFract.of, GenContFract.nums, Stream'.get, Stream'.map, Stream'.tail
-- 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
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n'.succ + 1)
pred_conts : Pair K := g.contsAux n'.succ
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : ¬g.TerminatedAt n'
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) (n' + 1)

Tactic:
exact (SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_n

Premises used: SimpContFract.determinant
-- 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) n

Tactic:
match hn : n with
      | 0 => subst n; simp [pA, pB, A, B, pred_conts, conts]
      | n' + 1 =>
        subst n
        simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n
        rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n
        exact (SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
⊢ pA * B - pB * A = HPow.hPow (α := K) (-1) n

Tactic:
have determinant_eq : pA * B - pB * A = (-1) ^ n := by
      match hn : n with
      | 0 => subst n; simp [pA, pB, A, B, pred_conts, conts]
      | n' + 1 =>
        subst n
        simp only [succ_ne_zero, false_or] at n_eq_zero_or_not_terminatedAt_pred_n
        rw [add_tsub_cancel_right] at n_eq_zero_or_not_terminatedAt_pred_n
        exact (SimpContFract.of v).determinant n_eq_zero_or_not_terminatedAt_pred_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
inl : ∀ (n_eq_zero : n = 0), n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
inr : ∀ (not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)), n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
n_eq_zero : n = 0
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
simp [n_eq_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n

Premises used: HSub.hSub, mt, Nat.pred_le, GenContFract.terminated_stable, 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n

Premises used: HSub.hSub, mt, Nat.pred_le, GenContFract.terminated_stable, 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
⊢ (↑(fib n) : K) ≤ pB

Tactic:
have pB_ineq : (fib n : K) ≤ pB :=
      haveI : n ≤ 1 ∨ ¬g.TerminatedAt (n - 2) := by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr <| mt (terminated_stable (n - 1).pred_le) not_terminatedAt_pred_n
      fib_le_of_contsAux_b 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
inl : ∀ (n_eq_zero : n = 0), n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
inr : ∀ (not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)), n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
n_eq_zero : n = 0
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
simp [n_eq_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
Or.inr not_terminatedAt_pred_n

Premises used: 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
exact Or.inr not_terminatedAt_pred_n

Premises used: 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
⊢ (↑(fib (n + 1)) : K) ≤ B

Tactic:
have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2) := by
        rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr not_terminatedAt_pred_n
      fib_le_of_contsAux_b 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
⊢ 0 < B

Tactic:
have zero_lt_B : 0 < B := B_ineq.trans_lt' <| cast_pos.2 <| fib_pos.2 n.succ_pos
-- 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
⊢ 0 ≤ pB

Tactic:
have : 0 ≤ pB := (Nat.cast_nonneg _).trans pB_ineq
-- 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
this : 0 ≤ pB
⊢ 0 < ifp.fr

Tactic:
have : 0 < ifp.fr :=
      ifp_fr_ne_zero.lt_of_le' <| IntFractPair.nth_stream_fr_nonneg stream_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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
this_1 : 0 ≤ pB
this : 0 < ifp.fr
⊢ pB + ifp.fr⁻¹ * B ≠ 0

Tactic:
positivity
-- 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
this_1 : 0 ≤ pB
this : 0 < ifp.fr
⊢ pB + ifp.fr⁻¹ * B ≠ 0

Tactic:
have : pB + ifp.fr⁻¹ * B ≠ 0 := by positivity
-- 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
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = HPow.hPow (α := K) (-1) n
pB_ineq : (↑(fib n) : K) ≤ pB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
this_1 : 0 ≤ pB
this_2 : 0 < ifp.fr
this : pB + ifp.fr⁻¹ * B ≠ 0
⊢ (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B) - A / B = HPow.hPow (α := K) (-1) n / (B * (ifp.fr⁻¹ * B + pB))

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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
⊢ let conts := g.contsAux (n + 1);
  conts = g.contsAux (n + 1)

Tactic:
set conts := contsAux g (n + 1) with conts_eq

Premises used: GenContFract.contsAux, GenContFract.conts, HAdd.hAdd, 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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
⊢ let pred_conts := g.contsAux n;
  pred_conts = g.contsAux n

Tactic:
set pred_conts := contsAux g n with pred_conts_eq

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
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
change : |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
⊢ |v - (of v).convs n| ≤ 1 / ((of v).dens n * (of v).dens (n + 1))

Tactic:
change |v - convs g n| ≤ 1 / (conts.b * nextConts.b)

Premises used: GenContFract.convs, GenContFract.Pair.b, HMul.hMul