awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have zero : 0 ≤ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr ∧ { b := ⌊v⌋, fr := fract v : IntFractPair K }.fr < 1
Tactic: rw [← this, IntFractPair.of]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have 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
Tactic: rcases succ_nth_stream_eq_some_iff.1 nth_stream_eq with ⟨_, _, _, ifp_of_eq_ifp_n⟩
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
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 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have succ : 0 ≤ { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr ∧
  { b := ⌊w.fr⁻¹⌋, fr := fract w.fr⁻¹ : IntFractPair K }.fr < 1
Tactic: rw [← ifp_of_eq_ifp_n, IntFractPair.of]
-- 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
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have zero : ∀ (nth_stream_eq : IntFractPair.stream v 0 = some ifp_n), 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 _⟩
Cleared hypotheses: n, 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
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
⊢ 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
have succ : ∀ (n : ℕ) (nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n), 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 _⟩
Cleared hypotheses: n, 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
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ 1 ≤ ifp_succ_n.b
have 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
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
Cleared hypotheses: ifp_succ_n, 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
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
have rw : ifp_n.fr ≤ 1
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)]
-- 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 : 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⁻¹
⊢ (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹
have 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⁻¹
Tactic: obtain ⟨_, ifp_n_fr⟩ := ifp_n
Cleared hypotheses: ifp_n, nth_stream_eq, 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 : 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_succ_n.b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
have this₁ : 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
-- 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 : 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
⊢ (↑ifp_succ_n.b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
have this₁ : 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
-- 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 : 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
⊢ (↑ifp_succ_n.b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
have rwa : (↑(IntFractPair.of ifp_n_fr⁻¹).b : K) ≤ { b := b, fr := ifp_n_fr : IntFractPair K }.fr⁻¹
Tactic: 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 : 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
⊢ (↑ifp_succ_n.b : K) ≤ ifp_n.fr⁻¹
have suffices : (↑⌊ifp_n.fr⁻¹⌋ : 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]
-- 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
⊢ 1 ≤ b
have obtain : ∀ (gp_n : Pair K) (nth_s_eq : (of v).s.get? n = some gp_n) (nth_partDen_eq : (of v).partDens.get? n = some gp_n.b),
  1 ≤ gp_n.b
Tactic: obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
Cleared hypotheses: b, 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
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
⊢ 1 ≤ gp_n.b
have obtain : ∀ (ifp_n : IntFractPair K) (succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n)
  (ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b), 1 ≤ gp_n.b
Tactic: obtain ⟨ifp_n, succ_nth_stream_eq, ifp_n_b_eq_gp_n_b⟩ :
      ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_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
gp_n : Pair K
nth_s_eq : (of v).s.get? n = some gp_n
nth_partDen_eq : (of v).partDens.get? n = some gp_n.b
ifp_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_n
ifp_n_b_eq_gp_n_b : (↑ifp_n.b : K) = gp_n.b
⊢ 1 ≤ gp_n.b
have rw : LE.le.{u_1} (α := K) 1 (↑ifp_n.b : K)
Tactic: rw [← ifp_n_b_eq_gp_n_b]
-- 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
⊢ gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)
have obtain : ∀ (ifp : IntFractPair K) (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp),
  gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)
Tactic: obtain ⟨ifp, stream_succ_nth_eq, -⟩ : ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ _ :=
    IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some nth_s_eq
-- 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
⊢ gp = { a := 1, b := (↑ifp.b : K) }
have this : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
Tactic: have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
⊢ some gp = some { a := 1, b := (↑ifp.b : K) }
have rwa : ∀ (this : some gp = some { a := 1, b := (↑ifp.b : K) }), some gp = some { a := 1, b := (↑ifp.b : K) }
Tactic: rwa [nth_s_eq] at this
Cleared hypotheses: 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : (of v).s.get? n = some { a := 1, b := (↑ifp.b : K) }
⊢ gp = { a := 1, b := (↑ifp.b : K) }
have this₁ : some gp = some { a := 1, b := (↑ifp.b : K) }
Tactic: have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
⊢ gp.a = 1 ∧ ∃ (z : ℤ), gp.b = (↑z : K)
have this : gp = { a := 1, b := (↑ifp.b : K) }
Tactic: have : gp = ⟨1, ifp.b⟩ := by
    have : (of v).s.get? n = some ⟨1, ifp.b⟩ :=
      get?_of_eq_some_of_succ_get?_intFractPair_stream stream_succ_nth_eq
    have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this
    injection 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
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
⊢ a = 1
have obtain : ∀ (gp : Pair K) (nth_s_eq : (of v).s.get? n = some gp) (gp_a_eq_a_n : gp.a = a), a = 1
Tactic: obtain ⟨gp, nth_s_eq, gp_a_eq_a_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.a = a :=
    exists_s_a_of_partNum nth_partNum_eq
-- 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
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
⊢ a = 1
have this : gp.a = 1
Tactic: have : gp.a = 1 := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).left
-- 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
a : K
nth_partNum_eq : (of v).partNums.get? n = some a
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_a_eq_a_n : gp.a = a
this : gp.a = 1
⊢ a = 1
have rwa : ∀ (this : a = 1), a = 1
Tactic: rwa [gp_a_eq_a_n] at this
Cleared hypotheses: 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
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ ∃ (z : ℤ), b = (↑z : K)
have obtain : ∀ (gp : Pair K) (nth_s_eq : (of v).s.get? n = some gp) (gp_b_eq_b_n : gp.b = b), ∃ (z : ℤ), b = (↑z : K)
Tactic: obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
-- 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
⊢ ∃ (z : ℤ), b = (↑z : K)
have this : ∃ (z : ℤ), gp.b = (↑z : K)
Tactic: have : ∃ z : ℤ, gp.b = (z : K) := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).right
-- 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
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
this : ∃ (z : ℤ), gp.b = (↑z : K)
⊢ ∃ (z : ℤ), b = (↑z : K)
have rwa : ∀ (this : ∃ (z : ℤ), b = (↑z : K)), ∃ (z : ℤ), b = (↑z : K)
Tactic: rwa [gp_b_eq_b_n] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
⊢ (↑(fib n) : K) ≤ ((of v).contsAux n).b
have zero : ∀ (IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
  (hyp : LE.le (α := ℕ) 0 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 2)), (↑(fib 0) : K) ≤ ((of v).contsAux 0).b
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH, hyp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
zero :
  ∀ (IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : LE.le (α := ℕ) 0 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 2)), (↑(fib 0) : K) ≤ ((of v).contsAux 0).b
