Theorem: LO.FirstOrder.UFormula.bindq_eq_bind (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
p : UFormula L μ₁
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m p = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) p
Tactic:
induction' p generalizing b e m <;> simp [bind, bindq]
State after:
case and
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case or
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case all
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝

case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝

State before:
case and
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case or
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝¹ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝¹
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e m a✝¹ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝¹ ∧
    bindq b e m a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 0 a✝

case all
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝

case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝
Tactic:
all_goals simp [*]
State after:
no goals

State before:
case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ {m : ℕ} (b : ℕ → UTerm L μ₂) (e : μ₁ → UTerm L μ₂),
    bindq b e m a✝ = bind (shiftb b m) (fun x => UTerm.bShifts m (e x)) a✝
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
⊢ bindq b e (m + 1) a✝ = bindq (shiftb b m) (fun x => UTerm.bShifts m (e x)) 1 a✝
Tactic:
simp [*]
State after:
no goals