Theorem: LO.FirstOrder.Semiformula.lMap_toS (Logic/FirstOrder/Basic/Syntax/Rew.lean)

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

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

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