Theorem: WType.encode_decode_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 β
e : ℕ
⊢ (Option.casesOn (Option.map SubWType.toW (decode e)) 0 fun w => encode (SubWType.ofW w) + 1) =
    encode
      ((encodeDecode (SubWType β e.unpair.1) e.unpair.2).bind fun c =>
        Option.map (fun d => d.pair c) (Option.map (fun w => (↑w).depth) (decode c)))
Tactic:
simp[Function.comp, encodeDecode_eq_encode_map_decode]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ Option.rec 0 (fun val => encode (SubWType.ofW val) + 1)
      (Option.map (fun x => SubWType.toW ⟨e.unpair.1, x⟩) (decode e.unpair.2)) =
    encode ((Option.map encode (decode e.unpair.2)).bind fun a => Option.map (fun x => (↑x).depth.pair a) (decode a))

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
⊢ Option.rec 0 (fun val => encode (SubWType.ofW val) + 1)
      (Option.map (fun x => SubWType.toW ⟨e.unpair.1, x⟩) (decode e.unpair.2)) =
    encode ((Option.map encode (decode e.unpair.2)).bind fun a => Option.map (fun x => (↑x).depth.pair a) (decode a))
Tactic:
rcases (decode e.unpair.2) with (_ | w) <;> simp[SubWType.toW, SubWType.ofW]
State after:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w

State before:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
Tactic:
{ simp[SubWType.encode_eq_elim']; apply SubWType.elim_const; simp }
State after:
no goals

State before:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ encode (SubWType.ofWType (↑w) (↑w).depth ⋯) = encode w
Tactic:
simp[SubWType.encode_eq_elim']
State after:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ SubWType.elim' ℕ encode (↑w).depth (SubWType.ofWType (↑w) (↑w).depth ⋯) = SubWType.elim' ℕ encode e.unpair.1 w

State before:
case some
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ SubWType.elim' ℕ encode (↑w).depth (SubWType.ofWType (↑w) (↑w).depth ⋯) = SubWType.elim' ℕ encode e.unpair.1 w
Tactic:
apply SubWType.elim_const
State after:
case some.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ ↑(SubWType.ofWType (↑w) (↑w).depth ⋯) = ↑w

State before:
case some.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
e : ℕ
w : SubWType β e.unpair.1
⊢ ↑(SubWType.ofWType (↑w) (↑w).depth ⋯) = ↑w
Tactic:
simp
State after:
no goals