internlm/Lean-Github huggingface dataset:
Theorem: WType.decode_elimL_eq
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
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (elim γ fun x =>
        match x with
        | ⟨a, v⟩ => f a (List.ofFn (fintypeArrowEquivFinArrow v)))
      (decode e) =
    SubWType.elimDecode β f e.unpair.1 e.unpair.2
Tactic:
simp[elimL, decode_eq, Function.comp, SubWType.elimDecode, SubWType.elim']
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
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (fun x => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (SubWType.toW ⟨e.unpair.1, x⟩))
      (decode e.unpair.2) =
    Option.map (SubWType.elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) e.unpair.1)
      (decode e.unpair.2)
Theorem: WType.decode_elimL_eq
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
e : ℕ
f : α → List γ → γ
⊢ Option.map
      (fun x => elim γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) (SubWType.toW ⟨e.unpair.1, x⟩))
      (decode e.unpair.2) =
    Option.map (SubWType.elim' γ (fun x => f x.fst (List.ofFn (fintypeArrowEquivFinArrow x.snd))) e.unpair.1)
      (decode e.unpair.2)
Tactic:
rcases (decode e.unpair.2) with (_ | ⟨_, _⟩) <;> simp[SubWType.toW]
Proof state after:
no goals
Theorem: WType.elimvL_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 β
σ : Type u_3
γ : Type u_4
x : σ
fs : α → σ → σ
fγ : σ → α → List γ → γ
a : α
v : β a → WType β
⊢ elimvL fs fγ x (mk a v) = fγ x a (List.ofFn (fintypeArrowEquivFinArrow fun b => elimvL fs fγ (fs a x) (v b)))
Tactic:
simp[elimvL, elimv]
Proof state after:
no goals
Theorem: WType.encode_mk_eq
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 β
a : α
f : β a → WType β
⊢ encode (mk a f) =
    ((Finset.univ.sup fun n => (f n).depth) + 1).pair ((encode a).pair (encode fun b => (encode (f b)).unpair.2))
Tactic:
simp[encode_eq, SubWType.ofW, depth, SubWType.encode_mk]
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 β
a : α
f : β a → WType β
⊢ (fun b => encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯)) = fun b =>
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Theorem: WType.encode_mk_eq
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 β
a : α
f : β a → WType β
⊢ (fun b => encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯)) = fun b =>
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Tactic:
funext b
Proof state after:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
b : β a
⊢ encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯) =
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Theorem: WType.encode_mk_eq
Proof state before:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
b : β a
⊢ encode (SubWType.ofWType (f b) (Finset.univ.sup fun n => (f n).depth) ⋯) =
    encode (SubWType.ofWType (f b) (f b).depth ⋯)
Tactic:
simp[SubWType.encode_eq_elim']
Proof state after:
no goals
Theorem: WType.mk₀_eq
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 β
a : α
h : IsEmpty (β a)
⊢ mk₀ a = some (mk a h.elim')
Tactic:
simp[mk₀, mkL, Fintype.card_eq_zero_iff.mpr 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 β
a : α
h : IsEmpty (β a)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [].get (Fin.cast ⋯ i)) = h.elim'
Theorem: WType.mk₀_eq
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 β
a : α
h : IsEmpty (β a)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [].get (Fin.cast ⋯ i)) = h.elim'
Tactic:
funext x
Proof state after:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
x : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => [].get (Fin.cast ⋯ i)) x = h.elim' x
Theorem: WType.mk₀_eq
Proof state before:
case h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
h : IsEmpty (β a)
x : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => [].get (Fin.cast ⋯ i)) x = h.elim' x
Tactic:
exact IsEmpty.elim h x
Proof state after:
no goals
Theorem: WType.mkL_inversion
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 β
w : WType β
⊢ mkL w.inversion.1 w.inversion.2 = some w
Tactic:
rcases w with ⟨a, f⟩
Proof state after:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ mkL (mk a f).inversion.1 (mk a f).inversion.2 = some (mk a f)
Theorem: WType.mkL_inversion
Proof state before:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ mkL (mk a f).inversion.1 (mk a f).inversion.2 = some (mk a f)
Tactic:
simp[inversion, mkL]
Proof state after:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ (fintypeArrowEquivFinArrow.symm fun i => f (fintypeEquivFin.symm i)) = f
Theorem: WType.mkL_inversion
Proof state before:
case mk
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
⊢ (fintypeArrowEquivFinArrow.symm fun i => f (fintypeEquivFin.symm i)) = f
Tactic:
funext
Proof state after:
case mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
x✝ : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => f (fintypeEquivFin.symm i)) x✝ = f x✝
Theorem: WType.mkL_inversion
Proof state before:
case mk.h
α : Type u_1
β : α → Type u_2
inst✝⁴ : Primcodable α
inst✝³ : (a : α) → Fintype (β a)
inst✝² : (a : α) → DecidableEq (β a)
inst✝¹ : (a : α) → Primcodable (β a)
inst✝ : PrimrecCard β
a : α
f : β a → WType β
x✝ : β a
⊢ fintypeArrowEquivFinArrow.symm (fun i => f (fintypeEquivFin.symm i)) x✝ = f x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Primrec.w_depth
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
⊢ Primrec depth
Tactic:
have : Primrec (fun n => (encodeDecode (WType β) n).map $ fun e => e.unpair.1) :=
  option_map Primrec.encodeDecode (fst.comp₂ $ unpair.comp₂ Primrec₂.right)
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
⊢ Primrec depth
Theorem: Primrec.w_depth
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
⊢ Primrec depth
Tactic:
exact decode_iff.mp (this.of_eq $ fun n => by
  simp[encodeDecode_eq_encode_map_decode]
  rcases decode n <;> simp[WType.encode_eq, WType.SubWType.ofW])
Proof state after:
no goals
Theorem: Primrec.w_depth
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n) = Option.map depth (decode n)
Tactic:
simp[encodeDecode_eq_encode_map_decode]
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map ((fun e => e.unpair.1) ∘ encode) (decode n) = Option.map depth (decode n)
Theorem: Primrec.w_depth
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this : Primrec fun n => Option.map (fun e => e.unpair.1) (encodeDecode (WType β) n)
n : ℕ
⊢ Option.map ((fun e => e.unpair.1) ∘ encode) (decode n) = Option.map depth (decode n)
Tactic:
rcases decode n <;> simp[WType.encode_eq, WType.SubWType.ofW]
Proof state after:
no goals
Theorem: Primrec.w_elimL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → List γ → γ
hf : Primrec₂ f
⊢ Primrec fun n => Option.map (elimL f) (decode n)
Tactic:
simp[decode_elimL_eq]
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → List γ → γ
hf : Primrec₂ f
⊢ Primrec fun n => SubWType.elimDecode β f n.unpair.1 n.unpair.2
Theorem: Primrec.w_elimL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : α → List γ → γ
hf : Primrec₂ f
⊢ Primrec fun n => SubWType.elimDecode β f n.unpair.1 n.unpair.2
Tactic:
apply SubWType.primrec_elimDecode β hf
Proof state after:
no goals
Theorem: Primrec.w_elimL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)
Tactic:
have : Primrec₂ (fun x w => elimL (fun p l => f x (p, l)) w : σ → WType β → γ) :=
Primrec₂.decode_iff₂.mp
  (by simp[decode_elimL_eq]
      exact (SubWType.primrec_elimDecode_param β hf).comp₂ Primrec₂.left
        (Primrec.pair (fst.comp $ Primrec.unpair.comp snd) (snd.comp $ Primrec.unpair.comp snd)).to₂)
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
this : Primrec₂ fun x w => elimL (fun p l => f x (p, l)) w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)
Theorem: Primrec.w_elimL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
this : Primrec₂ fun x w => elimL (fun p l => f x (p, l)) w
⊢ Primrec fun x => elimL (fun p l => f x (p, l)) (w x)
Tactic:
exact this.comp Primrec.id hw
Proof state after:
no goals
Theorem: Primrec.w_elimL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => Option.map (fun w => elimL (fun p l => f a (p, l)) w) (decode n)
Tactic:
simp[decode_elimL_eq]
Proof state after:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => SubWType.elimDecode β (fun p l => f a (p, l)) n.unpair.1 n.unpair.2
Theorem: Primrec.w_elimL_param
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
f : σ → α × List γ → γ
w : σ → WType β
hf : Primrec₂ f
hw : Primrec w
⊢ Primrec₂ fun a n => SubWType.elimDecode β (fun p l => f a (p, l)) n.unpair.1 n.unpair.2
Tactic:
exact (SubWType.primrec_elimDecode_param β hf).comp₂ Primrec₂.left
  (Primrec.pair (fst.comp $ Primrec.unpair.comp snd) (snd.comp $ Primrec.unpair.comp snd)).to₂
Proof state after:
no goals
Theorem: Primrec.w_elim
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁸ : Primcodable τ
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
f : (a : α) × (β a → γ) → γ
hf : Primrec₂ fun a l => f ⟨a, fintypeArrowEquivFinArrow.symm fun i => l.getI ↑i⟩
w : WType β
⊢ elimL (fun a l => f ⟨a, fintypeArrowEquivFinArrow.symm fun i => l.getI ↑i⟩) w = elim γ f w
Tactic:
simp[elim_eq_elimL]
Proof state after:
no goals
Theorem: Primrec.w_mkL
Proof state before:
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
⊢ (if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0) =
    encode (mkL a l)
Tactic:
by_cases h : l.length = Fintype.card (β a) <;> simp[WType.mkL, *]
Proof state after:
case pos
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) =
    encode (WType.mk a (fintypeArrowEquivFinArrow.symm fun i => l.get (Fin.cast ⋯ i)))
Theorem: Primrec.w_mkL
Proof state before:
case pos
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) =
    encode (WType.mk a (fintypeArrowEquivFinArrow.symm fun i => l.get (Fin.cast ⋯ i)))
Tactic:
simp[encode_mk_eq]
Proof state after:
case pos
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ ((List.map depth l).sup = Finset.univ.sup fun n => (l.get (Fin.cast ⋯ (fintypeEquivFin n))).depth) ∧
    encode (List.map (fun w => (encode w).unpair.2) l) =
      encode fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2
Theorem: Primrec.w_mkL
Proof state before:
case pos
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ ((List.map depth l).sup = Finset.univ.sup fun n => (l.get (Fin.cast ⋯ (fintypeEquivFin n))).depth) ∧
    encode (List.map (fun w => (encode w).unpair.2) l) =
      encode fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2
Tactic:
constructor
Proof state after:
case pos.left
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ (List.map depth l).sup = Finset.univ.sup fun n => (l.get (Fin.cast ⋯ (fintypeEquivFin n))).depth

case pos.right
τ : Type u_1
σ : Type u_2
α : Type u_3
γ : Type u_4
β : α → Type u_5
inst✝⁷ : Primcodable τ
inst✝⁶ : Primcodable σ
inst✝⁵ : Primcodable α
inst✝⁴ : (a : α) → Fintype (β a)
inst✝³ : (a : α) → DecidableEq (β a)
inst✝² : (a : α) → Primcodable (β a)
inst✝¹ : PrimrecCard β
inst✝ : Primcodable γ
this :
  Primrec₂ fun a l =>
    if l.length = Fintype.card (β a) then
      ((List.map depth l).sup + 1).pair ((encode a).pair (encode (List.map (fun w => (encode w).unpair.2) l))) + 1
    else 0
a : α
l : List (WType β)
h : l.length = Fintype.card (β a)
⊢ encode (List.map (fun w => (encode w).unpair.2) l) =
    encode fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2