@[simp]

theorem LeanSubst.RenVec.normalize_unit : RenUnit.unit = nil

@[simp]

theorem LeanSubst.SubstVec.normalize_unit : SubstUnit.unit = nil

@[reducible]

instance LeanSubst.instRenMapConsNilOfRenMapAll {T : Type u2} {V : List (Type u2)} [i : RenMapAll (T :: V)] : RenMap T [T]

Equations

• LeanSubst.instRenMapConsNilOfRenMapAll = { rmap := LeanSubst.rmap }

@[reducible]

instance LeanSubst.instRenMapOfRenMapAllCons {T : Type u2} {V : List (Type u2)} [i : RenMapAll (T :: V)] : RenMap T V

Equations

• LeanSubst.instRenMapOfRenMapAllCons = { rmap := LeanSubst.rmap }

@[reducible]

instance LeanSubst.instRenSuffixOfRenMapAllCons {T : Type u2} {V : List (Type u2)} [i : RenMapAll (T :: V)] : RenSuffix T V

Equations

• LeanSubst.instRenSuffixOfRenMapAllCons = inst_1

@[reducible]

instance LeanSubst.instRenMapAllOfCons {T : Type u2} {V : List (Type u2)} [i : RenMapAll (T :: V)] : RenMapAll V

Equations

• LeanSubst.instRenMapAllOfCons = a

@[reducible]

instance LeanSubst.instSubstMapConsNilOfSubstMapAll {T : Type u2} {V : List (Type u2)} [i : SubstMapAll (T :: V)] : SubstMap T [T]

Equations

• LeanSubst.instSubstMapConsNilOfSubstMapAll = { smap := LeanSubst.smap }

@[reducible]

instance LeanSubst.instSubstMapOfSubstMapAllCons {T : Type u2} {V : List (Type u2)} [i : SubstMapAll (T :: V)] : SubstMap T V

Equations

• LeanSubst.instSubstMapOfSubstMapAllCons = { smap := LeanSubst.smap }

@[reducible]

instance LeanSubst.instSubstSuffixOfSubstMapAllCons {T : Type u2} {V : List (Type u2)} [i : SubstMapAll (T :: V)] : SubstSuffix T V

Equations

• LeanSubst.instSubstSuffixOfSubstMapAllCons = inst_1

@[reducible]

instance LeanSubst.instSubstMapAllOfCons {T : Type u2} {V : List (Type u2)} [i : SubstMapAll (T :: V)] : SubstMapAll V

Equations

• LeanSubst.instSubstMapAllOfCons = a

@[simp]

theorem LeanSubst.Subst.act_inner {T : Type u2} {f : Nat → Action T} {x : Nat} : { inner := f }.act x = f x

def LeanSubst.Action.rmap1 {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] (r : RenVec (T :: V)) : Action T → Action T

Equations

• LeanSubst.Action.rmap1 r (LeanSubst.re x_1) = LeanSubst.re (r.fst.act x_1)
• LeanSubst.Action.rmap1 r (LeanSubst.su t) = LeanSubst.su t⟨r,⟩

@[instance_reducible]

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

Equations

• LeanSubst.instRenMapActionCons = { rmap := fun (v : LeanSubst.RenVec (T :: V)) => LeanSubst.Action.rmap1 v }

@[simp]

theorem LeanSubst.Action.rmap1_re {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] {r : RenVec (T :: V)} {x : Var T} : (re x)⟨r,⟩ = re (r.fst.act x)

@[simp]

theorem LeanSubst.Action.rmap1_su {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] {r : RenVec (T :: V)} {t : T} : (su t)⟨r,⟩ = su t⟨r,⟩

def LeanSubst.Action.rmap0 {S : Type u1} {V : List (Type u2)} [RenMap S V] (r : RenVec V) : Action S → Action S

Equations

• LeanSubst.Action.rmap0 r (LeanSubst.re x_1) = LeanSubst.re x_1
• LeanSubst.Action.rmap0 r (LeanSubst.su t) = LeanSubst.su t⟨r,⟩

@[instance_reducible]

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

Equations

• LeanSubst.instRenMapActionOfRenSuffix = { rmap := LeanSubst.Action.rmap0 }

@[simp]

theorem LeanSubst.Action.rmap0_re {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] {r : RenVec V} {x : Var S} : (re x)⟨r,⟩ = re x

@[simp]

theorem LeanSubst.Action.rmap0_su {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] {r : RenVec V} {t : S} : (su t)⟨r,⟩ = su t⟨r,⟩

def LeanSubst.Action.smap1 {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] (σ : SubstVec (T :: V)) : Action T → Action T

Equations

• LeanSubst.Action.smap1 σ (LeanSubst.re x_1) = σ.fst.act x_1
• LeanSubst.Action.smap1 σ (LeanSubst.su t) = LeanSubst.su t[σ,]

@[instance_reducible]

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

Equations

• LeanSubst.instSubstMapActionCons = { smap := fun (v : LeanSubst.SubstVec (T :: V)) => LeanSubst.Action.smap1 v }

@[simp]

theorem LeanSubst.Action.smap1_re {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] {σ : SubstVec (T :: V)} {x : Nat} : (re x)[σ,] = σ.fst.act x

@[simp]

theorem LeanSubst.Action.smap1_su {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] {σ : SubstVec (T :: V)} {t : T} : (su t)[σ,] = su t[σ,]

def LeanSubst.Action.smap0 {S : Type u1} {V : List (Type u2)} [SubstMap S V] (σ : SubstVec V) : Action S → Action S

Equations

