Inline subsitution

Stream: new members

[Marcus Rossel]

I often find myself in proofs doing something like:

  example {n m o : ℕ} : (n < m) → (m = o) → (n < o) :=
  begin
    intros h_lt h_eq,
    rw h_eq at h_lt, -- focus point 1
    exact h_lt       -- focus point 2
  end

Is there a way to perform the substitution inline in some way? So that I can write something like:

...
    intros h_lt h_eq,
    exact (h_lt <~ h_eq)
  end

[Kevin Buzzard]

exact h_eq ▸ h_lt,

[Kevin Buzzard]

The triangle is just notation for eq.subst and after a while you learn that the rw tactic is _far_ more sophisticated, however it will work if the stars are aligned.

[Damiano Testa]

While not shorter, calc produces very readable code:

λ hlt heq, calc n < m : hlt
   ... = o : heq

(I'm not at a computer: the code above is untested.)

[Alistair Tucker]

A third option: rwa h_eq at hlt

[Marcus Rossel]

Kevin Buzzard said:

The triangle is just notation for eq.subst and after a while you learn that the rw tactic is _far_ more sophisticated, however it will work if the stars are aligned.

Ok yeah, the stars being aligned was my problem :D
I tried this syntax but there were metavariables messing it up.