Theorem: Primrec.w_mk₁ (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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
⊢ Primrec₂ fun x w => WType.mk (f x) fun x => w
Tactic:
have : Primrec₂ (fun x w => Nat.pair (w.depth + 1) (Nat.pair (encode $ f x) (encode [(encode w).unpair.2])) : σ → WType β → ℕ) :=
  Primrec₂.natPair.comp
    (succ.comp $ w_depth.comp snd)
    (Primrec₂.natPair.comp (Primrec.encode.comp $ hf.comp fst)
      (Primrec.encode.comp $ list_cons.comp (snd.comp $ unpair.comp $ Primrec.encode.comp snd) (const [])))
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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
⊢ Primrec₂ fun x w => WType.mk (f x) fun x => w

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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
⊢ Primrec₂ fun x w => WType.mk (f x) fun x => w
Tactic:
exact Primrec₂.encode_iff.mp (this.of_eq $ fun x w => by
  simp[encode_mk_eq, encode_fintypeArrow_card_one (h x) ℕ _ (fintypeEquivFin.symm ((0 : Fin 1).cast (h x).symm))]
  have : Finset.univ = {fintypeEquivFin.symm ((0 : Fin 1).cast (h x).symm)} := by
    have : Subsingleton (β (f x)) := Fintype.card_le_one_iff_subsingleton.mp (by simp[h x])
    ext; simp; exact this.allEq _ _
  rw[this, Finset.sup_singleton])
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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
⊢ (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2])) = encode (WType.mk (f x) fun x => w)
Tactic:
simp[encode_mk_eq, encode_fintypeArrow_card_one (h x) ℕ _ (fintypeEquivFin.symm ((0 : Fin 1).cast (h x).symm))]
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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
⊢ w.depth = Finset.univ.sup fun n => w.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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
⊢ w.depth = Finset.univ.sup fun n => w.depth
Tactic:
have : Finset.univ = {fintypeEquivFin.symm ((0 : Fin 1).cast (h x).symm)} := by
  have : Subsingleton (β (f x)) := Fintype.card_le_one_iff_subsingleton.mp (by simp[h x])
  ext; simp; exact this.allEq _ _
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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Finset.univ = {fintypeEquivFin.symm (Fin.cast ⋯ 0)}
⊢ w.depth = Finset.univ.sup fun n => w.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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Finset.univ = {fintypeEquivFin.symm (Fin.cast ⋯ 0)}
⊢ w.depth = Finset.univ.sup fun n => w.depth
Tactic:
rw[this, Finset.sup_singleton]
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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
⊢ Finset.univ = {fintypeEquivFin.symm (Fin.cast ⋯ 0)}
Tactic:
have : Subsingleton (β (f x)) := Fintype.card_le_one_iff_subsingleton.mp (by simp[h x])
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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
⊢ Finset.univ = {fintypeEquivFin.symm (Fin.cast ⋯ 0)}

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 : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
⊢ Finset.univ = {fintypeEquivFin.symm (Fin.cast ⋯ 0)}
Tactic:
ext
State after:
case 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
a✝ : β (f x)
⊢ a✝ ∈ Finset.univ ↔ a✝ ∈ {fintypeEquivFin.symm (Fin.cast ⋯ 0)}

State before:
case 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
a✝ : β (f x)
⊢ a✝ ∈ Finset.univ ↔ a✝ ∈ {fintypeEquivFin.symm (Fin.cast ⋯ 0)}
Tactic:
simp
State after:
case 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
a✝ : β (f x)
⊢ a✝ = fintypeEquivFin.symm 0

State before:
case 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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this✝ : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
this : Subsingleton (β (f x))
a✝ : β (f x)
⊢ a✝ = fintypeEquivFin.symm 0
Tactic:
exact this.allEq _ _
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 γ
f : σ → α
h : ∀ (x : σ), Fintype.card (β (f x)) = 1
hf : Primrec f
this : Primrec₂ fun x w => (w.depth + 1).pair ((encode (f x)).pair (encode [(encode w).unpair.2]))
x : σ
w : WType β
⊢ Fintype.card (β (f x)) ≤ 1
Tactic:
simp[h x]
State after:
no goals