Theorem: WType.SubWType.decode_succ (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 : ℕ
a : α
l : List (SubWType β s)
v : Vector (SubWType β s) (Fintype.card (β a))
⊢ (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)).depth ≤ s + 1
Tactic:
simp[depth, Equiv.vectorEquivFin]
State after:
no goals

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 : ℕ
x : (a : α) × (β a → SubWType β s)
⊢ (WType.mk x.fst fun b => ↑(x.snd b)).depth ≤ s + 1
Tactic:
simp[depth]
State after:
no goals

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 : ℕ
⊢ decode e = Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯) (decode e)
Tactic:
simp[Primcodable.SubWType, primcodable_succ, Primcodable.ofEquiv_toEncodable]
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 : ℕ
⊢ decode e =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (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 β
s e : ℕ
⊢ decode e =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Tactic:
rw[Encodable.decode_ofEquiv equiv_succ, equiv_succ]
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
      (⇑{
            toFun := fun x =>
              match x with
              | ⟨t, h⟩ =>
                WType.casesOn (motive := fun x => x.depth ≤ s + 1 → (a : α) × (β a → SubWType β s)) t
                  (fun a f h => ⟨a, fun b => ⟨f b, ⋯⟩⟩) h,
            invFun := fun x =>
              match x with
              | ⟨a, f⟩ => ofWType (WType.mk a fun b => ↑(f b)) (s + 1) ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm)
      (decode e) =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (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 β
s e : ℕ
⊢ Option.map
      (⇑{
            toFun := fun x =>
              match x with
              | ⟨t, h⟩ =>
                WType.casesOn (motive := fun x => x.depth ≤ s + 1 → (a : α) × (β a → SubWType β s)) t
                  (fun a f h => ⟨a, fun b => ⟨f b, ⋯⟩⟩) h,
            invFun := fun x =>
              match x with
              | ⟨a, f⟩ => ofWType (WType.mk a fun b => ↑(f b)) (s + 1) ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm)
      (decode e) =
    Option.map (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯)
      ((decode e.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode e.unpair.2))
Tactic:
simp
State after:
no goals

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 : ℕ
a : α
x : β a → SubWType β s
⊢ (WType.mk a fun b => ↑(x b)).depth ≤ s + 1
Tactic:
simp[depth]
State after:
no goals

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 (fun x => ofWType (WType.mk x.fst fun b => ↑(x.snd b)) (s + 1) ⋯) (decode e) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)
Tactic:
simp[Encodable.decode_sigma_val, Option.map_bind', Function.comp]
State after:
no goals

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 : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)) =
    (decode e.unpair.1).bind fun a =>
      (decode e.unpair.2).bind fun l =>
        Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
          (List.toVector (Fintype.card (β a)) l)
Tactic:
congr
State after:
case e_a
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ (fun a => Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)) = fun a =>
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)

State before:
case e_a
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
s e : ℕ
⊢ (fun a => Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2)) = fun a =>
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)
Tactic:
funext a
State after:
case e_a.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 : ℕ
a : α
⊢ Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2) =
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)

State before:
case e_a.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 : ℕ
a : α
⊢ Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) (decode e.unpair.2) =
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)
Tactic:
rw[decode_fintypeArrow]
State after:
case e_a.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 : ℕ
a : α
⊢ Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯)
      ((decode e.unpair.2).bind fun l =>
        Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card (β a)) l)) =
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)

State before:
case e_a.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 : ℕ
a : α
⊢ Option.map (fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯)
      ((decode e.unpair.2).bind fun l =>
        Option.map (⇑fintypeArrowEquivVector.symm) (List.toVector (Fintype.card (β a)) l)) =
    (decode e.unpair.2).bind fun l =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(fintypeArrowEquivVector.symm v b)) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) l)
Tactic:
simp[Option.map_bind']
State after:
case e_a.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 : ℕ
a : α
⊢ ((decode e.unpair.2).bind fun a_1 =>
      Option.map ((fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) ∘ ⇑fintypeArrowEquivVector.symm)
        (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.2).bind fun a_1 =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(v.get (fintypeEquivFin b))) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) a_1)

State before:
case e_a.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 : ℕ
a : α
⊢ ((decode e.unpair.2).bind fun a_1 =>
      Option.map ((fun x => ofWType (WType.mk a fun b => ↑(x b)) (s + 1) ⋯) ∘ ⇑fintypeArrowEquivVector.symm)
        (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.2).bind fun a_1 =>
      Option.map (fun v => ofWType (WType.mk a fun b => ↑(v.get (fintypeEquivFin b))) (s + 1) ⋯)
        (List.toVector (Fintype.card (β a)) a_1)
Tactic:
congr
State after:
no goals