Theorem: Primrec.w_mkFin (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 : σ → α
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))
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)

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)
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 : σ → α
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]
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

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 β
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm w
Tactic:
have := (fintypeArrowEquivFinArrow' (α := WType β) (h x)).injective
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm 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 : σ → α
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm w
Tactic:
apply this
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 : σ → α
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm w)

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 : σ → α
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm w)
Tactic:
funext i
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 : σ → α
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin k
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) i =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm w) i

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 : σ → α
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
i : Fin k
⊢ (fintypeArrowEquivFinArrow' ⋯) (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) i =
    (fintypeArrowEquivFinArrow' ⋯) ((fintypeArrowEquivFinArrow' ⋯).symm w) i
Tactic:
simp
State after:
no goals