Theorem: WType.decode_elimL_eq (Logic/Vorspiel/W.lean)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map (elimL f) (decode e) = SubWType.elimDecode β f e.unpair.1 e.unpair.2
Tactic:
unfold elimL
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (elim γ fun x =>
        match x with
        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
      (decode e) =
    SubWType.elimDecode β f e.unpair.1 e.unpair.2

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (elim γ fun x =>
        match x with
        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
      (decode e) =
    SubWType.elimDecode β f e.unpair.1 e.unpair.2
Tactic:
simp[elimL, decode_eq, Function.comp, SubWType.elimDecode, SubWType.elim']
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (fun x => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (SubWType.toW ⟨e.unpair.1, x⟩))
      (decode e.unpair.2) =
    Option.map (SubWType.elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) e.unpair.1)
      (decode e.unpair.2)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
γ : Type u_3
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (fun x => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (SubWType.toW ⟨e.unpair.1, x⟩))
      (decode e.unpair.2) =
    Option.map (SubWType.elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) e.unpair.1)
      (decode e.unpair.2)
Tactic:
rcases (decode e.unpair.2) with (_ | ⟨_, _⟩) <;> simp[SubWType.toW]
State after:
no goals