internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.embSubsts_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
m : ℕ
t : Semiterm L Empty n
v : Fin n → Semiterm L ξ (m + 1)
⊢ (∀ (x : Fin (m + 1)), ∀ x_1 ∈ t.bv, x ∈ (v x_1).bv → 0 < x) ↔ ∀ i ∈ t.bv, ∀ x ∈ (v i).bv, 0 < x
Tactic:
exact ⟨fun H i hi x hx ↦ H x i hi hx, fun H x i hi hx ↦ H i hi x hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.bshift_positive
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ n
⊢ (bShift t).Positive
Tactic:
induction t <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_emb
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
o : Type u_6
e : IsEmpty o
t : Semiterm L o n
⊢ (Rew.emb t).fvarList = []
Tactic:
induction t <;> simp[*, List.eq_nil_iff_forall_not_mem, Rew.func]
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
o : Type u_6
e : IsEmpty o
a✝ : o
⊢ ∀ (a : ξ), a ∉ (Rew.emb &a✝).fvarList
Theorem: LO.FirstOrder.Semiterm.fvarList_emb
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
o : Type u_6
e : IsEmpty o
x : o
⊢ ∀ (a : ξ), a ∉ (Rew.emb &x).fvarList
Tactic:
case fvar x => exact IsEmpty.elim' e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.fvarList_emb
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
o : Type u_6
e : IsEmpty o
x : o
⊢ ∀ (a : ξ), a ∉ (Rew.emb &x).fvarList
Tactic:
exact IsEmpty.elim' e x
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
he : Function.funEqOn t.fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ t = ω₂ t
Tactic:
induction t <;> try simp[Rew.func, hb]
Proof state after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝

