Theorems / mh_ineq_040adc
Mathlib held-out
Inequalities · hard
theorem lg_target {R : Type u_1} {S : Type u_2} [LinearOrder R] [LinearOrder S] [CommRing R] [IsStrictOrderedRing R] [Ring S] [IsStrictOrderedRing S] [DenselyOrdered R] [Archimedean R] {x y : S} (f : R →+* S) (hf : StrictMono ⇑f) : ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x| := by- Mathlib declaration
- ArchimedeanClass.mk_le_mk_iff_denselyOrdered
- Held-out module
- Mathlib.Algebra.Order.Ring.Archimedean
- Banned modules (itself + downstream)
- 3
- Reference proof premises (reachable / held-out)
- 56 / 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.00098
Attempts
- sample 0 · round 0Syntax error41.7 s model time
Proof ```lean intro h split · intro hxy obtain ⟨q, hq, hqy⟩ := ArchimedeanClass.mk_le_mk_iff_exists_q.1 hxy exact ⟨q, hq, mul_le_mul_right hqy (le_refl _)⟩ · intro hq have hq' : 0 < f q := hq.1 have hfqy : f q * |y| ≤ |x| := hq.2 have hfx : |x| ≤ |x| := le_refl _ have hfy : |y| ≤ |y| := le_refl _ have hqy : 0 < |y| := le_zero_iff_neg.1 (ne_of_gt hq'.1) have hqy' : 0 < |y| := hqy have hqy'' : 0 < |y| := hqy' have hqy''' : 0 < |y| := hqy'' have hqy'''' : 0 < |y| := hqy''' have hqy''''' : 0 < |y| := hqy'''' have hqy'''''' : 0 < |y| := hqy''''' have hqy''''''' : 0 < |y| := hqy'''''' have hqy'''''''' : 0 < |y| := hqy''''''' have hqy''''''''' : 0 < |y| := hqy'''''''' have hqy'''''''''' : 0 < |y| := hqy''''''''' have hqy''''''''''' : 0 < |y| := hqy'''''''''' have hqy'''''''''''' : 0 < |y| := hqy''''''''''' have hqy''''''''''''' : 0 < |y| := hqy'''''''''''' have hqy'''''''''''''' : 0 < |y| := hqy''''''''''''' have hqy''''''''''''''' : 0 < |y| := hqy'''''''''''''' have hqy'''''''''''''''' : 0 < |y| := hqy''''''''''''''' have hqy''''''''''''''''' : 0 < |y| := hqy'''''''''''''''' have hqy'''''''''''''''''' : 0 < |y| := hqy''''''''''''''''' have hqy''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''' have hqy'''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''' have hqy''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''' have hqy'''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''' have hqy''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''' have hqy'''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''' have hqy''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''' have hqy'''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''''''''''' have hqy'''''''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy''''''''''''''''''''''''''''''''''''''''''''' have hqy''''''''''''''''''''''''''''''''''''''''''''''' : 0 < |y| := hqy'''''''''''''''''''''''''''''''''''''''''''''' have h
What Lean printed (this is all the model sees on repair) 3:314: error: unsolved goals R : Type u_1 S : Type u_2 inst✝⁷ : LinearOrder R inst✝⁶ : LinearOrder S inst✝⁵ : CommRing R inst✝⁴ : IsStrictOrderedRing R inst✝³ : Ring S inst✝² : IsStrictOrderedRing S inst✝¹ : DenselyOrdered R inst✝ : Archimedean R x y : S f : R →+* S hf : StrictMono ⇑f ⊢ ArchimedeanClass.mk x ≤ ArchimedeanClass.mk y ↔ ∃ q, 0 < f q ∧ f q * |y| ≤ |x| 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.
theorem mk_le_mk_iff_denselyOrdered [Ring S] [IsStrictOrderedRing S]
[DenselyOrdered R] [Archimedean R] {x y : S} (f : R →+* S) (hf : StrictMono f) :
mk x ≤ mk y ↔ ∃ q : R, 0 < f q ∧ f q * |y| ≤ |x| := by
have H {q} : 0 < f q ↔ 0 < q := by simpa using hf.lt_iff_lt (a := 0)
constructor
· rintro ⟨(_ | n), hn⟩
· simp_all [exists_zero_lt]
· obtain ⟨q, hq₀, hq⟩ := exists_nsmul_lt_of_pos (one_pos (α := R)) (n + 1)
refine ⟨q, H.2 hq₀, le_of_mul_le_mul_left ?_ n.cast_add_one_pos⟩
simpa [← mul_assoc] using mul_le_mul (hf hq).le hn (abs_nonneg y) (by simp)
· rintro ⟨q, hq₀, hq⟩
have hq₀' := H.1 hq₀
obtain ⟨n, hn⟩ := exists_lt_nsmul hq₀' 1
refine ⟨n, le_of_mul_le_mul_left ?_ hq₀⟩
have h : 0 ≤ f (n • q) := by
rw [← f.map_zero]
exact hf.monotone (nsmul_nonneg hq₀'.le n)
simpa [mul_comm, mul_assoc] using mul_le_mul (hf hn).le hq (mul_nonneg hq₀.le (abs_nonneg y)) h