internlm/Lean-Github huggingface dataset:
Theorem: WType.SubWType.decode_succ
Proof 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
Proof 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)
Theorem: WType.SubWType.decode_succ
Proof 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]
Proof 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)
Theorem: WType.SubWType.decode_succ
Proof 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']
Proof 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)
Theorem: WType.SubWType.decode_succ
Proof 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
Proof state after:
no goals
Theorem: WType.SubWType.encode_mk
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
b : β a
⊢ (f b).depth ≤ s
Tactic:
simp[depth] at h
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 β
s : ℕ
a : α
f : β a → WType β
b : β a
h : ∀ (b : β a), (f b).depth ≤ s
⊢ (f b).depth ≤ s
Theorem: WType.SubWType.encode_mk
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 β
s : ℕ
a : α
f : β a → WType β
b : β a
h : ∀ (b : β a), (f b).depth ≤ s
⊢ (f b).depth ≤ s
Tactic:
exact h b
Proof state after:
no goals
Theorem: WType.SubWType.encode_mk
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode (ofWType (WType.mk a f) (s + 1) h) = (encode a).pair (encode fun b => encode (ofWType (f b) s ⋯))
Tactic:
rw [Encodable.encode_ofEquiv equiv_succ, equiv_succ, ofWType, Equiv.coe_fn_mk, Encodable.encode_sigma_val, Nat.pair_eq_pair]
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode a = encode a ∧ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Theorem: WType.SubWType.encode_mk
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ encode a = encode a ∧ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Tactic:
simp
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Theorem: WType.SubWType.encode_mk
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 β
s : ℕ
a : α
f : β a → WType β
h : (WType.mk a f).depth ≤ s + 1
⊢ (encode fun b => ⟨f b, ⋯⟩) = encode fun b => encode (ofWType (f b) s ⋯)
Tactic:
exact encode_fintypeArrow' (β a) (SubWType β s) _
Proof state after:
no goals
Theorem: WType.SubWType.encode_cast
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 β
s : ℕ
w : SubWType β s
s' : ℕ
hs : s = s'
⊢ encode w = encode (cast hs w)
Tactic:
rcases hs with rfl
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 β
s : ℕ
w : SubWType β s
⊢ encode w = encode (cast ⋯ w)
Theorem: WType.SubWType.encode_cast
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 β
s : ℕ
w : SubWType β s
⊢ encode w = encode (cast ⋯ w)
Tactic:
simp
Proof state after:
no goals
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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
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 γ → γ
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)
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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)
Proof 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)
Theorem: WType.SubWType.elimDecode_eq_induction
Proof 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
Proof state after:
no goals
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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]
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 γ → γ
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)
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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
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 γ → γ
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)
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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
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 γ → γ
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)
Theorem: WType.SubWType.elimDecode_eq_induction
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 γ → γ
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
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) ⋯))
      (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)
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]
  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 } }
Proof state after:
no goals