internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]))
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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)
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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])
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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
Proof 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
Theorem: LO.FirstOrder.Rew.eq_hom_rewriteMap_of_funEqOn_fv
Proof 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]))
Proof state after:
no goals