Theorem: LO.FirstOrder.Rew.eq_nrel_iff (Logic/FirstOrder/Basic/Syntax/Rew.lean)

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₁
k : ℕ
r : L.Rel k
v : Fin k → Semiterm L ξ₂ n₂
⊢ ω.hom p = nrel r v ↔ ∃ v', ⇑ω ∘ v' = v ∧ p = nrel r v'
Tactic:
cases p using Semiformula.rec' <;> simp[Rew.rel, Rew.nrel]
State after:
case hnrel
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₂
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n₁
⊢ k✝ = k ∧ HEq r✝ r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ k✝ = k ∧ HEq r✝ r ∧ HEq v✝ v'

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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
case hnrel k' r' v =>
  by_cases hk : k' = k <;> simp[hk]; rcases hk with rfl; simp
  by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
State after:
no goals

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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
Tactic:
by_cases hk : k' = k <;> simp[hk]
State after:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'

State before:
case pos
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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'
Tactic:
rcases hk with rfl
State after:
case pos
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₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'

State before:
case pos
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₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ HEq r' r ∧ HEq (fun i => ω (v✝ i)) v ↔ ∃ v', ⇑ω ∘ v' = v ∧ HEq r' r ∧ HEq v✝ v'
Tactic:
simp
State after:
case pos
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₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r

State before:
case pos
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₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
Tactic:
by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
State after:
no goals