Proving lemma without doing pattern matching

Stream: general

[petercommand]

lemma eq.subst' {α : Sort u} {a b : α} {P : Π (m: α), (m = a) ∨ (m = b) → Prop}
    (h₁ : a = b) (h₂ : P a (or.inl rfl)) : P b (or.inr rfl) := by cases h₁; assumption

Is it possible to prove this lemma with eliminators without doing pattern matching?

[petercommand]

In this example, I am trying to prove a variant of the traditional Leibniz equality (subst)

[Patrick Massot]

Of course it's possible, this is what Lean does in the end. You can #print eq.subst'. Or am I missing something?

[petercommand]

You are right, it's just that I need to set_option pp.implicit true before #print eq.subst'

[petercommand]

I thought the generated program doesn't typecheck

[Patrick Massot]

(deleted)