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

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]
State after:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ

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
State after:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
this : (Semiformula.fvarList σ).length = 0
⊢ ∀* Rew.empty.hom σ = ∀' Rew.empty.hom σ

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
State after:
no goals

State before:
ξ : Type u_1
L : Language
h : IsEmpty ξ
inst✝ : DecidableEq ξ
σ : Formula L ξ
⊢ (Semiformula.fvarList σ).length = 0
Tactic:
simp
State after:
no goals