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

【问题标题】：How to prove (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r in Lean?如何在精益中证明 (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r？
【发布时间】：2020-02-01 03:22:29
【问题描述】：

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

      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)

【问题讨论】：

标签： lean

【解决方案1】：

@lizhengxian 这个例子有帮助吗（online Lean editor）：

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

【讨论】：

谢谢，真的很有帮助