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

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
t : UTerm L μ₁
hb : ∀ x < t.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind b₁ e₁ t = bind b₂ e₂ t
Tactic:
induction t <;> simp[bind, he]
State after:
case bvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, b₁ x = b₂ x
⊢ b₁ a✝ = b₂ a✝

case func
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ₁
a_ih✝ : ∀ (a : Fin arity✝), (∀ x < (a✝ a).bv, b₁ x = b₂ x) → bind b₁ e₁ (a✝ a) = bind b₂ e₂ (a✝ a)
hb : ∀ x < (func a✝¹ a✝).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (a✝ i)) = fun i => bind b₂ e₂ (a✝ i)

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ b₁ x = b₂ x
Tactic:
case bvar x => exact hb x (by simp)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (v i)) = fun i => bind b₂ e₂ (v i)
Tactic:
case func k f v ih => funext i; exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ b₁ x = b₂ x
Tactic:
exact hb x (by simp)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hb : ∀ x_1 < (bvar x).bv, b₁ x_1 = b₂ x_1
⊢ x < (bvar x).bv
Tactic:
simp
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
⊢ (fun i => bind b₁ e₁ (v i)) = fun i => bind b₂ e₂ (v i)
Tactic:
funext i
State after:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
⊢ bind b₁ e₁ (v i) = bind b₂ e₂ (v i)

State before:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
⊢ bind b₁ e₁ (v i) = bind b₂ e₂ (v i)
Tactic:
exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (func f v).bv
Tactic:
simp[bv]
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), e₁ x = e₂ x
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, b₁ x = b₂ x) → bind b₁ e₁ (v a) = bind b₂ e₂ (v a)
hb : ∀ x < (func f v).bv, b₁ x = b₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
State after:
no goals