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

State before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ subst σ (const c :: e₁ ++ e₂) = subst σ (const c :: e₁) ++ subst σ e₂
Tactic:
simp only [subst, List.append_eq]
State after:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂

State before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: subst σ (e₁ ++ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Tactic:
rw [subst_append ..]
State after:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: (subst σ e₁ ++ subst σ e₂) = const c :: subst σ e₁ ++ subst σ e₂

State before:
σ : VR → Expr
c : CN
e₁ e₂ : Expr
⊢ const c :: (subst σ e₁ ++ subst σ e₂) = const c :: subst σ e₁ ++ subst σ e₂
Tactic:
rfl
State after:
no goals

State before:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: e ++ e₂) = subst σ (var v :: e) ++ subst σ e₂
Tactic:
rw [List.cons_append]
State after:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ subst σ (var v :: (e ++ e₂)) = subst σ (var v :: e) ++ subst σ e₂

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

State before:
σ : VR → Expr
v : VR
e : List Sym
e₂ : Expr
⊢ σ v ++ subst σ (e ++ e₂) = σ v ++ subst σ e ++ subst σ e₂
Tactic:
rw [List.append_assoc, subst_append ..]
State after:
no goals