[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a✝ b✝ : α
hr : Symmetric r
a b : α
⊢ Pairwise (r on fun c => bif c then a else b) ↔ r a b
[PROOFSTEP]
simpa [Pairwise, Function.onFun] using @hr a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
[PROOFSTEP]
rcases hs with ⟨y, hy⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
⊢ Set.Pairwise s (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
[PROOFSTEP]
refine' fun H => ⟨f y, fun x hx => _⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
⊢ r (f x) (f y)
[PROOFSTEP]
rcases eq_or_ne x y with (rfl | hne)
[GOAL]
case mp.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
H : Set.Pairwise s (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)
[PROOFSTEP]
apply IsRefl.refl
[GOAL]
case mp.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : Set.Pairwise s (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)
[PROOFSTEP]
exact H hx hy hne
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → Set.Pairwise s (r on f)
[PROOFSTEP]
rintro ⟨z, hz⟩ x hx y hy _
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
inst✝ : IsEquiv α r
s : Set ι
hs : Set.Nonempty s
z : α
hz : ∀ (x : ι), x ∈ s → r (f x) z
x : ι
hx : x ∈ s
y : ι
hy : y ∈ s
a✝ : x ≠ y
⊢ (r on f) x y
[PROOFSTEP]
exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (IsSymm.symm _ _ <| hz _ hy)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r✝ p q : α → α → Prop
f✝ g : ι → α
s✝ t u : Set α
a b : α
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with (rfl | hne)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r✝ p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ Set.Pairwise ∅ (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r✝ p q : α → α → Prop
f✝ g : ι → α
s✝ t u : Set α
a b : α
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : Set.Nonempty s
⊢ Set.Pairwise s (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
[PROOFSTEP]
exact hne.pairwise_iff_exists_forall
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise (s ∪ t) r ↔
    Set.Pairwise s r ∧ Set.Pairwise t r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a
[PROOFSTEP]
simp only [Set.Pairwise, mem_union, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ (((∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        ∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ↔
    (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → x ≠ x_1 → r x x_1) ∧
      (∀ (x : α), x ∈ t → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
        (∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ t → x ≠ x_1 → r x x_1) ∧
          ∀ (x : α), x ∈ s → ∀ (x_2 : α), x_2 ∈ t → x ≠ x_2 → r x_2 x
[PROOFSTEP]
exact
  ⟨fun H => ⟨H.1.1, H.2.2, H.2.1, fun x hx y hy hne => H.1.2 y hy x hx hne.symm⟩, fun H =>
    ⟨⟨H.1, fun x hx y hy hne => H.2.2.2 y hy x hx hne.symm⟩, H.2.2.1, H.2.1⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
⊢ (Set.Pairwise s r ∧ Set.Pairwise t r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a) ↔
    Set.Pairwise s r ∧ Set.Pairwise t r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b
[PROOFSTEP]
simp only [hr.iff, and_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a
[PROOFSTEP]
simp only [insert_eq, pairwise_union, pairwise_singleton, true_and_iff, mem_singleton_iff, forall_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b✝ : α
ha : ¬a ∈ s
b : α
hb : b ∈ s
⊢ a ≠ b → r a b ∧ r b a ↔ r a b ∧ r b a
[PROOFSTEP]
simp [(ne_of_mem_of_not_mem hb ha).symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b
[PROOFSTEP]
simp only [pairwise_insert, hr.iff a, and_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
ha : ¬a ∈ s
⊢ Set.Pairwise (insert a s) r ↔ Set.Pairwise s r ∧ ∀ (b : α), b ∈ s → r a b
[PROOFSTEP]
simp only [pairwise_insert_of_not_mem ha, hr.iff a, and_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a
[PROOFSTEP]
simp [pairwise_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
hr : Symmetric r
⊢ Set.Pairwise {a, b} r ↔ a ≠ b → r a b
[PROOFSTEP]
simp [pairwise_insert_of_symmetric hr]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s t u : Set α
a b : α
⊢ Set.Pairwise univ r ↔ Pairwise r
[PROOFSTEP]
simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
s : Set ι
h : InjOn f s
⊢ Set.Pairwise (f '' s) r ↔ Set.Pairwise s (r on f)
[PROOFSTEP]
simp (config := { contextual := true }) [h.eq_iff, Set.Pairwise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r✝ p q : α → α → Prop
s : Set α
r : α → α → Prop
⊢ (Pairwise fun x y => r ↑x ↑y) ↔ Set.Pairwise s r
[PROOFSTEP]
simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne.def, Subtype.ext_iff, Subtype.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
hs : PairwiseDisjoint s f
g : ι → ι
hg : f ∘ g ≤ f
⊢ PairwiseDisjoint (g '' s) f
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
hs : PairwiseDisjoint s f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)
[PROOFSTEP]
exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : PairwiseDisjoint s f
⊢ PairwiseDisjoint (Set.range g) f
[PROOFSTEP]
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : PairwiseDisjoint s f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)
[PROOFSTEP]
exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
⊢ PairwiseDisjoint (range singleton) id
[PROOFSTEP]
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
a b : ι
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
[PROOFSTEP]
exact disjoint_singleton.2 (ne_of_apply_ne _ h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
⊢ (PairwiseDisjoint s fun a => f a '' t) ↔ InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
[PROOFSTEP]
refine' ⟨fun hs x hx y hy (h : f _ _ = _) => _, fun hs x hx y hy h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x = y
[PROOFSTEP]
suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.fst = y.fst
⊢ x = y
[PROOFSTEP]
exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.fst = y.fst
⊢ (fun p => f p.fst p.snd) y = f x.fst y.snd
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x.fst = y.fst
[PROOFSTEP]
refine' hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, _⟩)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ f x.fst x.snd ∈ f y.fst '' t
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : PairwiseDisjoint s fun a => f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ (fun p => f p.fst p.snd) y ∈ f y.fst '' t
[PROOFSTEP]
exact mem_image_of_mem _ hy.2
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a => f a '' t) x y
[PROOFSTEP]
refine' disjoint_iff_inf_le.mpr _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (fun a => f a '' t) x ⊓ (fun a => f a '' t) y ≤ ⊥
[PROOFSTEP]
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p => f p.fst p.snd) (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
⊢ f y b ∈ ⊥
[PROOFSTEP]
exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
⊢ (PairwiseDisjoint t fun b => (fun a => f a b) '' s) ↔ InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
[PROOFSTEP]
refine' ⟨fun ht x hx y hy (h : f _ _ = _) => _, fun ht x hx y hy h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x = y
[PROOFSTEP]
suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.snd = y.snd
⊢ x = y
[PROOFSTEP]
exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
this : x.snd = y.snd
⊢ (fun p => f p.fst p.snd) y = (fun a => f a x.snd) y.fst
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ x.snd = y.snd
[PROOFSTEP]
refine' ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, _⟩)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ f x.fst x.snd ∈ (fun a => f a y.snd) '' s
[PROOFSTEP]
rw [h]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : PairwiseDisjoint t fun b => (fun a => f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.fst x.snd = (fun p => f p.fst p.snd) y
⊢ (fun p => f p.fst p.snd) y ∈ (fun a => f a y.snd) '' s
[PROOFSTEP]
exact mem_image_of_mem _ hy.1
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b => (fun a => f a b) '' s) x y
[PROOFSTEP]
refine' disjoint_iff_inf_le.mpr _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (fun b => (fun a => f a b) '' s) x ⊓ (fun b => (fun a => f a b) '' s) y ≤ ⊥
[PROOFSTEP]
rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s✝ : Set ι
t✝ : Set ι'
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a => f a b
ht : InjOn (fun p => f p.fst p.snd) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : (fun a => f a x) a = (fun a => f a y) b
⊢ (fun a => f a y) b ∈ ⊥
[PROOFSTEP]
exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
f : ι → Set α
h : ¬PairwiseDisjoint s f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
change ¬∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
f : ι → Set α
h : ¬∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → ∀ (t : Set α), t ≤ f i → t ≤ f j → t ≤ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
simp only [not_forall] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
f : ι → Set α
h : ∃ x h x_1 h h x_2 h x, ¬x_2 ≤ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t✝ : 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, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
replace ht : t.Nonempty := by rwa [le_bot_iff, bot_eq_empty, ← Ne.def, ← nonempty_iff_ne_empty] at ht 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t✝ : 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 ≤ ⊥
⊢ Set.Nonempty t
[PROOFSTEP]
rwa [le_bot_iff, bot_eq_empty, ← Ne.def, ← nonempty_iff_ne_empty] at ht 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t✝ : 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 : Set.Nonempty t
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
obtain ⟨x, hx⟩ := ht
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t✝ : 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 ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬PairwiseDisjoint s f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬PairwiseDisjoint s f
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 ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
cases' lt_or_lt_iff_ne.mpr hne with h_lt h_lt
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬PairwiseDisjoint s 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 ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
s : Set ι
t : Set ι'
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬PairwiseDisjoint s 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 ∧ ∃ _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
rw [← pairwise_univ] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
⊢ ∃ i j _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
f : ι → Set α
h✝ : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : ∃ _hij x, x ∈ f i ∩ f j
⊢ ∃ i j _hij x, x ∈ f i ∩ f j
[PROOFSTEP]
exact ⟨i, j, h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j x x, x ∈ f i ∩ f j
[PROOFSTEP]
rw [← pairwise_univ] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Set.Pairwise univ (Disjoint on f)
⊢ ∃ i j x x, x ∈ f i ∩ f j
[PROOFSTEP]
obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
r p q : α → α → Prop
inst✝ : LinearOrder ι
f : ι → Set α
h✝ : ¬Set.Pairwise univ (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : ∃ _hij x, x ∈ f i ∩ f j
⊢ ∃ i j x x, x ∈ f i ∩ f j
[PROOFSTEP]
exact ⟨i, j, h⟩
