如何在精益中证明 (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ 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 这个例子有帮助吗(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

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

How to prove (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r in Lean?

lean