awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this_1 : 1 / den' ≤ 1 / den
this : 0 ≤ pred_conts.b
⊢ 0 < den'
have this₁ : 0 < ifp_n.fr⁻¹
Tactic: have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : 1 / den' ≤ 1 / den
⊢ 1 / |den'| = 1 / den'
have this₁ : 0 < den'
Tactic: have : 0 < den' := by
        have : 0 ≤ pred_conts.b :=
          haveI : (fib n : K) ≤ pred_conts.b :=
            haveI : ¬g.TerminatedAt (n - 2) :=
              mt (terminated_stable (n.sub_le 2)) not_terminatedAt_n
            fib_le_of_contsAux_b <| Or.inr this
          le_trans (mod_cast (fib n).zero_le) this
        have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)
        positivity
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this_1 : 1 / den' ≤ 1 / den
this : 0 < den'
⊢ 1 / |den'| = 1 / den'
have rw : 1 / den' = 1 / den'
Tactic: rw [abs_of_pos this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : 1 / den' ≤ 1 / den
⊢ |HPow.hPow (α := K) (-1) n / den'| ≤ 1 / den
have this₁ : |HPow.hPow (α := K) (-1) n / den'| = 1 / den'
Tactic: have : |(-1) ^ n / den'| = 1 / den' := by
      suffices 1 / |den'| = 1 / den' by rwa [abs_div, abs_neg_one_pow n]
      have : 0 < den' := by
        have : 0 ≤ pred_conts.b :=
          haveI : (fib n : K) ≤ pred_conts.b :=
            haveI : ¬g.TerminatedAt (n - 2) :=
              mt (terminated_stable (n.sub_le 2)) not_terminatedAt_n
            fib_le_of_contsAux_b <| Or.inr this
          le_trans (mod_cast (fib n).zero_le) this
        have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)
        positivity
      rw [abs_of_pos this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ |HPow.hPow (α := K) (-1) n / den'| ≤ 1 / den
have suffices : 1 / den' ≤ 1 / den
Tactic: suffices 1 / den' ≤ 1 / den by
    have : |(-1) ^ n / den'| = 1 / den' := by
      suffices 1 / |den'| = 1 / den' by rwa [abs_div, abs_neg_one_pow n]
      have : 0 < den' := by
        have : 0 ≤ pred_conts.b :=
          haveI : (fib n : K) ≤ pred_conts.b :=
            haveI : ¬g.TerminatedAt (n - 2) :=
              mt (terminated_stable (n.sub_le 2)) not_terminatedAt_n
            fib_le_of_contsAux_b <| Or.inr this
          le_trans (mod_cast (fib n).zero_le) this
        have : 0 < ifp_n.fr⁻¹ :=
          haveI zero_le_ifp_n_fract : 0 ≤ ifp_n.fr :=
            IntFractPair.nth_stream_fr_nonneg stream_nth_eq
          inv_pos.2 (lt_of_le_of_ne zero_le_ifp_n_fract stream_nth_fr_ne_zero.symm)
        positivity
      rw [abs_of_pos this]
    rwa [this]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 1 / den' ≤ 1 / den
have suffices : 0 < den ∧ den ≤ den'
Tactic: suffices 0 < den ∧ den ≤ den' from div_le_div_of_nonneg_left zero_le_one this.1 this.2
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 0 < den ∧ den ≤ den'
have left : 0 < den
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
left : 0 < den
⊢ 0 < den ∧ den ≤ den'
have right : den ≤ den'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ 0 < den
have this : 0 < pred_conts.b + gp.b * conts.b
Tactic: have : 0 < pred_conts.b + gp.b * conts.b :=
      nextConts_b_ineq.trans_lt' <| mod_cast fib_pos.2 <| succ_pos _
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
⊢ conts.b * (pred_conts.b + gp.b * conts.b) ≤ conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
have ha : 0 ≤ conts.b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ den ≤ den'
have right : gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
Tactic: suffices gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b by
      simp only [den, den']; gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ gp.b * conts.b ≤ ifp_n.fr⁻¹ * conts.b
have right : (↑ifp_succ_n.b : K) * conts.b ≤ ifp_n.fr⁻¹ * conts.b
Tactic: suffices (ifp_succ_n.b : K) * conts.b ≤ ifp_n.fr⁻¹ * conts.b by rwa [← ifp_succ_n_b_eq_gp_b]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
⊢ (↑ifp_succ_n.b : K) * conts.b ≤ ifp_n.fr⁻¹ * conts.b
have this : (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹
Tactic: have : (ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹ :=
      IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv stream_nth_eq succ_nth_stream_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
den : K := conts.b * (pred_conts.b + gp.b * conts.b)
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_succ_n_b_eq_gp_b : (↑ifp_succ_n.b : K) = gp.b
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
stream_nth_fr_ne_zero : ifp_n.fr ≠ 0
if_of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
den' : K := conts.b * (pred_conts.b + ifp_n.fr⁻¹ * conts.b)
nextConts_b_ineq : (↑(fib (n + 2)) : K) ≤ pred_conts.b + gp.b * conts.b
conts_b_ineq : (↑(fib (n + 1)) : K) ≤ conts.b
zero_lt_conts_b : 0 < conts.b
this : (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹
⊢ (↑ifp_succ_n.b : K) * conts.b ≤ ifp_n.fr⁻¹ * conts.b
have right : 0 ≤ conts.b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
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
⊢ |v - (of v).convs n| ≤ 1 / (b * (of v).dens n * (of v).dens n)
have not_terminatedAt_n : ¬(of v).TerminatedAt n
Tactic: have not_terminatedAt_n : ¬(of v).TerminatedAt n := by
    simp [terminatedAt_iff_partDen_none, nth_partDen_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
⊢ |v - (of v).convs n| ≤ 1 / (b * (of v).dens n * (of v).dens n)
have refine : 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
Tactic: refine (abs_sub_convs_le not_terminatedAt_n).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
have inl : ∀ (hB : (of v).dens n = 0), 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
Tactic: rcases (zero_le_of_den (K := K)).eq_or_lt' with
    ((hB : (GenContFract.of v).dens n = 0) | hB)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
inl : ∀ (hB : (of v).dens n = 0), 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
have inr : ∀ (hB : 0 < (of v).dens n), 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
Tactic: rcases (zero_le_of_den (K := K)).eq_or_lt' with
    ((hB : (GenContFract.of v).dens n = 0) | hB)
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
have inr : 0 < b * (of v).dens n * (of v).dens n
Tactic: apply one_div_le_one_div_of_le
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
inr : 0 < b * (of v).dens n * (of v).dens n
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
have inr₁ : b * (of v).dens n * (of v).dens n ≤ (of v).dens n * (of v).dens (n + 1)
Tactic: apply one_div_le_one_div_of_le