class LeanSubst.RenMapEmpty (S : Type u1) [RenMap S []] : Prop

• apply_empty {s : S} {r : RenVec []} : s⟨r,⟩ = s

class LeanSubst.RenMapVecDef (S : Type u1) (T : Type u2) (V : List (Type u2)) [RenMap S [T]] [RenMap S (T :: V)] [RenMap S V] : Prop

• apply_vecdef {s : S} {r : RenVec (T :: V)} : s⟨r,⟩ = s⟨r.snd,⟩⟨r.fst⟩

theorem LeanSubst.Ren.apply_vecdef {S : Type u1} {T : Type u2} {V : List (Type u2)} [RenMap S [T]] [RenMap S (T :: V)] [RenMap S V] [RenMapVecDef S T V] {s : S} {r : RenVec (T :: V)} : s⟨r,⟩ = s⟨r.snd,⟩⟨r.fst⟩

@[simp]

theorem LeanSubst.Ren.apply_empty {S : Type u1} [RenMap S []] [RenMapEmpty S] {s : S} {r : RenVec []} : s⟨r,⟩ = s

class LeanSubst.RenMapId (S : Type u1) (V : List (Type u2)) [RenMap S V] : Prop

• apply_id {s : S} : s⟨RenVec.id V,⟩ = s

@[simp]

theorem LeanSubst.Ren.apply_id {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapId S V] {s : S} : s⟨RenVec.id V,⟩ = s

@[simp]

theorem LeanSubst.Ren.apply_id1 {S : Type u1} {T : Type u2} [RenMap S [T]] [RenMapId S [T]] {s : S} : s⟨𝐫0(T)⟩ = s

@[simp]

theorem LeanSubst.Ren.apply_id2 {S : Type u1} {T1 T2 : Type u2} [RenMap S [T1, T2]] [RenMapId S [T1, T2]] {s : S} : s⟨𝐫0(T1), 𝐫0(T2)⟩ = s

class LeanSubst.RenMapCompose (S : Type u1) (V : List (Type u2)) [RenMap S V] : Prop

• apply_compose {s : S} {r1 r2 : RenVec V} : s⟨r1,⟩⟨r2,⟩ = s⟨r1 >> r2,⟩

class LeanSubst.SuffixCommuteRenRen (S : Type u1) (V : List (Type u2)) [RenMap S [S]] [RenMap S V] [RenSuffix S V] : Prop

• ren_ren {s : S} {r1 : Ren S} {r2 : RenVec V} : s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩

class LeanSubst.SuffixCommuteRenSub (S : Type u1) (V : List (Type u2)) [RenMap S [S]] [SubstMap S V] [SubstSuffix S V] : Prop

• ren_sub {s : S} {r : Ren S} {τ : SubstVec V} : s⟨r⟩[τ,] = s[τ,]⟨r⟩

class LeanSubst.SuffixCommuteSubRen (S : Type u1) (V : List (Type u2)) [SubstMap S [S]] [RenMap S V] [RenSuffix S V] : Prop

• sub_ren {s : S} {σ : Subst S} {r : RenVec V} : s[σ]⟨r,⟩ = s⟨r,⟩[σ⟨r,⟩]

theorem LeanSubst.Subst.suffix_ren_ren {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteRenRen S V] {s : S} {r1 : Ren S} {r2 : RenVec V} : s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩

