def LeanSubst.Subst.Action.coe_map {A B : Type} [Coe A B] : Action A → Action B

Equations

• ↑(LeanSubst.re k) = LeanSubst.re k
• ↑(LeanSubst.su t) = LeanSubst.su (Coe.coe t)

instance LeanSubst.Subst.Action.instCoe {A B : Type} [Coe A B] : Coe (Action A) (Action B)

Equations

• LeanSubst.Subst.Action.instCoe = { coe := LeanSubst.Subst.Action.coe_map }

def LeanSubst.Subst.coe_map {A B : Type} [Coe A B] : Subst A → Subst B

Equations

• ↑x✝¹ x✝ = ↑(x✝¹ x✝)

instance LeanSubst.Subst.instCoe {A B : Type} [Coe A B] : Coe (Subst A) (Subst B)

Equations

• LeanSubst.Subst.instCoe = { coe := LeanSubst.Subst.coe_map }

class LeanSubst.Subst.CommutesWithSmap (A B : Type) [SubstMap A] [SubstMap B] [c : Coe A B] : Prop

• coe_commutes (a : A) (σ : Subst A) : Coe.coe a[σ] = (Coe.coe a)[Coe.coe σ]

@[simp]

theorem LeanSubst.Subst.coe_cons {A B : Type} {a : Action A} {σ : Subst A} [Coe A B] : Coe.coe (a::σ) = Coe.coe a::Coe.coe σ

@[simp]

theorem LeanSubst.Subst.coe_comp {A B : Type} {σ τ : Subst A} [SubstMap A] [SubstMap B] [Coe A B] [i : CommutesWithSmap A B] : Coe.coe (σ ∘ τ) = Coe.coe σ ∘ Coe.coe τ