Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv (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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
p : Semiformula L ξ₁ n₁
f g : ξ₁ → Semiterm L ξ₂ n₂
h : Function.funEqOn (fun x => x ∈ p.fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p
Tactic:
induction p using rec'
State after:
case hverum
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤

case hfalsum
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥

case hrel
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r✝ v✝).fv) f g
⊢ (rewriteMap f).hom (rel r✝ v✝) = (rewriteMap g).hom (rel r✝ v✝)

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r✝ v✝).fv) f g
⊢ (rewriteMap f).hom (nrel r✝ v✝) = (rewriteMap g).hom (nrel r✝ v✝)

case hand
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
a✝ : Function.funEqOn (fun x => x ∈ q✝.fv) f g → (rewriteMap f).hom q✝ = (rewriteMap g).hom q✝
h : Function.funEqOn (fun x => x ∈ (p✝ ⋏ q✝).fv) f g
⊢ (rewriteMap f).hom (p✝ ⋏ q✝) = (rewriteMap g).hom (p✝ ⋏ q✝)

case hor
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
a✝¹ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
a✝ : Function.funEqOn (fun x => x ∈ q✝.fv) f g → (rewriteMap f).hom q✝ = (rewriteMap g).hom q✝
h : Function.funEqOn (fun x => x ∈ (p✝ ⋎ q✝).fv) f g
⊢ (rewriteMap f).hom (p✝ ⋎ q✝) = (rewriteMap g).hom (p✝ ⋎ q✝)

case hall
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
h : Function.funEqOn (fun x => x ∈ (∀' p✝).fv) f g
⊢ (rewriteMap f).hom (∀' p✝) = (rewriteMap g).hom (∀' p✝)

case hex
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
a✝ : Function.funEqOn (fun x => x ∈ p✝.fv) f g → (rewriteMap f).hom p✝ = (rewriteMap g).hom p✝
h : Function.funEqOn (fun x => x ∈ (∃' p✝).fv) f g
⊢ (rewriteMap f).hom (∃' p✝) = (rewriteMap g).hom (∃' p✝)

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤
Tactic:
case hverum => simp
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥
Tactic:
case hfalsum => simp
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (rewriteMap f).hom (rel r v) = (rewriteMap g).hom (rel r v)
Tactic:
case hrel r v =>
  simp [Rew.rel]; funext i
  exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (rewriteMap f).hom (nrel r v) = (rewriteMap g).hom (nrel r v)
Tactic:
case hnrel r v =>
  simp [Rew.nrel]; funext i
  exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_nrel]; exact ⟨i, hx⟩))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ (rewriteMap f).hom (p ⋏ q) = (rewriteMap g).hom (p ⋏ q)
Tactic:
case hand p q ihp ihq =>
  simp; exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ (rewriteMap f).hom (p ⋎ q) = (rewriteMap g).hom (p ⋎ q)
Tactic:
case hor p q ihp ihq =>
  simp; exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ (rewriteMap f).hom (∀' p) = (rewriteMap g).hom (∀' p)
Tactic:
case hall p ih => simp; exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom (∃' p) = (rewriteMap g).hom (∃' p)
Tactic:
case hex p ih => simp; exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊤.fv) f g
⊢ (rewriteMap f).hom ⊤ = (rewriteMap g).hom ⊤
Tactic:
simp
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
h : Function.funEqOn (fun x => x ∈ ⊥.fv) f g
⊢ (rewriteMap f).hom ⊥ = (rewriteMap g).hom ⊥
Tactic:
simp
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (rewriteMap f).hom (rel r v) = (rewriteMap g).hom (rel r v)
Tactic:
simp [Rew.rel]
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
Tactic:
funext i
State after:
case h
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)

