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

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

State before:
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
f : ℕ → SyntacticTerm L
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ ((Rew.rewrite f).comp [→ t]).hom p = ([→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))).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
t : Semiterm L ℕ 0
p : SyntacticSemiformula L 1
⊢ (Rew.rewrite f).comp [→ t] = [→ (Rew.rewrite f) t].comp (Rew.rewrite (⇑Rew.bShift ∘ f))
Tactic:
ext x <;> simp[Rew.comp_app]
State after:
no goals