Как доказать дистрибутивность (свойство пропозициональной валидности 6) в LEAN?

Question

Пройдя через большинство упражнений, а также решив / доказав в LEAN первые пять пропозициональных истинностей / свойств в конце главы 3 руководства по LEAN, у меня все еще возникают проблемы со следующим подтекстом (одно из следствий, необходимых для доказательства свойства 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