internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Semiformula.Operator.operator_or
Proof state before:
L : Language
k : ℕ
ξ : Type u_1
n : ℕ
o₁ o₂ : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (o₁.or o₂).operator v = o₁.operator v ⋎ o₂.operator v
Tactic:
simp [operator, or]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.Eq.equal_inj
Proof state before:
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝ : L.Eq
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(=).operator ![t₁, u₁] = op(=).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
Tactic:
simp [operator, Eq.sentence_eq, Matrix.fun_eq_vec₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.LT.lt_inj
Proof state before:
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝ : L.LT
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(<).operator ![t₁, u₁] = op(<).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
Tactic:
simp [operator, LT.sentence_eq, Matrix.fun_eq_vec₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.LE.le_inj
Proof state before:
L : Language
ξ₂ : Type u_1
n₂ : ℕ
inst✝¹ : L.Eq
inst✝ : L.LT
t₁ t₂ u₁ u₂ : Semiterm L ξ₂ n₂
⊢ op(≤).operator ![t₁, u₁] = op(≤).operator ![t₂, u₂] ↔ t₁ = t₂ ∧ u₁ = u₂
Tactic:
simp [operator, LE.sentence_eq, Eq.sentence_eq, LT.sentence_eq, Matrix.fun_eq_vec₂]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.Eq.open
Proof state before:
L✝ : Language
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(=).operator ![t, u]).Open
Tactic:
simp [Operator.operator, Operator.Eq.sentence_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.LT.open
Proof state before:
L✝ : Language
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(<).operator ![t, u]).Open
Tactic:
simp [Operator.operator, Operator.LT.sentence_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.Operator.LE.open
Proof state before:
L✝ : Language
L : Language
inst✝¹ : L.Eq
inst✝ : L.LT
ξ : Type u_1
n : ℕ
t u : Semiterm L ξ n
⊢ (op(≤).operator ![t, u]).Open
Tactic:
simp [Operator.operator, Operator.LE.sentence_eq, Operator.Eq.sentence_eq, Operator.LT.sentence_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_operator_and
Proof state before:
L : Language
M : Type w
s : Structure L M
k : ℕ
o₁ o₂ : Operator L k
v : Fin k → M
⊢ (o₁.and o₂).val v ↔ o₁.val v ∧ o₂.val v
Tactic:
simp [Operator.and, Operator.val]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.val_operator_or
Proof state before:
L : Language
M : Type w
s : Structure L M
k : ℕ
o₁ o₂ : Operator L k
v : Fin k → M
⊢ (o₁.or o₂).val v ↔ o₁.val v ∨ o₂.val v
Tactic:
simp [Operator.or, Operator.val]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator
Proof state before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ n
⊢ (Eval s e ε) (o.operator v) ↔ o.val fun i => Semiterm.val s e ε (v i)
Tactic:
simp [Operator.operator, eval_substs, Operator.val]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator₀
Proof state before:
L : Language
M : Type w
s : Structure L M
n✝ : ℕ
e : Fin n✝ → M
ξ✝ : Type u_1
ε : ξ✝ → M
o : Const L
v : Fin 0 → Semiterm L ξ✝ n✝
⊢ (Eval s e ε) (Operator.operator o v) ↔ Operator.val o ![]
Tactic:
simp [eval_operator, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator₁
Proof state before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 1
t : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t]) ↔ o.val ![Semiterm.val s e ε t]
Tactic:
simp [eval_operator, Matrix.constant_eq_singleton]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_operator₂
Proof state before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (Eval s e ε) (o.operator ![t₁, t₂]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
simp [eval_operator]
Proof state after:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_operator₂
Proof state before:
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
apply of_eq
Proof state after:
case a
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) = o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_operator₂
Proof state before:
case a
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (o.val fun i => Semiterm.val s e ε (![t₁, t₂] i)) = o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
congr
Proof state after:
case a.e_v
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (fun i => Semiterm.val s e ε (![t₁, t₂] i)) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Theorem: LO.FirstOrder.Semiformula.eval_operator₂
Proof state before:
case a.e_v
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
⊢ (fun i => Semiterm.val s e ε (![t₁, t₂] i)) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂]
Tactic:
funext i
Proof state after:
case a.e_v.h
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
i : Fin 2
⊢ Semiterm.val s e ε (![t₁, t₂] i) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂] i
Theorem: LO.FirstOrder.Semiformula.eval_operator₂
Proof state before:
case a.e_v.h
L : Language
M : Type w
s : Structure L M
ξ : Type u_1
n : ℕ
e : Fin n → M
ε : ξ → M
o : Operator L 2
t₁ t₂ : Semiterm L ξ n
i : Fin 2
⊢ Semiterm.val s e ε (![t₁, t₂] i) = ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂] i
Tactic:
cases' i using Fin.cases with i <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.operator
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω (o.operator v) = o.operator fun i => ω (v i)
Tactic:
simp [Semiterm.Operator.operator, ←comp_app]
Proof state after:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)) o.term = ((substs fun i => ω (v i)).comp emb) o.term
Theorem: LO.FirstOrder.Rew.operator
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)) o.term = ((substs fun i => ω (v i)).comp emb) o.term
Tactic:
congr 1
Proof state after:
case e_a
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb
Theorem: LO.FirstOrder.Rew.operator
Proof state before:
case e_a
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb
Tactic:
ext <;> simp [comp_app]
Proof state after:
case e_a.hf
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Theorem: LO.FirstOrder.Rew.operator
Proof state before:
case e_a.hf
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Tactic:
try contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.operator
Proof state before:
case e_a.hf
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiterm.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.finitary0
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiterm.Operator L 0
v : Fin 0 → Semiterm L ξ₁ n₁
⊢ ω (o.operator v) = o.operator ![]
Tactic:
simp [ω.operator', Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.finitary1
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiterm.Operator L 1
t : Semiterm L ξ₁ n₁
⊢ ω (o.operator ![t]) = o.operator ![ω t]
Tactic:
simp [ω.operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.finitary2
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiterm.Operator L 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ ω (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]
Tactic:
simp [ω.operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.finitary3
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiterm.Operator L 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]
Tactic:
simp [ω.operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.const
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
c : Semiterm.Const L
⊢ ω (Semiterm.Operator.const c) = Semiterm.Operator.const c
Tactic:
simp [Semiterm.Operator.const, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_operator
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator v) = o.operator fun i => ω (v i)
Tactic:
simp [Semiformula.Operator.operator, ←Rew.hom_comp_app]
Proof state after:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)).hom o.sentence = ((substs fun i => ω (v i)).comp emb).hom o.sentence
Theorem: LO.FirstOrder.Rew.hom_operator
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ (ω.comp ((substs v).comp emb)).hom o.sentence = ((substs fun i => ω (v i)).comp emb).hom o.sentence
Tactic:
congr 2
Proof state after:
case e_a.e_ω
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb
Theorem: LO.FirstOrder.Rew.hom_operator
Proof state before:
case e_a.e_ω
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
⊢ ω.comp ((substs v).comp emb) = (substs fun i => ω (v i)).comp emb
Tactic:
ext <;> simp [Rew.comp_app]
Proof state after:
case e_a.e_ω.hf
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Theorem: LO.FirstOrder.Rew.hom_operator
Proof state before:
case e_a.e_ω.hf
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k : ℕ
o : Semiformula.Operator L k
v : Fin k → Semiterm L ξ₁ n₁
x✝ : Empty
⊢ ω ((substs v) (emb &x✝)) = (substs fun i => ω (v i)) (emb &x✝)
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_finitary0
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiformula.Operator L 0
v : Fin 0 → Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator v) = o.operator ![]
Tactic:
simp [ω.hom_operator', Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_finitary1
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiformula.Operator L 1
t : Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator ![t]) = o.operator ![ω t]
Tactic:
simp [ω.hom_operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_finitary2
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiformula.Operator L 2
t₁ t₂ : Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator ![t₁, t₂]) = o.operator ![ω t₁, ω t₂]
Tactic:
simp [ω.hom_operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_finitary3
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
o : Semiformula.Operator L 3
t₁ t₂ t₃ : Semiterm L ξ₁ n₁
⊢ ω.hom (o.operator ![t₁, t₂, t₃]) = o.operator ![ω t₁, ω t₂, ω t₃]
Tactic:
simp [ω.hom_operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.hom_const
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
c : Semiformula.Const L
⊢ ω.hom (Semiformula.Operator.const c) = Semiformula.Operator.const c
Tactic:
simp [Semiformula.Operator.const, ω.hom_operator']
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
p : Semiformula L ξ₁ n₁
t u : Semiterm L ξ₂ n₂
⊢ ω.hom p = op(=).operator ![t, u] ↔ ∃ t' u', ω t' = t ∧ ω u' = u ∧ p = op(=).operator ![t', u']
Tactic:
cases p using Semiformula.rec' <;> simp [Rew.rel, Rew.nrel, Operator.operator, Operator.Eq.sentence_eq]
Proof state after:
case hrel
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n₁
⊢ (k✝ = 2 ∧ HEq r✝ Language.Eq.eq ∧ HEq (fun i => ω (v✝ i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ k✝ = 2 ∧ HEq r✝ Language.Eq.eq ∧ HEq v✝ fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ (k' = 2 ∧ HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ k' = 2 ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i
Tactic:
by_cases hk : k' = 2 <;> simp [hk]
Proof state after:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = 2
⊢ (HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = 2
⊢ (HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i
Tactic:
rcases hk with rfl
Proof state after:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i
Tactic:
simp
Proof state after:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (r' = Language.Eq.eq ∧ (fun i => ω (v i)) = fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ r' = Language.Eq.eq ∧ v = fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (r' = Language.Eq.eq ∧ (fun i => ω (v i)) = fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ r' = Language.Eq.eq ∧ v = fun i => ![t', x] i
Tactic:
by_cases hr : r' = Language.Eq.eq <;> simp [hr, Function.funext_iff]
Proof state after:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∀ (a : Fin 2), ω (v a) = ![t, u] a) ↔ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∀ (a : Fin 2), ω (v a) = ![t, u] a) ↔ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
Tactic:
constructor
Proof state after:
case pos.mp
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∀ (a : Fin 2), ω (v a) = ![t, u] a) → ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a

case pos.mpr
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a) → ∀ (a : Fin 2), ω (v a) = ![t, u] a
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos.mp
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∀ (a : Fin 2), ω (v a) = ![t, u] a) → ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
Tactic:
rintro H
Proof state after:
case pos.mp
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
⊢ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos.mp
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
⊢ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a
Tactic:
exact ⟨v 0, H 0, v 1, H 1, by intro i; cases i using Fin.cases <;> simp [Fin.eq_zero]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
⊢ ∀ (a : Fin 2), v a = ![v 0, v 1] a
Tactic:
intro i
Proof state after:
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
i : Fin 2
⊢ v i = ![v 0, v 1] i