internlm/Lean-Github huggingface dataset:
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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]
Proof 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)
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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']
Proof 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)
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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 }
Proof state after:
no goals
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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]
Proof 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)
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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
Proof 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
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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)]
Proof 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
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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]
Proof 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
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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
Proof state after:
no goals
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
s e : ℕ
⊢ WType.SubWType.elimDecodeG β f x (s, e)
      (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))) =
    elimDecode β (f x) s e
Tactic:
simp[elimDecode_eq_induction β (f x) s e, elimDecodeG]
Proof 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 γ → γ
x : σ
s e : ℕ
⊢ Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM'
                  (fun c =>
                    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))).getI
                      (n.pair c))
                  (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
              fun l => if l.length = Fintype.card (β a) then some l else none))
      s =
    Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM' (elimDecode β (f x) n) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
              if l.length = Fintype.card (β a) then some l else none))
      s
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
s e : ℕ
⊢ Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM'
                  (fun c =>
                    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range (s.pair e))).getI
                      (n.pair c))
                  (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
              fun l => if l.length = Fintype.card (β a) then some l else none))
      s =
    Nat.rec none
      (fun n n_ih =>
        (decode e.unpair.1).bind fun a =>
          Option.map (fun v => f x a v)
            ((mapM' (elimDecode β (f x) n) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
              if l.length = Fintype.card (β a) then some l else none))
      s
Tactic:
rcases s with (_ | s) <;> simp
Proof 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 γ → γ
x : σ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
          if l.length = Fintype.card (β a) then some l else none)
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
⊢ ((decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    (decode e.unpair.1).bind fun a =>
      Option.map (fun v => f x a v)
        ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
          if l.length = Fintype.card (β a) then some l else none)
Tactic:
congr
Proof 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 γ → γ
x : σ
e s : ℕ
⊢ (fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    fun a =>
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
⊢ (fun a =>
      Option.map (fun v => f x a v)
        ((mapM'
              (fun c =>
                (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                  (s.pair c))
              (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
          fun l => if l.length = Fintype.card (β a) then some l else none)) =
    fun a =>
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
funext a
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
have :
  mapM' (fun c => ((List.range ((s + 1).pair e)).map $ fun i => elimDecode β (f x) i.unpair.fst i.unpair.snd).getI (s.pair c))
    (Denumerable.ofNat (List ℕ) e.unpair.2) =
  mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2) :=
List.mapM'_eq_mapM'_of_eq _ (by
{ intro c hc
  have : s.pair c < (s + 1).pair e := by
    have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
    exact lt_of_lt_of_le (Nat.pair_lt_pair_right s this) (Nat.pair_le_pair_of_le (Nat.le_succ s) (Nat.unpair_right_le e))
  simp[List.getI_map_range _ this] })
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
this :
  mapM'
      (fun c =>
        (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c))
      (Denumerable.ofNat (List ℕ) e.unpair.2) =
    mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
this :
  mapM'
      (fun c =>
        (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c))
      (Denumerable.ofNat (List ℕ) e.unpair.2) =
    mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)
⊢ Option.map (fun v => f x a v)
      ((mapM'
            (fun c =>
              (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI
                (s.pair c))
            (Denumerable.ofNat (List ℕ) e.unpair.2)).bind
        fun l => if l.length = Fintype.card (β a) then some l else none) =
    Option.map (fun v => f x a v)
      ((mapM' (elimDecode β (f x) s) (Denumerable.ofNat (List ℕ) e.unpair.2)).bind fun l =>
        if l.length = Fintype.card (β a) then some l else none)
Tactic:
rw[this]
Proof state after:
no goals
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
⊢ ∀ a ∈ Denumerable.ofNat (List ℕ) e.unpair.2,
    (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair a) =
      elimDecode β (f x) s a
Tactic:
intro c hc
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Tactic:
have : s.pair c < (s + 1).pair e := by
  have : c < e.unpair.2 := Denumerable.lt_of_mem_list _ _ hc
  exact lt_of_lt_of_le (Nat.pair_lt_pair_right s this) (Nat.pair_le_pair_of_le (Nat.le_succ s) (Nat.unpair_right_le e))
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
this : s.pair c < (s + 1).pair e
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Theorem: WType.SubWType.elimDecodeG_eq_elimDecode
Proof 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 γ → γ
x : σ
e s : ℕ
a : α
c : ℕ
hc : c ∈ Denumerable.ofNat (List ℕ) e.unpair.2
this : s.pair c < (s + 1).pair e
⊢ (List.map (fun i => elimDecode β (f x) i.unpair.1 i.unpair.2) (List.range ((s + 1).pair e))).getI (s.pair c) =
    elimDecode β (f x) s c
Tactic:
simp[List.getI_map_range _ this]
Proof state after:
no goals