case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (a✝ i)) = fun i => ω₂ (a✝ i)
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝
Tactic:
case fvar => simpa[fvar?, Function.funEqOn] using he
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (v i)) = fun i => ω₂ (v i)
Tactic:
case func k f v ih =>
  funext i
  exact ih i (he.of_subset $ by simp[fvar?]; intro x hx; exact ⟨i, hx⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ (func a✝¹ a✝) = ω₂ (func a✝¹ a✝)
Tactic:
simp[Rew.func, hb]
Proof state after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (a✝ i)) = fun i => ω₂ (a✝ i)
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝
Tactic:
simpa[fvar?, Function.funEqOn] using he
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (v i)) = fun i => ω₂ (v i)
Tactic:
funext i
Proof state after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ω₁ (v i) = ω₂ (v i)
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ω₁ (v i) = ω₂ (v i)
Tactic:
exact ih i (he.of_subset $ by simp[fvar?]; intro x hx; exact ⟨i, hx⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ (a : ξ₁), (v i).fvar? a → (func f v).fvar? a
Tactic:
simp[fvar?]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ a ∈ (v i).fvarList, ∃ i, a ∈ (v i).fvarList
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ a ∈ (v i).fvarList, ∃ i, a ∈ (v i).fvarList
Tactic:
intro x hx
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
x : ξ₁
hx : x ∈ (v i).fvarList
⊢ ∃ i, x ∈ (v i).fvarList
Theorem: LO.FirstOrder.Semiterm.rew_eq_of_funEqOn
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
x : ξ₁
hx : x ∈ (v i).fvarList
⊢ ∃ i, x ∈ (v i).fvarList
Tactic:
exact ⟨i, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_bind
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
b : Fin n₁ → Semiterm L₁ ξ₂ n₂
e : ξ₁ → Semiterm L₁ ξ₂ n₂
t : Semiterm L₁ ξ₁ n₁
⊢ lMap Φ ((Rew.bind b e) t) = (Rew.bind (lMap Φ ∘ b) (lMap Φ ∘ e)) (lMap Φ t)
Tactic:
induction t <;> simp[*, lMap_func, Rew.func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_map
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
b : Fin n₁ → Fin n₂
e : ξ₁ → ξ₂
t : Semiterm L₁ ξ₁ n₁
⊢ lMap Φ ((map b e) t) = (map b e) (lMap Φ t)
Tactic:
simp[map, lMap_bind, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_bShift
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : Semiterm L₁ ξ₁ n
⊢ lMap Φ (bShift t) = bShift (lMap Φ t)
Tactic:
simp[bShift, lMap_map]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_shift
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ lMap Φ (⇑ t) = ⇑ (lMap Φ t)
Tactic:
simp[shift, lMap_map]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_free
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ lMap Φ (free t) = free (lMap Φ t)
Tactic:
simp[free, lMap_bind]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ (Rew.bind (lMap Φ ∘ (bvar <: &0)) (lMap Φ ∘ fun m => &(m + 1))) (lMap Φ t) =
    (Rew.bind (bvar <: &0) fun m => &(m + 1)) (lMap Φ t)
Theorem: LO.FirstOrder.Semiterm.lMap_free
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ (Rew.bind (lMap Φ ∘ (bvar <: &0)) (lMap Φ ∘ fun m => &(m + 1))) (lMap Φ t) =
    (Rew.bind (bvar <: &0) fun m => &(m + 1)) (lMap Φ t)
Tactic:
congr
Proof state after:
case e_a.e_b
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ lMap Φ ∘ (bvar <: &0) = bvar <: &0
Theorem: LO.FirstOrder.Semiterm.lMap_free
Proof state before:
case e_a.e_b
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ lMap Φ ∘ (bvar <: &0) = bvar <: &0
Tactic:
exact funext $ Fin.lastCases (by simp) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_free
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ (lMap Φ ∘ (bvar <: &0)) (Fin.last n) = (bvar <: &0) (Fin.last n)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_free
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ (n + 1)
⊢ ∀ (i : Fin n), (lMap Φ ∘ (bvar <: &0)) i.castSucc = (bvar <: &0) i.castSucc
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.lMap_fix
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ lMap Φ (fix t) = fix (lMap Φ t)
Tactic:
simp[fix, lMap_bind]
Proof state after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ (Rew.bind (lMap Φ ∘ fun x => #x.castSucc) (lMap Φ ∘ (#(Fin.last n) :>ₙ fvar))) (lMap Φ t) =
    (Rew.bind (fun x => #x.castSucc) (#(Fin.last n) :>ₙ fvar)) (lMap Φ t)
Theorem: LO.FirstOrder.Semiterm.lMap_fix
Proof state before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ (Rew.bind (lMap Φ ∘ fun x => #x.castSucc) (lMap Φ ∘ (#(Fin.last n) :>ₙ fvar))) (lMap Φ t) =
    (Rew.bind (fun x => #x.castSucc) (#(Fin.last n) :>ₙ fvar)) (lMap Φ t)
Tactic:
congr
Proof state after:
case e_a.e_e
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ lMap Φ ∘ (#(Fin.last n) :>ₙ fvar) = #(Fin.last n) :>ₙ fvar
Theorem: LO.FirstOrder.Semiterm.lMap_fix
Proof state before:
case e_a.e_e
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
⊢ lMap Φ ∘ (#(Fin.last n) :>ₙ fvar) = #(Fin.last n) :>ₙ fvar
Tactic:
funext x
Proof state after:
case e_a.e_e.h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
x : ℕ
⊢ (lMap Φ ∘ (#(Fin.last n) :>ₙ fvar)) x = (#(Fin.last n) :>ₙ fvar) x
Theorem: LO.FirstOrder.Semiterm.lMap_fix
Proof state before:
case e_a.e_e.h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
Φ : L₁ →ᵥ L₂
t : SyntacticSemiterm L₁ n
x : ℕ
⊢ (lMap Φ ∘ (#(Fin.last n) :>ₙ fvar)) x = (#(Fin.last n) :>ₙ fvar) x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.loMap_neg
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
⊢ ω.loMap (~p) = ~ω.loMap p
Tactic:
induction p using Semiformula.rec' generalizing n₂ <;> simp[*, loMap, ←Semiformula.neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.ext_loMap'
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
h : ω₁ = ω₂
p : Semiformula L ξ₁ n₁
⊢ ω₁.loMap p = ω₂.loMap p
Tactic:
simp[h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.or'
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
p q : Semiformula L ξ₁ n₁
⊢ ω.loMap (p ⋎ q) = ω.loMap p ⋎ ω.loMap q
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.nrel
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r v) = nrel r fun i => ω (v i)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rel'
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.hom (rel r v) = rel r (⇑ω ∘ v)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.nrel'
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r v) = nrel r (⇑ω ∘ v)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rel0
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 0
v : Fin 0 → Semiterm L ξ₁ n₁
⊢ ω.hom (rel r v) = rel r ![]
Tactic:
simp[ω.rel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rel1
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 1
t : Semiterm L ξ₁ n₁
⊢ ω.hom (rel r ![t]) = rel r ![ω t]
Tactic:
simp[ω.rel, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rel2
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ ω.hom (rel r ![t₁, t₂]) = rel r ![ω t₁, ω t₂]
Tactic:
simp[ω.rel]
Proof state after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Theorem: LO.FirstOrder.Rew.rel2
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂] i)) = ![ω t₁, ω t₂]
Tactic:
funext i
Proof state after:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Theorem: LO.FirstOrder.Rew.rel2
Proof state before:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 2
t₁ t₂ : Semiterm L ξ₁ n₁
i : Fin 2
⊢ ω (![t₁, t₂] i) = ![ω t₁, ω t₂] i
Tactic:
induction i using Fin.induction <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.rel3
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω.hom (rel r ![t₁, t₂, t₃]) = rel r ![ω t₁, ω t₂, ω t₃]
Tactic:
simp[ω.rel]
Proof state after:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂, t₃] i)) = ![ω t₁, ω t₂, ω t₃]
Theorem: LO.FirstOrder.Rew.rel3
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ (fun i => ω (![t₁, t₂, t₃] i)) = ![ω t₁, ω t₂, ω t₃]
Tactic:
funext i
Proof state after:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 3
⊢ ω (![t₁, t₂, t₃] i) = ![ω t₁, ω t₂, ω t₃] i
Theorem: LO.FirstOrder.Rew.rel3
Proof state before:
case h
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 3
⊢ ω (![t₁, t₂, t₃] i) = ![ω t₁, ω t₂, ω t₃] i
Tactic:
induction' i using Fin.induction with i <;> simp
Proof state after:
case h.succ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 2
a✝ : ω (![t₁, t₂, t₃] i.castSucc) = ![ω t₁, ω t₂, ω t₃] i.castSucc
⊢ ω (![t₂, t₃] i) = ![ω t₂, ω t₃] i
Theorem: LO.FirstOrder.Rew.rel3
Proof state before:
case h.succ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
i : Fin 2
a✝ : ω (![t₁, t₂, t₃] i.castSucc) = ![ω t₁, ω t₂, ω t₃] i.castSucc
⊢ ω (![t₂, t₃] i) = ![ω t₂, ω t₃] i
Tactic:
induction' i using Fin.induction with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.nrel0
Proof state before:
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
r : L.Rel 0
v : Fin 0 → Semiterm L ξ₁ n₁
⊢ ω.hom (nrel r v) = nrel r ![]
Tactic:
simp[ω.nrel, Matrix.empty_eq]
Proof state after:
no goals