∃! (xy : α × β), P xy.fst xy.snd vs. ∃! (x : α) ∃! (y : β), P x y

exists_unique_prod.lean

theorem eu_prod_imp_eu_eu {α β} (P : α → β → Prop) :
  (∃! (xy : α × β), P xy.fst xy.snd) → (∃! (x : α) (y : β), P x y) :=
λ ⟨xy,he,hu⟩, ⟨xy.fst, ⟨xy.snd, he, λ y h, congr_arg prod.snd (hu (xy.fst,y) h)⟩,
  λ x ⟨y,hy⟩, congr_arg prod.fst (hu (x,y) hy.1)⟩
#print axioms eu_prod_imp_eu_eu -- no axioms

def eu_eu_and_not_eu_prod {α} (P : α → α → Prop) :=
  (∃! (x y : α), P x y) ∧ ¬(∃! (xy : α × α), P xy.fst xy.snd)

theorem eenep_bor : eu_eu_and_not_eu_prod (λ x y, x || y) :=
⟨⟨ff, ⟨tt, rfl, λ y, id⟩, λ x hx, by {cases x, refl, exact unique_of_exists_unique hx rfl rfl}⟩,
 λ h, by cases @unique_of_exists_unique _ _ h (tt,tt) (tt,ff) rfl rfl⟩
#print axioms eenep_bor -- no axioms

theorem eenep_or : eu_eu_and_not_eu_prod or :=
⟨⟨false, ⟨true, or.inr trivial, λ x y, y.elim false.elim eq_true_intro⟩,
    λ y heu, cast eq_false.symm
      (λ hy, cast (unique_of_exists_unique heu (or.inl hy) (or.inl hy)) hy)⟩,
 λ h, cast eq_true $ congr_arg prod.snd $ @unique_of_exists_unique _ _ h
   (true,false) (true,true) (or.inl trivial) (or.inl trivial)⟩
#print axioms eenep_or -- propext

theorem eenep_or' : eu_eu_and_not_eu_prod (λ x y, x = true ∨ (x = false ∧ y = true)) :=
⟨⟨false, ⟨true, or.inr ⟨rfl,rfl⟩,
  λ y hu, hu.elim (λ he, (true_ne_false he.symm).elim) and.right⟩,
  λ x heu, let ⟨_,hs,_⟩ := heu in
    hs.elim (λ ht, unique_of_exists_unique heu (or.inl ht) (or.inl ht)) and.left⟩,
 λ h, true_ne_false $ congr_arg prod.snd $ @unique_of_exists_unique _ _ h
   (true,true) (true,false) (or.inl rfl) (or.inl rfl)⟩
#print axioms eenep_or' -- no axioms

theorem eenep_imp : eu_eu_and_not_eu_prod (→) :=
⟨⟨true, ⟨true, id, λ y h, eq_true_intro (h trivial)⟩,
  λ x heu, unique_of_exists_unique heu id (λ _, trivial)⟩,
 λ h, true_ne_false $ congr_arg prod.snd $ @unique_of_exists_unique _ _ h
   (true,true) (false,false) id id⟩
#print axioms eenep_imp -- propext

theorem eenep_impby : eu_eu_and_not_eu_prod (λ x y, y → x) :=
⟨⟨false, ⟨false, id, λ _, eq_false_intro⟩, λ x heu, unique_of_exists_unique heu id false.elim⟩,
 λ h, true_ne_false $ congr_arg prod.snd $ @unique_of_exists_unique _ _ h
   (true,true) (false,false) id id⟩
#print axioms eenep_impby -- propext

theorem eenep_nand : eu_eu_and_not_eu_prod (λ x y, ¬ (x ∧ y)) := sorry