⊢ (↑(fib n) : K) ≤ ((of v).contsAux n).b
have succ : ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
  (hyp : HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HAdd.hAdd (α := ℕ) 0 1 - 2)),
  (↑(fib (HAdd.hAdd (α := ℕ) 0 1)) : K) ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH, hyp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
zero :
  ∀ (IH : ∀ m < 0, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : LE.le (α := ℕ) 0 1 ∨ ¬(of v).TerminatedAt (HSub.hSub (α := ℕ) 0 2)), (↑(fib 0) : K) ≤ ((of v).contsAux 0).b
succ :
  ∀ (IH : ∀ m < HAdd.hAdd (α := ℕ) 0 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
    (hyp : HAdd.hAdd (α := ℕ) 0 1 ≤ 1 ∨ ¬(of v).TerminatedAt (HAdd.hAdd (α := ℕ) 0 1 - 2)),
    (↑(fib (HAdd.hAdd (α := ℕ) 0 1)) : K) ≤ ((of v).contsAux (HAdd.hAdd (α := ℕ) 0 1)).b
⊢ (↑(fib n) : K) ≤ ((of v).contsAux n).b
have succ₁ : ∀ (n : ℕ) (IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b)
  (hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)),
  (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
Tactic: rcases n with (_ | _ | n)
Cleared hypotheses: n, IH, hyp
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
have this : ¬n + 2 ≤ 1
Tactic: have : ¬n + 2 ≤ 1 := by lia
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
have not_terminatedAt_n : ¬g.TerminatedAt n
Tactic: have not_terminatedAt_n : ¬g.TerminatedAt n := Or.resolve_left hyp this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
have succ : ∀ (gp : Pair K) (s_ppred_nth_eq : g.s.get? n = some gp), (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
Tactic: obtain ⟨gp, s_ppred_nth_eq⟩ : ∃ gp, g.s.get? n = some gp :=
          Option.ne_none_iff_exists'.mp not_terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
have pconts_eq : let pconts := g.contsAux (n + 1);
pconts = g.contsAux (n + 1)
Tactic: set pconts := g.contsAux (n + 1) with pconts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (hypothesis)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
⊢ (↑(fib (n + 1 + 1)) : K) ≤ ((of v).contsAux (n + 1 + 1)).b
have ppconts_eq : let ppconts := g.contsAux n;
ppconts = g.contsAux n
Tactic: set ppconts := g.contsAux n with ppconts_eq
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Computation.Approximations (goal)
Goal:
K : Type u_1
v : K
n_1 : ℕ
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → (↑(fib m) : K) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ (↑(fib (n + 2)) : K) ≤ ((of v).contsAux (n + 2)).b
have succ : HAdd.hAdd (α := K) (↑(fib n) : K) (↑(fib (n + 1)) : K) ≤ gp.a * ppconts.b + gp.b * pconts.b
Tactic: suffices (fib n : K) + fib (n + 1) ≤ gp.a * ppconts.b + gp.b * pconts.b by
          simpa [g, fib_add_two, add_comm, contsAux_recurrence s_ppred_nth_eq ppconts_eq pconts_eq]