homInduction — Mathlib

Lean4
/-- An induction principle for morphisms in a join of category: a morphism is either of the form
`(inclLeft _ _).map _`, `(inclRight _ _).map _`, or is `edge _ _`. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
def homInduction {P : {x y : C ⋆ D} → (x ⟶ y) → Sort*} (left : ∀ x y : C, (f : x ⟶ y) → P ((inclLeft C D).map f))
    (right : ∀ x y : D, (f : x ⟶ y) → P ((inclRight C D).map f)) (edge : ∀ (c : C) (d : D), P (edge c d)) {x y : C ⋆ D}
    (f : x ⟶ y) : P f :=
  match x, y, f with
  | .left x, .left y, .up f => left x y f
  | .right x, .right y, .up f => right x y f
  | .left x, .right y, _ => edge x y
Похожие утверждения