Avoid mentioning long expression

Stream: new members

[Bjørn Kjos-Hanssen]

Suppose I want to prove the following without having to type out the long expressions a_longExpression, b_longExpression in the middle of the proof.

example (U : Type*) (R : U → Prop) (a_longExpression b_longExpression : U)
  (h : R a_longExpression) : R b_longExpression := by
  revert h
  apply Iff.mp
  apply Eq.to_iff
  congr
  -- let's say that a_longExpression = b_longExpression
  -- can now be proved by some tactic
  sorry

I made up the method above, consisting of the four tactic lines, myself; perhaps there's a more canonical way?

In other words, how to point out that it suffices to prove a_longExpression = b_longExpression without mentioning a_longExpression, b_longExpression explicitly?

[Kenny Lau]

convert h

[Kenny Lau]

@Bjørn Kjos-Hanssen

[Bjørn Kjos-Hanssen]

Perfect, thanks!