awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
inr : ε * (↑N' : K) ≤ ε * (B * nB)
⊢ 1 < ε * (B * nB)

Tactic:
calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
      _ ≤ ε * (B * nB) := ?_

Premises used: HMul.hMul, Nat.cast, div_lt_iff₀', Iff.mp
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
inr : (↑N' : K) ≤ B * nB
⊢ ε * (↑N' : K) ≤ ε * (B * nB)

Tactic:
gcongr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ LE.le.{u_1} (α := K) (↑N' : K) (↑N : K)

Tactic:
exact_mod_cast le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ LE.le.{u_1} (α := K) (↑N : K) (↑n : K)

Tactic:
exact_mod_cast n_ge_N
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ LE.le.{u_1} (α := K) (↑n : K) (↑(fib n) : K)

Tactic:
exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N

Premises used: le_max_right, Nat.le_fib_self, OfNat.ofNat, le_trans
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ LE.le.{u_1} (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K)

Tactic:
exact_mod_cast fib_le_fib_succ

Premises used: Nat.fib_le_fib_succ
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ (↑(fib (n + 1)) : K) ≤ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K)

Tactic:
exact_mod_cast (fib (n + 1)).le_mul_self

Premises used: HAdd.hAdd, Nat.fib, Nat.le_mul_self, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
hbc : n ≤ n + 1
⊢ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K) ≤
    HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K)

Tactic:
gcongr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
c0 : LE.le.{u_1} (α := K) 0 (↑(fib (n + 2)) : K)
b0 : 0 ≤ B
⊢ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K) ≤ B * nB

Tactic:
gcongr
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < (↑N' : K)
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
B_ineq : (↑(fib (n + 1)) : K) ≤ B
zero_lt_B : 0 < B
nB_pos : 0 < nB
zero_lt_mul_conts : 0 < B * nB
by : LE.le.{u_1} (α := K) (↑N' : K) (↑N : K)
by₁ : LE.le.{u_1} (α := K) (↑N : K) (↑n : K)
by₂ : LE.le.{u_1} (α := K) (↑n : K) (↑(fib n) : K)
by₃ : LE.le.{u_1} (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K)
by₄ : (↑(fib (n + 1)) : K) ≤ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K)
by₅ :
  HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K) ≤
    HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K)
