Stuck on disjunction of a forall and something

Stream: new members

[Lars Ericson]

I am doing exercises in Chapter 4 and I've got this one:

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
begin
  split,
  {
    intro h,
    left,
    assume x,
    have hpr := h x,
    cases hpr,
    exact hpr,
    have h2 := h x,
  },
  sorry,
end

Just after the have h2 := h x I am in goal state

α : Type u_1,
p : α → Prop,
r : Prop,
h : ∀ (x : α), p x ∨ r,
x : α,
hpr : r,
h2 : p x ∨ r
⊢ p x

At this point I don't have any reason to believe p x, I only know r. I got to this state reasonably though. The state is weak but not contradictory. If it was contradictory I could say exfalso and be done. So I've run out of ideas. Any hints would be greatly appreciated!

[Antoine Labelle]

I think you reached an impossible goal by doing left at the beginning. You will need left or right depending on the case for hpr.

[Lars Ericson]

@Antoine Labelle the problem is that right doesn't have any support either. right gives a goal of r but we don't have any way of proving r. Suppose I do right:

example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
begin
  split,
  {
    intro h,
    right,
  },
  {

  },
end

then the goal state becomes

α : Type u_1,
p : α → Prop,
r : Prop,
h : ∀ (x : α), p x ∨ r
⊢ r

and there is nothing there that will prove r.

[Antoine Labelle]

You can't do neither left or right before doing cases on your hypothesis, because which part of the disjunction in the goal is true will depend on which part of the disjunction in the hypothesis is true (for each x)

[Antoine Labelle]

Actually I think the simplest way to do this would be by cases on r

[Lars Ericson]

Thank you @Antoine Labelle that's a good point by_cases hr : r,.