Documentation

LeanSubst.Expanded

source
@[simp]
theorem LeanSubst.RenVec.proj_eta {T : Type u2} {V : List (Type u2)} {r : RenVec (T :: V)} :
(r.fst, r.snd) = r
source
theorem LeanSubst.RenVec.proj_eta1 {T1 : Type u2} {r : RenVec [T1]} :
(r.fst, nil) = r
source
@[simp]
theorem LeanSubst.SubstVec.proj_eta {T : Type u2} {V : List (Type u2)} (σ : SubstVec (T :: V)) :
(σ.fst, σ.snd) = σ
source
theorem LeanSubst.SubstVec.proj_eta1 {T1 : Type u2} {σ : SubstVec [T1]} :
(σ.fst, nil) = σ
source
@[simp]
theorem LeanSubst.RenVec.lift_size1_0 {T1 : Type u2} {r : RenVec [T1]} :
r.lift [0] = r
source
@[simp]
theorem LeanSubst.SubstVec.lift_size1_0 {T1 : Type u2} [RenMapAll [T1]] [RenMapId T1 [T1]] {σ : SubstVec [T1]} :
lift [0] σ = σ
source
@[simp]
theorem LeanSubst.RenVec.compose_components1 {T1 : Type u2} {r1 k1 : Ren T1} :
(r1, nil) >> (k1, nil) = (r1 >> k1, nil)
source
@[simp]
theorem LeanSubst.RenVec.compose_components2 {T1 T2 : Type u2} {r1 k1 : Ren T1} {r2 k2 : Ren T2} :
(r1, r2, nil) >> (k1, k2, nil) = (r1 >> k1, r2 >> k2, nil)
source
@[simp]
theorem LeanSubst.RenVec.compose_components3 {T1 T2 T3 : Type u2} {r1 k1 : Ren T1} {r2 k2 : Ren T2} {r3 k3 : Ren T3} :
(r1, r2, r3, nil) >> (k1, k2, k3, nil) = (r1 >> k1, r2 >> k2, r3 >> k3, nil)
source
@[simp]
theorem LeanSubst.RenVec.compose_components4 {T1 T2 T3 T4 : Type u2} {r1 k1 : Ren T1} {r2 k2 : Ren T2} {r3 k3 : Ren T3} {r4 k4 : Ren T4} :
(r1, r2, r3, r4, nil) >> (k1, k2, k3, k4, nil) = (r1 >> k1, r2 >> k2, r3 >> k3, r4 >> k4, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_left_proj {T : Type u2} {V : List (Type u2)} {r1 : Ren T} {r2 : RenVec V} {τ1 : Subst T} {τ2 : SubstVec V} :
(r1, r2) >> (τ1, τ2) = (r1 >> τ1, r2 >> τ2)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_right_proj {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ1 : Subst T} {σ2 : SubstVec V} {r1 : Ren T} {r2 : RenVec V} :
(σ1, σ2) >> (r1, r2) = (σ1⟨r2,⟩ >> r1, σ2 >> r2)
source
@[simp]
theorem LeanSubst.SubstVec.compose_proj {T : Type u2} {V : List (Type u2)} [SubstMapAll (T :: V)] {σ1 τ1 : Subst T} {σ2 τ2 : SubstVec V} :
(σ1, σ2) >> (τ1, τ2) = (σ1[τ2,] >> τ1, σ2 >> τ2)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_left_components {T1 : Type u2} {r1 : Ren T1} {τ1 : Subst T1} :
(r1, RenVec.nil) >> (τ1, nil) = (r1 >> τ1, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_left_components2 {T1 T2 : Type u2} {r1 : Ren T1} {τ1 : Subst T1} {r2 : Ren T2} {τ2 : Subst T2} :
(r1, r2, RenVec.nil) >> (τ1, τ2, nil) = (r1 >> τ1, r2 >> τ2, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_left_components3 {T1 T2 T3 : Type u2} {r1 : Ren T1} {τ1 : Subst T1} {r2 : Ren T2} {τ2 : Subst T2} {r3 : Ren T3} {τ3 : Subst T3} :
(r1, r2, r3, RenVec.nil) >> (τ1, τ2, τ3, nil) = (r1 >> τ1, r2 >> τ2, r3 >> τ3, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_left_components4 {T1 T2 T3 T4 : Type u2} {r1 : Ren T1} {τ1 : Subst T1} {r2 : Ren T2} {τ2 : Subst T2} {r3 : Ren T3} {τ3 : Subst T3} {r4 : Ren T4} {τ4 : Subst T4} :
(r1, r2, r3, r4, RenVec.nil) >> (τ1, τ2, τ3, τ4, nil) = (r1 >> τ1, r2 >> τ2, r3 >> τ3, r4 >> τ4, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_right_components1 {T1 : Type u2} [RenMapAll [T1]] [RenMapEmpty T1] {σ1 : Subst T1} {r1 : Ren T1} :
(σ1, nil) >> (r1, RenVec.nil) = (σ1 >> r1, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_right_components2 {T1 T2 : Type u2} [RenMapAll [T1, T2]] [RenMapEmpty T2] {σ1 : Subst T1} {r1 : Ren T1} {σ2 : Subst T2} {r2 : Ren T2} :
(σ1, σ2, nil) >> (r1, r2, RenVec.nil) = (σ1⟨r2⟩ >> r1, σ2 >> r2, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_right_components3 {T1 T2 T3 : Type u2} [RenMapAll [T1, T2, T3]] [RenMapEmpty T3] {σ1 : Subst T1} {r1 : Ren T1} {σ2 : Subst T2} {r2 : Ren T2} {σ3 : Subst T3} {r3 : Ren T3} :
(σ1, σ2, σ3, nil) >> (r1, r2, r3, RenVec.nil) = (σ1⟨r2, r3⟩ >> r1, σ2⟨r3⟩ >> r2, σ3 >> r3, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_ren_right_components4 {T1 T2 T3 T4 : Type u2} [RenMapAll [T1, T2, T3, T4]] [RenMapEmpty T4] {σ1 : Subst T1} {r1 : Ren T1} {σ2 : Subst T2} {r2 : Ren T2} {σ3 : Subst T3} {r3 : Ren T3} {σ4 : Subst T4} {r4 : Ren T4} :
(σ1, σ2, σ3, σ4, nil) >> (r1, r2, r3, r4, RenVec.nil) = (σ1⟨r2, r3, r4⟩ >> r1, σ2⟨r3, r4⟩ >> r2, σ3⟨r4⟩ >> r3, σ4 >> r4, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_components1 {T1 : Type u2} [SubstMapAll [T1]] [SubstMapEmpty T1] {σ1 τ1 : Subst T1} :
(σ1, nil) >> (τ1, nil) = (σ1 >> τ1, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_components2 {T1 T2 : Type u2} [SubstMapAll [T1, T2]] [SubstMapEmpty T2] {σ1 τ1 : Subst T1} {σ2 τ2 : Subst T2} :
(σ1, σ2, nil) >> (τ1, τ2, nil) = (σ1[(τ2, nil),] >> τ1, σ2 >> τ2, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_components3 {T1 T2 T3 : Type u2} [SubstMapAll [T1, T2, T3]] [SubstMapEmpty T3] {σ1 τ1 : Subst T1} {σ2 τ2 : Subst T2} {σ3 τ3 : Subst T3} :
(σ1, σ2, σ3, nil) >> (τ1, τ2, τ3, nil) = (σ1[(τ2, τ3, nil),] >> τ1, σ2[(τ3, nil),] >> τ2, σ3 >> τ3, nil)
source
@[simp]
theorem LeanSubst.SubstVec.compose_components4 {T1 T2 T3 T4 : Type u2} [SubstMapAll [T1, T2, T3, T4]] [SubstMapEmpty T4] {σ1 τ1 : Subst T1} {σ2 τ2 : Subst T2} {σ3 τ3 : Subst T3} {σ4 τ4 : Subst T4} :
(σ1, σ2, σ3, σ4, nil) >> (τ1, τ2, τ3, τ4, nil) = (σ1[(τ2, τ3, τ4, nil),] >> τ1, σ2[(τ3, τ4, nil),] >> τ2, σ3[(τ4, nil),] >> τ3, σ4 >> τ4, nil)