theorem LeanSubst.Subst.suffix_ren_sub {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [SubstMap S V] [SubstSuffix S V] [SuffixCommuteRenSub S V] {s : S} {r : Ren S} {τ : SubstVec V} : s⟨r⟩[τ,] = s[τ,]⟨r⟩

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

@[simp]

theorem LeanSubst.Ren.apply_compose {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapCompose S V] {s : S} {r1 r2 : RenVec V} : s⟨r1,⟩⟨r2,⟩ = s⟨r1 >> r2,⟩

@[simp]

theorem LeanSubst.Ren.apply_compose1 {S : Type u1} {T : Type u2} [RenMap S [T]] [RenMapCompose S [T]] {s : S} {r1 r2 : Ren T} : s⟨r1⟩⟨r2⟩ = s⟨r1 >> r2⟩

@[simp]

theorem LeanSubst.Ren.apply_compose2 {S : Type u1} {T1 T2 : Type u2} [RenMap S [T1, T2]] [RenMapCompose S [T1, T2]] {s : S} {r1 r2 : Ren T1} {k1 k2 : Ren T2} : s⟨r1, k1⟩⟨r2, k2⟩ = s⟨r1 >> r2, k1 >> k2⟩

instance LeanSubst.instRenMapEmptyAction {S : Type u1} [RenMap S []] [RenSuffix S []] [RenMapEmpty S] : RenMapEmpty (Action S)

instance LeanSubst.instRenMapVecDefAction {T : Type u2} {V : List (Type u2)} [RenMap T [T]] [RenMap T (T :: V)] [RenMap T V] [RenSuffix T V] [RenMapVecDef T T V] : RenMapVecDef (Action T) T V

instance LeanSubst.instRenMapVecDefSubst {T : Type u2} {V : List (Type u2)} [RenMap T [T]] [RenMap T (T :: V)] [RenMap T V] [RenSuffix T V] [RenMapVecDef T T V] : RenMapVecDef (Subst T) T V

instance LeanSubst.instRenMapIdActionCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [RenMapId T (T :: V)] : RenMapId (Action T) (T :: V)

instance LeanSubst.instRenMapIdAction {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] [RenMapId S V] : RenMapId (Action S) V

instance LeanSubst.instRenMapEmptySubst {S : Type u1} [RenMap S []] [RenSuffix S []] [RenMapEmpty S] : RenMapEmpty (Subst S)

instance LeanSubst.instRenMapIdSubstCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [RenMapId T (T :: V)] : RenMapId (Subst T) (T :: V)

instance LeanSubst.instRenMapIdSubst {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] [RenMapId S V] : RenMapId (Subst S) V

instance LeanSubst.instRenMapComposeActionCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [RenMapCompose T (T :: V)] : RenMapCompose (Action T) (T :: V)

instance LeanSubst.instRenMapComposeAction {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] [RenMapCompose S V] : RenMapCompose (Action S) V

instance LeanSubst.instRenMapComposeSubstCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [RenMapCompose T (T :: V)] : RenMapCompose (Subst T) (T :: V)

instance LeanSubst.instRenMapComposeSubst {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] [RenMapCompose S V] : RenMapCompose (Subst S) V

theorem LeanSubst.Subst.suffix_ren_ren_commute_action {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteRenRen S V] {s : Action S} {r1 : Ren S} {r2 : RenVec V} : s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩

theorem LeanSubst.Subst.suffix_ren_ren_commute_subst {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [RenMap S V] [RenSuffix S V] [SuffixCommuteRenRen S V] {s : Subst S} {r1 : Ren S} {r2 : RenVec V} : s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩

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

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

theorem LeanSubst.Subst.suffix_ren_sub_commute_action {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [SubstMap S V] [SubstSuffix S V] [SuffixCommuteRenSub S V] {s : Action S} {r : Ren S} {τ : SubstVec V} : s⟨r⟩[τ,] = s[τ,]⟨r⟩

theorem LeanSubst.Subst.suffix_ren_sub_commute_subst {S : Type u1} {V : List (Type u2)} [RenMap S [S]] [SubstMap S V] [SubstSuffix S V] [SuffixCommuteRenSub S V] {s : Subst S} {r : Ren S} {τ : SubstVec V} : s⟨r⟩[τ,] = s[τ,]⟨r⟩

class LeanSubst.SubstMapStable (S : Type u1) (V : List (Type u2)) [RenMap S V] [SubstMap S V] : Prop

• apply_stable (r : RenVec V) (σ : SubstVec V) : r.to = σ → rmap r = smap σ

theorem LeanSubst.Subst.apply_stable {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [SubstMapStable S V] {r : RenVec V} {σ : SubstVec V} (h : r.to = σ) : rmap r = smap σ

class LeanSubst.SubstMapEmpty (S : Type u1) [SubstMap S []] : Prop

• apply_empty {s : S} {σ : SubstVec []} : s[σ,] = s

@[simp]

theorem LeanSubst.Subst.apply_empty {S : Type u1} [SubstMap S []] [SubstMapEmpty S] {s : S} {σ : SubstVec []} : s[σ,] = s

class LeanSubst.SubstMapVecDef (S : Type u1) (T : Type u2) (V : List (Type u2)) [SubstMap S [T]] [SubstMap S (T :: V)] [SubstMap S V] : Prop

• apply_vecdef {s : S} {σ : SubstVec (T :: V)} : s[σ,] = s[σ.snd,][σ.fst]

theorem LeanSubst.Subst.apply_vecdef {S : Type u1} {T : Type u2} {V : List (Type u2)} [SubstMap S [T]] [SubstMap S (T :: V)] [SubstMap S V] [SubstMapVecDef S T V] {s : S} {σ : SubstVec (T :: V)} : s[σ,] = s[σ.snd,][σ.fst]

class LeanSubst.SubstMapId (S : Type u1) (V : List (Type u2)) [SubstMap S V] : Prop

• apply_id {s : S} : s[SubstVec.id V,] = s

@[simp]

theorem LeanSubst.Subst.apply_id {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstMapId S V] {s : S} : s[SubstVec.id V,] = s

@[simp]

theorem LeanSubst.Subst.apply_id1 {S : Type u1} {T : Type u2} [SubstMap S [T]] [SubstMapId S [T]] {s : S} : s[𝐬0(T)] = s

@[simp]

theorem LeanSubst.Subst.apply_id2 {S : Type u1} {T1 T2 : Type u2} [SubstMap S [T1, T2]] [SubstMapId S [T1, T2]] {s : S} : s[𝐬0(T1), 𝐬0(T2)] = s

class LeanSubst.SubstMapRenComposeLeft (S : Type u1) (V : List (Type u2)) [RenMap S V] [SubstMap S V] : Prop

• apply_ren_compose_left {s : S} {r : RenVec V} {τ : SubstVec V} : s⟨r,⟩[τ,] = s[r >> τ,]

@[simp]

theorem LeanSubst.Subst.apply_ren_compose_left {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [SubstMapRenComposeLeft S V] {s : S} {r : RenVec V} {σ : SubstVec V} : s⟨r,⟩[σ,] = s[r >> σ,]

@[simp]

theorem LeanSubst.Subst.apply_ren_compose_left1 {S : Type u1} {T : Type u2} [RenMap S [T]] [SubstMap S [T]] [SubstMapRenComposeLeft S [T]] {s : S} {r : Ren T} {σ : Subst T} : s⟨r⟩[σ] = s[r >> σ]

@[simp]

theorem LeanSubst.Subst.apply_ren_compose_left2 {S : Type u1} {T1 T2 : Type u2} [RenMap S [T1, T2]] [SubstMap S [T1, T2]] [SubstMapRenComposeLeft S [T1, T2]] {s : S} {r1 : Ren T1} {r2 : Ren T2} {σ1 : Subst T1} {σ2 : Subst T2} : s⟨r1, r2⟩[σ1, σ2] = s[r1 >> σ1, r2 >> σ2]

class LeanSubst.SubstMapRenComposeRight (S : Type u1) (V : List (Type u2)) [RenMap S V] [RenMapAll V] [SubstMap S V] : Prop

• apply_ren_compose_right {s : S} {r : RenVec V} {σ : SubstVec V} : s[σ,]⟨r,⟩ = s[σ >> r,]

@[simp]

theorem LeanSubst.Subst.apply_ren_compose_right {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapAll V] [SubstMap S V] [SubstMapRenComposeRight S V] {s : S} {r : RenVec V} {σ : SubstVec V} : s[σ,]⟨r,⟩ = s[σ >> r,]

class LeanSubst.SubstMapCompose (S : Type u1) (V : List (Type u2)) [SubstMap S V] [SubstMapAll V] : Prop

• apply_compose {s : S} {σ τ : SubstVec V} : s[σ,][τ,] = s[σ >> τ,]

@[simp]

theorem LeanSubst.Subst.apply_compose {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstMapAll V] [SubstMapCompose S V] {s : S} {σ1 σ2 : SubstVec V} : s[σ1,][σ2,] = s[σ1 >> σ2,]

instance LeanSubst.instSubstMapEmptyAction {S : Type u1} [SubstMap S []] [SubstSuffix S []] [SubstMapEmpty S] : SubstMapEmpty (Action S)

instance LeanSubst.instSubstMapVecDefAction {T : Type u2} {V : List (Type u2)} [SubstMap T [T]] [SubstMap T (T :: V)] [SubstMap T V] [SubstSuffix T V] [SubstMapVecDef T T V] : SubstMapVecDef (Action T) T V

instance LeanSubst.instSubstMapVecDefSubst {T : Type u2} {V : List (Type u2)} [SubstMap T [T]] [SubstMap T (T :: V)] [SubstMap T V] [SubstSuffix T V] [SubstMapVecDef T T V] : SubstMapVecDef (Subst T) T V

instance LeanSubst.instSubstMapIdActionCons {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] [SubstMapId T (T :: V)] : SubstMapId (Action T) (T :: V)

instance LeanSubst.instSubstMapIdAction {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] [SubstMapId S V] : SubstMapId (Action S) V

instance LeanSubst.instSubstMapEmptySubst {S : Type u1} [SubstMap S []] [SubstSuffix S []] [SubstMapEmpty S] : SubstMapEmpty (Subst S)

instance LeanSubst.instSubstMapIdSubstCons {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] [SubstMapId T (T :: V)] : SubstMapId (Subst T) (T :: V)

instance LeanSubst.instSubstMapIdSubst {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] [SubstMapId S V] : SubstMapId (Subst S) V

instance LeanSubst.instSubstMapRenComposeLeftActionCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [SubstMap T (T :: V)] [SubstMapRenComposeLeft T (T :: V)] : SubstMapRenComposeLeft (Action T) (T :: V)

instance LeanSubst.instSubstMapRenComposeLeftAction {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [RenSuffix S V] [SubstSuffix S V] [SubstMapRenComposeLeft S V] : SubstMapRenComposeLeft (Action S) V

instance LeanSubst.instSubstMapRenComposeRightActionConsOfRenMapVecDef {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [RenMapAll (T :: V)] [SubstMap T (T :: V)] [RenMapVecDef T T V] [SubstMapRenComposeRight T (T :: V)] : SubstMapRenComposeRight (Action T) (T :: V)

instance LeanSubst.instSubstMapRenComposeRightAction {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapAll V] [SubstMap S V] [RenSuffix S V] [SubstSuffix S V] [SubstMapRenComposeRight S V] : SubstMapRenComposeRight (Action S) V

instance LeanSubst.instSubstMapComposeActionConsOfSubstMapVecDef {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] [i : SubstMapAll (T :: V)] [SubstMapCompose T (T :: V)] [SubstMapVecDef T T V] : SubstMapCompose (Action T) (T :: V)

instance LeanSubst.instSubstMapComposeAction {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] [SubstMapAll V] [SubstMapCompose S V] : SubstMapCompose (Action S) V

instance LeanSubst.instSubstMapRenComposeLeftSubstCons {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [SubstMap T (T :: V)] [SubstMapRenComposeLeft T (T :: V)] : SubstMapRenComposeLeft (Subst T) (T :: V)

instance LeanSubst.instSubstMapRenComposeLeftSubst {S : Type u1} {V : List (Type u2)} [RenMap S V] [SubstMap S V] [RenSuffix S V] [SubstSuffix S V] [SubstMapRenComposeLeft S V] : SubstMapRenComposeLeft (Subst S) V

instance LeanSubst.instSubstMapRenComposeRightSubstConsOfRenMapVecDef {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] [inst : RenMapAll (T :: V)] [SubstMap T (T :: V)] [RenMapVecDef T T V] [SubstMapRenComposeRight T (T :: V)] : SubstMapRenComposeRight (Subst T) (T :: V)

instance LeanSubst.instSubstMapRenComposeRightSubst {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenMapAll V] [SubstMap S V] [RenSuffix S V] [SubstSuffix S V] [SubstMapRenComposeRight S V] : SubstMapRenComposeRight (Subst S) V

theorem LeanSubst.Subst.apply_compose_lemma {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] [SubstMapAll (T :: V)] [SubstMapCompose T (T :: V)] [SubstMapVecDef T T V] {s : Subst T} {σ τ : SubstVec (T :: V)} : s[σ,][τ,] = s[σ >> τ,]

instance LeanSubst.instSubstMapComposeSubstConsOfSubstMapVecDef {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] [SubstMapAll (T :: V)] [SubstMapCompose T (T :: V)] [SubstMapVecDef T T V] : SubstMapCompose (Subst T) (T :: V)

instance LeanSubst.instSubstMapComposeSubst {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] [SubstMapAll V] [SubstMapCompose S V] : SubstMapCompose (Subst S) V