Number theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {K : Type u_2} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] (k : Subfield K) : Algebra.IsAlgebraic (↥k) K := by

Mathlib declaration: NumberField.instIsAlgebraicSubtypeMemSubfield
Held-out module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
Banned modules (itself + downstream): 17
Reference proof premises (reachable / held-out): 6 / 0

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.00007

Attempts

sample 0 · round 0Hallucinated theorem2.2 s model time

Proof

haveI : IsField k := field_of_subfield k
haveI : IsAlgebraic ℚ k := algebraic_of_subfield k
exact Algebra.IsAlgebraic.trans (Algebra.isAlgebraic_subfield k) (Algebra.IsAlgebraic.of_isAlgebraic k)

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

4:23: error: Unknown identifier `field_of_subfield`
4:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
5:10: error: failed to synthesize instance of type class
  Ring (Subfield K)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
5:29: error: Unknown identifier `algebraic_of_subfield`
5:2: warning: Try this: 
  haveI̵

The goal is a proposition, so `have` is preferred over `haveI`.
The difference between `have` and `haveI` is that `haveI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
6:35: error: Unknown constant `Algebra.isAlgebraic_subfield`
6:68: error: Unknown constant `Algebra.IsAlgebraic.of_isAlgebraic`

Reference proof

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

local instance (k : Subfield K) : Algebra.IsAlgebraic k K :=
  Algebra.IsAlgebraic.tower_top k (K := ℚ) (A := K)