Partition lemma without LEM

Stream: new members

[Brandon Brown]

Is it possible to prove this set partition lemma without using the law of excluded middle?

lemma partition_els_eq_if_share_el
{F : set (set X)}
{disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅}
{cover : ∀ x : X, ∃ A ∈ F, x ∈ A}
{nonempty : ∀ A ∈ F, A ≠ ∅}
{A B : set X}
{h0 : A ∈ F} {h1 : B ∈ F}
(h2 : ∃ x : X, x ∈ A ∧ x ∈ B) : A = B :=
begin
cases h2,
cases h2_h,
by_contra,
have z : A ∩ B = ∅,
apply disjoint,
repeat {tauto},
have z2 : h2_w ∈ A ∩ B,
apply mem_inter,
repeat {tauto},
rw z at z2,
tauto,
end

[Mario Carneiro]

not with that statement

[Mario Carneiro]

if you rewrite disjoint to disjoint : ∀ A B ∈ F, A = B ∨ A ∩ B = ∅ then it can be done

[Mario Carneiro]

lemma partition_els_eq_if_share_el {X}
  {F : set (set X)}
  (disjoint : ∀ A B ∈ F, A = B ∨ A ∩ B = ∅)
  {A B : set X}
  (h0 : A ∈ F) (h1 : B ∈ F)
  (h2 : ∃ x : X, x ∈ A ∧ x ∈ B) : A = B :=
(disjoint _ _ h0 h1).resolve_right $ λ h,
let ⟨x, hx⟩ := h2 in
show x ∈ (∅ : set X), from h ▸ hx

#print axioms partition_els_eq_if_share_el
-- no axioms

[Brandon Brown]

Thanks for the confirmation and reformulation!