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

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

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

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

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

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

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