Theorem: Primrec.w_elimvL_param (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 γ
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 }) }
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)

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

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

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

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 })
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 γ
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)
⊢ ∀ (b b' : τ × σ × WType β),
    b' ∈ List.map (fun w => (b.1, fs b.1 (b.2.2.inversion.1, b.2.1), w)) b.2.2.inversion.2 → b'.2.2.depth < b.2.2.depth
Tactic:
rintro ⟨z, x, ⟨a, f⟩⟩ ⟨z', x', w'⟩
State after:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ (z', x', w') ∈
      List.map
        (fun w =>
          ((z, x, WType.mk a f).1,
            fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
        (z, x, WType.mk a f).2.2.inversion.2 →
    (z', x', w').2.2.depth < (z, x, WType.mk a f).2.2.depth

State before:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ (z', x', w') ∈
      List.map
        (fun w =>
          ((z, x, WType.mk a f).1,
            fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
        (z, x, WType.mk a f).2.2.inversion.2 →
    (z', x', w').2.2.depth < (z, x, WType.mk a f).2.2.depth
Tactic:
simp[inversion, Function.comp, List.mem_ofFn]
State after:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ z = z' →
    fs z (a, x) = x' →
      ∀ (x : Fin (Fintype.card (β a))), f (fintypeEquivFin.symm x) = w' → w'.depth < (WType.mk a f).depth

State before:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
z' : τ
x' : σ
w' : WType β
⊢ z = z' →
    fs z (a, x) = x' →
      ∀ (x : Fin (Fintype.card (β a))), f (fintypeEquivFin.symm x) = w' → w'.depth < (WType.mk a f).depth
Tactic:
rintro rfl rfl i rfl
State after:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
i : Fin (Fintype.card (β a))
⊢ (f (fintypeEquivFin.symm i)).depth < (WType.mk a f).depth

State before:
case mk.mk.mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
i : Fin (Fintype.card (β a))
⊢ (f (fintypeEquivFin.symm i)).depth < (WType.mk a f).depth
Tactic:
exact depth_lt_depth_mk _ _ _
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 γ
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)
⊢ ∀ (b : τ × σ × WType β),
    some
        (fγ b.1
          (b.2.1, b.2.2.inversion.1,
            List.map (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)
              (List.map (fun w => (b.1, fs b.1 (b.2.2.inversion.1, b.2.1), w)) b.2.2.inversion.2))) =
      some (elimvL (fun a x => fs b.1 (a, x)) (fun x a l => fγ b.1 (x, a, l)) b.2.1 b.2.2)
Tactic:
rintro ⟨z, x, ⟨a, f⟩⟩
State after:
case mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
⊢ some
      (fγ (z, x, WType.mk a f).1
        ((z, x, WType.mk a f).2.1, (z, x, WType.mk a f).2.2.inversion.1,
          List.map (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)
            (List.map
              (fun w =>
                ((z, x, WType.mk a f).1,
                  fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
              (z, x, WType.mk a f).2.2.inversion.2))) =
    some
      (elimvL (fun a_1 x_1 => fs (z, x, WType.mk a f).1 (a_1, x_1))
        (fun x_1 a_1 l => fγ (z, x, WType.mk a f).1 (x_1, a_1, l)) (z, x, WType.mk a f).2.1 (z, x, WType.mk a f).2.2)

State before:
case mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
⊢ some
      (fγ (z, x, WType.mk a f).1
        ((z, x, WType.mk a f).2.1, (z, x, WType.mk a f).2.2.inversion.1,
          List.map (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)
            (List.map
              (fun w =>
                ((z, x, WType.mk a f).1,
                  fs (z, x, WType.mk a f).1 ((z, x, WType.mk a f).2.2.inversion.1, (z, x, WType.mk a f).2.1), w))
              (z, x, WType.mk a f).2.2.inversion.2))) =
    some
      (elimvL (fun a_1 x_1 => fs (z, x, WType.mk a f).1 (a_1, x_1))
        (fun x_1 a_1 l => fγ (z, x, WType.mk a f).1 (x_1, a_1, l)) (z, x, WType.mk a f).2.1 (z, x, WType.mk a f).2.2)
Tactic:
simp[inversion, Function.comp, elimvL_mk]
State after:
case mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
⊢ fγ z
      (x, a,
        List.ofFn fun x_1 =>
          elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f (fintypeEquivFin.symm x_1))) =
    fγ z
      (x, a,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b =>
            elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f b)))

State before:
case mk.mk.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 β)
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)
z : τ
x : σ
a : α
f : β a → WType β
⊢ fγ z
      (x, a,
        List.ofFn fun x_1 =>
          elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f (fintypeEquivFin.symm x_1))) =
    fγ z
      (x, a,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b =>
            elimvL (fun a x => fs z (a, x)) (fun x a l => fγ z (x, a, l)) (fs z (a, x)) (f b)))
Tactic:
congr
State after:
no goals