unification under pattern matches inside `structure`s

Stream: lean4

[Andrés Goens]

I'm having issues when trying to do pattern matching and use that to build new terms because Lean doesn't unfold the definition, i.e. it "forgets" the pattern match. Here's an attempt at an MWE:

inductive SomeType
  | someConstructor : Nat → SomeType

def SomeType.getN : SomeType → Nat
  | .someConstructor n => n

inductive DependentType (n : Nat)
  | mk : Fin n → DependentType n

structure SomeStruct where
  ty : SomeType
  depTy : DependentType ty.getN

def someFunction : SomeStruct → SomeStruct
  | struct => match struct.ty with
    |.someConstructor n =>
      have h : struct.ty.getN = n := by
        simp [SomeType.getN]
        rfl
      let depTy : DependentType (n+1) := match struct.depTy with
        | .mk n => .mk <| h ▸ n.succ
      { ty := .someConstructor (n+1), depTy := depTy }

Here, struct.tyshould be replaced by .someConstructor n through the pattern match, and I should be able to prove that h basically with unfolding, but it doesn't work. The rfl tactic there fails with:

x✝: SomeStruct
struct: SomeStruct := x✝
n: Nat
⊢ x✝.1.1 = n
Messages (1)
MWE.lean:19:8
tactic 'rfl' failed, equality lhs
  x✝.1.1
is not definitionally equal to rhs
  n
x✝: SomeStruct
struct: SomeStruct := x✝
n: Nat
⊢ x✝.1.1 = n

Somehow, the elaborator is building this extra x and there is no equality relating the pattern match (in this case n with struct.ty, i.e something like struct.ty = .someConstructor n. I think the structure is what's getting in the way here, but in my real case I also have (more complicated structures). Does anyone know if there's a way to get around this issue?

[Kyle Miller]

When a match discriminant is given something that's not just a variable, it turns it into let x := v; match x with ...

Option 1: write match h : struct.ty with and then use this h equality in your proofs

Option 2: fully destruct your struct and match on the resulting variable, like | {ty, depTy} => match ty with

[Marcus Rossel]

(deleted)