Number theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {R : Type u_2} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite ℤ R] [Module.Free ℤ R] : 1 < Ideal.absNorm v.asIdeal := by

Mathlib declaration: NumberField.HeightOneSpectrum.one_lt_absNorm
Held-out module: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Banned modules (itself + downstream): 5
Reference proof premises (reachable / held-out): 8 / 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.00097

Attempts

sample 0 · round 0Syntax error55.3 s model time

Proof

```lean
intro v
obtain ⟨p, hp⟩ := v
have h1 : p ≠ 0 := by contradiction hp
have h2 : Ideal.isPrime p := Ideal.isPrime_of_is_prime_spectrum hp
have h3 : Ideal.isMaximal p := Ideal.isMaximal_of_is_prime p h2
have h4 : Ideal.absNorm p = Ideal.idealAbsNorm p := rfl
have h5 : Ideal.idealAbsNorm p = Ideal.idealNorm p := by rw [Ideal.idealAbsNorm_eq_idealNorm]
have h6 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := rfl
have h7 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h6
have h8 : (Ideal.idealNorm p).toNat = Ideal.idealNorm p := rfl
have h9 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h8
have h10 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h9
have h11 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h10
have h12 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h11
have h13 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h12
have h14 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h13
have h15 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h14
have h16 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h15
have h17 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h16
have h18 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h17
have h19 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h18
have h20 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h19
have h21 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h20
have h22 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h21
have h23 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h22
have h24 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h23
have h25 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h24
have h26 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h25
have h27 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h26
have h28 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h27
have h29 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h28
have h30 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h29
have h31 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h30
have h32 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h31
have h33 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h32
have h34 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h33
have h35 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h34
have h36 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h35
have h37 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h36
have h38 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h37
have h39 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h38
have h40 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h39
have h41 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h40
have h42 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h41
have h43 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h42
have h44 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h43
have h45 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h44
have h46 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h45
have h47 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h46
have h48 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h47
have h49 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h48
have h50 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h49
have h51 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h50
have h52 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h51
have h53 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h52
have h54 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h53
have h55 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h54
have h56 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h55
have h57 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h56
have h58 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h57
have h59 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h58
have h60 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h59
have h61 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h60
have h62 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h61
have h63 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h62
have h64 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h63
have h65 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h64
have h66 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h65
have h67 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h66
have h68 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h67
have h69 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h68
have h70 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h69
have h71 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h70
have h72 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h71
have h73 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h72
have h74 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h73
have h75 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h74
have h76 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h75
have h77 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h76
have h78 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h77
have h79 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h78
have h80 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h79
have h81 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h80
have h82 : Ideal.idealNorm p = (Ideal.idealNorm p).toNat := h81
have h83 : Ideal.idealNorm p = (Ideal.idealNorm p

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

3:181: error: unsolved goals
R : Type u_2
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
v : IsDedekindDomain.HeightOneSpectrum R
inst✝¹ : Module.Finite ℤ R
inst✝ : Module.Free ℤ R
⊢ 1 < Ideal.absNorm v.asIdeal
4:2: error: unexpected token '`'; expected command

Reference proof

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

/-- The norm of a maximal ideal is `> 1` -/
lemma one_lt_absNorm : 1 < absNorm v.asIdeal := by
  by_contra! h
  apply IsPrime.ne_top v.isPrime
  rw [← absNorm_eq_one_iff]
  have : 0 < absNorm v.asIdeal := by
    rw [Nat.pos_iff_ne_zero, absNorm_ne_zero_iff]
    exact v.asIdeal.finiteQuotientOfFreeOfNeBot v.ne_bot
  lia