Theorem: LO.FirstOrder.Derivation.free_rewrite_eq (Logic/FirstOrder/Basic/Calculus.lean)

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.hom Rew.free) ((Rew.rewrite fun x => Rew.bShift (f x)).hom p) =
    (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).hom ((Rew.hom Rew.free) p)
Tactic:
simp[←Rew.hom_comp_app]
State after:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x))).hom p =
    ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free).hom p

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ (Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x))).hom p =
    ((Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free).hom p
Tactic:
exact Rew.hom_ext' (by ext x <;> simp[Rew.comp_app, Fin.eq_zero])
State after:
no goals

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
p : SyntacticSemiformula L 1
⊢ Rew.comp Rew.free (Rew.rewrite fun x => Rew.bShift (f x)) = (Rew.rewrite (&0 :>ₙ fun x => ⇑ (f x))).comp Rew.free
Tactic:
ext x <;> simp[Rew.comp_app, Fin.eq_zero]
State after:
no goals