Theorem: Primrec.w_inversion (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 β)
⊢ 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)))
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

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

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

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

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

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