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

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

State before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
⊢ (fun i => ↑(ofSubterm ((v i).toSubterm ⋯))) = v
Tactic:
case func f v ih =>
  funext i
  have h : ∀ i, (v i).bv ≤ n := by simpa[bv] using h
  exact ih i (h i)
State after:
no goals

State before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
⊢ (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✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
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✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
i : Fin arity✝
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i
Tactic:
have h : ∀ i, (v i).bv ≤ n := by simpa[bv] using h
State after:
case h
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h✝ : (func f v).bv ≤ n
i : Fin arity✝
h : ∀ (i : Fin arity✝), (v i).bv ≤ n
⊢ ↑(ofSubterm ((v i).toSubterm ⋯)) = v i

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

State before:
L : Language
μ : Type v
n arity✝ : ℕ
f : L.Func arity✝
v : Fin arity✝ → UTerm L μ
ih : ∀ (a : Fin arity✝) (h : (v a).bv ≤ n), ↑(ofSubterm ((v a).toSubterm h)) = v a
h : (func f v).bv ≤ n
i : Fin arity✝
⊢ ∀ (i : Fin arity✝), (v i).bv ≤ n
Tactic:
simpa[bv] using h
State after:
no goals