class LeanSubst.SubstMapId (S T : Type) [RenMap T] [SubstMap S T] : Prop

• apply_id {t : S} : t[+0:_] = t

class LeanSubst.SubstMapStable (S : Type) [RenMap S] [SubstMap S S] : Prop

• apply_stable (r : Ren) (σ : Subst S) : ↑r = σ → rmap r = smap σ

class LeanSubst.SubstMapCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] : Prop

• apply_compose {s : S} {σ τ : Subst T} : s[σ:_][τ:_] = s[σ ∘ τ:_]

class LeanSubst.SubstMapRenCommute (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] : Prop

• apply_ren_commute {s : S} (r : Ren) (τ : Subst T) : s[↑r][τ:_] = s[τ:_][↑r]

class LeanSubst.SubstMapHetCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] : Prop

• apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ:_] = s[τ:_][σ ◾ τ]

theorem LeanSubst.Ren.lift_eq_from_eq {S T : Type} [RenMap T] [SubstMap S T] {r : Ren} {σ : Subst T} : ↑r = σ → ↑r.lift = σ.lift

@[simp]

theorem LeanSubst.Subst.rewrite1 {T : Type} : re 0 :: +1 = +0

@[simp]

theorem LeanSubst.Subst.I_lift {T : Type} [RenMap T] : +0.lift = +0

@[simp]

theorem LeanSubst.Subst.rewrite2 {T : Type} [RenMap T] [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ

@[simp]

theorem LeanSubst.Subst.rewrite3_replace {T : Type} [RenMap T] [SubstMap T T] {σ τ : Subst T} {s : T} : (su s :: σ) ∘ τ = su s[τ] :: σ ∘ τ

@[simp]

theorem LeanSubst.Subst.rewrite3_rename {T : Type} [RenMap T] [SubstMap T T] {s : Nat} {σ τ : Subst T} : (re s :: σ) ∘ τ = τ s :: σ ∘ τ

@[simp]

theorem LeanSubst.Subst.rewrite4 {T : Type} [RenMap T] [SubstMap T T] {s : Action T} {σ : Subst T} : +1 ∘ (s :: σ) = σ

@[simp]

theorem LeanSubst.Subst.rewrite5 {T : Type} [RenMap T] [SubstMap T T] {σ : Subst T} : σ 0 :: +1 ∘ σ = σ

@[simp]

theorem LeanSubst.Subst.apply_I_is_id {S T : Type} [RenMap T] [SubstMap S T] [SubstMapId S T] {s : S} : s[+0:_] = s

@[simp]

theorem LeanSubst.Subst.rewrite_lift {T : Type} [RenMap T] [SubstMap T T] [SubstMapStable T] {σ : Subst T} : σ.lift = re 0 :: σ ∘ +1

@[simp]

theorem LeanSubst.Subst.rewrite6 {T : Type} [RenMap T] [SubstMap T T] [SubstMapId T T] {σ : Subst T} : σ ∘ +0 = σ

@[simp]

theorem LeanSubst.Subst.apply_compose_commute {S T : Type} [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] {s : S} {σ τ : Subst T} : s[σ:_][τ:_] = s[σ ∘ τ:_]

@[simp]

theorem LeanSubst.Subst.rewrite7 {T : Type} [RenMap T] [SubstMap T T] [SubstMapCompose T T] {σ τ μ : Subst T} : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ

@[simp]

theorem LeanSubst.Subst.hrewrite1 {S T : Type} [RenMap T] [SubstMap S T] [SubstMapId S T] {σ : Subst S} : σ ◾ +0 = σ

@[simp]

theorem LeanSubst.Subst.hcomp_ren_left {S T : Type} [RenMap S] [RenMap T] [SubstMap S T] (r : Ren) (σ : Subst T) : ↑r ◾ σ = ↑r

@[simp]

theorem LeanSubst.Subst.hrewrite2 {S T : Type} [RenMap S] [RenMap T] [SubstMap S T] {σ : Subst T} : +0 ◾ σ = +0

@[simp]

theorem LeanSubst.Subst.hrewrite3 {S T : Type} [RenMap S] [RenMap T] [SubstMap S T] {σ : Subst T} : +1 ◾ σ = +1

@[simp]

theorem LeanSubst.Subst.hrewrite4 {S T : Type} [RenMap T] [SubstMap S T] {x : Nat} {σ : Subst S} {τ : Subst T} : (re x :: σ) ◾ τ = re x :: σ ◾ τ

theorem LeanSubst.Subst.hcomp_dist_ren_left {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] (r : Ren) {σ : Subst S} {τ : Subst T} : (↑r ∘ σ) ◾ τ = ↑r ∘ σ ◾ τ

@[simp]

theorem LeanSubst.Subst.hrewrite5 {S T : Type} [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] {σ : Subst S} {τ μ : Subst T} : (σ ◾ τ) ◾ μ = σ ◾ τ ∘ μ

theorem LeanSubst.Subst.hcomp_distr_ren_right {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] (r : Ren) (σ : Subst S) (μ : Subst T) : (σ ∘ ↑r) ◾ μ = (σ ◾ μ) ∘ ↑r

@[simp]

theorem LeanSubst.Subst.hrewrite6 {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] (r : Ren) (σ : Subst S) : (σ ∘ ↑r) ◾ +1 = (σ ◾ +1) ∘ ↑r

@[simp]

theorem LeanSubst.Subst.apply_hcompose {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ:_] = s[τ:_][σ ◾ τ]

@[simp]

theorem LeanSubst.Subst.hrewrite7 {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] {σ τ : Subst S} (μ : Subst T) : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ

def LeanSubst.«tacticSubst_solve_id_,_,_» : Lean.ParserDescr

Equations

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

def LeanSubst.«tacticSubst_solve_stable_,_» : Lean.ParserDescr

Equations

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

def LeanSubst.«tacticSubst_solve_hcompose_,_,_,_,_» : Lean.ParserDescr

Equations

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

def LeanSubst.«tacticSubst_solve_compose_,_,_,_» : Lean.ParserDescr

Equations

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