smart unfolding with Option.map

Stream: general

[Eric Wieser]

Is this expected behavior?

import Mathlib

namespace WithOne
variable {α β} [Mul α] [Mul β]

theorem map_injective {f : α →ₙ* β} (hf : Function.Injective f) : Function.Injective (map f) := by
  haveI := Option.map_injective hf
  eta_expand at this
  dsimp [Option.map.eq_def] at this
  delta Option.getD.match_1 at this  -- I couldn't work out how else to unfold this
  exact this

#print map_injective  -- proof is `id (fun this => this) (Option.map_injective hf)`

This works as expected:

import Mathlib

namespace WithOne
variable {α β} [Mul α] [Mul β]

set_option smartUnfolding false in
theorem map_injective {f : α →ₙ* β} (hf : Function.Injective f) : Function.Injective (map f) :=
  Option.map_injective hf

[Kenny Lau]

does convert work or am i missing the point?

import Mathlib

namespace WithOne
variable {α β} [Mul α] [Mul β]

theorem map_injective {f : α →ₙ* β} (hf : Function.Injective f) : Function.Injective (map f) := by
  convert Option.map_injective hf
  ext x; cases x <;> rfl

#print map_injective

[Eric Wieser]

The point is that this is defeq so I wasn't expecting to have to do anything

[Eric Wieser]

(of course you could argue that this shouldn't be defeq, but what I'm confused by is this "defeq but only if pushed" behavior)

[Kenny Lau]

hmm that is quite strange, they aren't even irreducible

[Aaron Liu]

it's smart unfolding