awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ onFun.{u_1 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (a : α) ↦ f a '' t) x y

Tactic:
disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
refine_2 : LE.le.{u_3} (α := Set γ) ((fun (a : α) ↦ f a '' t) x ⊓ (fun (a : α) ↦ f a '' t) y) ⊥
⊢ onFun.{u_1 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (a : α) ↦ f a '' t) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
a : β
ha : a ∈ t
b : β
hb : b ∈ t
hab : f x a = f y b
⊢ Membership.mem (γ := Set γ) ⊥ (f y b)

Tactic:
h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Premises used: Set.Mem, Prod.fst, congr_arg, Set.mk_mem_prod
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
a : β
ha : a ∈ t
b : β
hb : b ∈ t
hab : f x a = f y b
⊢ Membership.mem (γ := Set γ) ⊥ (f y b)

Tactic:
exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Premises used: Prod.fst, congr_arg, Set.mk_mem_prod
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
⊢ (PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
refine_1 :
  ∀ (ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) (x : α × β)
    (hx : x ∈ s ×ˢ t) (y : α × β) (hy : y ∈ s ×ˢ t) (h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y), x = y
refine_2 :
  ∀ (ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)) (x : β) (hx : x ∈ t) (y : β) (hy : y ∈ t) (h : x ≠ y),
    onFun.{u_2 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) x y
⊢ (PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) ↔
    InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)

Tactic:
refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.2 = y.2
rw rw₁ : Eq.{u_3 + 1} (α := γ) ((fun (p : α × β) ↦ f p.1 p.2) y) ((fun (a : α) ↦ f a y.2) y.1)
⊢ Eq.{u_3 + 1} (α := γ) ((fun (p : α × β) ↦ f p.1 p.2) y) ((fun (a : α) ↦ f a x.2) y.1)

Tactic:
rw [this]
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
this : x.2 = y.2
⊢ x = y

Tactic:
exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this

Premises used: And.right, Prod.ext, Eq.trans
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : x.2 = y.2
⊢ x = y

Tactic:
suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ x.2 = y.2

Tactic:
ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)

Premises used: Iff.mpr, Set.not_disjoint_iff, And.right, And.left, Set.mem_image_of_mem, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) (f x.1 x.2)
⊢ x.2 = y.2

Tactic:
refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)

Premises used: Iff.mpr, Set.not_disjoint_iff, And.right, And.left, Set.mem_image_of_mem, Set.PairwiseDisjoint.elim, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
refine_1 : Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) ((fun (p : α × β) ↦ f p.1 p.2) y)
⊢ Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) (f x.1 x.2)

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) ((fun (p : α × β) ↦ f p.1 p.2) y)

Tactic:
mem_image_of_mem _ hy.1

Premises used: Set.Mem, And.left, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : PairwiseDisjoint.{u_3, u_2} (α := Set γ) t fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun (p : α × β) ↦ f p.1 p.2) y
⊢ Membership.mem (γ := Set γ) ((fun (a : α) ↦ f a y.2) '' s) ((fun (p : α × β) ↦ f p.1 p.2) y)

Tactic:
exact mem_image_of_mem _ hy.1

Premises used: And.left, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ onFun.{u_2 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) x y

Tactic:
disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
refine_2 :
  LE.le.{u_3} (α := Set γ)
    ((fun (b : β) ↦ ((fun (a : α) ↦ f a b) '' s : Set γ)) x ⊓ (fun (b : β) ↦ ((fun (a : α) ↦ f a b) '' s : Set γ)) y) ⊥
⊢ onFun.{u_2 + 1, u_3 + 1, 1} (β := Set γ) Disjoint (fun (b : β) ↦ (fun (a : α) ↦ f a b) '' s) x y

Tactic:
refine disjoint_iff_inf_le.mpr ?_

Premises used: Iff.mpr, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Eq.{u_3 + 1} (α := γ) ((fun (a : α) ↦ f a x) a) ((fun (a : α) ↦ f a y) b)
⊢ Membership.mem (γ := Set γ) ⊥ ((fun (a : α) ↦ f a y) b)

Tactic:
h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)

Premises used: Set.Mem, congr_arg, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective.{u_1 + 1, u_3 + 1} (β := γ) fun (a : α) ↦ f a b
ht : InjOn (β := γ) (fun (p : α × β) ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : Eq.{u_3 + 1} (α := γ) ((fun (a : α) ↦ f a x) a) ((fun (a : α) ↦ f a y) b)
⊢ Membership.mem (γ := Set γ) ⊥ ((fun (a : α) ↦ f a y) b)

Tactic:
exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)

Premises used: congr_arg, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ≤ f i → t ≤ f j → t ≤ ⊥

