Cases not resolving match

Stream: lean4

[Marcus Rossel]

In the following (contrived) example ...

inductive Raw
  | one   (x : Nat)
  | two   (x : Nat)
  | three (x : Nat)

inductive Thing
  | one   (x : Nat)
  | two   (x : Nat)
  | three (x : Nat)

def Raw.toThing (r : Raw) : Thing :=
  match h:r with
  | one   x => Thing.one x
  | two   x => Thing.two x
  | three x => Thing.three x

inductive Thing.rawEquiv (t : Thing) (r : Raw) : Prop
  | one   {x} : t = one x   → r = Raw.one x   → rawEquiv t r
  | two   {x} : t = two x   → r = Raw.two x   → rawEquiv t r
  | three {x} : t = three x → r = Raw.three x → rawEquiv t r

... I'm trying to prove:

theorem Thing.toThing_rawEquiv (t : Thing) (r : Raw) : t = r.toThing → t.rawEquiv r :=
  by ...

If I do ...

intro h
cases r
case one =>
  cases t
  case one =>
    simp [Raw.toThing] at h

... I get ...

x✝¹ x✝ : ℕ
h : x✝ = x✝¹
⊢ rawEquiv (one x✝) (Raw.one x✝¹)

Which is nice in that it gives me x✝ = x✝¹, but I also need r = Raw.one x✝¹ and t = one x✝.
So I tried:

  intro h
  cases h₁ : r
  case one =>
    cases h₂ : t
    case one =>
      simp [Raw.toThing] at h

... which gives me:

t : Thing
r : Raw
x✝¹ : ℕ
h₁ : r = Raw.one x✝¹
x✝ : ℕ
h₂ : t = one x✝
h : t =
  match r, (_ : r = r) with
  | Raw.one x, h => one x
  | Raw.two x, h => two x
  | Raw.three x, h => three x
⊢ rawEquiv (one x✝) (Raw.one x✝¹)

But no matter what I do, I can't reduce the match expression to get x✝ = x✝¹.

Why does adding the proof labels h₁ and h₂ remove the ability to resolve the match?

[Henrik Böving]

I was able to solve the first case like this:

theorem Thing.toThing_rawEquiv (t : Thing) (r : Raw) : t = r.toThing → t.rawEquiv r := by
  intro h
  cases r with
  | one x1 =>
    cases t with
    | one x2 =>
      simp [Raw.toThing] at h
      rw [h]
      apply rawEquiv.one
      rfl
      rfl
    | two x2 => sorry
    | three x2 => sorry
  | two => sorry
  | three => sorry

Although the proof state after apply rawEquiv.one looks a bit weird:

Goals (3)
case one.one.a
x1 x2 : Nat
h : x2 = x1
⊢ one x1 = one ?one.one.x

case one.one.a
x1 x2 : Nat
h : x2 = x1
⊢ Raw.one x1 = Raw.one ?one.one.x

case one.one.x
x1 x2 : Nat
h : x2 = x1
⊢ Nat

But lean figures out the meta variable out itself based on my use of the refl tactic it seems?

[Mac]

Printing out the definition of the partial theorems shows that Lean deduces a different motive when the labels are added for some reason:

theorem Thing.toThing_rawEquiv (t : Thing) (r : Raw) : t = r.toThing → t.rawEquiv r := by
  intro h
  cases r
  case one =>
    cases t
    case one =>
      simp [Raw.toThing] at h

#print Thing.toThing_rawEquiv
/-
theorem Thing.toThing_rawEquiv : ∀ (t : Thing) (r : Raw), t = Raw.toThing r → Thing.rawEquiv t r :=
fun t r h =>
  Raw.casesOn (motive := fun t_1 => r = t_1 → Thing.rawEquiv t r) r
    (fun x h_1 =>
      Eq.ndrec (motive := fun r => t = Raw.toThing r → Thing.rawEquiv t r)
        (fun h => sorryAx (Thing.rawEquiv t (Raw.one x))) (Eq.symm h_1) h)
    (fun x h_1 =>
      Eq.ndrec (motive := fun r => t = Raw.toThing r → Thing.rawEquiv t r)
        (fun h => sorryAx (Thing.rawEquiv t (Raw.two x))) (Eq.symm h_1) h)
    (fun x h_1 =>
      Eq.ndrec (motive := fun r => t = Raw.toThing r → Thing.rawEquiv t r)
        (fun h => sorryAx (Thing.rawEquiv t (Raw.three x))) (Eq.symm h_1) h)
    (Eq.refl r)
-/

theorem Thing.toThing_rawEquiv' (t : Thing) (r : Raw) : t = r.toThing → t.rawEquiv r := by
  intro h
  cases h₁ : r
  case one =>
    cases h₂ : t
    case one =>
      simp [Raw.toThing] at h

#print Thing.toThing_rawEquiv'
/-
theorem Thing.toThing_rawEquiv' : ∀ (t : Thing) (r : Raw), t = Raw.toThing r → Thing.rawEquiv t r :=
fun t r h =>
  Raw.casesOn (motive := fun t_1 => r = t_1 → Thing.rawEquiv t r) r
    (fun x h =>
      Eq.ndrec (motive := fun x => r = x → Thing.rawEquiv t x) (fun h₁ => sorryAx (Thing.rawEquiv t (Raw.one x)))
        (Eq.symm h) (Eq.refl r))
    (fun x h =>
      Eq.ndrec (motive := fun x => r = x → Thing.rawEquiv t x) (fun h₁ => sorryAx (Thing.rawEquiv t (Raw.two x)))
        (Eq.symm h) (Eq.refl r))
    (fun x h =>
      Eq.ndrec (motive := fun x => r = x → Thing.rawEquiv t x) (fun h₁ => sorryAx (Thing.rawEquiv t (Raw.three x)))
        (Eq.symm h) (Eq.refl r))
    (Eq.refl r)
-/

[Marcus Rossel]

(deleted)