theorem LeanSubst.Ren.lift_eq_from_eq {T : Type u2} [RenMap T [T]] {r : Ren T} {σ : Subst T} : r.to = σ → r.to.lift = σ.lift

@[simp]

theorem LeanSubst.Subst.id_rmap {T : Type u_1} {V : List (Type u_2)} [RenMap T V] [RenSuffix T V] (r : RenVec V) : 𝐬0(T)⟨r,⟩ = 𝐬0(T)

@[simp]

theorem LeanSubst.Subst.rewrite0 {T : Type u2} [RenMap T [T]] : 𝐬0(T) >> 𝐫1(T) = 𝐬1(T)

@[simp]

theorem LeanSubst.Subst.rewrite1 {T : Type u2} : re 0 :: 𝐬1(T) = 𝐬0(T)

@[simp]

theorem LeanSubst.Subst.rewrite1_ren {T : Type u2} : 0 :: 𝐫1(T) = 𝐫0(T)

@[simp]

theorem LeanSubst.Subst.I_lift {T : Type u2} [RenMap T [T]] {k : Nat} : 𝐬0(T).lift k = 𝐬0(T)

@[simp]

theorem LeanSubst.Subst.rewrite2 {T : Type u2} [SubstMap T [T]] {σ : Subst T} : 𝐬0(T) >> σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite2_ren {T : Type u2} [SubstMap T [T]] {σ : Subst T} : 𝐫0(T) >> σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite3_cons {T : Type u2} [SubstMap T [T]] {σ τ : Subst T} {a : Action T} : a :: σ >> τ = a[τ] :: (σ >> τ)

@[simp]

