awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
rw : (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
⊢ (of v).convs (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
have rw₁ : (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
Tactic: rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
Goal:
K : Type u_1
v : K
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
rw : (of v).convs' (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
rw₁ : (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
⊢ (of v).convs (n + 1) = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs n
have rw₂ : (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n = (↑⌊v⌋ : K) + 1 / (of (Int.fract v)⁻¹).convs' n
Tactic: rw [of_convs_eq_convs', convs'_succ, of_convs_eq_convs']
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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 : ℕ), ∀ n ≥ N, |v - (of v).convs n| < ε
have rcases : ∀ (N' : ℕ) (one_div_ε_lt_N' : 1 / ε < (↑N' : K)), ∃ (N : ℕ), ∀ n ≥ N, |v - (of v).convs n| < ε
Tactic: rcases (exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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 ≥ N, |v - (of v).convs n| < ε
have exists : ∀ n ≥ N, |v - (of v).convs n| < ε
Tactic: exists N
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
⊢ |v - (of v).convs n| < ε
have inl : ∀ (terminatedAt_n : g.TerminatedAt n), |v - (of v).convs n| < ε
Tactic: rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
inl : ∀ (terminatedAt_n : g.TerminatedAt n), |v - (of v).convs n| < ε
⊢ |v - (of v).convs n| < ε
have inr : ∀ (not_terminatedAt_n : ¬g.TerminatedAt n), |v - (of v).convs n| < ε
Tactic: rcases Decidable.em (g.TerminatedAt n) with terminatedAt_n | not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
terminatedAt_n : g.TerminatedAt n
⊢ |v - (of v).convs n| < ε
have this : v = g.convs n
Tactic: have : v = g.convs n := of_correctness_of_terminatedAt terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
terminatedAt_n : g.TerminatedAt n
this : v = g.convs n
⊢ |v - (of v).convs n| < ε
have this₁ : v - g.convs n = 0
Tactic: have : v - g.convs n = 0 := sub_eq_zero.mpr this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
terminatedAt_n : g.TerminatedAt n
this_1 : v = g.convs n
this : v - g.convs n = 0
⊢ |v - (of v).convs n| < ε
have inl : |0| < ε
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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)
⊢ |v - (of v).convs n| < ε
have abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
Tactic: have abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB) :=
      abs_sub_convs_le not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ |v - (of v).convs n| < ε
have inr : 1 / (B * nB) < ε
Tactic: suffices 1 / (B * nB) < ε from lt_of_le_of_lt abs_v_sub_conv_le this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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)
⊢ 1 / (B * nB) < ε
have nB_ineq : (↑(fib (n + 2)) : K) ≤ nB
Tactic: have nB_ineq : (fib (n + 2) : K) ≤ nB :=
      haveI : ¬g.TerminatedAt (n + 1 - 1) := not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
⊢ 1 / (B * nB) < ε
have B_ineq : (↑(fib (n + 1)) : K) ≤ B
Tactic: have B_ineq : (fib (n + 1) : K) ≤ B :=
      haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminatedAt_n
      succ_nth_fib_le_of_nth_den (Or.inr this)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
⊢ 1 / (B * nB) < ε
have zero_lt_B : 0 < B
Tactic: have zero_lt_B : 0 < B := B_ineq.trans_lt' <| mod_cast fib_pos.2 n.succ_pos
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
⊢ 1 / (B * nB) < ε
have nB_pos : 0 < nB
Tactic: have nB_pos : 0 < nB := nB_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (hypothesis)
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
⊢ 1 / (B * nB) < ε
have zero_lt_mul_conts : 0 < B * nB
Tactic: have zero_lt_mul_conts : 0 < B * nB := by positivity
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
⊢ 1 / (B * nB) < ε
have inr : 1 < ε * (B * nB)
Tactic: suffices 1 < ε * (B * nB) from (div_lt_iff₀ zero_lt_mul_conts).mpr this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
⊢ 1 < ε * (B * nB)
have inr : ε * (↑N' : K) ≤ ε * (B * nB)
Tactic: calc 1 < ε * (N' : K) := (div_lt_iff₀' ε_pos).mp one_div_ε_lt_N'
      _ ≤ ε * (B * nB) := ?_
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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' : K) ≤ ε * (B * nB)
have inr : (↑N' : K) ≤ B * nB
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
⊢ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K) ≤
    HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K)
have hbc : n ≤ n + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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
⊢ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K) ≤ B * nB
have c0 : LE.le.{u_1} (α := K) 0 (↑(fib (n + 2)) : K)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K) ≤ B * nB
have b0 : 0 ≤ B
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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' : K) ≤ B * nB
have by : LE.le.{u_1} (α := K) (↑N' : K) (↑N : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₁ : LE.le.{u_1} (α := K) (↑N : K) (↑n : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₂ : LE.le.{u_1} (α := K) (↑n : K) (↑(fib n) : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₃ : LE.le.{u_1} (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₄ : (↑(fib (n + 1)) : K) ≤ HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₅ : HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 1)) : K) ≤
  HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : K)
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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries (goal)
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)
⊢ (↑N' : K) ≤ B * nB
have by₆ : HMul.hMul (α := K) (↑(fib (n + 1)) : K) (↑(fib (n + 2)) : 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
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have this : IntFractPair.of v = ifp_n
Tactic: have : IntFractPair.of v = ifp_n := by injection nth_stream_eq