-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma exists_ne_mem_inter_of_not_pairwiseDisjoint
    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
    ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x : α, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
x : α
hx : x ∈ t
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h

Result:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ t ≤ f i, t ≤ f j → t ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
replace ht : t.Nonempty := by
  rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : t.Nonempty
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : x ≠ x_1), ∃ x_2, ∃ (_ : x_2 ≤ f x) (_ : x_2 ≤ f x_1), ¬x_2 ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : ¬t ≤ ⊥
⊢ t.Nonempty

Tactic:
rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ i ∈ s, ∀ j ∈ s, i ≠ j → ∀ t ≤ f i, t ≤ f j → t ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
simp only [not_forall] at h

Result:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ∃ x, ∃ (_ : x ∈ s), ∃ x_1, ∃ (_ : x_1 ∈ s) (_ : x ≠ x_1), ∃ x_2, ∃ (_ : x_2 ≤ f x) (_ : x_2 ≤ f x_1), ¬x_2 ≤ ⊥
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
ht : t.Nonempty
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨x, hx⟩ := ht

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ≤ f i
hfj : t ≤ f j
x : α
hx : x ∈ t
⊢ ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j