π_comp_cokernelIsoOfEq_inv — Mathlib

English

If h: f = g, then (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he]).

Русский

Если h: f = g, то (cokernelIsoOfEq h).inv ∘ cokernel.desc _ e he = cokernel.desc _ e (по доказательству).

LaTeX

$$$(cokernelIsoOfEq(h)).inv \circ cokernel.desc\_f e he = cokernel.desc\_f e (by simp [\Leftarrow h, he])$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_cokernelIsoOfEq_inv {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.π _ ≫ (cokernelIsoOfEq h).inv = cokernel.π _ := by cases h; simp

Похожие утверждения