Unfold a cast expression

Stream: new members

[Oskar Berndal]

How can I simplify/unfold a cast expression? Below should illustrate an example of what I mean.

import data.nat.parity

inductive parity
| even : parity
| odd : parity

def suitable : parity → ℕ → Prop
| parity.even n := (n%2 = 0)
| parity.odd  n := (n%2 = 1)

def pa_nat (σ : parity) := {n : ℕ // suitable σ n}

def pa_nat_to_nat {σ : parity} : pa_nat σ → ℕ
| ⟨n, _⟩ := n

instance pa_nat_to_nat_coe {σ : parity} : has_coe (pa_nat σ) ℕ :=
⟨ pa_nat_to_nat ⟩

def opaque_function : ℕ → ℕ → ℕ
| n m := n + m

lemma apply_opaque_function {σ σ' : parity} :  ∀ (n : pa_nat σ) (m : pa_nat σ'), σ ≠ σ' → (opaque_function n m)%2 = 1
| ⟨n, p⟩ ⟨m, q⟩ neq :=
begin
  sorry --how to unfold the casts?
end

I know that I can use the change tactic to say what I want the goal to be but that is quite cumbersome in my use case and it feels like there should be a way that 'uses' the casts.

[Johan Commelin]

@Oskar Berndal unfold_coes is a tactic made exactly for this job :smiley:

[Oskar Berndal]

Indeed it did! Many thanks ^___^