Algebra · easy

Statement, exactly as the model and Lean see it

theorem lg_target {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.nums 0 = g.h := by

Mathlib declaration: GenContFract.zeroth_num_eq_h
Held-out module: Mathlib.Algebra.ContinuedFractions.Translations
Banned modules (itself + downstream): 11
Reference proof premises (reachable / held-out): 0 / 0

Traces

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

Verified2 model calls · 2 Lean checks · $0.00021

Plan

To prove the theorem `lg_target`, we need to show that the zeroth numerator of the continued fraction `g` is equal to its height `g.h`. ### Explanation: - The function `g.nums` returns a sequence of numerators for the continued fraction `g`. - By definition, the zeroth numerator (i.e., `g.nums 0`) corresponds to the first term in the continued fraction expansion, which is the integer part or the initial value. - The height `g.h` is defined as this same initial value. - Therefore, the theorem is essentially a definitional equality: `g.nums 0` is defined to be equal to `g.h`. ### Lean Proof Skeleton: This skeleton sets up the key intermediate step, where we assert that `g.nums 0` equals `g.h`, and then use that to complete the proof. You would replace the `sorry` with the actual proof if needed.

Skeleton — Lean accepts it with only sorry steps left

have : g.nums 0 = g.h := sorry
exact this

Attempts

sample 0 · round 0Verified1.5 s model time
Proof
```
have : g.nums 0 = g.h := rfl
exact this
```

Verified proof

theorem lg_target {K : Type u_1} {g : GenContFract K} [DivisionRing K] : g.nums 0 = g.h := by
  have : g.nums 0 = g.h := rfl
  exact this

Axioms used: propext, Quot.sound

Reference proof

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

@[simp]
theorem zeroth_num_eq_h : g.nums 0 = g.h :=
  rfl