Theorem: LO.FirstOrder.UTerm.funcL_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr ⟨k, f⟩)) (List.map (⇑(equivW L μ)) l)) = funcL ⟨k, f⟩ l
Tactic:
simp[WType.mkL, Edge]
State after:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm)
      (if h : l.length = k then
        some
          (WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) (fintypeArrowEquivFinArrow.symm fun i => (equivW L μ) (l.get ⟨↑i, ⋯⟩)))
      else none) =
    funcL ⟨k, f⟩ l

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
⊢ Option.map (⇑(equivW L μ).symm)
      (if h : l.length = k then
        some
          (WType.mk (Sum.inr (Sum.inr ⟨k, f⟩)) (fintypeArrowEquivFinArrow.symm fun i => (equivW L μ) (l.get ⟨↑i, ⋯⟩)))
      else none) =
    funcL ⟨k, f⟩ l
Tactic:
by_cases hl : l.length = k <;> simp[hl, funcL]
State after:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)

State before:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)
Tactic:
{ funext i; congr }
State after:
no goals

State before:
case pos
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
⊢ (fun i => l.get ⟨↑i, ⋯⟩) = fun i => l.get (Fin.cast ⋯ i)
Tactic:
funext i
State after:
case pos.h
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
i : Fin k
⊢ l.get ⟨↑i, ⋯⟩ = l.get (Fin.cast ⋯ i)

State before:
case pos.h
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
this✝ : Primrec₂ fun a l => Option.map (⇑(equivW L μ).symm) (WType.mkL a (List.map (⇑(equivW L μ)) l))
this :
  Primrec₂ fun f l => Option.map (⇑(equivW L μ).symm) (WType.mkL (Sum.inr (Sum.inr f)) (List.map (⇑(equivW L μ)) l))
x✝ : (k : ℕ) × L.Func k
l : List (UTerm L μ)
k : ℕ
f : L.Func k
hl : l.length = k
i : Fin k
⊢ l.get ⟨↑i, ⋯⟩ = l.get (Fin.cast ⋯ i)
Tactic:
congr
State after:
no goals