Algebra · medium

Statement, exactly as the model and Lean see it

theorem lg_target {K : Type u_1} {v : K} {n : ℕ} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {b : K} (nth_partDenom_eq : (GenContFract.of v).partDens.get? n = some b) : b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1) := by

Mathlib declaration: GenContFract.le_of_succ_get?_den
Held-out module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Banned modules (itself + downstream): 4
Reference proof premises (reachable / held-out): 2 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00029

Attempts

sample 0 · round 0Wrong tactic17.1 s model time

Proof

intros
have h : (GenContFract.of v).partDens.get? n = some b := nth_partDenom_eq
obtain ⟨a, ha⟩ := h
have h_a : (GenContFract.of v).dens n = a := ha
have h_dens_n_plus_1 : (GenContFract.of v).dens (n + 1) = a * (GenContFract.of v).dens n + (GenContFract.of v).dens (n + 1 - 1)
  := by rw [GenContFract.dens_rec]
rw [h_a] at h_dens_n_plus_1
have h_dens_n_plus_1' : (GenContFract.of v).dens (n + 1) = a * (GenContFract.of v).dens n + (GenContFract.of v).dens n
  := by rw [h_a] at h_dens_n_plus_1; exact h_dens_n_plus_1
rw [h_a] at h_dens_n_plus_1'
have h_dens_n_plus_1'' : (GenContFract.of v).dens (n + 1) = a * (GenContFract.of v).dens n + (GenContFract.of v).dens n
  := h_dens_n_plus_1'
have h_dens_n_plus_1''' : (GenContFract.of v).dens (n + 1) = (a + 1) * (GenContFract.of v).dens n
  := by rw [h_dens_n_plus_1'']
rw [h_a] at h_dens_n_plus_1'''
have h_dens_n_plus_1'''' : (GenContFract.of v).dens (n + 1) = (a + 1) * (GenContFract.of v).dens n
  := h_dens_n_plus_1'''
have h_b_times_dens_n : b * (GenContFract.of v).dens n = a * (GenContFract.of v).dens n
  := by rw [h_a]
rw [h_b_times_dens_n] at h_dens_n_plus_1''''
have h_le : b * (GenContFract.of v).dens n ≤ (GenContFract.of v).dens (n + 1)
  := by rw [h_b_times_dens_n, h_dens_n_plus_1'''']
exact h_le

What Lean printed (this is all the model sees on repair)

6:9: error: Tactic `cases` failed with a nested error:
Dependent elimination failed: Failed to solve equation
  some b =
    match
      (Stream'.map (Option.map fun p => { a := 1, b := ↑p.b }) (↑⟨GenContFract.IntFractPair.stream v, ⋯⟩).tail).get
        n with
    | some x => some x.b
    | none => none
at case `Eq.refl`

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- Shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is the `n`th partial denominator and `Bₙ₊₁` and `Bₙ` are
the `n + 1`th and `n`th denominator of the continued fraction. -/
theorem le_of_succ_get?_den {b : K}
    (nth_partDenom_eq : (of v).partDens.get? n = some b) :
    b * (of v).dens n ≤ (of v).dens (n + 1) := by
  rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]
  exact le_of_succ_succ_get?_contsAux_b nth_partDenom_eq