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

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

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

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