internlm/Lean-Github huggingface dataset:
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 β
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm 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 : σ → α
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
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 β
this : Function.Injective ⇑(fintypeArrowEquivFinArrow' ⋯)
⊢ (fintypeArrowEquivFinArrow.symm fun i => w (Fin.cast ⋯ i)) = (fintypeArrowEquivFinArrow' ⋯).symm 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 : σ → α
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)
Theorem: Primrec.w_mkFin
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 : σ → α
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
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 : σ → α
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
Theorem: Primrec.w_mkFin
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 : σ → α
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
Proof state after:
no goals
Theorem: Primrec.w_inversion
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 γ
inst✝ : Inhabited (WType β)
⊢ Primrec inversion
Tactic:
have : Primrec₂ (fun a l => (a, l.map (fun p => (mkL p.1 p.2).get!)) : α → List (α × List (WType β)) → α × List (WType β)) :=
  Primrec₂.pair.comp₂ Primrec₂.left
    (to₂' <| list_map snd (option_get!.comp₂ $ w_mkL.comp₂ (fst.comp₂ $ Primrec₂.right) (snd.comp₂ $ Primrec₂.right)))
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 γ
inst✝ : Inhabited (WType β)
this : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
⊢ Primrec inversion
Theorem: Primrec.w_inversion
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 γ
inst✝ : Inhabited (WType β)
this : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
⊢ Primrec inversion
Tactic:
have := w_elimL (β := β) this
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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
⊢ Primrec inversion
Theorem: Primrec.w_inversion
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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
⊢ Primrec inversion
Tactic:
exact this.of_eq <| fun w => by
  induction w
  simp[inversion, elimL_mk, Function.comp]
  funext i; simp[*, mkL_inversion]
Proof state after:
no goals
Theorem: Primrec.w_inversion
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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
w : WType β
⊢ elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) w = w.inversion
Tactic:
induction w
Proof state after:
case mk
τ : 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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
⊢ elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (WType.mk a✝ f✝) = (WType.mk a✝ f✝).inversion
Theorem: Primrec.w_inversion
Proof state before:
case mk
τ : 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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
⊢ elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (WType.mk a✝ f✝) = (WType.mk a✝ f✝).inversion
Tactic:
simp[inversion, elimL_mk, Function.comp]
Proof state after:
case mk
τ : 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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
⊢ (fun x =>
      (mkL (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm x))).1
          (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm x))).2).get!) =
    fintypeArrowEquivFinArrow f✝
Theorem: Primrec.w_inversion
Proof state before:
case mk
τ : 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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
⊢ (fun x =>
      (mkL (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm x))).1
          (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm x))).2).get!) =
    fintypeArrowEquivFinArrow f✝
Tactic:
funext i
Proof state after:
case mk.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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
i : Fin (Fintype.card (β a✝))
⊢ (mkL (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm i))).1
        (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm i))).2).get! =
    fintypeArrowEquivFinArrow f✝ i
Theorem: Primrec.w_inversion
Proof state before:
case mk.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 γ
inst✝ : Inhabited (WType β)
this✝ : Primrec₂ fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)
this : Primrec (elimL fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l))
a✝ : α
f✝ : β a✝ → WType β
f_ih✝ : ∀ (a : β a✝), elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ a) = (f✝ a).inversion
i : Fin (Fintype.card (β a✝))
⊢ (mkL (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm i))).1
        (elimL (fun a l => (a, List.map (fun p => (mkL p.1 p.2).get!) l)) (f✝ (fintypeEquivFin.symm i))).2).get! =
    fintypeArrowEquivFinArrow f✝ i
