Theorem: LO.FirstOrder.Rew.eq_equal_iff (Logic/FirstOrder/Basic/Operator.lean)

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]
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

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]
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

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
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

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
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

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]
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

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
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

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
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

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]⟩
State after:
no goals

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
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

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]
State after:
no goals

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⟩
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

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
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

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]
State after:
no goals