halp.lean

open classical

variables (α : Type) (p q : α → Prop)
variable r : Prop
variable a : α

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
  (assume ⟨a, pair⟩,
   assume h : ∀ x, p x,
   show r, from pair $ h a)
  (assume h : (∀ (x : α), p x) → r,
   suffices pair : p a → r, from ⟨a, pair⟩,
   have hr : r, from h (λ y, _),
   /-
   context:
   α : Type,
   p : α → Prop,
   r : Prop,
   a : α,
   h : (∀ (x : α), p x) → r,
   y : α
   ⊢ p y
   -/
   (λ hpa, hr))

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
iff.intro
  (assume ⟨ha, ripa⟩,
   assume hr,
   show ∃ x, p x, from ⟨ha, ripa hr⟩)
  (assume h : r → (∃ (x : α), p x),
   suffices ripa : r → p a, from ⟨a, ripa⟩,
   assume hr,
   have x : (∃ x, p x), from h hr,
   exists.elim x
     (assume ha,
      assume hpa,
      _))
/- 
  context:
  α : Type,
  p : α → Prop,
  r : Prop,
  a : α,
  h : r → (∃ (x : α), p x),
  hr : r,
  x : ∃ (x : α), p x,
  ha : α,
  hpa : p ha
  ⊢ p a
-/