theorem LeanSubst.Subst.rewrite3_cons_ren {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {σ : Subst T} {r : Ren T} {x : Nat} : re x :: σ >> r = re (r.act x) :: (σ >> r)

@[simp]

theorem LeanSubst.Subst.rewrite3_append {T : Type u2} [SubstMap T [T]] {σ τ : Subst T} {ℓ : List (Action T)} : ℓ ++ σ >> τ = ℓ[τ] ++ (σ >> τ)

@[simp]

theorem LeanSubst.Subst.rewrite3_append_act {T : Type u2} [SubstMap T [T]] {σ τ : Subst T} {ℓ : List Nat} : ℓ ++ σ >> τ = τ.act ℓ ++ (σ >> τ)

@[simp]

theorem LeanSubst.Subst.rewrite3_append_ren {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {σ : Subst T} {r : Ren T} {ℓ : List Nat} : ℓ ++ σ >> r = ℓ⟨r⟩ ++ (σ >> r)

@[simp]

theorem LeanSubst.Subst.rewrite4_cons {T : Type u2} [SubstMap T [T]] {s : Action T} {σ : Subst T} : 𝐬1(T) >> s :: σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite4_cons_ren {T : Type u2} [SubstMap T [T]] {s : Action T} {σ : Subst T} : 𝐫1(T) >> s :: σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite5 {T : Type u2} [SubstMap T [T]] {σ : Subst T} : σ.act 0 :: (𝐬1(T) >> σ) = σ

@[simp]

theorem LeanSubst.Subst.rewrite5_ren {T : Type u2} [SubstMap T [T]] {σ : Subst T} : σ.act 0 :: (𝐫1(T) >> σ) = σ

theorem LeanSubst.Subst.rewrite_lift {T : Type u2} [RenMap T [T]] {σ : Subst T} : σ.lift = re 0 :: (σ >> 𝐫1(T))

@[simp]

theorem LeanSubst.Subst.rewrite_lift_zero {T : Type u2} [RenMap T [T]] [RenMapId T [T]] {σ : Subst T} : σ.lift 0 = σ

theorem LeanSubst.Subst.rewrite_lift_succ {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k : Nat} {σ : Subst T} : σ.lift (k + 1) = (σ.lift k).lift

@[simp]

theorem LeanSubst.Subst.rewrite6 {T : Type u2} [RenMap T [T]] [SubstMap T [T]] [SubstMapId T [T]] {σ : Subst T} : σ >> 𝐬0(T) = σ

@[simp]

theorem LeanSubst.Subst.rewrite6_ren {T : Type u2} [RenMap T [T]] [RenMapId T [T]] {σ : Subst T} : σ >> 𝐫0(T) = σ

@[simp]

theorem LeanSubst.Subst.rewrite7 {T : Type u2} [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapEmpty T] {σ τ μ : Subst T} : (σ >> τ) >> μ = σ >> τ >> μ

@[simp]

theorem LeanSubst.Subst.rewrite4_append_direct {T : Type u2} [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapEmpty T] {ℓ : List (Action T)} {σ : Subst T} : add T ℓ.length >> ℓ ++ σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite4_append_indirect {T : Type u2} [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapEmpty T] {k : Nat} {ℓ : List (Action T)} {σ : Subst T} (h : k = ℓ.length) : add T k >> ℓ ++ σ = σ

theorem LeanSubst.Subst.subst_append_assoc {T : Type u2} {xs ys : List (Action T)} {σ : Subst T} : xs ++ ys ++ σ = xs ++ (ys ++ σ)

theorem LeanSubst.Subst.subst_append_assoc_nat {T : Type u2} {xs ys : List Nat} {σ : Subst T} : xs ++ ys ++ σ = xs ++ (ys ++ σ)

@[simp]

theorem LeanSubst.Subst.range_act_succ {T : Type u2} {s e : Nat} {σ : Subst T} : 𝐬1(T).act (s..e) ++ σ = s.succ..e.succ ++ σ

@[simp]

theorem LeanSubst.Subst.range_act_succ_ren {T : Type u2} {s e : Nat} {σ : Subst T} : (s..e)⟨𝐫1(T)⟩ ++ σ = s.succ..e.succ ++ σ

@[simp]

theorem LeanSubst.Subst.rewrite_compose_subst_ren_ren_assoc {T : Type u2} [RenMap T [T]] [RenMapCompose T [T]] {σ : Subst T} {r1 r2 : Ren T} : (σ >> r1) >> r2 = σ >> r1 >> r2

theorem LeanSubst.Subst.rewrite_lift_k {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] [SubstMapAll [T]] [SubstMapId T [T]] [SubstMapCompose T [T]] {k : Nat} {σ : Subst T} : σ.lift k = 0..k ++ (σ >> Ren.add T k)

theorem LeanSubst.Subst.compose_commute_succ {T : Type u2} [RenMap T [T]] {τ : Subst T} : τ >> 𝐫1(T) = 𝐫1(T) >> τ.lift

theorem LeanSubst.Ren.compose_commute_succ {T : Type u2} {r : Ren T} : r >> 𝐫1(T) = 𝐫1(T) >> r.lift

theorem LeanSubst.Subst.rewrite_lift_compose_ren_left_k1 {T : Type u2} [RenMap T [T]] {r : Ren T} {τ : Subst T} : (r >> τ).lift = r.lift >> τ.lift

@[simp]

theorem LeanSubst.Subst.rewrite_lift_compose_ren_left {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k : Nat} {r : Ren T} {τ : Subst T} : (r >> τ).lift k = r.lift k >> τ.lift k

theorem LeanSubst.Subst.lift_compose_ren_right_k1 {T : Type u2} [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {σ : Subst T} {r : Ren T} : (σ >> r).lift = σ.lift >> r.lift

@[simp]

theorem LeanSubst.Subst.lift_compose_ren_right {T : Type u2} [RenMap T [T]] [SubstMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k : Nat} {σ : Subst T} {r : Ren T} : (σ >> r).lift k = σ.lift k >> r.lift k

@[simp]

theorem LeanSubst.Subst.rename_lift_commute {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteRenRen S V] {k : Nat} {σ : Subst S} {r : RenVec V} : (σ.lift k)⟨r,⟩ = σ⟨r,⟩.lift k

theorem LeanSubst.Subst.rewrite_lift_compose_k1 {T : Type u2} [RenMapAll [T]] [SubstMap T [T]] [RenMapEmpty T] [SubstMapRenComposeLeft T [T]] [SubstMapRenComposeRight T [T]] {σ τ : Subst T} : (σ >> τ).lift = σ.lift >> τ.lift

@[simp]

theorem LeanSubst.Subst.rewrite_lift_compose {T : Type u2} [RenMapAll [T]] [RenMapId T [T]] [RenMapEmpty T] [RenMapCompose T [T]] [SubstMap T [T]] [SubstMapRenComposeLeft T [T]] [SubstMapRenComposeRight T [T]] {k : Nat} {σ τ : Subst T} : (σ >> τ).lift k = σ.lift k >> τ.lift k

@[simp]

theorem LeanSubst.Subst.subst_lift_commute {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [SubstMap S V] [SubstSuffix S V] [SuffixCommuteRenSub S V] {k : Nat} {σ : Subst S} {τ : SubstVec V} : (σ.lift k)[τ,] = σ[τ,].lift k

@[simp]

theorem LeanSubst.Subst.rmap_compose_ren_left_commute {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] {r : RenVec V} {k : Ren S} {τ : Subst S} : (k >> τ)⟨r,⟩ = k >> τ⟨r,⟩

@[simp]

theorem LeanSubst.Subst.rmap_compose_ren_right_commute {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteRenRen S V] {r : RenVec V} {σ : Subst S} {k : Ren S} : (σ >> k)⟨r,⟩ = σ⟨r,⟩ >> k

@[simp]

theorem LeanSubst.Subst.rmap_compose_commute {S : Type u1} {V : List (Type u2)} [SubstMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteSubRen S V] {r : RenVec V} {σ τ : Subst S} : (σ >> τ)⟨r,⟩ = σ⟨r,⟩ >> τ⟨r,⟩