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

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
t : Semiterm L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
he : Function.funEqOn t.fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ t = ω₂ t
Tactic:
induction t <;> try simp[Rew.func, hb]
State after:
case fvar
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝

case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (a✝ i)) = fun i => ω₂ (a✝ i)

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝
Tactic:
case fvar => simpa[fvar?, Function.funEqOn] using he
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (v i)) = fun i => ω₂ (v i)
Tactic:
case func k f v ih =>
  funext i
  exact ih i (he.of_subset $ by simp[fvar?]; intro x hx; exact ⟨i, hx⟩)
State after:
no goals

State before:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ (func a✝¹ a✝) = ω₂ (func a✝¹ a✝)
Tactic:
simp[Rew.func, hb]
State after:
case func
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ξ₁ n₁
a_ih✝ : ∀ (a : Fin arity✝), Function.funEqOn (a✝ a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (a✝ a) = ω₂ (a✝ a)
he : Function.funEqOn (func a✝¹ a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (a✝ i)) = fun i => ω₂ (a✝ i)

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
a✝ : ξ₁
he : Function.funEqOn (&a✝).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ ω₁ &a✝ = ω₂ &a✝
Tactic:
simpa[fvar?, Function.funEqOn] using he
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
⊢ (fun i => ω₁ (v i)) = fun i => ω₂ (v i)
Tactic:
funext i
State after:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ω₁ (v i) = ω₂ (v i)

State before:
case h
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ω₁ (v i) = ω₂ (v i)
Tactic:
exact ih i (he.of_subset $ by simp[fvar?]; intro x hx; exact ⟨i, hx⟩)
State after:
no goals

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ (a : ξ₁), (v i).fvar? a → (func f v).fvar? a
Tactic:
simp[fvar?]
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ a ∈ (v i).fvarList, ∃ i, a ∈ (v i).fvarList

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
⊢ ∀ a ∈ (v i).fvarList, ∃ i, a ∈ (v i).fvarList
Tactic:
intro x hx
State after:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
x : ξ₁
hx : x ∈ (v i).fvarList
⊢ ∃ i, x ∈ (v i).fvarList

State before:
L : Language
L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ' : Type u_2
ξ₁ : Type u_3
ξ₂ : Type u_4
ξ₃ : Type u_5
n n₁ n₂ n₃ : ℕ
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
k : ℕ
f : L.Func k
v : Fin k → Semiterm L ξ₁ n₁
ih : ∀ (a : Fin k), Function.funEqOn (v a).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar) → ω₁ (v a) = ω₂ (v a)
he : Function.funEqOn (func f v).fvar? (⇑ω₁ ∘ fvar) (⇑ω₂ ∘ fvar)
i : Fin k
x : ξ₁
hx : x ∈ (v i).fvarList
⊢ ∃ i, x ∈ (v i).fvarList
Tactic:
exact ⟨i, hx⟩
State after:
no goals