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

State before:
L : Language
μ : Type v
n : ℕ
t : Semiterm L μ n
⊢ (↑(ofSubterm t)).toSubterm ⋯ = t
Tactic:
induction t <;> simp [ofSubterm, toSubterm]
State after:
case func
L : Language
μ : Type v
n arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L μ n
a_ih✝ : ∀ (a : Fin arity✝), (↑(ofSubterm (a✝ a))).toSubterm ⋯ = a✝ a
⊢ (fun i => (↑(ofSubterm (a✝ i))).toSubterm ⋯) = a✝

State before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
⊢ (fun i => (↑(ofSubterm (v i))).toSubterm ⋯) = v
Tactic:
case func f v ih => funext i; exact ih i
State after:
no goals

State before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
⊢ (fun i => (↑(ofSubterm (v i))).toSubterm ⋯) = v
Tactic:
funext i
State after:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
i : Fin arity✝
⊢ (↑(ofSubterm (v i))).toSubterm ⋯ = v i

State before:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → Semiterm L μ n
ih : ∀ (a : Fin arity✝), (↑(ofSubterm (v a))).toSubterm ⋯ = v a
i : Fin arity✝
⊢ (↑(ofSubterm (v i))).toSubterm ⋯ = v i
Tactic:
exact ih i
State after:
no goals