State before:
case h
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Tactic:
exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
⊢ Function.funEqOn (fun x => x ∈ (v i).fv) f g
Tactic:
intro x (hx : x ∈ (v i).fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x
Tactic:
exact h _ (by simp [fv_rel]; exact ⟨i, hx⟩)
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ (fun x => x ∈ (rel r v).fv) x
Tactic:
simp [fv_rel]
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (rel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv
Tactic:
exact ⟨i, hx⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (rewriteMap f).hom (nrel r v) = (rewriteMap g).hom (nrel r v)
Tactic:
simp [Rew.nrel]
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
⊢ (fun i => (rewriteMap f) (v i)) = fun i => (rewriteMap g) (v i)
Tactic:
funext i
State after:
case h
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)

State before:
case h
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ (rewriteMap f) (v i) = (rewriteMap g) (v i)
Tactic:
exact eq_rewriteMap_of_funEqOn_fv (v i) f g (by intro x (hx : x ∈ (v i).fv); exact h _ (by simp [fv_nrel]; exact ⟨i, hx⟩))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
⊢ Function.funEqOn (fun x => x ∈ (v i).fv) f g
Tactic:
intro x (hx : x ∈ (v i).fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ f x = g x
Tactic:
exact h _ (by simp [fv_nrel]; exact ⟨i, hx⟩)
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ (fun x => x ∈ (nrel r v).fv) x
Tactic:
simp [fv_nrel]
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ξ₁ n✝
h : Function.funEqOn (fun x => x ∈ (nrel r v).fv) f g
i : Fin k✝
x : ξ₁
hx : x ∈ (v i).fv
⊢ ∃ a, x ∈ (v a).fv
Tactic:
exact ⟨i, hx⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ (rewriteMap f).hom (p ⋏ q) = (rewriteMap g).hom (p ⋏ q)
Tactic:
simp
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p ∧ (rewriteMap f).hom q = (rewriteMap g).hom q

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p ∧ (rewriteMap f).hom q = (rewriteMap g).hom q
Tactic:
exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ Function.funEqOn (fun x => x ∈ p.fv) f g
Tactic:
intro x (hx : x ∈ p.fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ (fun x => x ∈ (p ⋏ q).fv) x
Tactic:
simp [hx]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
⊢ Function.funEqOn (fun x => x ∈ q.fv) f g
Tactic:
intro x (hx : x ∈ q.fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋏ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ (fun x => x ∈ (p ⋏ q).fv) x
Tactic:
simp [hx]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ (rewriteMap f).hom (p ⋎ q) = (rewriteMap g).hom (p ⋎ q)
Tactic:
simp
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p ∧ (rewriteMap f).hom q = (rewriteMap g).hom q

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p ∧ (rewriteMap f).hom q = (rewriteMap g).hom q
Tactic:
exact ⟨ihp (by intro x (hx : x ∈ p.fv); exact h _ (by simp [hx])), ihq (by intro x (hx : x ∈ q.fv); exact h _ (by simp [hx]))⟩
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ Function.funEqOn (fun x => x ∈ p.fv) f g
Tactic:
intro x (hx : x ∈ p.fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ (fun x => x ∈ (p ⋎ q).fv) x
Tactic:
simp [hx]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
⊢ Function.funEqOn (fun x => x ∈ q.fv) f g
Tactic:
intro x (hx : x ∈ q.fv)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p q : Semiformula L ξ₁ n✝
ihp : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
ihq : Function.funEqOn (fun x => x ∈ q.fv) f g → (rewriteMap f).hom q = (rewriteMap g).hom q
h : Function.funEqOn (fun x => x ∈ (p ⋎ q).fv) f g
x : ξ₁
hx : x ∈ q.fv
⊢ (fun x => x ∈ (p ⋎ q).fv) x
Tactic:
simp [hx]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ (rewriteMap f).hom (∀' p) = (rewriteMap g).hom (∀' p)
Tactic:
simp
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p
Tactic:
exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
⊢ Function.funEqOn (fun x => x ∈ p.fv) f g
Tactic:
intro x (hx : x ∈ fv p)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∀' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ (fun x => x ∈ (∀' p).fv) x
Tactic:
simp [hx]
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom (∃' p) = (rewriteMap g).hom (∃' p)
Tactic:
simp
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ (rewriteMap f).hom p = (rewriteMap g).hom p
Tactic:
exact ih (by intro x (hx : x ∈ fv p); exact h _ (by simp [hx]))
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
⊢ Function.funEqOn (fun x => x ∈ p.fv) f g
Tactic:
intro x (hx : x ∈ fv p)
State after:
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x

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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ f x = g x
Tactic:
exact h _ (by simp [hx])
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₂✝
ξ₁ : Type u_5
ξ₂ : Type u_6
n₁ n₂ : ℕ
inst✝ : DecidableEq ξ₁
f g : ξ₁ → Semiterm L ξ₂ n₂
n✝ : ℕ
p : Semiformula L ξ₁ (n✝ + 1)
ih : Function.funEqOn (fun x => x ∈ p.fv) f g → (rewriteMap f).hom p = (rewriteMap g).hom p
h : Function.funEqOn (fun x => x ∈ (∃' p).fv) f g
x : ξ₁
hx : x ∈ p.fv
⊢ (fun x => x ∈ (∃' p).fv) x
Tactic:
simp [hx]
State after:
no goals