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

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]
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 Φ) σ))

State before:
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 Φ) σ))
Tactic:
simp [←Rew.hom_comp_app]
State after:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ ∀* (Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ))).hom ((Semiformula.lMap Φ) σ) =
    ∀* (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing)).hom ((Semiformula.lMap Φ) σ)

State before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ (Semiformula.fvarList σ).length + 1 = ((Semiformula.lMap Φ) σ).fvarList.length + 1
Tactic:
simp
State after:
no goals

State before:
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
⊢ Rew.toS.comp (Rew.rewriteMap (Semiformula.fvListing σ)) =
    (Rew.castLE ⋯).comp (Rew.toS.comp (Rew.rewriteMap ((Semiformula.lMap Φ) σ).fvListing))
Tactic:
ext x <;> simp [Rew.comp_app]
State after:
case hb
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : Fin 0
⊢ Rew.toS #x = (Rew.castLE ⋯) (Rew.toS #x)

case hf
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ Semiformula.fvListing σ x = Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x)

State before:
case hb
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : Fin 0
⊢ Rew.toS #x = (Rew.castLE ⋯) (Rew.toS #x)
Tactic:
apply finZeroElim x
State after:
no goals

State before:
case hf
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ Semiformula.fvListing σ x = Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x)
Tactic:
ext
State after:
case hf.h
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ ↑(Semiformula.fvListing σ x) = ↑(Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x))

State before:
case hf.h
L₁ : Language
L₂ : Language
ξ : Type u_3
Φ : L₁ →ᵥ L₂
inst✝ : DecidableEq ξ
σ : Formula L₁ ξ
x : ξ
⊢ ↑(Semiformula.fvListing σ x) = ↑(Fin.castLE ⋯ (((Semiformula.lMap Φ) σ).fvListing x))
Tactic:
simp [Semiformula.fvListing]
State after:
no goals