Eliminate a disjunction

2/4 ~18 minlean

Use both branches of a disjunction to derive the same result.

3 lines · Lean 4

theorem or_elim (P Q R : Prop) :
    (P → R) → (Q → R) → P ∨ Q → R := by
  sorry

Objectifs

Use both branches of a disjunction to derive the same result.

Indices

Voir la solution

theorem or_elim (P Q R : Prop) :
    (P → R) → (Q → R) → P ∨ Q → R := by
  intro hPR hQR h
  cases h with
  | inl hP => exact hPR hP
  | inr hQ => exact hQR hQ