• LeanSubst.Action.smap0 σ (LeanSubst.re x_1) = LeanSubst.re x_1
• LeanSubst.Action.smap0 σ (LeanSubst.su t) = LeanSubst.su t[σ,]

@[instance_reducible]

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

Equations

• LeanSubst.instSubstMapActionOfSubstSuffix = { smap := LeanSubst.Action.smap0 }

@[simp]

theorem LeanSubst.Action.smap0_re {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] {σ : SubstVec V} {x : Var S} : (re x)[σ,] = re x

@[simp]

theorem LeanSubst.Action.smap0_su {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] {σ : SubstVec V} {t : S} : (su t)[σ,] = su t[σ,]

def LeanSubst.Subst.rmap0 {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] (r : RenVec (T :: V)) (σ : Subst T) : Subst T

Equations

• LeanSubst.Subst.rmap0 r σ = { inner := fun (n : Nat) => (σ.act n)⟨r,⟩ }

@[instance_reducible]

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

Equations

• LeanSubst.instRenMapSubstCons = { rmap := LeanSubst.Subst.rmap0 }

@[simp]

theorem LeanSubst.Subst.rmap0_simp {T : Type u2} {V : List (Type u2)} [RenMap T (T :: V)] {r : RenVec (T :: V)} {σ : Subst T} {n : Nat} : (σ.act n)⟨r,⟩ = σ⟨r,⟩.act n

def LeanSubst.Subst.rmap1 {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] (r : RenVec V) (σ : Subst S) : Subst S

Equations

• LeanSubst.Subst.rmap1 r σ = { inner := fun (n : Nat) => (σ.act n)⟨r,⟩ }

@[instance_reducible]

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

Equations

• LeanSubst.instRenMapSubstOfRenSuffix = { rmap := LeanSubst.Subst.rmap1 }

@[simp]

theorem LeanSubst.Subst.rmap1_simp {S : Type u1} {V : List (Type u2)} [RenMap S V] [RenSuffix S V] {r : RenVec V} {σ : Subst S} {n : Nat} : (σ.act n)⟨r,⟩ = σ⟨r,⟩.act n

def LeanSubst.Subst.smap0 {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] (τ : SubstVec (T :: V)) (σ : Subst T) : Subst T

Equations

• LeanSubst.Subst.smap0 τ σ = { inner := fun (n : Nat) => (σ.act n)[τ,] }

@[instance_reducible]

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

Equations

• LeanSubst.instSubstMapSubstCons = { smap := LeanSubst.Subst.smap0 }

@[simp]

theorem LeanSubst.Subst.smap0_simp {T : Type u2} {V : List (Type u2)} [SubstMap T (T :: V)] {τ : SubstVec (T :: V)} {σ : Subst T} {n : Nat} : (σ.act n)[τ,] = σ[τ,].act n

def LeanSubst.Subst.smap1 {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] (τ : SubstVec V) (σ : Subst S) : Subst S

Equations

• LeanSubst.Subst.smap1 τ σ = { inner := fun (n : Nat) => (σ.act n)[τ,] }

@[instance_reducible]

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

Equations

• LeanSubst.instSubstMapSubstOfSubstSuffix = { smap := LeanSubst.Subst.smap1 }

@[simp]

theorem LeanSubst.Subst.smap1_simp {S : Type u1} {V : List (Type u2)} [SubstMap S V] [SubstSuffix S V] {τ : SubstVec V} {σ : Subst S} {n : Nat} : (σ.act n)[τ,] = σ[τ,].act n

def LeanSubst.Ren.id (T : Type u_1) : Ren T

Equations

• 𝐫0(T) = { act := fun (x : Nat) => x }

def LeanSubst.«term𝐫0» : Lean.ParserDescr

Equations

• LeanSubst.«term𝐫0» = Lean.ParserDescr.node `LeanSubst.«term𝐫0» 1024 (Lean.ParserDescr.symbol "𝐫0")

def LeanSubst.«term𝐫0(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Ren.id_action {T : Type u2} {x : Nat} : 𝐫0(T).act x = x

@[reducible]

def LeanSubst.RenVec.id (V : List (Type u2)) : RenVec V

Equations

• LeanSubst.RenVec.id [] = LeanSubst.RenVec.nil
• LeanSubst.RenVec.id (x_1 :: xs) = (𝐫0(x_1), LeanSubst.RenVec.id xs)

def LeanSubst.Subst.id (T : Type u_1) : Subst T

Equations

• 𝐬0(T) = { inner := fun (x : Nat) => LeanSubst.re x }

def LeanSubst.«term𝐬0» : Lean.ParserDescr

Equations

• LeanSubst.«term𝐬0» = Lean.ParserDescr.node `LeanSubst.«term𝐬0» 1024 (Lean.ParserDescr.symbol "𝐬0")

