Theorem: WType.SubWType.encodeDecode_eq_elimDecode (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 β
s e : ℕ
⊢ encodeDecode (SubWType β s) e = elimDecode β (fun a l => encode (a, l)) s e
Tactic:
simp[elimDecode, 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 β
s e : ℕ
⊢ Option.map encode (decode e) =
    Option.map (elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s)
      (decode e)

State before:
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ Option.map encode (decode e) =
    Option.map (elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s)
      (decode e)
Tactic:
rcases (decode e) <;> simp[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 β
s e : ℕ
val✝ : SubWType β s
⊢ elim' ℕ encode s val✝ =
    elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s val✝

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 β
s e : ℕ
val✝ : SubWType β s
⊢ elim' ℕ encode s val✝ =
    elim' ℕ (fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))) s val✝
Tactic:
congr
State after:
case some.e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
val✝ : SubWType β s
⊢ encode = fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))

State before:
case some.e_fγ
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
val✝ : SubWType β s
⊢ encode = fun x => (encode x.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
Tactic:
funext ⟨a, f⟩
State after:
case some.e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ encode ⟨a, f⟩ = (encode ⟨a, f⟩.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)))

State before:
case some.e_fγ.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
val✝ : SubWType β s
a : α
f : β a → ℕ
⊢ encode ⟨a, f⟩ = (encode ⟨a, f⟩.fst).pair (encode (List.ofFn (fintypeArrowEquivFinArrow ⟨a, f⟩.snd)))
Tactic:
simp[encode_fintypeArrow, encode_finArrow]
State after:
no goals