lean_workbook_plus_68363

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given logical expressions $p \rightarrow s$ and $q \rightarrow s$ , both true. Determine if $(p \lor q) \rightarrow s$ is also true.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68363 (p q s : Prop) (h₁ : p → s) (h₂ : q → s) : p ∨ q → s   :=  by sorry

Source