Tactic:
simp[*, mkL_inversion]
Proof state after:
no goals
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)
Tactic:
have : Primrec₂ (fun z (p : σ × WType β) => WType.elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2) :=
  to₂' <| by {
    have hm : Primrec (fun (p : τ × σ × WType β) => p.2.2.depth) := w_depth.comp <| snd.comp snd
    have hl : Primrec (fun (p : τ × σ × WType β) =>
        p.2.2.inversion.2.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w))) :=
      list_map (snd.comp $ w_inversion.comp $ snd.comp snd)
        <| Primrec₂.pair.comp (fst.comp fst)
        <| Primrec₂.pair.comp
          (hfs.comp (fst.comp fst)
            (Primrec₂.pair.comp
              (fst.comp $ w_inversion.comp $ snd.comp $ snd.comp fst)
              (fst.comp $ snd.comp fst)))
        <| snd
    have hg : Primrec₂ (fun (p : τ × σ × WType β) (l : List γ) => fγ p.1 (p.2.1, p.2.2.inversion.1, l)) :=
      hfγ.comp₂ (fst.comp₂ Primrec₂.left)
        <| Primrec₂.pair.comp₂ (fst.comp₂ $ snd.comp₂ Primrec₂.left)
        <| Primrec₂.pair.comp₂ (fst.comp₂ $ w_inversion.comp₂ $ snd.comp₂ $ snd.comp₂ Primrec₂.left) Primrec₂.right
    apply nat_omega_rec' _ hm hl (option_some.comp₂ hg)
      (by rintro ⟨z, x, ⟨a, f⟩⟩ ⟨z', x', w'⟩
          simp[inversion, Function.comp, List.mem_ofFn]
          rintro rfl rfl i rfl; exact depth_lt_depth_mk _ _ _)
      (by { rintro ⟨z, x, ⟨a, f⟩⟩; simp[inversion, Function.comp, elimvL_mk]
            congr }) }
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
this : Primrec₂ fun z p => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
this : Primrec₂ fun z p => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) p.1 p.2
⊢ Primrec fun z => elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (g z) (w z)
Tactic:
exact this.comp Primrec.id (Primrec₂.pair.comp hg hw)
Proof state after:
no goals
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Tactic:
have hm : Primrec (fun (p : τ × σ × WType β) => p.2.2.depth) := w_depth.comp <| snd.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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Tactic:
have hl : Primrec (fun (p : τ × σ × WType β) =>
    p.2.2.inversion.2.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w))) :=
  list_map (snd.comp $ w_inversion.comp $ snd.comp snd)
    <| Primrec₂.pair.comp (fst.comp fst)
    <| Primrec₂.pair.comp
      (hfs.comp (fst.comp fst)
        (Primrec₂.pair.comp
          (fst.comp $ w_inversion.comp $ snd.comp $ snd.comp fst)
          (fst.comp $ snd.comp fst)))
    <| 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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Tactic:
have hg : Primrec₂ (fun (p : τ × σ × WType β) (l : List γ) => fγ p.1 (p.2.1, p.2.2.inversion.1, l)) :=
  hfγ.comp₂ (fst.comp₂ Primrec₂.left)
    <| Primrec₂.pair.comp₂ (fst.comp₂ $ snd.comp₂ Primrec₂.left)
    <| Primrec₂.pair.comp₂ (fst.comp₂ $ w_inversion.comp₂ $ snd.comp₂ $ snd.comp₂ Primrec₂.left) Primrec₂.right
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Theorem: Primrec.w_elimvL_param
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 γ
inst✝ : Inhabited (WType β)
fs : τ → α × σ → σ
fγ : τ → σ × α × List γ → γ
g : τ → σ
w : τ → WType β
hfs : Primrec₂ fs
hfγ : Primrec₂ fγ
hg✝ : Primrec g
hw : Primrec w
hm : Primrec fun p => p.2.2.depth
hl : Primrec fun p => List.map (fun w => (p.1, fs p.1 (p.2.2.inversion.1, p.2.1), w)) p.2.2.inversion.2
hg : Primrec₂ fun p l => fγ p.1 (p.2.1, p.2.2.inversion.1, l)
⊢ Primrec fun p => elimvL (fun a x => fs p.1 (a, x)) (fun x a l => fγ p.1 (x, a, l)) p.2.1 p.2.2
Tactic:
apply nat_omega_rec' _ hm hl (option_some.comp₂ hg)
  (by rintro ⟨z, x, ⟨a, f⟩⟩ ⟨z', x', w'⟩
      simp[inversion, Function.comp, List.mem_ofFn]
      rintro rfl rfl i rfl; exact depth_lt_depth_mk _ _ _)
  (by { rintro ⟨z, x, ⟨a, f⟩⟩; simp[inversion, Function.comp, elimvL_mk]
        congr })
Proof state after:
no goals