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

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
p : UFormula L μ₁
hb : ∀ x < p.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind b₁ e₁ p = bind b₂ e₂ p
Tactic:
induction p generalizing b₁ b₂ e₁ e₂ <;> simp[bind, bindq, he]
State after:
case rel
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
arity✝ : ℕ
a✝¹ : L.Rel arity✝
a✝ : Fin arity✝ → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel a✝¹ a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ (fun i => UTerm.bind b₁ (fun x => e₂ x) (a✝ i)) = fun i => UTerm.bind b₂ (fun x => e₂ x) (a✝ i)

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

case and
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝¹.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝¹ = bind b₂ e₂ a✝¹
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (a✝¹.and a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 a✝¹ = bindq b₂ e₂ 0 a✝¹ ∧ bindq b₁ e₁ 0 a✝ = bindq b₂ e₂ 0 a✝

case or
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝¹ a✝ : UFormula L μ₁
a_ih✝¹ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝¹.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝¹ = bind b₂ e₂ a✝¹
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (a✝¹.or a✝).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 a✝¹ = bindq b₂ e₂ 0 a✝¹ ∧ bindq b₁ e₁ 0 a✝ = bindq b₂ e₂ 0 a✝

case all
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < a✝.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 a✝ = bindq b₂ e₂ 1 a✝

case ex
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
a✝ : UFormula L μ₁
a_ih✝ :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < a✝.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ a✝ = bind b₂ e₂ a✝
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < a✝.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 a✝ = bindq b₂ e₂ 1 a✝

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.and q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 p = bindq b₂ e₂ 0 p ∧ bindq b₁ e₁ 0 q = bindq b₂ e₂ 0 q
Tactic:
case and p q ihp ihq =>
  exact ⟨ihp b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he, ihq b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he⟩
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.or q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 p = bindq b₂ e₂ 0 p ∧ bindq b₁ e₁ 0 q = bindq b₂ e₂ 0 q
Tactic:
case or p q ihp ihq =>
  exact ⟨ihp b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he, ihq b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he⟩
State after:
no goals

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

State before:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ UTerm.bind b₁ (fun x => e₂ x) (v i) = UTerm.bind b₂ (fun x => e₂ x) (v i)
Tactic:
apply UTerm.bind_eq_bind_of_eq
State after:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ x < (v i).bv, b₁ x = b₂ x

case h.he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ (x : μ₁), e₂ x = e₂ x

State before:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ x < (v i).bv, b₁ x = b₂ x
Tactic:
intro x hx
State after:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ b₁ x = b₂ x

State before:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ b₁ x = b₂ x
Tactic:
exact hb x (by simp; exact ⟨i, hx⟩)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (rel r v).bv
Tactic:
simp
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ 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
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
State after:
no goals

State before:
case h.he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (rel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ (x : μ₁), e₂ x = e₂ x
Tactic:
simp
State after:
no goals

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

State before:
case h
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ UTerm.bind b₁ (fun x => e₂ x) (v i) = UTerm.bind b₂ (fun x => e₂ x) (v i)
Tactic:
apply UTerm.bind_eq_bind_of_eq
State after:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ x < (v i).bv, b₁ x = b₂ x

case h.he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ (x : μ₁), e₂ x = e₂ x

State before:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ x < (v i).bv, b₁ x = b₂ x
Tactic:
intro x hx
State after:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ b₁ x = b₂ x

State before:
case h.hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ b₁ x = b₂ x
Tactic:
exact hb x (by simp; exact ⟨i, hx⟩)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (nrel r v).bv
Tactic:
simp
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ 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
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
State after:
no goals

State before:
case h.he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ₁
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (nrel r v).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
i : Fin k
⊢ ∀ (x : μ₁), e₂ x = e₂ x
Tactic:
simp
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.and q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 p = bindq b₂ e₂ 0 p ∧ bindq b₁ e₁ 0 q = bindq b₂ e₂ 0 q
Tactic:
exact ⟨ihp b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he, ihq b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he⟩
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.and q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ x < (p.and q).bv
Tactic:
simp[hx]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.and q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < q.bv
⊢ x < (p.and q).bv
Tactic:
simp[hx]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.or q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 0 p = bindq b₂ e₂ 0 p ∧ bindq b₁ e₁ 0 q = bindq b₂ e₂ 0 q
Tactic:
exact ⟨ihp b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he, ihq b₁ b₂ e₁ e₂ (fun x hx => hb x (by simp[hx])) he⟩
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.or q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ x < (p.or q).bv
Tactic:
simp[hx]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p q : UFormula L μ₁
ihp :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
ihq :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < q.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ q = bind b₂ e₂ q
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < (p.or q).bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < q.bv
⊢ x < (p.or q).bv
Tactic:
simp[hx]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 p = bindq b₂ e₂ 1 p
Tactic:
simp[bindq_eq_bind]
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind (shiftb b₁ 1) (fun x => UTerm.bShifts 1 (e₁ x)) p = bind (shiftb b₂ 1) (fun x => UTerm.bShifts 1 (e₂ x)) p

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind (shiftb b₁ 1) (fun x => UTerm.bShifts 1 (e₁ x)) p = bind (shiftb b₂ 1) (fun x => UTerm.bShifts 1 (e₂ x)) p
Tactic:
apply ih
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ x < p.bv, shiftb b₁ 1 x = shiftb b₂ 1 x

case he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ (x : μ₁), UTerm.bShifts 1 (e₁ x) = UTerm.bShifts 1 (e₂ x)

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ x < p.bv, shiftb b₁ 1 x = shiftb b₂ 1 x
Tactic:
intro x hx
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ shiftb b₁ 1 x = shiftb b₂ 1 x

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ shiftb b₁ 1 x = shiftb b₂ 1 x
Tactic:
simp[shiftb]
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ (if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₁ (x - 1))) =
    if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₂ (x - 1))

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ (if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₁ (x - 1))) =
    if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₂ (x - 1))
