internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof 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))
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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)]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof 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))
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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)
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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)]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof 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
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bind_eq_bind_of_eq
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (↑(ofSubformula (Semiformula.rel r v))).toSubformula ⋯ = Semiformula.rel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.toSubterm_ofSubterm]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (↑(ofSubformula (Semiformula.nrel r v))).toSubformula ⋯ = Semiformula.nrel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.toSubterm_ofSubterm]
Proof state after:
no goals