def LeanSubst.«term𝐬0(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Subst.id_action {T : Type u2} {x : Nat} : 𝐬0(T).act x = re x

@[reducible]

def LeanSubst.SubstVec.id (V : List (Type u2)) : SubstVec V

Equations

• LeanSubst.SubstVec.id [] = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.id (x_1 :: xs) = (𝐬0(x_1), LeanSubst.SubstVec.id xs)

def LeanSubst.Ren.succ (T : Type u_1) : Ren T

Equations

• 𝐫1(T) = { act := fun (x : Nat) => x + 1 }

def LeanSubst.«term𝐫1» : Lean.ParserDescr

Equations

• LeanSubst.«term𝐫1» = Lean.ParserDescr.node `LeanSubst.«term𝐫1» 1024 (Lean.ParserDescr.symbol "𝐫1")

def LeanSubst.«term𝐫1(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Ren.succ_action {T : Type u2} {x : Nat} : 𝐫1(T).act x = x + 1

def LeanSubst.Subst.succ (T : Type u_1) : Subst T

Equations

• 𝐬1(T) = { inner := fun (x : Nat) => LeanSubst.re (x + 1) }

def LeanSubst.«term𝐬1» : Lean.ParserDescr

Equations

• LeanSubst.«term𝐬1» = Lean.ParserDescr.node `LeanSubst.«term𝐬1» 1024 (Lean.ParserDescr.symbol "𝐬1")

def LeanSubst.«term𝐬1(_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Subst.succ_action {T : Type u2} {x : Nat} : 𝐬1(T).act x = re (x + 1)

def LeanSubst.Ren.pred (T : Type u_1) : Ren T

Equations

• LeanSubst.Ren.pred T = { act := fun (x : Nat) => x - 1 }

@[simp]

theorem LeanSubst.Ren.pred_action {T : Type u2} {x : Nat} : (pred T).act x = x - 1

def LeanSubst.Subst.pred (T : Type u_1) : Subst T

Equations

• LeanSubst.Subst.pred T = { inner := fun (x : Nat) => LeanSubst.re (x - 1) }

@[simp]

theorem LeanSubst.Subst.pred_action {T : Type u2} {x : Nat} : (pred T).act x = re (x - 1)

def LeanSubst.Ren.add (T : Type u_1) (k : Nat) : Ren T

Equations

• LeanSubst.Ren.add T k = { act := fun (x : Nat) => x + k }

@[simp]

theorem LeanSubst.Ren.add_action {T : Type u2} {k x : Nat} : (add T k).act x = x + k

@[simp]

theorem LeanSubst.Ren.add_zero {T : Type u2} : add T 0 = 𝐫0(T)

@[simp]

theorem LeanSubst.Ren.add_one {T : Type u2} : add T 1 = 𝐫1(T)

def LeanSubst.Subst.add (T : Type u_1) (k : Nat) : Subst T

Equations

• LeanSubst.Subst.add T k = { inner := fun (x : Nat) => LeanSubst.re (x + k) }

@[simp]

theorem LeanSubst.Subst.add_action {T : Type u2} {k x : Nat} : (add T k).act x = re (x + k)

@[simp]

theorem LeanSubst.Subst.add_zero {T : Type u2} : add T 0 = 𝐬0(T)

@[simp]

theorem LeanSubst.Subst.add_one {T : Type u2} : add T 1 = 𝐬1(T)

def LeanSubst.Ren.sub (T : Type u_1) (k : Nat) : Ren T

Equations

• LeanSubst.Ren.sub T k = { act := fun (x : Nat) => x - k }

@[simp]

theorem LeanSubst.Ren.sub_action {T : Type u2} {k x : Nat} : (sub T k).act x = x - k

@[simp]

theorem LeanSubst.Ren.sub_zero {T : Type u2} : sub T 0 = 𝐫0(T)

@[simp]

theorem LeanSubst.Ren.sub_one {T : Type u2} : sub T 1 = pred T

def LeanSubst.Subst.sub (T : Type u_1) (k : Nat) : Subst T

Equations

• LeanSubst.Subst.sub T k = { inner := fun (x : Nat) => LeanSubst.re (x - k) }

@[simp]

theorem LeanSubst.Subst.sub_action {T : Type u2} {k x : Nat} : (sub T k).act x = re (x - k)

@[simp]

theorem LeanSubst.Subst.sub_zero {T : Type u2} : sub T 0 = 𝐬0(T)

@[simp]

theorem LeanSubst.Subst.sub_one {T : Type u2} : sub T 1 = pred T

def LeanSubst.Ren.cons {T : Type u2} (a : Nat) (r : Ren T) : Ren T

Equations

• a :: r = { act := fun (n : Nat) => match n with | 0 => a | n.succ => r.act n }

def LeanSubst.Ren.cons_notation : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Ren.cons_action0 {T : Type u2} {a : Nat} {r : Ren T} : (a :: r).act 0 = a

@[simp]

theorem LeanSubst.Ren.cons_action {T : Type u2} {a i : Nat} {r : Ren T} : (a :: r).act (i + 1) = r.act i

@[simp]

theorem LeanSubst.Ren.cons_add {T : Type u_1} {n : Nat} : n :: add T (n + 1) = add T n

def LeanSubst.Subst.cons {T : Type u2} (a : Action T) (σ : Subst T) : Subst T

Equations

• a :: σ = { inner := fun (n : Nat) => match n with | 0 => a | n.succ => σ.act n }

def LeanSubst.Subst.cons_notation : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LeanSubst.Subst.cons_action0 {T : Type u2} {a : Action T} {σ : Subst T} : (a :: σ).act 0 = a

@[simp]

theorem LeanSubst.Subst.cons_action {T : Type u2} {a : Action T} {i : Nat} {σ : Subst T} : (a :: σ).act (i + 1) = σ.act i

def LeanSubst.Ren.append {T : Type u2} : List Nat → Ren T → Ren T

Equations

• LeanSubst.Ren.append [] x✝ = x✝
• LeanSubst.Ren.append (hd :: tl) x✝ = hd :: LeanSubst.Ren.append tl x✝

@[instance_reducible]

instance LeanSubst.instHAppendListNatRen {T : Type u2} : HAppend (List Nat) (Ren T) (Ren T)

Equations

• LeanSubst.instHAppendListNatRen = { hAppend := LeanSubst.Ren.append }

@[simp]

theorem LeanSubst.Ren.append_nil {T : Type u2} {r : Ren T} : [] ++ r = r

@[simp]

theorem LeanSubst.Ren.append_cons {T : Type u2} {a : Nat} {ℓ : List Nat} {r : Ren T} : a :: ℓ ++ r = a :: (ℓ ++ r)

@[simp]

theorem LeanSubst.Ren.append_action_lt {T : Type u2} {r : Ren T} {i : Nat} {ℓ : List Nat} (h : i < ℓ.length) : (ℓ ++ r).act i = ℓ[i]

@[simp]

theorem LeanSubst.Ren.append_action_ge {T : Type u2} {r : Ren T} {i : Nat} {ℓ : List Nat} (h : i ≥ ℓ.length) : (ℓ ++ r).act i = r.act (i - ℓ.length)

def LeanSubst.Subst.append {T : Type u2} : List (Action T) → Subst T → Subst T

Equations

• LeanSubst.Subst.append [] x✝ = x✝
• LeanSubst.Subst.append (hd :: tl) x✝ = hd :: LeanSubst.Subst.append tl x✝

@[instance_reducible]

instance LeanSubst.instHAppendListActionSubst {T : Type u2} : HAppend (List (Action T)) (Subst T) (Subst T)

Equations

• LeanSubst.instHAppendListActionSubst = { hAppend := LeanSubst.Subst.append }

@[simp]

theorem LeanSubst.Subst.append_nil {T : Type u2} {σ : Subst T} : [] ++ σ = σ

@[simp]

theorem LeanSubst.Subst.append_cons {T : Type u2} {a : Action T} {ℓ : List (Action T)} {σ : Subst T} : a :: ℓ ++ σ = a :: (ℓ ++ σ)

@[simp]

theorem LeanSubst.Subst.append_action_lt {T : Type u2} {σ : Subst T} {i : Nat} {ℓ : List (Action T)} (h : i < ℓ.length) : (ℓ ++ σ).act i = ℓ[i]

@[simp]

theorem LeanSubst.Subst.append_action_ge {T : Type u2} {σ : Subst T} {i : Nat} {ℓ : List (Action T)} (h : i ≥ ℓ.length) : (ℓ ++ σ).act i = σ.act (i - ℓ.length)

def LeanSubst.Subst.append_ren {T : Type u2} : List Nat → Subst T → Subst T

Equations

• LeanSubst.Subst.append_ren [] x✝ = x✝
• LeanSubst.Subst.append_ren (hd :: tl) x✝ = LeanSubst.re hd :: LeanSubst.Subst.append_ren tl x✝

@[instance_reducible]

instance LeanSubst.instHAppendListNatSubst {T : Type u2} : HAppend (List Nat) (Subst T) (Subst T)

Equations

• LeanSubst.instHAppendListNatSubst = { hAppend := LeanSubst.Subst.append_ren }

@[simp]

theorem LeanSubst.Subst.append_ren_nil {T : Type u2} {σ : Subst T} : [] ++ σ = σ

@[simp]

theorem LeanSubst.Subst.append_ren_cons {T : Type u2} {a : Nat} {ℓ : List Nat} {σ : Subst T} : a :: ℓ ++ σ = re a :: (ℓ ++ σ)

@[simp]

theorem LeanSubst.Subst.append_ren_action_lt {T : Type u2} {σ : Subst T} {i : Nat} {ℓ : List Nat} (h : i < ℓ.length) : (ℓ ++ σ).act i = re ℓ[i]

@[simp]

theorem LeanSubst.Subst.append_ren_action_ge {T : Type u2} {σ : Subst T} {i : Nat} {ℓ : List Nat} (h : i ≥ ℓ.length) : (ℓ ++ σ).act i = σ.act (i - ℓ.length)

def LeanSubst.Ren.compose {T : Type u2} : Ren T → Ren T → Ren T

Equations

• x✝¹.compose x✝ = { act := fun (n : Nat) => x✝.act (x✝¹.act n) }

@[instance_reducible]

instance LeanSubst.instAndThenRen {T : Type u2} : AndThen (Ren T)

Equations

• LeanSubst.instAndThenRen = { andThen := fun (r : LeanSubst.Ren T) (f : Unit → LeanSubst.Ren T) => r.compose (f ()) }

def LeanSubst.RenVec.compose {V : List (Type u2)} : RenVec V → RenVec V → RenVec V

Equations

• x_3.compose x_4 = LeanSubst.RenVec.nil
• LeanSubst.RenVec.compose (v1, v1s) (v2, v2s) = (v1 >> v2, v1s.compose v2s)

@[instance_reducible]

instance LeanSubst.instAndThenRenVec {V : List (Type u2)} : AndThen (RenVec V)

Equations

• LeanSubst.instAndThenRenVec = { andThen := fun (r : LeanSubst.RenVec V) (f : Unit → LeanSubst.RenVec V) => r.compose (f ()) }

@[simp]

theorem LeanSubst.RenVec.compose_proj1 {T : Type u2} {V : List (Type u2)} {σ τ : RenVec (T :: V)} : (σ >> τ).fst = σ.fst >> τ.fst

@[simp]

theorem LeanSubst.RenVec.compose_proj2 {T : Type u2} {V : List (Type u2)} {σ τ : RenVec (T :: V)} : (σ >> τ).snd = σ.snd >> τ.snd

@[simp]

theorem LeanSubst.Ren.compose_action {T : Type u2} {r1 r2 : Ren T} {x : Nat} : (r1 >> r2).act x = r2.act (r1.act x)

@[simp]

theorem LeanSubst.Ren.compose_id_left {T : Type u2} {r : Ren T} : 𝐫0(T) >> r = r

@[simp]

theorem LeanSubst.Ren.compose_id_right {T : Type u2} {r : Ren T} : r >> 𝐫0(T) = r

@[simp]

theorem LeanSubst.Ren.compose_assoc {T : Type u2} {r1 r2 r3 : Ren T} : (r1 >> r2) >> r3 = r1 >> r2 >> r3

@[simp]

theorem LeanSubst.Ren.compose_pred_succ {T : Type u2} : 𝐫1(T) >> pred T = 𝐫0(T)

@[simp]

theorem LeanSubst.Ren.compose_sub_add {T : Type u2} {k : Nat} : add T k >> sub T k = 𝐫0(T)

theorem LeanSubst.Ren.compose_add_succ_right {T : Type u2} {k : Nat} : add T (k + 1) = add T k >> 𝐫1(T)

theorem LeanSubst.Ren.compose_add_succ_left {T : Type u2} {k : Nat} : add T (k + 1) = 𝐫1(T) >> add T k

def LeanSubst.Subst.compose {T : Type u2} [SubstMap T [T]] : Subst T → Subst T → Subst T

Equations

• x✝¹.compose x✝ = { inner := fun (n : Nat) => (x✝¹.act n)[(x✝, LeanSubst.SubstVec.nil),] }

@[instance_reducible]

instance LeanSubst.instAndThenSubstOfSubstMapConsNil {T : Type u2} [SubstMap T [T]] : AndThen (Subst T)

Equations

• LeanSubst.instAndThenSubstOfSubstMapConsNil = { andThen := fun (σ : LeanSubst.Subst T) (f : Unit → LeanSubst.Subst T) => σ.compose (f ()) }

def LeanSubst.SubstVec.compose {V : List (Type u2)} [SubstMapAll V] : SubstVec V → SubstVec V → SubstVec V

Equations

• x_5.compose x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.compose (v1, v1s) (v2, v2s) = (v1[v2s,] >> v2, v1s.compose v2s)

@[instance_reducible]

instance LeanSubst.instAndThenSubstVecOfSubstMapAll {V : List (Type u2)} [SubstMapAll V] : AndThen (SubstVec V)

Equations

• LeanSubst.instAndThenSubstVecOfSubstMapAll = { andThen := fun (σ : LeanSubst.SubstVec V) (f : Unit → LeanSubst.SubstVec V) => σ.compose (f ()) }

@[simp]

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

@[simp]

theorem LeanSubst.Subst.compose_action {T : Type u2} [SubstMap T [T]] {σ τ : Subst T} {x : Var T} : (σ >> τ).act x = (σ.act x)[τ]

@[simp]

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

@[simp]

theorem LeanSubst.Subst.compose_sub_add {T : Type u2} [SubstMap T [T]] {k : Nat} : add T k >> sub T k = 𝐬0(T)

theorem LeanSubst.Subst.compose_add_succ_right {T : Type u2} [SubstMap T [T]] {k : Nat} : add T (k + 1) = add T k >> 𝐬1(T)

theorem LeanSubst.Subst.compose_add_succ_left {T : Type u2} [SubstMap T [T]] {k : Nat} : add T (k + 1) = 𝐬1(T) >> add T k

def LeanSubst.SubstVec.suffix {V : List (Type u2)} [SubstMapAll V] : SubstVec V → SubstVec V → SubstVec V

Equations

• x_5.suffix x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.suffix (v1, v1s) (v2, v2s) = (v1[v2s,], v1s.suffix v2s)

def LeanSubst.SubstVec.compose_simple {V : List (Type u2)} [SubstMapAll V] : SubstVec V → SubstVec V → SubstVec V

Equations

• x_5.compose_simple x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.compose_simple (v1, v1s) (v2, v2s) = (v1 >> v2, v1s.compose_simple v2s)

@[instance_reducible]

instance LeanSubst.instHShiftRightSubstVecOfSubstMapAll {V : List (Type u2)} [SubstMapAll V] : HShiftRight (SubstVec V) (SubstVec V) (SubstVec V)

Equations

• LeanSubst.instHShiftRightSubstVecOfSubstMapAll = { hShiftRight := LeanSubst.SubstVec.compose_simple }

@[simp]

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

def LeanSubst.Subst.compose_ren_left {T : Type u2} : Ren T → Subst T → Subst T

Equations

• LeanSubst.Subst.compose_ren_left x✝¹ x✝ = { inner := fun (n : Nat) => x✝.act (x✝¹.act n) }

@[instance_reducible]

instance LeanSubst.instHAndThenRenSubst {T : Type u2} : HAndThen (Ren T) (Subst T) (Subst T)

Equations

• LeanSubst.instHAndThenRenSubst = { hAndThen := fun (r : LeanSubst.Ren T) (f : Unit → LeanSubst.Subst T) => LeanSubst.Subst.compose_ren_left r (f ()) }

def LeanSubst.SubstVec.compose_ren_left {V : List (Type u2)} : RenVec V → SubstVec V → SubstVec V

Equations

• LeanSubst.SubstVec.compose_ren_left x_3 x_4 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.compose_ren_left (v1, v1s) (v2, v2s) = (v1 >> v2, LeanSubst.SubstVec.compose_ren_left v1s v2s)

@[instance_reducible]

instance LeanSubst.instHAndThenRenVecSubstVec {V : List (Type u2)} : HAndThen (RenVec V) (SubstVec V) (SubstVec V)

Equations

• LeanSubst.instHAndThenRenVecSubstVec = { hAndThen := fun (r : LeanSubst.RenVec V) (f : Unit → LeanSubst.SubstVec V) => LeanSubst.SubstVec.compose_ren_left r (f ()) }

@[simp]

theorem LeanSubst.Subst.compose_ren_left_action {T : Type u2} {r : Ren T} {τ : Subst T} {x : Nat} : (r >> τ).act x = τ.act (r.act x)

def LeanSubst.Subst.compose_ren_right {T : Type u2} [RenMap T [T]] : Subst T → Ren T → Subst T

Equations

• x✝¹.compose_ren_right x✝ = { inner := fun (n : Nat) => (x✝¹.act n)⟨(x✝, LeanSubst.RenVec.nil),⟩ }

@[instance_reducible]

instance LeanSubst.instHAndThenSubstRenOfRenMapConsNil {T : Type u2} [RenMap T [T]] : HAndThen (Subst T) (Ren T) (Subst T)

Equations

• LeanSubst.instHAndThenSubstRenOfRenMapConsNil = { hAndThen := fun (σ : LeanSubst.Subst T) (f : Unit → LeanSubst.Ren T) => σ.compose_ren_right (f ()) }

def LeanSubst.SubstVec.rsuffix {V : List (Type u2)} [RenMapAll V] : SubstVec V → RenVec V → SubstVec V

Equations

• x_5.rsuffix x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.rsuffix (σ, σs) (fst, rs) = (σ⟨rs,⟩, σs.rsuffix rs)

def LeanSubst.SubstVec.compose_ren_right_simple {V : List (Type u2)} [RenMapAll V] : SubstVec V → RenVec V → SubstVec V

Equations

• x_5.compose_ren_right_simple x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.compose_ren_right_simple (σ, σs) (fst, rs) = (σ >> fst, σs.compose_ren_right_simple rs)

@[instance_reducible]

instance LeanSubst.instHShiftRightSubstVecRenVecOfRenMapAll {V : List (Type u2)} [RenMapAll V] : HShiftRight (SubstVec V) (RenVec V) (SubstVec V)

Equations

• LeanSubst.instHShiftRightSubstVecRenVecOfRenMapAll = { hShiftRight := LeanSubst.SubstVec.compose_ren_right_simple }

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_simple_simp {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ : Subst T} {σs : SubstVec V} {r : Ren T} {rs : RenVec V} : (σ, σs) >>> (r, rs) = (σ >> r, σs >>> rs)

def LeanSubst.SubstVec.compose_ren_right {V : List (Type u2)} [RenMapAll V] : SubstVec V → RenVec V → SubstVec V

Equations

• x_5.compose_ren_right x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.compose_ren_right (σ, σs) (fst, rs) = (σ⟨rs,⟩ >> fst, σs.compose_ren_right rs)

@[instance_reducible]

instance LeanSubst.instHAndThenSubstVecRenVecOfRenMapAll {V : List (Type u2)} [RenMapAll V] : HAndThen (SubstVec V) (RenVec V) (SubstVec V)

Equations

• LeanSubst.instHAndThenSubstVecRenVecOfRenMapAll = { hAndThen := fun (σ : LeanSubst.SubstVec V) (f : Unit → LeanSubst.RenVec V) => σ.compose_ren_right (f ()) }

@[simp]

theorem LeanSubst.Subst.compose_ren_right_action {T : Type u2} [RenMap T [T]] {σ : Subst T} {r : Ren T} {x : Nat} : (σ >> r).act x = (σ.act x)⟨r⟩

@[simp]

theorem LeanSubst.SubstVec.compose_ren_left_proj1 {T : Type u2} {V : List (Type u2)} {r : RenVec (T :: V)} {τ : SubstVec (T :: V)} : (r >> τ).fst = r.fst >> τ.fst

@[simp]

theorem LeanSubst.SubstVec.compose_ren_left_proj2 {T : Type u2} {V : List (Type u2)} {r : RenVec (T :: V)} {τ : SubstVec (T :: V)} : (r >> τ).snd = r.snd >> τ.snd

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_proj1 {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ : SubstVec (T :: V)} {r : RenVec (T :: V)} : (σ >> r).fst = σ.fst⟨r.snd,⟩ >> r.fst

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_proj2 {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ : SubstVec (T :: V)} {r : RenVec (T :: V)} : (σ >> r).snd = σ.snd >> r.snd

@[simp]

theorem LeanSubst.SubstVec.compose_proj1 {T : Type u2} {V : List (Type u2)} [SubstMapAll (T :: V)] {σ τ : SubstVec (T :: V)} : (σ >> τ).fst = σ.fst[τ.snd,] >> τ.fst

@[simp]

theorem LeanSubst.SubstVec.compose_proj2 {T : Type u2} {V : List (Type u2)} [SubstMapAll (T :: V)] {σ τ : SubstVec (T :: V)} : (σ >> τ).snd = σ.snd >> τ.snd

def LeanSubst.Ren.lift {T : Type u2} (r : Ren T) (k : Nat := 1) : Ren T

Equations

• r.lift k = { act := fun (n : Nat) => if n < k then n else r.act (n - k) + k }

def LeanSubst.RenVec.lift {V : List (Type u2)} : RenVec V → List Nat → RenVec V

Equations

• x_3.lift x✝ = LeanSubst.RenVec.nil
• LeanSubst.RenVec.lift (t, ts) [] = (t, ts)
• LeanSubst.RenVec.lift (t, ts) (k :: ks) = (t.lift k, ts.lift ks)

@[simp]

theorem LeanSubst.Ren.lift_action_lt {T : Type u2} {r : Ren T} {k i : Nat} (h : i < k) : (r.lift k).act i = i

@[simp]

theorem LeanSubst.Ren.lift_action_ge {T : Type u2} {r : Ren T} {k i : Nat} (h : i ≥ k) : (r.lift k).act i = r.act (i - k) + k

@[simp]

theorem LeanSubst.Ren.lift_of_zero {T : Type u2} {r : Ren T} : r.lift 0 = r

theorem LeanSubst.Ren.lift_of_succ {T : Type u2} {r : Ren T} {k : Nat} : r.lift (k + 1) = (r.lift k).lift

@[simp]

theorem LeanSubst.Ren.lift_id {T : Type u2} {k : Nat} : 𝐫0(T).lift k = 𝐫0(T)

theorem LeanSubst.Ren.lift_compose1 {T : Type u2} {r1 r2 : Ren T} : (r1 >> r2).lift = r1.lift >> r2.lift

@[simp]

theorem LeanSubst.Ren.lift_compose {T : Type u2} {k : Nat} {r1 r2 : Ren T} : (r1 >> r2).lift k = r1.lift k >> r2.lift k

@[simp]

theorem LeanSubst.RenVec.compose_nil : nil >> nil = nil

@[simp]

theorem LeanSubst.RenVec.compose_def {T : Type u2} {V : List (Type u2)} {r1 r2 : Ren T} {r1s r2s : RenVec V} : (r1, r1s) >> (r2, r2s) = (r1 >> r2, r1s >> r2s)

@[simp]

theorem LeanSubst.SubstVec.compose_ren_left_nil : RenVec.nil >> nil = nil

@[simp]

theorem LeanSubst.SubstVec.compose_ren_left_def {T : Type u2} {V : List (Type u2)} {r1 : Ren T} {σ2 : Subst T} {r1s : RenVec V} {σ2s : SubstVec V} : (r1, r1s) >> (σ2, σ2s) = (r1 >> σ2, r1s >> σ2s)

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_def {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ1 : Subst T} {r2 : Ren T} {σ1s : SubstVec V} {r2s : RenVec V} : (σ1, σ1s) >> (r2, r2s) = (σ1⟨r2s,⟩ >> r2, σ1s >> r2s)

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_nil [RenMapAll []] : nil >> RenVec.nil = nil

@[simp]

theorem LeanSubst.SubstVec.compose_ren_right_simple_nil [RenMapAll []] : nil >>> RenVec.nil = nil

@[simp]

theorem LeanSubst.SubstVec.rsuffix_nil [RenMapAll []] {r : RenVec []} : nil.rsuffix r = nil

@[simp]

theorem LeanSubst.SubstVec.compose_simple_nil [SubstMapAll []] : nil >>> nil = nil

@[simp]

theorem LeanSubst.SubstVec.suffix_nil [SubstMapAll []] {σ : SubstVec []} : nil.suffix σ = nil

@[simp]

theorem LeanSubst.SubstVec.compose_nil [SubstMapAll []] : nil >> nil = nil

@[simp]

theorem LeanSubst.SubstVec.compose_def {T : Type u2} {V : List (Type u2)} [SubstMapAll (T :: V)] {σ1 σ2 : Subst T} {σ1s σ2s : SubstVec V} : (σ1, σ1s) >> (σ2, σ2s) = (σ1[σ2s,] >> σ2, σ1s >> σ2s)

theorem LeanSubst.SubstVec.compose_ren_right_split {V : List (Type u2)} [RenMapAll V] {σ : SubstVec V} {r : RenVec V} : σ >> r = σ.rsuffix r >>> r

theorem LeanSubst.SubstVec.compose_split {V : List (Type u2)} [SubstMapAll V] {σ τ : SubstVec V} : σ >> τ = σ.suffix τ >>> τ

@[simp]

theorem LeanSubst.RenVec.lift_compose {V : List (Type u2)} {k : List Nat} {r1 r2 : RenVec V} : (r1 >> r2).lift k = r1.lift k >> r2.lift k

@[simp]

theorem LeanSubst.RenVec.lift_proj1 {T : Type u2} {V : List (Type u2)} {r : RenVec (T :: V)} {n : Nat} {k : List Nat} : (r.lift (n :: k)).fst = r.fst.lift n

@[simp]

theorem LeanSubst.RenVec.lift_proj2 {T : Type u2} {V : List (Type u2)} {r : RenVec (T :: V)} {n : Nat} {k : List Nat} : (r.lift (n :: k)).snd = r.snd.lift k

def LeanSubst.Subst.lift {T : Type u2} [RenMap T [T]] (σ : Subst T) (k : Nat := 1) : Subst T

Equations

• σ.lift k = { inner := fun (n : Nat) => if n < k then LeanSubst.re n else (σ.act (n - k))⟨(LeanSubst.Ren.add T k, LeanSubst.RenVec.nil),⟩ }

def LeanSubst.SubstVec.lift {V : List (Type u2)} [RenMapAll V] : List Nat → SubstVec V → SubstVec V

Equations

• LeanSubst.SubstVec.lift x✝ x_6 = LeanSubst.SubstVec.nil
• LeanSubst.SubstVec.lift [] (t, ts) = (t, ts)
• LeanSubst.SubstVec.lift (k :: ks) (t, ts) = (t.lift k, LeanSubst.SubstVec.lift ks ts)

@[simp]

theorem LeanSubst.Subst.lift_action_lt {T : Type u2} [RenMap T [T]] {σ : Subst T} {k i : Nat} (h : i < k) : (σ.lift k).act i = re i

@[simp]

theorem LeanSubst.Subst.lift_action_ge {T : Type u2} [RenMap T [T]] {σ : Subst T} {k i : Nat} (h : i ≥ k) : (σ.lift k).act i = (σ.act (i - k))⟨Ren.add T k⟩

@[simp]

theorem LeanSubst.SubstVec.lift_proj1 {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ : SubstVec (T :: V)} {n : Nat} {k : List Nat} : (lift (n :: k) σ).fst = σ.fst.lift n

@[simp]

theorem LeanSubst.SubstVec.lift_proj2 {T : Type u2} {V : List (Type u2)} [RenMapAll (T :: V)] {σ : SubstVec (T :: V)} {n : Nat} {k : List Nat} : (lift (n :: k) σ).snd = lift k σ.snd

def LeanSubst.Subst.act_list {T : Type u2} (σ : Subst T) (ℓ : List Nat) : List (Action T)

Equations

• σ.act_list [] = []
• σ.act_list (x_1 :: xs) = σ.act x_1 :: σ.act_list xs

@[instance_reducible]

instance LeanSubst.instSubstActionListNatAction {T : Type u2} : SubstAction T (List Nat) (List (Action T))

Equations

• LeanSubst.instSubstActionListNatAction = { act := LeanSubst.Subst.act_list }

@[simp]

theorem LeanSubst.Subst.act_list_nil {T : Type u2} {σ : Subst T} : σ.act [] = []

@[simp]

theorem LeanSubst.Subst.act_list_cons {T : Type u2} {σ : Subst T} {x : Nat} {ℓ : List Nat} : σ.act (x :: ℓ) = σ.act x :: σ.act ℓ

@[simp]

theorem LeanSubst.Subst.act_list_append {T : Type u2} {σ : Subst T} {x y : List Nat} : σ.act (x ++ y) = σ.act x ++ σ.act y

def LeanSubst.Ren.to {T : Type u2} (r : Ren T) : Subst T

Equations

• r.to = { inner := fun (x : Nat) => LeanSubst.re (r.act x) }

@[simp]

theorem LeanSubst.Ren.to_act {T : Type u2} {r : Ren T} {x : Nat} : r.to.act x = re (r.act x)

@[simp]

theorem LeanSubst.Ren.to_id {T : Type u2} : 𝐫0(T).to = 𝐬0(T)

@[simp]

theorem LeanSubst.Ren.to_succ {T : Type u2} : 𝐫1(T).to = 𝐬1(T)

@[simp]

theorem LeanSubst.Ren.to_pred {T : Type u2} : (pred T).to = Subst.pred T

@[simp]

theorem LeanSubst.Ren.to_add {T : Type u2} {k : Nat} : (add T k).to = Subst.add T k

@[simp]

theorem LeanSubst.Ren.to_sub {T : Type u2} {k : Nat} : (sub T k).to = Subst.sub T k

@[simp]

theorem LeanSubst.Ren.to_lift {T : Type u2} [RenMap T [T]] {r : Ren T} {k : Nat} : (r.lift k).to = r.to.lift k

@[simp]

theorem LeanSubst.Ren.to_compose {T : Type u2} [RenMap T [T]] [SubstMap T [T]] {r1 r2 : Ren T} : (r1 >> r2).to = r1.to >> r2.to

@[simp]

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

def LeanSubst.RenVec.to {V : List (Type u2)} (r : RenVec V) : SubstVec V

Equations

• x_2.to = LeanSubst.SubstVec.nil
• LeanSubst.RenVec.to (r, rs) = (r.to, rs.to)

@[simp]

theorem LeanSubst.RenVec.to_lift {V : List (Type u2)} [RenMapAll V] {r : RenVec V} {k : List Nat} : (r.lift k).to = SubstVec.lift k r.to

def LeanSubst.Ren.range : Nat → Nat → List Nat

Equations

• x✝..0 = []
• x✝..e.succ = if x✝ ≤ e then (x✝..e).concat e else []

def LeanSubst.«term_.._» : Lean.TrailingParserDescr

Equations

• LeanSubst.«term_.._» = Lean.ParserDescr.trailingNode `LeanSubst.«term_.._» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "..") (Lean.ParserDescr.cat `term 91))

