internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula (p ⋏ q))).toSubformula ⋯ = p ⋏ q
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q
Tactic:
exact ⟨toSubformula_ofSubformula p, toSubformula_ofSubformula q⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula (p ⋎ q))).toSubformula ⋯ = p ⋎ q
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : Semiformula L μ x✝
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p ∧ (↑(ofSubformula q)).toSubformula ⋯ = q
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula (∀' p))).toSubformula ⋯ = ∀' p
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p
Tactic:
exact toSubformula_ofSubformula p
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toSubformula_ofSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula (∃' p))).toSubformula ⋯ = ∃' p
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : Semiformula L μ (x✝ + 1)
⊢ (↑(ofSubformula p)).toSubformula ⋯ = p
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → UTerm L μ
h : (rel r v).bv ≤ x✝
⊢ ↑(ofSubformula ((rel r v).toSubformula h)) = rel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.ofSubterm_toSubterm]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → UTerm L μ
h : (nrel r v).bv ≤ x✝
⊢ ↑(ofSubformula ((nrel r v).toSubformula h)) = nrel r v
Tactic:
simp[ofSubformula, toSubformula, UTerm.ofSubterm_toSubterm]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ ↑(ofSubformula ((p.and q).toSubformula h)) = p.and q
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Tactic:
exact ⟨ofSubformula_toSubformula p (by simp at h; exact h.1), ofSubformula_toSubformula q (by simp at h; exact h.2)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
simp at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
exact h.1
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.and q).bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
simp at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
exact h.2
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ ↑(ofSubformula ((p.or q).toSubformula h)) = p.or q
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p ∧ ↑(ofSubformula (q.toSubformula ⋯)) = q
Tactic:
exact ⟨ofSubformula_toSubformula p (by simp at h; exact h.1), ofSubformula_toSubformula q (by simp at h; exact h.2)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ p.bv ≤ x✝
Tactic:
simp at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ p.bv ≤ x✝
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : (p.or q).bv ≤ x✝
⊢ q.bv ≤ x✝
Tactic:
simp at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p q : UFormula L μ
h : p.bv ≤ x✝ ∧ q.bv ≤ x✝
⊢ q.bv ≤ x✝
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.all.toSubformula h)) = p.all
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Tactic:
exact ofSubformula_toSubformula p (by simp only [bv_all] at h; exact Nat.le_add_of_sub_le h)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.all.bv ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
simp only [bv_all] at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
exact Nat.le_add_of_sub_le h
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.ex.toSubformula h)) = p.ex
Tactic:
simp[ofSubformula, toSubformula]
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ ↑(ofSubformula (p.toSubformula ⋯)) = p
Tactic:
exact ofSubformula_toSubformula p (by simp only [bv_ex] at h; exact Nat.le_add_of_sub_le h)
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.ofSubformula_toSubformula
Proof state before:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.ex.bv ≤ x✝
⊢ p.bv ≤ x✝ + 1
Tactic:
simp only [bv_ex] at h
Proof state after:
L : Language
μ : Type v
x✝ : ℕ
p : UFormula L μ
h : p.bv.pred ≤ x✝
⊢ p.bv ≤ x✝ + 1
Theorem: LO.FirstOrder.UFormula.subfEquiv_verum
Proof state before:
L : Language
μ : Type v
n : ℕ
⊢ verum.bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_falsum
Proof state before:
L : Language
μ : Type v
n : ℕ
⊢ falsum.bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_rel
Proof state before:
L : Language
μ : Type v
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ (rel r fun i => ↑(UTerm.subtEquiv (v i))).bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_nrel
Proof state before:
L : Language
μ : Type v
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
⊢ (nrel r fun i => ↑(UTerm.subtEquiv (v i))).bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_and
Proof state before:
L : Language
μ : Type v
n : ℕ
p q : Semiformula L μ n
⊢ ((↑(subfEquiv p)).and ↑(subfEquiv q)).bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_or
Proof state before:
L : Language
μ : Type v
n : ℕ
p q : Semiformula L μ n
⊢ ((↑(subfEquiv p)).or ↑(subfEquiv q)).bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_all
Proof state before:
L : Language
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
⊢ (↑(subfEquiv p)).all.bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.subfEquiv_ex
Proof state before:
L : Language
μ : Type v
n : ℕ
p : Semiformula L μ (n + 1)
⊢ (↑(subfEquiv p)).ex.bv ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
fst✝ : ℕ
r : L.Rel fst✝
v : Fin fst✝ → UTerm L μ
f✝ : Edge L μ (true, Sum.inl ⟨fst✝, (r, v)⟩) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inl ⟨fst✝, (r, v)⟩) f✝)).toW = WType.mk (true, Sum.inl ⟨fst✝, (r, v)⟩) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
fst✝ : ℕ
r : L.Rel fst✝
v : Fin fst✝ → UTerm L μ
f✝ : Edge L μ (false, Sum.inl ⟨fst✝, (r, v)⟩) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝)).toW = WType.mk (false, Sum.inl ⟨fst✝, (r, v)⟩) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
f✝ : Edge L μ (true, Sum.inr (Sum.inl ())) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inl ())) f✝)).toW = WType.mk (true, Sum.inr (Sum.inl ())) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
f✝ : Edge L μ (false, Sum.inr (Sum.inl ())) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inl ())) f✝)).toW = WType.mk (false, Sum.inr (Sum.inl ())) f✝
Tactic:
simp[ofW, toW, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) w)).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inl ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w false), toW_ofW (w true)]
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
Proof state after:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) w)).toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inl ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w false), toW_ofW (w true)]
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
Proof state after:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
case h
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inl ()))) → WType (Edge L μ)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (true, Sum.inr (Sum.inr (Sum.inr ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w)).toW = WType.mk (true, Sum.inr (Sum.inr (Sum.inr ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w ())]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.toW_ofW
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
w : Edge L μ (false, Sum.inr (Sum.inr (Sum.inr ()))) → WType (Edge L μ)
⊢ (ofW (WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) w)).toW = WType.mk (false, Sum.inr (Sum.inr (Sum.inr ()))) w
Tactic:
simp[ofW, toW, toW_ofW (w ())]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.qeq
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
α : Sort u_1
a b c d : α
h₁ : a = b
h₂ : b = c
h₃ : c = d
⊢ a = d
Tactic:
simp[*]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode (rel r v) = Nat.pair 1 ((Nat.pair 1 ((2 * k.pair) ((encode r).pair (encode v)))).pair 0)
Tactic:
simp[primcodable, Primcodable.ofEquiv_toEncodable,
  Encodable.encode_ofEquiv (equivW L μ), WType.encode_eq, WType.SubWType.ofW, WType.depth]
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
⊢ encode
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
have : (WType.depth (β := Edge L μ) (WType.mk (true, Sum.inl ⟨k, r, v⟩) Empty.elim)) = 1 := rfl
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode
      (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
        ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode
      (WType.SubWType.cast this
        (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
suffices encode (WType.SubWType.ofWType (β := Edge L μ) ⟨(true, Sum.inl ⟨k, r, v⟩), Empty.elim⟩ 1 (by rw[this])) =
  ((Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0) by
{ rw[←this]; apply congr_arg; simp }
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
simp[WType.SubWType.encode_mk, Encodable.encode_fintypeArrow_isEmpty, Edge]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
⊢ (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth ≤ 1
Tactic:
rw[this]
Proof state after:
no goals
Theorem: LO.FirstOrder.UFormula.encode_rel
Proof state before:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
Tactic:
rw[←this]
Proof state after:
L : Language
μ : Type v
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : (k : ℕ) → Primcodable (L.Rel k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : UniformlyPrimcodable L.Rel
inst✝ : Primcodable μ
k : ℕ
r : L.Rel k
v : Fin k → UTerm L μ
this✝ : (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim).depth = 1
this :
  encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯) =
    (Nat.pair 1 (2 * k.pair ((encode r).pair (encode v)))).pair 0
⊢ encode
      (WType.SubWType.cast this✝
        (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim)
          ((Finset.univ.sup fun n => (Empty.elim n).depth) + 1) ⋯)) =
    encode (WType.SubWType.ofWType (WType.mk (true, Sum.inl ⟨k, (r, v)⟩) Empty.elim) 1 ⋯)