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✝ : ℕ
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.Semiformula.fvarList_emb
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
o : Type u_2
inst✝ : IsEmpty o
p : Semiformula L o n
⊢ (Rew.emb.hom p).fvarList = []
Tactic:
induction p using rec' <;> simp[*, Rew.rel, Rew.nrel, fvarList, ←neg_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : Function.funEqOn p.fvar? (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p
Tactic:
unfold fvar? at*
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
ω₁ ω₂ : Rew L ξ₁ n₁ ξ₂ n₂
p : Semiformula L ξ₁ n₁
hb : ∀ (x : Fin n₁), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p = ω₂.hom p
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ (fun i => ω₁ (v✝ i)) = fun i => ω₂ (v✝ i)
Tactic:
case hrel =>
  funext i
  exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
    (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ (fun i => ω₁ (v✝ i)) = fun i => ω₂ (v✝ i)
Tactic:
case hnrel =>
  funext i
  exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
    (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
ihq :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝
Tactic:
case hand ihp ihq =>
  exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
ihq :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝
Tactic:
case hor ihp ihq =>
  exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝
Tactic:
case hall ih =>
  exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝
Tactic:
case hex ih =>
  exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ (fun i => ω₁ (v✝ i)) = fun i => ω₂ (v✝ i)
Tactic:
funext i
Proof state after:
case h
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
i : Fin k✝
⊢ ω₁ (v✝ i) = ω₂ (v✝ i)
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
case h
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ₁ n✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => ∃ a, x ∈ (v✝ a).fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
i : Fin k✝
⊢ ω₁ (v✝ i) = ω₂ (v✝ i)
Tactic:
exact Semiterm.rew_eq_of_funEqOn _ _ _ hb
  (hf.of_subset (fun x hx ↦ ⟨i, hx⟩))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ q✝ : Semiformula L ξ₁ n✝
ihp :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
ihq :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂},
    (∀ (x : Fin n✝), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom q✝ = ω₂.hom q✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList ∨ x ∈ q✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.hom p✝ = ω₂.hom p✝ ∧ ω₁.hom q✝ = ω₂.hom q✝
Tactic:
exact ⟨ihp hb (hf.of_subset (fun x hx => Or.inl hx)), ihq hb (hf.of_subset (fun x hx => Or.inr hx))⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝
Tactic:
exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
x : Fin (n✝ + 1)
⊢ ω₁.q #x = ω₂.q #x
Tactic:
cases x using Fin.cases <;> simp[hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ (⇑ω₁.q ∘ Semiterm.fvar) x = (⇑ω₂.q ∘ Semiterm.fvar) x
Tactic:
simp
Proof state after:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ Rew.bShift (ω₁ &x) = Rew.bShift (ω₂ &x)
Theorem: LO.FirstOrder.Semiformula.rew_eq_of_funEqOn
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
x : ξ₁
hx : (fun x => x ∈ p✝.fvarList) x
⊢ Rew.bShift (ω₁ &x) = Rew.bShift (ω₂ &x)
Tactic:
exact congr_arg _ (hf x hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.ex_ne_subst
Proof state before:
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : Semiformula L ξ 1
t : Semiterm L ξ 0
⊢ ([→ t].hom p).complexity ≠ (∃' p).complexity
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_bind
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
ξ₂ : Type u_3
ξ₁ : Type u_4
b : Fin n₁ → Semiterm L₁ ξ₂ n₂
e : ξ₁ → Semiterm L₁ ξ₂ n₂
p : Semiformula L₁ ξ₁ n₁
⊢ (lMap Φ) ((Rew.bind b e).hom p) = (Rew.bind (Semiterm.lMap Φ ∘ b) (Semiterm.lMap Φ ∘ e)).hom ((lMap Φ) p)
Tactic:
induction p using rec' generalizing ξ₂ n₂ <;>
simp[*, Rew.rel, Rew.nrel, lMap_rel, lMap_nrel, Semiterm.lMap_bind, Rew.q_bind, Matrix.comp_vecCons', Semiterm.lMap_bShift, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_rewrite
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
ξ₁ : Type u_3
ξ₂ : Type u_4
f : ξ₁ → Semiterm L₁ ξ₂ n
p : Semiformula L₁ ξ₁ n
⊢ (lMap Φ) ((Rew.rewrite f).hom p) = (Rew.rewrite (Semiterm.lMap Φ ∘ f)).hom ((lMap Φ) p)
Tactic:
simp[Rew.rewrite, lMap_bind, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_free
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ (n + 1)
⊢ (lMap Φ) ((Rew.hom Rew.free) p) = (Rew.hom Rew.free) ((lMap Φ) p)
Tactic:
simp[Rew.free, lMap_bind, Function.comp, Matrix.comp_vecConsLast]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_fix
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (lMap Φ) ((Rew.hom Rew.fix) p) = (Rew.hom Rew.fix) ((lMap Φ) p)
Tactic:
simp[Rew.fix, lMap_bind, Function.comp]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (Rew.bind (fun x => #x.castSucc) fun x => Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x)).hom ((lMap Φ) p) =
    (Rew.bind (fun x => #x.castSucc) (#(Fin.last n) :>ₙ Semiterm.fvar)).hom ((lMap Φ) p)
Theorem: LO.FirstOrder.Semiformula.lMap_fix
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (Rew.bind (fun x => #x.castSucc) fun x => Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x)).hom ((lMap Φ) p) =
    (Rew.bind (fun x => #x.castSucc) (#(Fin.last n) :>ₙ Semiterm.fvar)).hom ((lMap Φ) p)
Tactic:
congr
Proof state after:
case e_a.e_ω.e_e
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (fun x => Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x)) = #(Fin.last n) :>ₙ Semiterm.fvar
Theorem: LO.FirstOrder.Semiformula.lMap_fix
Proof state before:
case e_a.e_ω.e_e
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (fun x => Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x)) = #(Fin.last n) :>ₙ Semiterm.fvar
Tactic:
{ funext x; cases x <;> simp }
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_fix
Proof state before:
case e_a.e_ω.e_e
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
⊢ (fun x => Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x)) = #(Fin.last n) :>ₙ Semiterm.fvar
Tactic:
funext x
Proof state after:
case e_a.e_ω.e_e.h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
x : ℕ
⊢ Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x) = (#(Fin.last n) :>ₙ Semiterm.fvar) x
Theorem: LO.FirstOrder.Semiformula.lMap_fix
Proof state before:
case e_a.e_ω.e_e.h
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : SyntacticSemiformula L₁ n
x : ℕ
⊢ Semiterm.lMap Φ ((#(Fin.last n) :>ₙ Semiterm.fvar) x) = (#(Fin.last n) :>ₙ Semiterm.fvar) x
Tactic:
cases x <;> simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_toS
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (lMap Φ) (Rew.toS.hom p) = Rew.toS.hom ((lMap Φ) p)
Tactic:
rw [Rew.eq_bind Rew.toS, lMap_bind]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (Rew.bind (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.bvar) (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.fvar)).hom
      ((lMap Φ) p) =
    Rew.toS.hom ((lMap Φ) p)
Theorem: LO.FirstOrder.Semiformula.lMap_toS
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (Rew.bind (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.bvar) (Semiterm.lMap Φ ∘ ⇑Rew.toS ∘ Semiterm.fvar)).hom
      ((lMap Φ) p) =
    Rew.toS.hom ((lMap Φ) p)
Tactic:
simp [Function.comp, Matrix.empty_eq]
Proof state after:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (Rew.bind ![] fun x => #x).hom ((lMap Φ) p) = Rew.toS.hom ((lMap Φ) p)
Theorem: LO.FirstOrder.Semiformula.lMap_toS
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
p : Semiformula L₁ (Fin n) 0
⊢ (Rew.bind ![] fun x => #x).hom ((lMap Φ) p) = Rew.toS.hom ((lMap Φ) p)
Tactic:
congr
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.lMap_rewriteMap
Proof state before:
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ : L₁ →ᵥ L₂
ξ₁ : Type u_3
ξ₂ : Type u_4
p : Semiformula L₁ ξ₁ n
f : ξ₁ → ξ₂
⊢ (lMap Φ) ((Rew.rewriteMap f).hom p) = (Rew.rewriteMap f).hom ((lMap Φ) p)
Tactic:
simp [Rew.rewriteMap, lMap_rewrite, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.fvUnivClosure_sentence
Proof state before:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ ∀ᶠ* σ = ∀' Rew.empty.hom σ
Tactic:
simp [fvUnivClosure, ←Rew.hom_comp_app, Rew.eq_empty]
Proof state after:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ
Theorem: LO.FirstOrder.Formula.fvUnivClosure_sentence
Proof state before:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ
Tactic:
have : σ.fvarList.length = 0 := by simp
Proof state after:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
this : (Semiformula.fvarList σ).length = 0
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ
Theorem: LO.FirstOrder.Formula.fvUnivClosure_sentence
Proof state before:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
this : (Semiformula.fvarList σ).length = 0
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.fvUnivClosure_sentence
Proof state before:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ (Semiformula.fvarList σ).length = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.univClosure_rew_eq_of_eq
Proof state before:
L : Language
ξ₁ : Type ?u.1797290
n₁ : ℕ
ξ₂ : Type ?u.1797295
n₂ n₂' : ℕ
p : Semiformula L ξ₁ n₁
ω : Rew L ξ₁ n₁ ξ₂ n₂
ω' : Rew L ξ₁ n₁ ξ₂ n₂'
eq : n₂ = n₂'
⊢ n₂' ≤ n₂
Tactic:
simp [eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.univClosure_rew_eq_of_eq
Proof state before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ n₂' : ℕ
p : Semiformula L ξ₁ n₁
ω : Rew L ξ₁ n₁ ξ₂ n₂
ω' : Rew L ξ₁ n₁ ξ₂ n₂'
eq : n₂ = n₂'
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p
Tactic:
rcases eq with rfl
Proof state after:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω ω' : Rew L ξ₁ n₁ ξ₂ n₂
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p
Theorem: LO.FirstOrder.Formula.univClosure_rew_eq_of_eq
Proof state before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω ω' : Rew L ξ₁ n₁ ξ₂ n₂
H : ω = (Rew.castLE ⋯).comp ω'
⊢ ∀* ω.hom p = ∀* ω'.hom p
Tactic:
rcases H with rfl
Proof state after:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω' : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀* ((Rew.castLE ⋯).comp ω').hom p = ∀* ω'.hom p
Theorem: LO.FirstOrder.Formula.univClosure_rew_eq_of_eq
Proof state before:
L : Language
ξ₁ : Type u_2
n₁ : ℕ
ξ₂ : Type u_3
n₂ : ℕ
p : Semiformula L ξ₁ n₁
ω' : Rew L ξ₁ n₁ ξ₂ n₂
⊢ ∀* ((Rew.castLE ⋯).comp ω').hom p = ∀* ω'.hom p
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Formula.lMap_fvUnivClosure
Proof state before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ (Semiformula.lMap Φ) (∀ᶠ* σ) = ∀ᶠ* (Semiformula.lMap Φ) σ
Tactic:
simp [Formula.fvUnivClosure, Semiformula.lMap_toS, Semiformula.lMap_rewriteMap]
Proof state after:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* Rew.toS.hom ((Rew.rewriteMap (Semiformula.fvListing σ)).hom ((Semiformula.lMap Φ) σ)) =
    ∀* Rew.toS.hom ((Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing).hom ((Semiformula.lMap Φ) σ))