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

• apply_id {t : S} : t⟨Ren.id⟩ = t

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

• apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 >> r2⟩

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.SubstMapRenCommute (S T : Type) [RenMap S] [RenMap T] [SubstMap S T] : Prop

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

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

• apply_ren_compose_left {s : S} {r : Ren} {τ : Subst T} : s[↑r:_][τ:_] = s[↑r ∘ τ:_]

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

• apply_ren_compose_right {s : S} {r : Ren} {σ : Subst T} : s[σ:_][↑r:_] = s[σ ∘ ↑r:_]

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.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[τ:_][σ ◾ τ]

@[simp]

theorem LeanSubst.Ren.apply_id {T : Type} [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t

@[simp]

theorem LeanSubst.Ren.apply_compose {T : Type} [RenMap T] [RenMapCompose T] {t : T} {r1 r2 : Ren} : t⟨r1⟩⟨r2⟩ = t⟨r1 >> r2⟩

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] {k : Nat} : +0.lift k = +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.rewrite_lift_zero {S : Type} [RenMap S] [RenMapId S] {σ : Subst S} : σ.lift 0 = σ

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

@[simp]

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

@[simp]

theorem LeanSubst.Subst.apply_compose {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] [SubstMapStable S] [SubstMapRenCommute S T] (r : Ren) (σ : Subst S) (μ : Subst T) : (σ ∘ ↑r) ◾ μ = (σ ◾ μ) ∘ ↑r

theorem LeanSubst.Subst.hcomp_distr_ren_right_p1 {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapStable S] [SubstMapRenCommute S T] (σ : Subst S) (μ : Subst T) : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1

@[simp]

theorem LeanSubst.Subst.hrewrite6 {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapStable S] [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) : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ

theorem LeanSubst.Subst.hrewrite_lift1 {S T : Type} [RenMap S] [RenMap T] [SubstMap S T] [SubstMapRenCommute S T] {σ : Subst S} {τ : Subst T} : (σ ◾ τ).lift = σ.lift ◾ τ

@[simp]

theorem LeanSubst.Subst.hrewrite_lift {S T : Type} [RenMap S] [RenMap T] [SubstMap S T] [RenMapId S] [RenMapCompose S] [SubstMapRenCommute S T] {k : Nat} {σ : Subst S} {τ : Subst T} : (σ ◾ τ).lift k = σ.lift k ◾ τ

theorem LeanSubst.Subst.Compose.lemma1 {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] {k : Nat} {τ : Subst S} : (↑fun (x : Nat) => x + 1) ∘ τ.lift (k + 1) = τ.lift k ∘ ↑fun (x : Nat) => x + 1

theorem LeanSubst.Subst.Compose.lemma1s {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] {k : Nat} {τ : Subst S} : +1 ∘ τ.lift (k + 1) = τ.lift k ∘ +1

theorem LeanSubst.Subst.Compose.lemma2_k1 {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] {σ : Subst S} {r : Ren} : (↑r ∘ σ).lift = (↑r).lift ∘ σ.lift

theorem LeanSubst.Subst.Compose.lemma2 {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] {k : Nat} {σ : Subst S} {r : Ren} : (↑r ∘ σ).lift k = (↑r).lift k ∘ σ.lift k

theorem LeanSubst.Subst.Compose.lemma2s {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] {k : Nat} {σ : Subst S} : (+1 ∘ σ).lift k = +1.lift k ∘ σ.lift k

theorem LeanSubst.Subst.Compose.lemma3 {S T : Type} [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeLeft S T] {s : S} {σ : Subst T} : s[+1:_][σ:_] = s[+1 ∘ σ:_]

theorem LeanSubst.Subst.Compose.lemma4 {T : Type} [RenMap T] [SubstMap T T] {σ τ : Subst T} : +1 ∘ τ ∘ σ = (+1 ∘ τ) ∘ σ

theorem LeanSubst.Subst.compose.lemma5 {T : Type} [RenMap T] [SubstMap T T] [RenMapCompose T] [SubstMapStable T] {r1 r2 : Ren} {τ : Subst T} : (τ ∘ ↑r2) ∘ ↑r1 = τ ∘ ↑r2 ∘ ↑r1

theorem LeanSubst.Subst.Compose.lemma6_k1 {S : Type} [RenMap S] [SubstMap S S] [SubstMapStable S] [SubstMapRenComposeLeft S S] {σ : Subst S} {r : Ren} : (σ ∘ ↑r).lift = σ.lift ∘ (↑r).lift

theorem LeanSubst.Subst.Compose.lemma6 {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] [SubstMapRenComposeLeft S S] {k : Nat} {σ : Subst S} {r : Ren} : (σ ∘ ↑r).lift k = σ.lift k ∘ (↑r).lift k

theorem LeanSubst.Subst.Compose.lemma6s {S : Type} [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] [SubstMapRenComposeLeft S S] {k : Nat} {σ : Subst S} : (σ ∘ +1).lift k = σ.lift k ∘ +1.lift k

theorem LeanSubst.Subst.Compose.lemma7 {S T : Type} [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] {s : S} {τ : Subst T} : s[τ:_][+1:_] = s[τ ∘ +1:_]

theorem LeanSubst.Subst.Compose.lemma8 {T : Type} [RenMap T] [SubstMap T T] [SubstMapRenComposeLeft T T] {σ τ : Subst T} : (σ ∘ +1) ∘ τ = σ ∘ +1 ∘ τ

theorem LeanSubst.Subst.Compose.lemma9 {T : Type} [RenMap T] [SubstMap T T] [SubstMapRenComposeRight T T] {σ τ : Subst T} : (σ ∘ τ) ∘ +1 = σ ∘ τ ∘ +1

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

theorem LeanSubst.Subst.Compose.lemma10s {S T : Type} [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapStable S] [SubstMapRenCommute S T] {σ : Subst S} {μ : Subst T} : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1

theorem LeanSubst.Subst.rewrite_lift_compose_k1 {T : Type} [RenMap T] [SubstMap T T] [SubstMapStable T] [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] {σ τ : Subst T} : (σ ∘ τ).lift = σ.lift ∘ τ.lift

@[simp]

theorem LeanSubst.Subst.rewrite_lift_compose {T : Type} [RenMap T] [SubstMap T T] [RenMapId T] [RenMapCompose T] [SubstMapStable T] [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] {k : Nat} {σ τ : Subst T} : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k

def LeanSubst.tacticSubst_solve_id : Lean.ParserDescr

Equations

• LeanSubst.tacticSubst_solve_id = Lean.ParserDescr.node `LeanSubst.tacticSubst_solve_id 1024 (Lean.ParserDescr.nonReservedSymbol "subst_solve_id" false)

def LeanSubst.tacticSubst_solve_stable : Lean.ParserDescr

Equations

• LeanSubst.tacticSubst_solve_stable = Lean.ParserDescr.node `LeanSubst.tacticSubst_solve_stable 1024 (Lean.ParserDescr.nonReservedSymbol "subst_solve_stable" false)

def LeanSubst.tacticSubst_solve_compose : Lean.ParserDescr

Equations

• LeanSubst.tacticSubst_solve_compose = Lean.ParserDescr.node `LeanSubst.tacticSubst_solve_compose 1024 (Lean.ParserDescr.nonReservedSymbol "subst_solve_compose" false)