Tactic:
change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ≤ f i → t ≤ f j → t ≤ ⊥
⊢ ∃ (x : ι),
    ∃ (h : x ∈ s),
      ∃ (x_1 : ι), ∃ (h : x_1 ∈ s), ∃ (h : x ≠ x_1), ∃ (x_2 : Set α), ∃ (h : x_2 ≤ f x), ∃ (x : x_2 ≤ f x_1), ¬x_2 ≤ ⊥

Tactic:
simp only [not_forall] at h

Premises used: Classical.not_forall
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h :
  ∃ (x : ι),
    ∃ (h : x ∈ s),
      ∃ (x_1 : ι), ∃ (h : x_1 ∈ s), ∃ (h : x ≠ x_1), ∃ (x_2 : Set α), ∃ (h : x_2 ≤ f x), ∃ (x : x_2 ≤ f x_1), ¬x_2 ≤ ⊥
obtain :
  ∀ (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 : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : 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 ≤ ⊥
rwa : ∀ (ht : ¬t = ⊥), t.Nonempty
rwa₁ : ∀ (ht : ¬t = ∅), t.Nonempty
rwa₂ : ∀ (ht : t ≠ ∅), t.Nonempty
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (ht : t.Nonempty), t.Nonempty
⊢ t.Nonempty

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

Premises used: le_bot_iff, Ne, Set.bot_eq_empty, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : 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:
replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : 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
obtain : ∀ (x : α) (hx : x ∈ t), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
obtain ⟨x, hx⟩ := ht
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : 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 : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : 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 : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
obtain :
  ∀ (i : ι) (hi : i ∈ s) (j : ι) (hj : j ∈ s) (hne : i ≠ j) (x : α) (hx₁ : x ∈ f i) (hx₂ : x ∈ f j),
    ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h

Premises used: Set.exists_ne_mem_inter_of_not_pairwiseDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
inl : ∀ (h_lt : i < j), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
inr : ∀ (h_lt : j < i), ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt

Premises used: Iff.mpr, lt_or_lt_iff_ne
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
inst : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ (i : ι), i ∈ s ∧ ∃ (j : ι), j ∈ s ∧ i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → α
⊢ (PairwiseDisjoint.{u_1, u_4} (α := Set α) s fun (i : ι) ↦ {f i}) ↔ InjOn f s

Tactic:
simp [PairwiseDisjoint, InjOn, Set.Pairwise, not_imp_not]

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Set.InjOn, not_imp_not
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ¬Set.Pairwise univ (Disjoint on f)

Tactic:
rw [← pairwise_univ] at h

Premises used: Set.pairwise_univ
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
obtain :
  ∀ (i : ι) (_hi : Membership.mem (γ := Set ι) univ i) (j : ι) (_hj : Membership.mem (γ := Set ι) univ j)
    (h : i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j), ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h

Premises used: Set.exists_ne_mem_inter_of_not_pairwiseDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h_1 : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : Membership.mem (γ := Set ι) univ i
j : ι
_hj : Membership.mem (γ := Set ι) univ j
h : i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
⟨i, j, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
h_1 : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : Membership.mem (γ := Set ι) univ i
j : ι
_hj : Membership.mem (γ := Set ι) univ j
h : i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i ≠ j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ¬Set.Pairwise univ (Disjoint on f)

Tactic:
rw [← pairwise_univ] at h

Premises used: Set.pairwise_univ
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
obtain :
  ∀ (i : ι) (_hi : Membership.mem (γ := Set ι) univ i) (j : ι) (_hj : Membership.mem (γ := Set ι) univ j)
    (h : i < j ∧ ∃ (x : α), x ∈ f i ∩ f j), ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h

Premises used: Set.exists_lt_mem_inter_of_not_pairwiseDisjoint
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h_1 : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : Membership.mem (γ := Set ι) univ i
j : ι
_hj : Membership.mem (γ := Set ι) univ j
h : i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
⟨i, j, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder ι
f : ι → Set α
h_1 : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : Membership.mem (γ := Set ι) univ i
j : ι
_hj : Membership.mem (γ := Set ι) univ j
h : i < j ∧ ∃ (x : α), x ∈ f i ∩ f j
⊢ ∃ (i : ι), ∃ (j : ι), i < j ∧ ∃ (x : α), x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → α
⊢ Pairwise.{u_1} (α := α) (onFun.{u_1 + 1, u_4 + 1, 1} (β := Set ι) Disjoint fun (a : α) ↦ f ⁻¹' {a})

Tactic:
pairwise_univ.1 <| Set.pairwiseDisjoint_fiber f univ

Premises used: Set.univ, Set.pairwise_univ, Iff.mp, Set.pairwiseDisjoint_fiber
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → Set α
⊢ (∀ (a : α), Set.Subsingleton.{u_4} (α := ι) {i : ι | a ∈ f i}) ↔ Pairwise (Disjoint on f)

Tactic:
⟨fun h _ _ hij ↦ disjoint_left.2 fun a hi hj ↦ hij (h a hi hj),
   fun h _ _ hx _ hy ↦ by_contra fun hne ↦ disjoint_left.1 (h hne) hx hy⟩

Premises used: Iff.mpr, Set.disjoint_left, Iff.intro, Iff.mp, by_contra
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun (i j : ι) ↦ ¬f i = f j) ↔ Injective f

Tactic:
simp [Pairwise, Function.Injective, not_imp_not]

Premises used: Pairwise, Function.Injective, not_imp_not
-- Module: Mathlib.Data.Set.Pairwise.Basic
Goal:
α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun (i j : ι) ↦ f i ≠ f j) ↔ Injective f

