Proof by rfl fails after adding rcases on choose

Stream: mathlib4

[Michael Rothgang]

I'd like to prove a "trivial lemma" about a new definition I've made; this ought to be a proof by rfl, but fails. I don't understand why; I've narrowed it down to an rcases call on the result of a choose tactic. Any pointers appreciated.
(Broader context is my in-progress PR #8738xx.)

Somewhat minimal example; I suspect this is not related to my new definition:

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {H : Type*} [TopologicalSpace H]
  {G : Type*} [TopologicalSpace G]
  (I : ModelWithCorners 𝕜 E H) (J : ModelWithCorners 𝕜 F G)
  (M : Type*) [TopologicalSpace M] [ChartedSpace H M]
  (N : Type*) [TopologicalSpace N] [ChartedSpace G N] (n : ℕ∞)
  [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners J N]

structure PartialDiffeomorph extends PartialEquiv M N where
  open_source : IsOpen source
  open_target : IsOpen target
  contMDiffOn_toFun : ContMDiffOn I J n toFun source
  contMDiffOn_invFun : ContMDiffOn J I n invFun target

instance : CoeFun (PartialDiffeomorph I J M N n) fun _ => M → N :=
  ⟨fun Φ => Φ.toFun⟩

variable {M N} in
def IsLocalDiffeomorphAt (f : M → N) (x : M) : Prop :=
  ∃ Φ : PartialDiffeomorph I J M N n, x ∈ Φ.source ∧ Set.EqOn f Φ Φ.source

noncomputable def IsLocalDiffeomorphAt.mydef {f : M → N} {x : M}
    (hf : IsLocalDiffeomorphAt I J n f x) :
    ContinuousLinearEquiv (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace J (f x)) := by
  choose Φ hyp using hf
  --rcases hyp with ⟨hxU, heq⟩ -- uncommenting this line breaks the proof below!
  exact {
    toFun := mfderiv I J f x
    invFun := sorry
    left_inv := sorry
    right_inv := sorry
    continuous_toFun := sorry
    continuous_invFun := sorry
    map_add' := sorry
    map_smul' := sorry
  }

lemma foo {f : M → N} {x : M} (hf : IsLocalDiffeomorphAt I J n f x) :
  hf.mydef = mfderiv I J f x := by rfl

[Michael Rothgang]

I'm not sure if this is best posted in #new members, #mathlib4 or #lean4; feel free to move accordingly.

[Eric Wieser]

This is because eta reduction does not work on And, cf https://leanprover.zulipchat.com/#narrow/stream/236446-Type-theory/topic/And.2Erec/near/398483665

[Eric Wieser]

But also, using tactic blocks for anything non-trivial (ie, anything more than refine, intro, convert) when constructing data is usually ill-advised

[Eric Wieser]

Is docs#ContinuousLinearEquiv.ofBijective helpful to you?

[Michael Rothgang]

Thanks for the prompt response, this is really helpful!

[Michael Rothgang]

Eric Wieser said:

Is docs#ContinuousLinearEquiv.ofBijective helpful to you?

It solves my problem - at the price of having to impose a completeness assumption. (This means my result will only apply to Banach manifolds, as opposed to ones modelled on general normed space. I guess that's fine in practice.)

[Kevin Buzzard]

I think it's good practice to try and make everything work in as much generality as possible; future generations will thank you!