Theorem: WType.encode_mk_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 β
a : α
f : β a → WType β
⊢ encode (mk a f) =
    ((Finset.univ.sup fun n => (f n).depth) + 1).pair ((encode a).pair (encode fun b => (encode (f b)).unpair.2))
Tactic:
simp[encode_eq, SubWType.ofW, depth, SubWType.encode_mk]
State after:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ (fun b => encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯)) = fun b =>
    encode (SubWType.ofWType (f b) (f b).depth ⋯)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ (fun b => encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯)) = fun b =>
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Tactic:
funext b
State after:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
b : β a
⊢ encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯) =
    encode (SubWType.ofWType (f b) (f b).depth ⋯)

State before:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
b : β a
⊢ encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯) =
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Tactic:
simp[SubWType.encode_eq_elim']
State after:
no goals