lean_workbook_plus_74616

Proved

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

Prove that, if $p$ , $q$ and $r$ are logical statements then \n\n $\left(p\longrightarrow q\vee r\right)\longleftrightarrow\left(\left(p\longrightarrow q\right)\vee\left(p\longrightarrow r\right)\right)$ where $\longrightarrow$ stands for the logical implication and $\longleftrightarrow$ for the logical bi-implication (aka. equivalence).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74616 (p q r : Prop) : (p → q ∨ r) ↔ (p → q) ∨ (p → r)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph