Theorem: LO.FirstOrder.Semiformula.subfEquiv_bind_eq_bind (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ ↑(subfEquiv ((Rew.bind b e).hom p)) =
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subfEquiv p)
Tactic:
induction p using rec' generalizing n₂ μ₂ e <;>
  simp [Semiterm.subtEquiv_bind_eq_bind, bindq, Rew.rel, Rew.nrel, UFormula.bind,
    ofSubterm_eq_subtEquiv, ofSubformula_eq_subfEquiv, *]
State after:
case hall
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)

case hex
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p)) =
    bindq (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p)
Tactic:
simp[Rew.q_bind, ih, bindq_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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv (Rew.bShift (e x)))) ↑(subfEquiv p) =
    UFormula.bind (shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1)
      (fun x => bShifts 1 ↑(subtEquiv (e x))) ↑(subfEquiv p)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default)
      (fun x => ↑(subtEquiv (Rew.bShift (e x)))) ↑(subfEquiv p) =
    UFormula.bind (shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1)
      (fun x => bShifts 1 ↑(subtEquiv (e x))) ↑(subfEquiv p)
Tactic:
apply UFormula.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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ x < (↑(subfEquiv p)).bv,
    (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
      shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x

case he
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ (x : μ₁), ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ x < (↑(subfEquiv p)).bv,
    (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
      shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    shiftb (fun x => if hx : x < k then ↑(subtEquiv (b ⟨x, hx⟩)) else default) 1 x
Tactic:
simp[shiftb]
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    if x = 0 then bvar x else bShifts 1 (if hx : x - 1 < k then ↑(subtEquiv (b ⟨x - 1, hx⟩)) else default)

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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x < (↑(subfEquiv p)).bv
⊢ (if hx : x < k + 1 then ↑(subtEquiv ((#0 :> ⇑Rew.bShift ∘ b) ⟨x, hx⟩)) else default) =
    if x = 0 then bvar x else bShifts 1 (if hx : x - 1 < k then ↑(subtEquiv (b ⟨x - 1, hx⟩)) else default)
Tactic:
cases' x with x <;> simp[Nat.succ_eq_add_one]
State after:
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)

State before:
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Tactic:
have : x < k := Nat.succ_lt_succ_iff.mp (lt_of_lt_of_le hx (bv_subtEquiv p))
State after:
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
this : x < k
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)

State before:
case hb.succ
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : ℕ
hx : x + 1 < (↑(subfEquiv p)).bv
this : x < k
⊢ (if h : x < k then ↑(subtEquiv (Rew.bShift (b ⟨x, ⋯⟩))) else default) =
    bShifts 1 (if h : x < k then ↑(subtEquiv (b ⟨x, ⋯⟩)) else default)
Tactic:
simp[this, Semiterm.subtEquiv_bShift_eq_bShift]
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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ∀ (x : μ₁), ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Tactic:
intro x
State after:
case he
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : μ₁
⊢ ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))

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
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
k : ℕ
p : Semiformula L μ₁ (k + 1)
ih :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (k + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p)) =
      UFormula.bind (fun x => if hx : x < k + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p)
μ₂ : Type u_2
n₂ : ℕ
b : Fin k → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
x : μ₁
⊢ ↑(subtEquiv (Rew.bShift (e x))) = bShifts 1 ↑(subtEquiv (e x))
Tactic:
exact Semiterm.subtEquiv_bShift_eq_bShift (e x)
State after:
no goals