Theorem: LO.FirstOrder.Semiterm.subtEquiv_bind_eq_bind (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
t : Semiterm L μ₁ n₁
⊢ ↑(subtEquiv ((Rew.bind b e) t)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv t)
Tactic:
induction t <;> simp[UTerm.bind]
State after:
case func
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L μ₁ n₁
a_ih✝ :
  ∀ (a : Fin arity✝),
    ↑(subtEquiv ((Rew.bind b e) (a✝ a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (a✝ a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func a✝¹ a✝))) =
    UTerm.func a✝¹ fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (a✝ i))

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func f v))) =
    UTerm.func f fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (v i))
Tactic:
case func k f v ih =>
  simp[Rew.func]
  funext i; simp[ih]; rfl
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ ↑(subtEquiv ((Rew.bind b e) (func f v))) =
    UTerm.func f fun i =>
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(ofSubterm (v i))
Tactic:
simp[Rew.func]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ (fun i => ↑(subtEquiv ((Rew.bind b e) (v i)))) = fun i =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
⊢ (fun i => ↑(subtEquiv ((Rew.bind b e) (v i)))) = fun i =>
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
funext i
State after:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ ↑(subtEquiv ((Rew.bind b e) (v i))) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))

State before:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ ↑(subtEquiv ((Rew.bind b e) (v i))) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
simp[ih]
State after:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv (v i)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))

State before:
case h
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ₁ n₁
ih :
  ∀ (a : Fin k),
    ↑(subtEquiv ((Rew.bind b e) (v a))) =
      UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
        ↑(subtEquiv (v a))
i : Fin k
⊢ UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subtEquiv (v i)) =
    UTerm.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(ofSubterm (v i))
Tactic:
rfl
State after:
no goals