by₆ : HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K) ≤ B * nB
⊢ (↑N' : K) ≤ B * nB

Tactic:
calc
      (N' : K) ≤ (N : K) := by exact_mod_cast le_max_left _ _
      _ ≤ n := by exact_mod_cast n_ge_N
      _ ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
      _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
      _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
      _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; lia
      _ ≤ B * nB := by gcongr

Premises used: Nat.cast, HAdd.hAdd, Nat.fib, OfNat.ofNat
-- Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Archimedean K
inst_5 : TopologicalSpace K
inst_6 : OrderTopology K
⊢ Filter.Tendsto (of v).convs Filter.atTop (𝓝 v)

Tactic:
simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v

Premises used: GenContFract.of_convergence_epsilon, abs_sub_comm, LinearOrderedAddCommGroup.tendsto_nhds
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ IntFractPair.of v = ifp_n

Tactic:
injection nth_stream_eq
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
⊢ IntFractPair.of v = ifp_n

Tactic:
have : IntFractPair.of v = ifp_n := by injection nth_stream_eq
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
zero : 0 ≤ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr ∧ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr < 1
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rw [← this, IntFractPair.of]

Premises used: GenContFract.IntFractPair.of
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr ∧ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr < 1

Tactic:
⟨fract_nonneg _, fract_lt_one _⟩

Premises used: And.intro, Int.fract_lt_one, Int.fract_nonneg
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v 0 = some ifp_n
this : IntFractPair.of v = ifp_n
⊢ 0 ≤ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr ∧ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩
-- 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_n : IntFractPair K
n : ℕ
nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
succ :
  ∀ (w : IntFractPair K),
    IntFractPair.stream v n = some w →
      w.fr ≠ 0 → ∀ (ifp_of_eq_ifp_n : IntFractPair.of w.fr⁻¹ = ifp_n), 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩

Premises used: Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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_n : IntFractPair K
n : ℕ
nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
w : IntFractPair K
left : IntFractPair.stream v n = some w
left_1 : w.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w.fr⁻¹ = ifp_n
succ :
  0 ≤ { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr ∧
    { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr < 1
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
rw [← ifp_of_eq_ifp_n, IntFractPair.of]

Premises used: GenContFract.IntFractPair.of
-- 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_n : IntFractPair K
n : ℕ
nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
w : IntFractPair K
left : IntFractPair.stream v n = some w
left_1 : w.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w.fr⁻¹ = ifp_n
⊢ 0 ≤ { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr ∧
    { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr < 1

Tactic:
⟨fract_nonneg _, fract_lt_one _⟩

Premises used: And.intro, Int.fract_lt_one, Int.fract_nonneg
-- 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_n : IntFractPair K
n : ℕ
nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
w : IntFractPair K
left : IntFractPair.stream v n = some w
left_1 : w.fr ≠ 0
ifp_of_eq_ifp_n : IntFractPair.of w.fr⁻¹ = ifp_n
⊢ 0 ≤ { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr ∧
    { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr < 1

Tactic:
exact ⟨fract_nonneg _, fract_lt_one _⟩
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
zero : ∀ (nth_stream_eq : IntFractPair.stream v 0 = some ifp_n), 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
succ : ∀ (n : ℕ) (nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n), 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Tactic:
cases n with
  | zero =>
    have : IntFractPair.of v = ifp_n := by injection nth_stream_eq
    rw [← this, IntFractPair.of]
    exact ⟨fract_nonneg _, fract_lt_one _⟩
  | succ =>
    rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩
    rw [← ifp_of_eq_ifp_n, IntFractPair.of]
    exact ⟨fract_nonneg _, fract_lt_one _⟩

Premises used: GenContFract.IntFractPair.of, Int.succ, Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
⊢ 0 ≤ ifp_n.fr

Tactic:
(nth_stream_fr_nonneg_lt_one nth_stream_eq).left

Premises used: GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one, And.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
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
⊢ ifp_n.fr < 1

Tactic:
(nth_stream_fr_nonneg_lt_one nth_stream_eq).right

Premises used: GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one, And.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
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ ∃ (ifp_n : IntFractPair K),
    IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0 ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n

Tactic:
succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Premises used: Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
obtain :
  ∀ (ifp_n : IntFractPair K) (nth_stream_eq : IntFractPair.stream v n = some ifp_n)
    (stream_nth_fr_ne_zero : ifp_n.fr ≠ 0)
    (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)),
    1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b
⊢ 1 ≤ ifp_succ_n.b

Tactic:
obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
        ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq

Premises used: GenContFract.IntFractPair.stream, Iff.mp, GenContFract.IntFractPair.succ_nth_stream_eq_some_iff
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
rw : ifp_n.fr ≤ 1
⊢ 1 ≤ (IntFractPair.of ifp_n.fr⁻¹).b

Tactic:
rw [IntFractPair.of, le_floor, cast_one, one_le_inv₀
    ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)]

Premises used: one_le_inv₀, GenContFract.IntFractPair.of, Int.le_floor, LE.le.lt_of_ne', Int.cast_one, GenContFract.IntFractPair.nth_stream_fr_nonneg
-- 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_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ifp_n.fr ≤ 1

Tactic:
(nth_stream_fr_lt_one nth_stream_eq).le

Premises used: GenContFract.IntFractPair.nth_stream_fr_lt_one, LT.lt.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
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
⊢ ifp_n.fr ≤ 1

Tactic:
exact (nth_stream_fr_lt_one nth_stream_eq).le

Premises used: GenContFract.IntFractPair.nth_stream_fr_lt_one, LT.lt.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
this : (↑⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹
obtain :
  ∀ (b : ℤ) (ifp_n_fr : K) (nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr })
    (this :
      (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹),
    (↑ifp_succ_n.b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
⊢ (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹

Tactic:
obtain ⟨_, ifp_n_fr⟩ := ifp_n
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr }
this : (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
h : ifp_n_fr = 0
⊢ False

Tactic:
simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq

Premises used: GenContFract.IntFractPair.stream
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr }
this : (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
⊢ ifp_n_fr ≠ 0

Tactic:
have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr }
this_1 : (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
this : ifp_n_fr ≠ 0
⊢ IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n

Tactic:
simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq

Premises used: GenContFract.IntFractPair.stream, Option.coe_def
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr }
this_1 : (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
this : ifp_n_fr ≠ 0
⊢ IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n

Tactic:
have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
-- 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_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
b : ℤ
ifp_n_fr : K
nth_stream_eq : IntFractPair.stream v n = some { b := b, fr := ifp_n_fr }
this_1 : (↑⌊{ b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹⌋ : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
this_2 : ifp_n_fr ≠ 0
this : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n
rwa rwa₁ rwa₂ rwa₃ : (↑(IntFractPair.of ifp_n_fr⁻¹).b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
⊢ (↑ifp_succ_n.b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹

Tactic:
rwa [← this]
-- 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
suffices : (↑⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹
⊢ (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹

Tactic:
suffices (⌊ifp_n.fr⁻¹⌋ : K) ≤ ifp_n.fr⁻¹ by
    obtain ⟨_, ifp_n_fr⟩ := ifp_n
    have : ifp_n_fr ≠ 0 := by
      intro h
      simp [h, IntFractPair.stream, nth_stream_eq] at succ_nth_stream_eq
    have : IntFractPair.of ifp_n_fr⁻¹ = ifp_succ_n := by
      simpa [this, IntFractPair.stream, nth_stream_eq, Option.coe_def] using succ_nth_stream_eq
    rwa [← this]