Number theory · easy

Statement, exactly as the model and Lean see it

theorem lg_target {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) : NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv = NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv := by

Mathlib declaration: NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex.congr_simp
Held-out module: Mathlib.NumberTheory.NumberField.Completion.Ramification
Banned modules (itself + downstream): 1
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.00024

Plan

The theorem you're trying to prove is a trivial identity: it asserts that the ring equivalence from the completion of a complex infinite place to the complex numbers is equal to itself. This is essentially a reflexive equality, and the proof is straightforward — it's just an application of reflexivity. Here's a Lean 4 tactic proof skeleton with key intermediate steps marked as `sorry`, which you can later fill in with actual proofs or simplifications: Alternatively, if you wanted to structure the proof using `have` statements for clarity (even though they are not necessary here), you could write: In this case, no additional lemmas or intermediate steps are needed because the equality is immediate.

Skeleton — Lean accepts it with only sorry steps left

-- The two sides of the equality are identical, so we can use reflexivity.
rfl

Attempts

sample 0 · round 0Verified1.2 s model time
Proof
```
rfl
```

Verified proof

theorem lg_target {K : Type u_1} [Field K] {v : NumberField.InfinitePlace K} (hv : v.IsComplex) : NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv = NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex hv := by
  rfl

Axioms used: propext, Classical.choice, 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.