Theorem: Metamath.Expr.subst_tr (Metamath/Translate.lean)

State before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst (subst.trans σ σ') (var v :: e) = subst σ' (subst σ (var v :: e))
Tactic:
simp only [subst]
State after:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)

State before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst (subst.trans σ σ') e = subst σ' (σ v ++ subst σ e)
Tactic:
rw [subst_append, subst_tr _ _ e]
State after:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst σ' (subst σ e) = subst σ' (σ v) ++ subst σ' (subst σ e)

State before:
σ σ' : VR → Expr
v : VR
e : List Sym
⊢ subst.trans σ σ' v ++ subst σ' (subst σ e) = subst σ' (σ v) ++ subst σ' (subst σ e)
Tactic:
rfl
State after:
no goals