@[simp]

theorem LeanSubst.Ren.range_same {n : Nat} : n..n = []

@[simp]

theorem LeanSubst.Ren.range_ge_nil {s e : Nat} {h : s ≥ e} : s..e = []

@[simp]

theorem LeanSubst.Ren.range_lt_cons {s e : Nat} {h : s < e} : s..e = s :: s.succ..e

def LeanSubst.SubstVec.ren (S : Type u2) (T : List (Type u2)) [RenMap S T] [RenSuffix S T] (r : RenVec T) {V : List (Type u2)} (x : Nat) (_h : V[x]? = some S := by grind) : SubstVec V → SubstVec V

Equations

• One or more equations did not get rendered due to their size.
• LeanSubst.SubstVec.ren S T r x x_1 σ = σ
• LeanSubst.SubstVec.ren S T r x_4.succ h (σ, σs) = (σ, LeanSubst.SubstVec.ren S T r x_4 h σs)

@[simp]

theorem LeanSubst.SubstVec.ren_zero_proj1 {V : List (Type u2)} {S : Type u2} {T : List (Type u2)} [RenMap S T] [RenSuffix S T] {r : RenVec T} {h : (S :: V)[0]? = some S} {σ : SubstVec (S :: V)} : (ren S T r 0 h σ).fst = σ.fst⟨r,⟩

@[simp]

theorem LeanSubst.SubstVec.ren_zero_proj2 {V : List (Type u2)} {S : Type u2} {T : List (Type u2)} [RenMap S T] [RenSuffix S T] {r : RenVec T} {h : (S :: V)[0]? = some S} {σ : SubstVec (S :: V)} : (ren S T r 0 h σ).snd = σ.snd