Theorems / mh_ineq_910a5c

Mathlib held-out

Inequalities · hard

Statement, exactly as the model and Lean see it
theorem lg_target (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] : HahnSeries.archimedeanClassOrderIsoWithTop Γ R = HahnSeries.archimedeanClassOrderIsoWithTop Γ R := by
Mathlib declaration
HahnSeries.archimedeanClassOrderIsoWithTop.congr_simp
Held-out module
Mathlib.Algebra.Order.Module.HahnEmbedding
Banned modules (itself + downstream)
2
Reference proof premises (reachable / held-out)
5 / 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.00041

Retrieved lemmas

  1. 1. HahnSeries.archimedeanClassOrderIsoWithTop_apply
  2. 2. HahnSeries.finiteArchimedeanClassOrderIso.congr_simp
  3. 3. HahnSeries.finiteArchimedeanClassOrderIso_apply
  4. 4. HahnSeries.archimedeanClassMk_eq_archimedeanClassMk_iff
  5. 5. HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff
  6. 6. HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff_of_orderTop_ofLex
  7. 7. HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd
  8. 8. HahnSeries.inv_single

Plan

The given theorem is a tautology: it asserts that a function is equal to itself. Therefore, the proof is trivial and can be completed by directly applying reflexivity. ### Explanation: - The theorem `lg_target` simply states that `HahnSeries.archimedeanClassOrderIsoWithTop Γ R` is equal to itself. - This is a direct application of the reflexive property of equality. - There's no need for any lemmas or intermediate steps since the goal is immediate. --- ### Lean Proof Skeleton: This proof uses `rfl` (reflexivity), which is the most direct way to prove that an expression is equal to itself in Lean.

Skeleton — Lean accepts it with only sorry steps left
rfl

Attempts

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

Verified proof

theorem lg_target (Γ : Type u_1) (R : Type u_2) [LinearOrder Γ] [LinearOrder R] [AddCommGroup R] [IsOrderedAddMonoid R] [Archimedean R] [Nontrivial R] : HahnSeries.archimedeanClassOrderIsoWithTop Γ R = HahnSeries.archimedeanClassOrderIsoWithTop Γ R := 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.