Tactic:
cases' x with x <;> simp
State after:
case hb.succ
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ UTerm.bShifts 1 (b₁ x) = UTerm.bShifts 1 (b₂ x)

State before:
case hb.succ
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ UTerm.bShifts 1 (b₁ x) = UTerm.bShifts 1 (b₂ x)
Tactic:
simp[hb x (by simp; exact Nat.lt_pred_iff.mpr hx)]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.all.bv
Tactic:
simp
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.bv - 1

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.bv - 1
Tactic:
exact Nat.lt_pred_iff.mpr hx
State after:
no goals

State before:
case he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.all.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ (x : μ₁), UTerm.bShifts 1 (e₁ x) = UTerm.bShifts 1 (e₂ x)
Tactic:
simp[he]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bindq b₁ e₁ 1 p = bindq b₂ e₂ 1 p
Tactic:
simp[bindq_eq_bind]
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind (shiftb b₁ 1) (fun x => UTerm.bShifts 1 (e₁ x)) p = bind (shiftb b₂ 1) (fun x => UTerm.bShifts 1 (e₂ x)) p

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ bind (shiftb b₁ 1) (fun x => UTerm.bShifts 1 (e₁ x)) p = bind (shiftb b₂ 1) (fun x => UTerm.bShifts 1 (e₂ x)) p
Tactic:
apply ih
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ x < p.bv, shiftb b₁ 1 x = shiftb b₂ 1 x

case he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ (x : μ₁), UTerm.bShifts 1 (e₁ x) = UTerm.bShifts 1 (e₂ x)

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ x < p.bv, shiftb b₁ 1 x = shiftb b₂ 1 x
Tactic:
intro x hx
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ shiftb b₁ 1 x = shiftb b₂ 1 x

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ shiftb b₁ 1 x = shiftb b₂ 1 x
Tactic:
simp[shiftb]
State after:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ (if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₁ (x - 1))) =
    if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₂ (x - 1))

State before:
case hb
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x < p.bv
⊢ (if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₁ (x - 1))) =
    if x = 0 then UTerm.bvar x else UTerm.bShifts 1 (b₂ (x - 1))
Tactic:
cases' x with x <;> simp
State after:
case hb.succ
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ UTerm.bShifts 1 (b₁ x) = UTerm.bShifts 1 (b₂ x)

State before:
case hb.succ
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ UTerm.bShifts 1 (b₁ x) = UTerm.bShifts 1 (b₂ x)
Tactic:
simp[hb x (by simp; exact Nat.lt_pred_iff.mpr hx)]
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.ex.bv
Tactic:
simp
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.bv - 1

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
x : ℕ
hx : x + 1 < p.bv
⊢ x < p.bv - 1
Tactic:
exact Nat.lt_pred_iff.mpr hx
State after:
no goals

State before:
case he
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
p : UFormula L μ₁
ih :
  ∀ (b₁ b₂ : ℕ → UTerm L μ₂) (e₁ e₂ : μ₁ → UTerm L μ₂),
    (∀ x < p.bv, b₁ x = b₂ x) → (∀ (x : μ₁), e₁ x = e₂ x) → bind b₁ e₁ p = bind b₂ e₂ p
b₁ b₂ : ℕ → UTerm L μ₂
e₁ e₂ : μ₁ → UTerm L μ₂
hb : ∀ x < p.ex.bv, b₁ x = b₂ x
he : ∀ (x : μ₁), e₁ x = e₂ x
⊢ ∀ (x : μ₁), UTerm.bShifts 1 (e₁ x) = UTerm.bShifts 1 (e₂ x)
Tactic:
simp[he]
State after:
no goals