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

State before:
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
t : UTerm L μ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
⊢ elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) t =
    WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) t)
Tactic:
induction t <;> simp[elim, WType.elimL_mk, F, *]
State after:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))

State before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))
Tactic:
{ simp[Edge] }
State after:
no goals

State before:
case func
L : Language
μ : Type v
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
σ : Sort u_1
γ : Type u_2
x : σ
b : σ → ℕ → γ
e : σ → μ → γ
u : σ → ((k : ℕ) × L.Func k) × List γ → γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ
a_ih✝ :
  ∀ (a : Fin arity✝),
    elim (b x) (e x) (fun {k} f v => u x (⟨k, f⟩, List.ofFn v)) (a✝ a) =
      WType.elimL (fun p l => LO.FirstOrder.UTerm.F b e u x (p, l)) ((equivW L μ) (a✝ a))
⊢ u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn fun i =>
          WType.elimL
            (fun p l =>
              Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
            ((equivW L μ) (a✝ i))) =
    u x
      (⟨arity✝, a✝¹⟩,
        List.ofFn
          (fintypeArrowEquivFinArrow fun b_1 =>
            WType.elimL
              (fun p l =>
                Sum.rec (fun val => b x val) (fun val => Sum.rec (fun val => e x val) (fun val => u x (val, l)) val) p)
              ((equivW L μ) (a✝ b_1))))
Tactic:
simp[Edge]
State after:
no goals