lean - 如何在精益中证明 (∀ x, px ∨ r) ↔ (∀ x, px) ∨ r？

Question

我的证明如下，但它是错误的，我不知道如何更正

      assume h : ∀ x, p x ∨ r, assume a: α,
      or.elim (h a)
      (assume hl: p a,
        show p a ∨ r, from
         or.inl hl)
      (assume hr: r,
        show p a ∨ r, from or.inr hr)

Answer 1

@lizhengxian 这个例子有帮助吗（在线精益编辑器）：

variables {α : Type*} (p : α → Prop) (r : Prop) [decidable r]

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
begin
  split,
  { assume h,
    by_cases hr : r,
    { right, assumption },
    { left,
      assume x,
      specialize h x,
      cases h,
      { assumption },
      { contradiction } } },
  { assume h x,
    cases h with h h,
    { left, apply h },
    { right, assumption } }
end