Tactic:
simp
-- Module: Mathlib.Data.Set.Pairwise.Chain
Goal:
α : Type u_1
c : Set (Set α)
r : α → α → Prop
hc : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
⊢ Set.Pairwise (⋃ s ∈ c, s) r ↔ ∀ s ∈ c, s.Pairwise r

Tactic:
pairwise_iUnion₂_iff hc.directedOn

Premises used: IsChain.directedOn, Set.pairwise_iUnion₂_iff
-- Module: Mathlib.Data.Set.Pairwise.Chain
Goal:
α : Type u_1
β : Type u_2
c : Set (Set α)
hc : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
inst : PartialOrder β
inst_1 : OrderBot β
f : α → β
⊢ PairwiseDisjoint (⋃ s ∈ c, s) f ↔ ∀ s ∈ c, s.PairwiseDisjoint f

Tactic:
hc.pairwise_iUnion₂

Premises used: Set.PairwiseDisjoint, IsChain.pairwise_iUnion₂
-- Module: Mathlib.Data.Set.Pairwise.Chain
Goal:
α : Type u_1
c : Set (Set α)
r : α → α → Prop
hc : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
⊢ (⋃₀ c).Pairwise r ↔ ∀ s ∈ c, s.Pairwise r

Tactic:
Set.pairwise_sUnion hc.directedOn

Premises used: Set.pairwise_sUnion, IsChain.directedOn
-- Module: Mathlib.Data.Set.Pairwise.Chain
Goal:
α : Type u_1
β : Type u_2
c : Set (Set α)
hc : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
inst : PartialOrder β
inst_1 : OrderBot β
f : α → β
⊢ (⋃₀ c).PairwiseDisjoint f ↔ ∀ s ∈ c, s.PairwiseDisjoint f

Tactic:
hc.pairwise_sUnion

Premises used: Set.PairwiseDisjoint, IsChain.pairwise_sUnion
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
mp : Set.Pairwise (⋃ (n : κ), f n) r → ∀ (n : κ), (f n).Pairwise r
mpr : (∀ (n : κ), (f n).Pairwise r) → Set.Pairwise (⋃ (n : κ), f n) r
⊢ Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), (f n).Pairwise r

Tactic:
constructor
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : Set.Pairwise (⋃ (n : κ), f n) r
n : κ
⊢ (f n).Pairwise r

Tactic:
Pairwise.mono (subset_iUnion _ _) H

Premises used: Set.Pairwise.mono, Set.subset_iUnion
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : Set.Pairwise (⋃ (n : κ), f n) r
n : κ
⊢ (f n).Pairwise r

Tactic:
exact Pairwise.mono (subset_iUnion _ _) H

Premises used: Set.Pairwise.mono, Set.subset_iUnion
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : Membership.mem (γ := Set α) (⋃ (n : κ), f n) i
j : α
hj : Membership.mem (γ := Set α) (⋃ (n : κ), f n) j
hij : i ≠ j
mpr : ∀ (m : κ) (hm : i ∈ f m), r i j
⊢ r i j

Tactic:
rcases mem_iUnion.1 hi with ⟨m, hm⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Data.Set.Pairwise.Lattice
Goal:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : Membership.mem (γ := Set α) (⋃ (n : κ), f n) i
j : α
hj : Membership.mem (γ := Set α) (⋃ (n : κ), f n) j
hij : i ≠ j
m : κ
hm : i ∈ f m
mpr : ∀ (n : κ) (hn : j ∈ f n), r i j
⊢ r i j

Tactic:
rcases mem_iUnion.1 hj with ⟨n, hn⟩

Premises used: Set.mem_iUnion, Iff.mp