picking up lean4 with math

Stream: maths

[Iocta]

linarith used to do the trick for both of these in lean3, what do I need now in lean4?

import Mathlib.Tactic.Linarith
import Mathlib.Data.Real.Basic


example (a b : ℝ) (h : ∀(ε:ℝ), ε > 0 → a ≤ b + ε) : a ≤ b :=
by_contradiction (fun not_a_le_b => by
  have foo: a ≤ b + ((a - b) / 2) := by
    have: 0 < ((a - b) / 2) := by linarith
    apply h ((a - b) / 2) this
  linarith)

[Heather Macbeth]

@Iocta You need to wait until someone writes that functionality into linarith. See !4#2714.

[Kevin Buzzard]

Alternatively you can go back to how we were doing this in 2017 before linarith existed, just applying lemmas like div_pos manually.

[Iocta]

(deleted)

[Notification Bot]

Iocta has marked this topic as resolved.

[Notification Bot]

Iocta has marked this topic as unresolved.

[Iocta]

If I've defined a variable let e := a + b then e appears in a hypothesis, how can I replace e in that hypothesis with a + b? I tried subst e at this but tactic 'subst' failed, variable '' is a let-declaration

[Sophie Morel]

set e :=a+b with he and then you do a rw he at this

[Sophie Morel]

(Uh, in Lean 3 at least. I just noticed that you're using Lean4, sorry...)

[Sophie Morel]

Kevin Buzzard said:

Alternatively you can go back to how we were doing this in 2017 before linarith existed, just applying lemmas like div_pos manually.

I thought that was what we all still did... Oops... :oops:

[Iocta]

Why does this fail?

import Mathlib.Data.Real.Basic

example (a y : ℝ) (x:ℕ→ℝ) (h: abs (x n - y) < abs ε / abs a) : abs a * abs (x n - y) < abs ε := by
/-
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-/
rw [lt_div_iff_mul_lt]

[Iocta]

Also is it just me, I can't copy text from the vscode infoview. I press copy but it doesn't do anything.

[Reid Barton]

did you mean at h? or <-?

[Iocta]

yeah but it doesn't like that either

[Reid Barton]

What is the new error?

[Reid Barton]

And what is the new code?

[Iocta]

example (a y : ℝ) (x:ℕ→ℝ) (h: abs (x n - y) < abs ε / abs a) : abs a * abs (x n - y) < abs ε := by
/-
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-/
rw [lt_div_iff_mul_lt] at h

[Reid Barton]

Oh because the reals are not a group.

[Reid Barton]

(under multiplication)

[Reid Barton]

docs4#lt_div_iff

[Reid Barton]

or docs4#lt_div_iff' even

[Reid Barton]

It would be neat if rw could detect that it "almost" found an occurrence to rewrite, but failed to synthesize some instance, and report that if it fails

[Moritz Doll]

Or we compile a list of all 'generic' algebra lemmas and have a tactic that tries every one (in both directions) and reports back those that do not fail

[Reid Barton]

Or both :smile: