internlm/Lean-Github huggingface dataset:
Theorem: Primrec.w_mkL
Proof state before:
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
Tactic:
{ exact Eq.trans (by rw[Finset.sup_univ_cast (fun i => depth (l.get i))]; exact Eq.symm <| Finset.sup_univ_list_eq_sup_map _ _)
    (Eq.symm <| Finset.sup_univ_equiv (fun i => depth (l.get (i.cast h.symm)) : Fin (Fintype.card (β a)) → ℕ) fintypeEquivFin) }
Proof state after:
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
Theorem: Primrec.w_mkL
Proof state before:
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
Tactic:
exact Eq.trans (by rw[Finset.sup_univ_cast (fun i => depth (l.get i))]; exact Eq.symm <| Finset.sup_univ_list_eq_sup_map _ _)
  (Eq.symm <| Finset.sup_univ_equiv (fun i => depth (l.get (i.cast h.symm)) : Fin (Fintype.card (β a)) → ℕ) fintypeEquivFin)
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 β)
h : l.length = Fintype.card (β a)
⊢ (List.map depth l).sup = Finset.univ.sup fun i => (l.get (Fin.cast ⋯ i)).depth
Tactic:
rw[Finset.sup_univ_cast (fun i => depth (l.get i))]
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 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 i => (l.get i).depth
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 β)
h : l.length = Fintype.card (β a)
⊢ (List.map depth l).sup = Finset.univ.sup fun i => (l.get i).depth
Tactic:
exact Eq.symm <| Finset.sup_univ_list_eq_sup_map _ _
Proof state after:
no goals
Theorem: Primrec.w_mkL
Proof state before:
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
Tactic:
simp[encode_fintypeArrow, encode_finArrow]
Proof state after:
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)
⊢ List.map (fun w => (encode w).unpair.2) l =
    List.ofFn (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2)
Theorem: Primrec.w_mkL
Proof state before:
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)
⊢ List.map (fun w => (encode w).unpair.2) l =
    List.ofFn (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2)
Tactic:
ext i c
Proof state after:
case pos.right.a.a
τ : 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)
i c : ℕ
⊢ c ∈ (List.map (fun w => (encode w).unpair.2) l).get? i ↔
    c ∈
      (List.ofFn (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2)).get? i
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a
τ : 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)
i c : ℕ
⊢ c ∈ (List.map (fun w => (encode w).unpair.2) l).get? i ↔
    c ∈
      (List.ofFn (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2)).get? i
Tactic:
simp
Proof state after:
case pos.right.a.a
τ : 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)
i c : ℕ
⊢ (∃ a, l.get? i = some a ∧ (encode a).unpair.2 = c) ↔
    List.ofFnNthVal (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2) i =
      some c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a
τ : 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)
i c : ℕ
⊢ (∃ a, l.get? i = some a ∧ (encode a).unpair.2 = c) ↔
    List.ofFnNthVal (fintypeArrowEquivFinArrow fun b => (encode (l.get (Fin.cast ⋯ (fintypeEquivFin b)))).unpair.2) i =
      some c
Tactic:
rcases hw : (l.get? i) with (_ | w) <;> simp[List.ofFnNthVal]
Proof state after:
case pos.right.a.a.none
τ : 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)
i c : ℕ
hw : l.get? i = none
⊢ ∀ (x : i < Fintype.card (β a)), ¬(encode (l.get ⟨i, ⋯⟩)).unpair.2 = c

case pos.right.a.a.some
τ : 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)
i c : ℕ
w : WType β
hw : l.get? i = some w
⊢ (encode w).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.none
τ : 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)
i c : ℕ
hw : l.get? i = none
⊢ ∀ (x : i < Fintype.card (β a)), ¬(encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
have : ¬i < Fintype.card (β a) := by simpa[h] using List.get?_eq_none.mp hw
Proof state after:
case pos.right.a.a.none
τ : 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)
i c : ℕ
hw : l.get? i = none
this : ¬i < Fintype.card (β a)
⊢ ∀ (x : i < Fintype.card (β a)), ¬(encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.none
τ : 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)
i c : ℕ
hw : l.get? i = none
this : ¬i < Fintype.card (β a)
⊢ ∀ (x : i < Fintype.card (β a)), ¬(encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
simp[this]
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 β)
h : l.length = Fintype.card (β a)
i c : ℕ
hw : l.get? i = none
⊢ ¬i < Fintype.card (β a)
Tactic:
simpa[h] using List.get?_eq_none.mp hw
Proof state after:
no goals
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.some
τ : 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)
i c : ℕ
w : WType β
hw : l.get? i = some w
⊢ (encode w).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
have : ∃ hi, l.get ⟨i, hi⟩ = w := List.get?_eq_some.mp hw
Proof state after:
case pos.right.a.a.some
τ : 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)
i c : ℕ
w : WType β
hw : l.get? i = some w
this : ∃ (hi : i < l.length), l.get ⟨i, hi⟩ = w
⊢ (encode w).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.some
τ : 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)
i c : ℕ
w : WType β
hw : l.get? i = some w
this : ∃ (hi : i < l.length), l.get ⟨i, hi⟩ = w
⊢ (encode w).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
rcases this with ⟨hi, rfl⟩
Proof state after:
case pos.right.a.a.some.intro
τ : 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)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
⊢ (encode (l.get ⟨i, hi⟩)).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.some.intro
τ : 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)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
⊢ (encode (l.get ⟨i, hi⟩)).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
have : i < Fintype.card (β a) := by simpa[h] using hi
Proof state after:
case pos.right.a.a.some.intro
τ : 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)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
this : i < Fintype.card (β a)
⊢ (encode (l.get ⟨i, hi⟩)).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Theorem: Primrec.w_mkL
Proof state before:
case pos.right.a.a.some.intro
τ : 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)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
this : i < Fintype.card (β a)
⊢ (encode (l.get ⟨i, hi⟩)).unpair.2 = c ↔ ∃ (h_1 : i < Fintype.card (β a)), (encode (l.get ⟨i, ⋯⟩)).unpair.2 = c
Tactic:
simp[this]
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 β)
h : l.length = Fintype.card (β a)
i c : ℕ
hi : i < l.length
hw : l.get? i = some (l.get ⟨i, hi⟩)
⊢ i < Fintype.card (β a)
Tactic:
simpa[h] using hi
Proof state after:
no goals
Theorem: Primrec.w_mk₀
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
⊢ Primrec fun x => WType.mk (f x) v
Tactic:
have : Primrec (fun x => Nat.pair 1 (Nat.pair (encode $ f x) 0) : σ → ℕ) :=
  Primrec₂.natPair.comp (const 1) (Primrec₂.natPair.comp (Primrec.encode.comp hf) (const 0))
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
⊢ Primrec fun x => WType.mk (f x) v
Theorem: Primrec.w_mk₀
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
⊢ Primrec fun x => WType.mk (f x) v
Tactic:
exact Primrec.encode_iff.mp (this.of_eq $ fun x => by simp[encode_mk_eq, encode_fintypeArrow_isEmpty])
Proof state after:
no goals
Theorem: Primrec.w_mk₀
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 : σ → α
h : ∀ (x : σ), IsEmpty (β (f x))
hf : Primrec f
v : {x : σ} → β (f x) → WType β
this : Primrec fun x => Nat.pair 1 ((encode (f x)).pair 0)
x : σ
⊢ Nat.pair 1 ((encode (f x)).pair 0) = encode (WType.mk (f x) v)
Tactic:
simp[encode_mk_eq, encode_fintypeArrow_isEmpty]
Proof state after:
no goals