LEAN中如何证明分配性（命题有效性属性6）？

Question

在完成了大多数练习以及精益手册第 3 章末尾的前五个命题 validities/properties solved/proved 之后，我仍然无法理解以下含义（其中之一属性 6):

证明所需的含义

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    sorry
end

我面临的困难主要是由于p不正确的情况，因为我不知道如何结合，使用LEAN工具，and的两侧获得 q 和 r 都必须在该场景下成立的事实的假设。我将不胜感激这里的任何帮助；请帮助我理解如何在上述设置中构建此证明，而不导入除标准 LEAN 中的策略之外的任何其他策略。为了完整起见，这是我对另一个方向的证明：

theorem Distr_or_R (p q r : Prop) : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) :=
begin
    intros pqr,
    exact or.elim pqr 
    ( assume hp: p, show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_left q hp) (or.intro_left r hp) ) 
    ( assume hqr : (q ∧ r), show (p ∨ q) ∧ (p ∨ r), from 
        and.intro (or.intro_right p hqr.left) (or.intro_right p hqr.right) ) 
end

Answer 1

提示。尝试对 porq 和 porr.

进行大小写拆分

这是一个解决方案

theorem Distr_or_L (p q r : Prop) : (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r) :=
begin
    intros pqpr, 
    have porq : p ∨ q, from pqpr.left,
    have porr : p ∨ r, from pqpr.right,
    { cases porq with hp hq,
      { exact or.inl hp },
      { cases porr with hp hr,
        { exact or.inl hp },
        { exact or.inr ⟨hq, hr⟩ } } }
end

LEAN中如何证明分配性（命题有效性属性6）？

How to prove distributivity (propositional validity property 6) in LEAN?

functional-programming

theorem-proving

lean