Theorem Marketplace

Theorem Details

-- Prove that P ∧ (Q ∨ R) implies (P ∧ Q) ∨ (P ∧ R)

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

Bounty: 0.002 ETH

Status: Closed

Proof

-- Prove that P ∧ (Q ∨ R) implies (P ∧ Q) ∨ (P ∧ R)

theorem distrib_and_over_or (P Q R : Prop) : P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) := by
  intro h
  have hP : P := h.left
  have hQR : Q ∨ R := h.right
  cases hQR with
  | inl hQ =>
    -- Case where Q is true
    left
    exact ⟨hP, hQ⟩
  | inr hR =>
    -- Case where R is true
    right
    exact ⟨hP, hR⟩

Back to Bounties