internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.fvEnumInv_fvEnum
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvarList.length ≤ List.indexOf x p.fvarList → default = x
Tactic:
intro h
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
h : p.fvarList.length ≤ List.indexOf x p.fvarList
⊢ default = x
Theorem: LO.FirstOrder.Semiformula.fvEnumInv_fvEnum
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
h : p.fvarList.length ≤ List.indexOf x p.fvarList
⊢ default = x
Tactic:
exact False.elim <| not_le.mpr (List.indexOf_lt_length.mpr hx) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.fvListingInv_fvListing
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvListingInv (p.fvListing x) = x
Tactic:
simp [fvListingInv, fvListing]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvarList.length ≤ List.indexOf x p.fvarList → default = x
Theorem: LO.FirstOrder.Semiformula.fvListingInv_fvListing
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
⊢ p.fvarList.length ≤ List.indexOf x p.fvarList → default = x
Tactic:
intro h
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
h : p.fvarList.length ≤ List.indexOf x p.fvarList
⊢ default = x
Theorem: LO.FirstOrder.Semiformula.fvListingInv_fvListing
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
inst✝¹ : DecidableEq ξ
inst✝ : Inhabited ξ
p : Semiformula L ξ n
x : ξ
hx : x ∈ p.fvarList
h : p.fvarList.length ≤ List.indexOf x p.fvarList
⊢ default = x
Tactic:
exact False.elim <| not_le.mpr (List.indexOf_lt_length.mpr hx) h
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.shiftb_zero
Proof state before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ shiftb b 0 = b
Tactic:
unfold shiftb
Proof state after:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ (fun x => if x < 0 then UTerm.bvar x else UTerm.bShifts 0 (b (x - 0))) = b
Theorem: LO.FirstOrder.UFormula.shiftb_zero
Proof state before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
⊢ (fun x => if x < 0 then UTerm.bvar x else UTerm.bShifts 0 (b (x - 0))) = b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ shiftb (shiftb b m₁) m₂ = shiftb b (m₁ + m₂)
Tactic:
unfold shiftb
Proof state after:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ (fun x =>
      if x < m₂ then UTerm.bvar x
      else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    fun x => if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ (fun x =>
      if x < m₂ then UTerm.bvar x
      else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    fun x => if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
funext x
Proof state after:
case h
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case h
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
by_cases hm₂ : x < m₂
Proof state after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : x < m₁ + m₂ := lt_add_of_nonneg_of_lt (Nat.zero_le m₁) hm₂
Proof state after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
this : x < m₁ + m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
this : x < m₁ + m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₂, this]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₂]
Proof state after:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
by_cases hm₁ : x < m₁ + m₂
Proof state after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : x - m₂ < m₁ := Nat.sub_lt_right_of_lt_add (Nat.not_lt.mp hm₂) hm₁
Proof state after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₁, this, UTerm.bShifts, UTerm.bind]
Proof state after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ x - m₂ + m₂ = x
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ x - m₂ + m₂ = x
Tactic:
exact tsub_add_cancel_of_le (Nat.not_lt.mp hm₂)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : ¬x - m₂ < m₁ := Nat.not_lt.mpr <| Nat.le_sub_of_add_le <| Nat.not_lt.mp hm₁
Proof state after:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
this : ¬x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero
Proof state before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
this : ¬x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₁, this, Nat.sub_sub, add_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_eq_bind
Proof 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]
Proof 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✝
Theorem: LO.FirstOrder.UFormula.bindq_eq_bind
Proof 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 [*]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.bindq_eq_bind
Proof 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 [*]
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
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]
Proof 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✝
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:
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⟩
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:
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⟩
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 < (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
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 < (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)
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 < (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
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 < (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
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 < (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
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 < (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
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 < (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⟩)
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 < (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
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 < (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
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 < (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⟩
Proof state after:
no goals