Theorem: LO.FirstOrder.Semiterm.subtEquiv_bShift_eq_bShift (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
k : ℕ
t : Semiterm L μ k
⊢ ↑(subtEquiv (Rew.bShift t)) = bShifts 1 ↑(subtEquiv t)
Tactic:
rw[Rew.eq_bind Rew.bShift, subtEquiv_bind_eq_bind]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if hx : x < k then ↑(subtEquiv ((⇑Rew.bShift ∘ bvar) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv ((⇑Rew.bShift ∘ fvar) x))) ↑(subtEquiv t) =
    bShifts 1 ↑(subtEquiv t)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if hx : x < k then ↑(subtEquiv ((⇑Rew.bShift ∘ bvar) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv ((⇑Rew.bShift ∘ fvar) x))) ↑(subtEquiv t) =
    bShifts 1 ↑(subtEquiv t)
Tactic:
simp[bShifts]
State after:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if x < k then UTerm.bvar (x + 1) else default) (fun x => UTerm.fvar x) ↑(subtEquiv t) =
    UTerm.bind (fun x => UTerm.bvar (x + 1)) UTerm.fvar ↑(subtEquiv t)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ UTerm.bind (fun x => if x < k then UTerm.bvar (x + 1) else default) (fun x => UTerm.fvar x) ↑(subtEquiv t) =
    UTerm.bind (fun x => UTerm.bvar (x + 1)) UTerm.fvar ↑(subtEquiv t)
Tactic:
apply bind_eq_bind_of_eq
State after:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ x < (↑(subtEquiv t)).bv, (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)

case he
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ (x : μ), UTerm.fvar x = UTerm.fvar x

State before:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ x < (↑(subtEquiv t)).bv, (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
Tactic:
intro x hx
State after:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
x : ℕ
hx : x < (↑(subtEquiv t)).bv
⊢ (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)

State before:
case hb
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
x : ℕ
hx : x < (↑(subtEquiv t)).bv
⊢ (if x < k then UTerm.bvar (x + 1) else default) = UTerm.bvar (x + 1)
Tactic:
simp[lt_of_lt_of_le hx (bv_subtEquiv t)]
State after:
no goals

State before:
case he
L : Language
μ : Type v
α : Type u_1
inst✝³ : Primcodable α
inst✝² : Primcodable μ
inst✝¹ : (k : ℕ) → Primcodable (L.Func k)
inst✝ : UniformlyPrimcodable L.Func
k : ℕ
t : Semiterm L μ k
⊢ ∀ (x : μ), UTerm.fvar x = UTerm.fvar x
Tactic:
simp
State after:
no goals