internlm/Lean-Github huggingface dataset:
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 : σ), 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 [])))
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 : σ), 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
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 : σ), 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])
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 : σ), 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))]
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 : σ), 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
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 : σ), 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 _ _
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 : σ), 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
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 : σ), 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]
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 : σ), 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])
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 : σ), 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)}
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 : σ), 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
Proof 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)}
Theorem: Primrec.w_mk₁
Proof 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
Proof 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
Theorem: Primrec.w_mk₁
Proof 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 _ _
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 : σ), 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]
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
Tactic:
have : Primrec₂ (fun x w => Nat.pred $ encode (WType.mkL (f x) [w.1, w.2]) : σ → WType β × WType β → ℕ) :=
  (pred.comp $ Primrec.encode.comp $ w_mkL.comp (hf.comp fst) (list_cons.comp (fst.comp snd) (list_cons.comp (snd.comp snd) (const []))))
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])
Tactic:
exact Primrec₂.encode_iff.mp (this.of_eq $ fun x ⟨w₁, w₂⟩ => by
  simp[mkL, h]
  have := (fintypeArrowEquivFinArrow' (α := WType β) (h x)).injective
  apply this
  funext i; simp
  cases i using Fin.cases <;> simp)
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
⊢ (encode (mkL (f x) [(w₁, w₂).1, (w₁, w₂).2])).pred =
    encode (WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm ![(w₁, w₂).1, (w₁, w₂).2]))
Tactic:
simp[mkL, h]
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
⊢ (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
⊢ (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]
Tactic:
have := (fintypeArrowEquivFinArrow' (α := WType β) (h x)).injective
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]
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 : σ), Fintype.card (β (f x)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]
Tactic:
apply this
Proof 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂])
Theorem: Primrec.w_mk₂
Proof 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂])
Tactic:
funext i
Proof state after:
case a.h
τ : 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin 2
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) i =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]) i
Theorem: Primrec.w_mk₂
Proof state before:
case a.h
τ : 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin 2
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => [w₁, w₂].get (Fin.cast ⋯ i)) i =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm ![w₁, w₂]) i
Tactic:
simp
Proof state after:
case a.h
τ : 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin 2
⊢ [w₁, w₂].get i = ![w₁, w₂] i
Theorem: Primrec.w_mk₂
Proof state before:
case a.h
τ : 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)) = 2
hf : Primrec f
this✝ : Primrec₂ fun x w => (encode (mkL (f x) [w.1, w.2])).pred
x : σ
x✝ : WType β × WType β
w₁ w₂ : WType β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin 2
⊢ [w₁, w₂].get i = ![w₁, w₂] i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: Primrec.w_mkFin
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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
Tactic:
have : Primrec₂ (fun x w => Nat.pred $ encode (WType.mkL (f x) (List.ofFn w)) : σ → (Fin k → WType β) → ℕ) :=
  (pred.comp $ Primrec.encode.comp $ w_mkL.comp (hf.comp fst) (finArrow_list_ofFn.comp snd))
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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) (List.ofFn w))).pred
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
Theorem: Primrec.w_mkFin
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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) (List.ofFn w))).pred
⊢ Primrec₂ fun x w => WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm w)
Tactic:
exact Primrec₂.encode_iff.mp (this.of_eq $ fun x w => by
  simp[mkL, h]
  have := (fintypeArrowEquivFinArrow' (α := WType β) (h x)).injective
  apply this
  funext i; simp)
Proof state after:
no goals
Theorem: Primrec.w_mkFin
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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) (List.ofFn w))).pred
x : σ
w : Fin k → WType β
⊢ (encode (mkL (f x) (List.ofFn w))).pred = encode (WType.mk (f x) ((fintypeArrowEquivFinArrow' ⋯).symm w))
Tactic:
simp[mkL, h]
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 : σ → α
k : ℕ
h : ∀ (x : σ), Fintype.card (β (f x)) = k
hf : Primrec f
this : Primrec₂ fun x w => (encode (mkL (f x) (List.ofFn w))).pred
x : σ
w : Fin k → WType β
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm w