Theorem: WType.SubWType.elimDecode_eq_induction (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
γ : Type u_4
f : α → List γ → γ
s e : ℕ
⊢ elimDecode β f s e =
    Nat.casesOn s none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM' (elimDecode β f s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
            if l.length = Fintype.card (β a) then some l else none)
Tactic:
unfold elimDecode
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
γ : Type u_4
f : α → List γ → γ
s e : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        s)
      (decode e) =
    Nat.casesOn s none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)

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
γ : Type u_4
f : α → List γ → γ
s e : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        s)
      (decode e) =
    Nat.casesOn s none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)
Tactic:
rcases s with (_ | s)
State after:
case zero
α : 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
γ : Type u_4
f : α → List γ → γ
e : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        0)
      (decode e) =
    Nat.casesOn 0 none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)

case succ
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        (s + 1))
      (decode e) =
    Nat.casesOn (s + 1) none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)

State before:
case zero
α : 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
γ : Type u_4
f : α → List γ → γ
e : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        0)
      (decode e) =
    Nat.casesOn 0 none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)
Tactic:
simp
State after:
no goals

State before:
case succ
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ Option.map
      (elim' γ
        (fun x =>
          match x with
          | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
        (s + 1))
      (decode e) =
    Nat.casesOn (s + 1) none fun s =>
      (decode e.unpair.1).bind fun a =>
        Option.map (fun v => f a v)
          ((mapM'
                (fun e =>
                  Option.map
                    (elim' γ
                      (fun x =>
                        match x with
                        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
                      s)
                    (decode e))
                (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
            fun l => if l.length = Fintype.card (β a) then some l else none)
Tactic:
simp[SubWType.decode_succ, Option.map_bind', decode_list, Function.comp, List.mapM'_option_map]
State after:
case succ
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
        Option.map
          (fun x =>
            elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
              (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
          (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.1).bind fun a =>
      (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
            (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
        fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)

State before:
case succ
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
        Option.map
          (fun x =>
            elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
              (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
          (List.toVector (Fintype.card (β a)) a_1)) =
    (decode e.unpair.1).bind fun a =>
      (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
            (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
        fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)
Tactic:
congr
State after:
case succ.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ (fun a =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
        Option.map
          (fun x =>
            elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
              (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
          (List.toVector (Fintype.card (β a)) a_1)) =
    fun a =>
    (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
          (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
      fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)

State before:
case succ.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
⊢ (fun a =>
      (mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
        Option.map
          (fun x =>
            elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
              (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
          (List.toVector (Fintype.card (β a)) a_1)) =
    fun a =>
    (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
          (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
      fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)
Tactic:
funext a
State after:
case succ.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 β
σ : Type u_3
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
⊢ ((mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
      Option.map
        (fun x =>
          elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
            (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
        (List.toVector (Fintype.card (β a)) a_1)) =
    (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
          (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
      fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)

State before:
case succ.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 β
σ : Type u_3
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
⊢ ((mapM' decode (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun a_1 =>
      Option.map
        (fun x =>
          elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
            (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
        (List.toVector (Fintype.card (β a)) a_1)) =
    (Option.map (fun bs => List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) bs)
          (mapM' (fun a => decode a) (Denumerable.ofNat (List ℕ) e.unpair.2))).bind
      fun a_1 => Option.map (fun v => f a v) (if a_1.length = Fintype.card (β a) then some a_1 else none)
Tactic:
rcases List.mapM' (decode : ℕ → Option (SubWType β s)) (Denumerable.ofNat (List ℕ) e.unpair.2) with (_ | w) <;> simp
State after:
case succ.e_a.h.some
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
⊢ Option.map
      (fun x =>
        elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
          (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
      (List.toVector (Fintype.card (β a)) w) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)

State before:
case succ.e_a.h.some
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
⊢ Option.map
      (fun x =>
        elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
          (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
      (List.toVector (Fintype.card (β a)) w) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)
Tactic:
{ simp[List.toVector]
  by_cases hlw : w.length = Fintype.card (β a) <;> simp[hlw, elim, elim']
  { simp[Vector.get_mk_eq_get, List.ofFn_get_eq_map_cast]; congr
    rw[Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin (fun i =>
      WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (w.get (i.cast hlw.symm)).val)];
    rw[List.ofFn_get_eq_map_cast (fun z => WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) z.val) w];rfl } }
State after:
no goals

State before:
case succ.e_a.h.some
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
⊢ Option.map
      (fun x =>
        elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
          (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
      (List.toVector (Fintype.card (β a)) w) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)
Tactic:
simp[List.toVector]
State after:
case succ.e_a.h.some
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
⊢ Option.map
      (fun x =>
        elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
          (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
      (if h : w.length = Fintype.card (β a) then some ⟨w, h⟩ else none) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)

State before:
case succ.e_a.h.some
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
⊢ Option.map
      (fun x =>
        elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (s + 1)
          (ofWType (WType.mk a fun b => ↑(x.get (fintypeEquivFin b))) (s + 1) ⋯))
      (if h : w.length = Fintype.card (β a) then some ⟨w, h⟩ else none) =
    Option.map (fun v => f a v)
      (if w.length = Fintype.card (β a) then
        some (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
      else none)
Tactic:
by_cases hlw : w.length = Fintype.card (β a) <;> simp[hlw, elim, elim']
State after:
case pos
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ f a
      (List.ofFn
        (fintypeArrowEquivFinArrow fun b =>
          elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
            ↑(Vector.get ⟨w, ⋯⟩ (fintypeEquivFin b)))) =
    f a (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)

State before:
case pos
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ f a
      (List.ofFn
        (fintypeArrowEquivFinArrow fun b =>
          elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
            ↑(Vector.get ⟨w, ⋯⟩ (fintypeEquivFin b)))) =
    f a (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
Tactic:
{ simp[Vector.get_mk_eq_get, List.ofFn_get_eq_map_cast]; congr
  rw[Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin (fun i =>
    WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (w.get (i.cast hlw.symm)).val)];
  rw[List.ofFn_get_eq_map_cast (fun z => WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) z.val) w];rfl }
State after:
no goals

State before:
case pos
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ f a
      (List.ofFn
        (fintypeArrowEquivFinArrow fun b =>
          elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
            ↑(Vector.get ⟨w, ⋯⟩ (fintypeEquivFin b)))) =
    f a (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
Tactic:
simp[Vector.get_mk_eq_get, List.ofFn_get_eq_map_cast]
State after:
case pos
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ f a
      (List.ofFn
        (fintypeArrowEquivFinArrow fun b =>
          elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
            ↑(w.get (Fin.cast ⋯ (fintypeEquivFin b))))) =
    f a (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)

State before:
case pos
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ f a
      (List.ofFn
        (fintypeArrowEquivFinArrow fun b =>
          elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
            ↑(w.get (Fin.cast ⋯ (fintypeEquivFin b))))) =
    f a (List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w)
Tactic:
congr
State after:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ List.ofFn
      (fintypeArrowEquivFinArrow fun b =>
        elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
          ↑(w.get (Fin.cast ⋯ (fintypeEquivFin b)))) =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w

State before:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ List.ofFn
      (fintypeArrowEquivFinArrow fun b =>
        elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd)))
          ↑(w.get (Fin.cast ⋯ (fintypeEquivFin b)))) =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w
Tactic:
rw[Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin (fun i =>
  WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (w.get (i.cast hlw.symm)).val)]
State after:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ (List.ofFn fun i => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) ↑(w.get (Fin.cast ⋯ i))) =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w

State before:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ (List.ofFn fun i => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) ↑(w.get (Fin.cast ⋯ i))) =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w
Tactic:
rw[List.ofFn_get_eq_map_cast (fun z => WType.elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) z.val) w]
State after:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ List.map (fun z => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) ↑z) w =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w

State before:
case pos.e_a
α : 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
γ : Type u_4
f : α → List γ → γ
e s : ℕ
a : α
w : List (SubWType β s)
hlw : w.length = Fintype.card (β a)
⊢ List.map (fun z => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) ↑z) w =
    List.map (elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) s) w
Tactic:
rfl
State after:
no goals