internlm/Lean-Github huggingface dataset:
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
i : Fin 2
⊢ v i = ![v 0, v 1] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
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
Tactic:
rintro ⟨t', rfl, u', rfl, H⟩
Proof state after:
case pos.mpr.intro.intro.intro.intro
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
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
⊢ ∀ (a : Fin 2), ω (v a) = ![ω t', ω u'] a
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos.mpr.intro.intro.intro.intro
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
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
⊢ ∀ (a : Fin 2), ω (v a) = ![ω t', ω u'] a
Tactic:
intro i
Proof state after:
case pos.mpr.intro.intro.intro.intro
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
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
i : Fin 2
⊢ ω (v i) = ![ω t', ω u'] i
Theorem: LO.FirstOrder.Rew.eq_equal_iff
Proof state before:
case pos.mpr.intro.intro.intro.intro
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
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
i : Fin 2
⊢ ω (v i) = ![ω t', ω u'] i
Tactic:
cases i using Fin.cases <;> simp [H, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
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.LT.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.LT
t u : Semiterm L ξ₂ n₂
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n₁
⊢ (k✝ = 2 ∧ HEq r✝ Language.LT.lt ∧ HEq (fun i => ω (v✝ i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ k✝ = 2 ∧ HEq r✝ Language.LT.lt ∧ HEq v✝ fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ (k' = 2 ∧ HEq r' Language.LT.lt ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ k' = 2 ∧ HEq r' Language.LT.lt ∧ 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.LT
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = 2
⊢ (HEq r' Language.LT.lt ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.LT.lt ∧ HEq v fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
t u : Semiterm L ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = 2
⊢ (HEq r' Language.LT.lt ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.LT.lt ∧ 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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (HEq r' Language.LT.lt ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.LT.lt ∧ HEq v fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (HEq r' Language.LT.lt ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.LT.lt ∧ 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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (r' = Language.LT.lt ∧ (fun i => ω (v i)) = fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ r' = Language.LT.lt ∧ v = fun i => ![t', x] i
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (r' = Language.LT.lt ∧ (fun i => ω (v i)) = fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ r' = Language.LT.lt ∧ v = fun i => ![t', x] i
Tactic:
by_cases hr : r' = Language.LT.lt <;> 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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∀ (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_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∀ (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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∀ (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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∃ 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_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∀ (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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
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_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
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_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
i : Fin 2
⊢ v i = ![v 0, v 1] i
Theorem: LO.FirstOrder.Rew.eq_lt_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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
H : ∀ (a : Fin 2), ω (v a) = ![t, u] a
i : Fin 2
⊢ v i = ![v 0, v 1] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_lt_iff
Proof state before:
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.LT
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
⊢ (∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a) → ∀ (a : Fin 2), ω (v a) = ![t, u] a
Tactic:
rintro ⟨t', rfl, u', rfl, H⟩
Proof state after:
case pos.mpr.intro.intro.intro.intro
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.LT
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
⊢ ∀ (a : Fin 2), ω (v a) = ![ω t', ω u'] a
Theorem: LO.FirstOrder.Rew.eq_lt_iff
Proof state before:
case pos.mpr.intro.intro.intro.intro
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.LT
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
⊢ ∀ (a : Fin 2), ω (v a) = ![ω t', ω u'] a
Tactic:
intro i
Proof state after:
case pos.mpr.intro.intro.intro.intro
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.LT
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
i : Fin 2
⊢ ω (v i) = ![ω t', ω u'] i
Theorem: LO.FirstOrder.Rew.eq_lt_iff
Proof state before:
case pos.mpr.intro.intro.intro.intro
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.LT
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.LT.lt
t' u' : Semiterm L ξ₁ n₁
H : ∀ (a : Fin 2), v a = ![t', u'] a
i : Fin 2
⊢ ω (v i) = ![ω t', ω u'] i
Tactic:
cases i using Fin.cases <;> simp [H, Fin.eq_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.zero_eq_of_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Zero
inst✝¹ : Zero M
inst✝ : Structure.Zero L M
⊢ func Language.Zero.zero ![] = 0
Tactic:
simpa[Semiterm.Operator.val, Semiterm.Operator.Zero.zero, val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Zero.zero (L := L) (M := M)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.one_eq_of_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.One
inst✝¹ : One M
inst✝ : Structure.One L M
⊢ func Language.One.one ![] = 1
Tactic:
simpa[Semiterm.Operator.val, Semiterm.Operator.One.one, val_func, ←Matrix.fun_eq_vec₂] using
  Structure.One.one (L := L) (M := M)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.add_eq_of_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Add
inst✝¹ : Add M
inst✝ : Structure.Add L M
v : Fin 2 → M
⊢ func Language.Add.add v = v 0 + v 1
Tactic:
simpa[val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Add.add (L := L) (v 0) (v 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.mul_eq_of_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Mul
inst✝¹ : Mul M
inst✝ : Structure.Mul L M
v : Fin 2 → M
⊢ func Language.Mul.mul v = v 0 * v 1
Tactic:
simpa[val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Mul.mul (L := L) (v 0) (v 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.exp_eq_of_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Exp
inst✝¹ : Exp M
inst✝ : Structure.Exp L M
v : Fin 1 → M
⊢ func Language.Exp.exp v = exp (v 0)
Tactic:
simpa[val_func, ←Matrix.constant_eq_singleton'] using
  Structure.Exp.exp (L := L) (v 0)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.le_iff_of_eq_of_lt
Proof state before:
L : Language
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Operator.Eq L
inst✝³ : Operator.LT L
inst✝² : LT M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
a b : M
⊢ op(≤).val ![a, b] ↔ a = b ∨ a < b
Tactic:
simp [Operator.LE.def_of_Eq_of_LT]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.eq_lang
Proof state before:
L : Language
M : Type u_1
inst✝² : Structure L M
inst✝¹ : L.Eq
inst✝ : Structure.Eq L M
v : Fin 2 → M
⊢ rel Language.Eq.eq v ↔ v 0 = v 1
Tactic:
simpa[Semiformula.Operator.Eq.sentence_eq, eval_rel, ←Matrix.fun_eq_vec₂] using
  Structure.Eq.eq (L := L) (v 0) (v 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.lt_lang
Proof state before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.LT
inst✝¹ : LT M
inst✝ : Structure.LT L M
v : Fin 2 → M
⊢ rel Language.LT.lt v ↔ v 0 < v 1
Tactic:
simpa[Semiformula.Operator.LT.sentence_eq, eval_rel, ←Matrix.fun_eq_vec₂] using
  Structure.LT.lt (L := L) (v 0) (v 1)
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.operator_val_ofEquiv_iff
Proof state before:
L : Language
M : Type u_1
inst✝ : Structure L M
N : Type u_2
φ : M ≃ N
k : ℕ
o : Semiformula.Operator L k
v : Fin k → N
⊢ o.val v ↔ o.val (⇑φ.symm ∘ v)
Tactic:
simp [Semiformula.Operator.val, eval_ofEquiv_iff, Empty.eq_elim]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballLT
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.LT L
inst✝¹ : LT M
inst✝ : Structure.LT L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (ballLT t p) ↔ ∀ x < Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [ballLT]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexLT
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.LT L
inst✝¹ : LT M
inst✝ : Structure.LT L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexLT t p) ↔ ∃ x < Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [bexLT]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballLE
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.LE L
inst✝¹ : LE M
inst✝ : Structure.LE L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (ballLE t p) ↔ ∀ x ≤ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [ballLE]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexLE
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.LE L
inst✝¹ : LE M
inst✝ : Structure.LE L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexLE t p) ↔ ∃ x ≤ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [bexLE]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_ballMem
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.Mem L
inst✝¹ : Membership M M
inst✝ : Structure.Mem L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (ballMem t p) ↔ ∀ x ∈ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [ballMem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_bexMem
Proof state before:
ξ : Type u_3
n : ℕ
L : Language
M : Type u_1
s : Structure L M
t : Semiterm L ξ n
p : Semiformula L ξ (n + 1)
inst✝² : Operator.Mem L
inst✝¹ : Membership M M
inst✝ : Structure.Mem L M
e : Fin n → M
ε : ξ → M
⊢ (Eval s e ε) (bexMem t p) ↔ ∃ x ∈ Semiterm.val s e ε t, (Eval s (x :> e) ε) p
Tactic:
simp [bexMem]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_zero_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ Semiterm.lMap oringEmb op(0).term = op(0).term
Tactic:
simp [Semiterm.Operator.Zero.term_eq, Semiterm.lMap_func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_one_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ Semiterm.lMap oringEmb op(1).term = op(1).term
Tactic:
simp [Semiterm.Operator.One.term_eq, Semiterm.lMap_func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_add_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ Semiterm.lMap oringEmb op(+).term = op(+).term
Tactic:
simp [Semiterm.Operator.Add.term_eq, Semiterm.lMap_func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_mul_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ Semiterm.lMap oringEmb op(*).term = op(*).term
Tactic:
simp [Semiterm.Operator.Mul.term_eq, Semiterm.lMap_func, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_eq_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ (Semiformula.lMap oringEmb) op(=).sentence = op(=).sentence
Tactic:
simp [Semiformula.Operator.Eq.sentence_eq, Semiformula.lMap_rel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.oringEmb_operator_lt_val
Proof state before:
L : Language
inst✝ : L.ORing
⊢ (Semiformula.lMap oringEmb) op(<).sentence = op(<).sentence
Tactic:
simp [Semiformula.Operator.LT.sentence_eq, Semiformula.lMap_rel, Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.Zero.zero x✝ = Structure.func Language.Zero.zero x✝
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.Func k
x✝ : Fin 0 → M
⊢ Structure.func Language.One.one x✝ = Structure.func Language.One.one x✝
Tactic:
simp[Matrix.empty_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Add.add x✝ = Structure.func Language.Add.add x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
f : ℒₒᵣ.Func k
x✝ : Fin 2 → M
⊢ Structure.func Language.Mul.mul x✝ = Structure.func Language.Mul.mul x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
r : ℒₒᵣ.Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(=) x✝ = Structure.rel op(=) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.standardModel_unique'
Proof state before:
M : Type u_1
inst✝⁴ : Zero M
inst✝³ : One M
inst✝² : Add M
inst✝¹ : Mul M
inst✝ : LT M
s : Structure ℒₒᵣ M
hZero : Structure.Zero ℒₒᵣ M
hOne : Structure.One ℒₒᵣ M
hAdd : Structure.Add ℒₒᵣ M
hMul : Structure.Mul ℒₒᵣ M
hEq : Structure.Eq ℒₒᵣ M
hLT : Structure.LT ℒₒᵣ M
k : ℕ
r : ℒₒᵣ.Rel k
x✝ : Fin 2 → M
⊢ Structure.rel op(<) x✝ = Structure.rel op(<) x✝
Tactic:
simp
Proof state after:
no goals