Theorem: Primrec.w_mkL (Logic/Vorspiel/W.lean)

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, *]
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)))

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]
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

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
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

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) }
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

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)
State after:
no goals

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))]
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

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 _ _
State after:
no goals

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]
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)

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
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

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
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

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]
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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⟩
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

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
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

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]
State after:
no goals

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
State after:
no goals