[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
p : α × β → Prop
⊢ (∃ x, x ∈ s ×ˢ t ∧ p x) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (x, y)
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
exact and_false_iff _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ ∅ ×ˢ t = ∅
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x✝ : α × β
⊢ x✝ ∈ ∅ ×ˢ t ↔ x✝ ∈ ∅
[PROOFSTEP]
exact false_and_iff _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ univ ×ˢ univ = univ
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x✝ : α × β
⊢ x✝ ∈ univ ×ˢ univ ↔ x✝ ∈ univ
[PROOFSTEP]
exact true_and_iff _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
t : Set β
⊢ univ ×ˢ t = Prod.snd ⁻¹' t
[PROOFSTEP]
simp [prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
s : Set α
⊢ s ×ˢ univ = Prod.fst ⁻¹' s
[PROOFSTEP]
simp [prod_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ {a} ×ˢ t = Prod.mk a '' t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ {b} = (fun a => (a, b)) '' s
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ {b} ↔ (x, y) ∈ (fun a => (a, b)) '' s
[PROOFSTEP]
simp [and_left_comm, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
[PROOFSTEP]
simp [or_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∪ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∪ s ×ˢ t₂
[PROOFSTEP]
simp [and_or_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∩ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∩ s₂ ×ˢ t
[PROOFSTEP]
simp only [← and_and_right, mem_inter_iff, mem_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
[PROOFSTEP]
simp only [← and_and_left, mem_inter_iff, mem_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
[PROOFSTEP]
simp [and_assoc, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
[PROOFSTEP]
simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ← @forall_or_left β, ←
  @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ insert a s ×ˢ t ↔ (x, y) ∈ Prod.mk a '' t ∪ s ×ˢ t
[PROOFSTEP]
simp (config := { contextual := true }) [image, iff_def, or_imp, Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t
[PROOFSTEP]
ext
  ⟨x, y⟩
      -- Porting note: was `simp (config := { contextual := true }) [image, iff_def, or_imp, Imp.swap]`
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ insert b t ↔ (x, y) ∈ (fun a => (a, b)) '' s ∪ s ×ˢ t
[PROOFSTEP]
simp [image, or_imp]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ x ∈ s ∧ (y = b ∨ y ∈ t) ↔ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => ?_⟩
[GOAL]
case h.mk.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : x ∈ s ∧ (y = b ∨ y ∈ t)
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
[PROOFSTEP]
obtain ⟨hx, rfl | hy⟩ := h
[GOAL]
case h.mk.refine_1.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a x : α
y : β
hx : x ∈ s
⊢ (∃ a, a ∈ s ∧ a = x ∧ y = y) ∨ x ∈ s ∧ y ∈ t
[PROOFSTEP]
exact Or.inl ⟨x, hx, rfl, rfl⟩
[GOAL]
case h.mk.refine_1.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
[PROOFSTEP]
exact Or.inr ⟨hx, hy⟩
[GOAL]
case h.mk.refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
h : (∃ a, a ∈ s ∧ a = x ∧ b = y) ∨ x ∈ s ∧ y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
[PROOFSTEP]
obtain ⟨x, hx, rfl, rfl⟩ | ⟨hx, hy⟩ := h
[GOAL]
case h.mk.refine_2.inl.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
hx : x ∈ s
⊢ x ∈ s ∧ (b = b ∨ b ∈ t)
[PROOFSTEP]
exact ⟨hx, Or.inl rfl⟩
[GOAL]
case h.mk.refine_2.inr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ x ∈ s ∧ (y = b ∨ y ∈ t)
[PROOFSTEP]
exact ⟨hx, Or.inr hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
hb : b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = s
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ s
[PROOFSTEP]
simp [hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ha : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b✝ : β
ha : a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ t
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
hb : ¬b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : ¬b ∈ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ ∅
[PROOFSTEP]
simp [hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ha : ¬a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b✝ : β
ha : ¬a ∈ s
b : β
⊢ b ∈ Prod.mk a ⁻¹' s ×ˢ t ↔ b ∈ ∅
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ t
h : b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = s
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ t
h : ¬b ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ s
h : a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = t
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ s
h : ¬a ∈ s
⊢ Prod.mk a ⁻¹' s ×ˢ t = ∅
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ t
f : γ → α
⊢ (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
[PROOFSTEP]
rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
inst✝ : DecidablePred fun x => x ∈ s
g : δ → β
⊢ (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅
[PROOFSTEP]
rw [← mk_preimage_prod_right_eq_if, prod_preimage_right, preimage_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
⊢ Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
x : β
y : α
⊢ (x, y) ∈ Prod.swap ⁻¹' s ×ˢ t ↔ (x, y) ∈ t ×ˢ s
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
⊢ Prod.swap '' s ×ˢ t = t ×ˢ s
[PROOFSTEP]
rw [image_swap_eq_preimage_swap, preimage_swap_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ (m₁ '' s) ×ˢ (m₂ '' t) ↔ x ∈ (fun p => (m₁ p.fst, m₂ p.snd)) '' s ×ˢ t
[PROOFSTEP]
simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
m₁ : α → γ
m₂ : β → δ
⊢ ∀ (x : γ × δ), x ∈ range m₁ ×ˢ range m₂ ↔ x ∈ range fun p => (m₁ p.fst, m₂ p.snd)
[PROOFSTEP]
simp [range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
m₁ : α → γ
⊢ ∀ (x : γ × β), x ∈ range m₁ ×ˢ univ ↔ x ∈ range fun p => (m₁ p.fst, p.snd)
[PROOFSTEP]
simp [range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
m₂ : β → δ
⊢ ∀ (x : α × δ), x ∈ univ ×ˢ range m₂ ↔ x ∈ range fun p => (p.fst, m₂ p.snd)
[PROOFSTEP]
simp [range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
⊢ (range fun x => (f x, g x)) ⊆ range f ×ˢ range g
[PROOFSTEP]
have : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x) := funext fun x => rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ (range fun x => (f x, g x)) ⊆ range f ×ˢ range g
[PROOFSTEP]
rw [this, ← range_prod_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
this : (fun x => (f x, g x)) = Prod.map f g ∘ fun x => (x, x)
⊢ range (Prod.map f g ∘ fun x => (x, x)) ⊆ range (Prod.map f g)
[PROOFSTEP]
apply range_comp_subset_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
[PROOFSTEP]
simp [subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
s : Set α
⊢ (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
f : α → β
g : α → γ
s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)
[PROOFSTEP]
exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
hb : b ∈ t
⊢ (fun a => (a, b)) '' s ⊆ s ×ˢ t
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a✝ : α
b : β
hb : b ∈ t
a : α
ha : a ∈ s
⊢ (fun a => (a, b)) a ∈ s ×ˢ t
[PROOFSTEP]
exact ⟨ha, hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ha : a ∈ s
⊢ Prod.mk a '' t ⊆ s ×ˢ t
[PROOFSTEP]
rintro _ ⟨b, hb, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b✝ : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (a, b) ∈ s ×ˢ t
[PROOFSTEP]
exact ⟨ha, hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
by_cases h₁ : x.1 ∈ s₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : x.fst ∈ s₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
by_cases h₂ : x.2 ∈ t₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : ¬x.fst ∈ s₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
by_cases h₂ : x.2 ∈ t₁
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : x.fst ∈ s₁
h₂ : ¬x.snd ∈ t₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : ¬x.fst ∈ s₁
h₂ : x.snd ∈ t₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α × β
h₁ : ¬x.fst ∈ s₁
h₂ : ¬x.snd ∈ t₁
⊢ x ∈ s ×ˢ t \ s₁ ×ˢ t₁ ↔ x ∈ s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
cases' (s ×ˢ t).eq_empty_or_nonempty with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [h, prod_eq_empty_iff.1 h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ Set.Nonempty s ∧ Set.Nonempty t
[PROOFSTEP]
rwa [prod_nonempty_iff] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
[PROOFSTEP]
refine' ⟨fun H => Or.inl ⟨_, _⟩, _⟩
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ s ⊆ s₁
[PROOFSTEP]
have := image_subset (Prod.fst : α × β → α) H
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁
[PROOFSTEP]
rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
⊢ t ⊆ t₁
[PROOFSTEP]
have := image_subset (Prod.snd : α × β → β) H
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.snd '' s ×ˢ t ⊆ Prod.snd '' s₁ ×ˢ t₁
⊢ t ⊆ t₁
[PROOFSTEP]
rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
[GOAL]
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
⊢ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ → s ×ˢ t ⊆ s₁ ×ˢ t₁
[PROOFSTEP]
intro H
[GOAL]
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
[PROOFSTEP]
simp only [st.1.ne_empty, st.2.ne_empty, or_false_iff] at H
[GOAL]
case inr.refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
st : Set.Nonempty s ∧ Set.Nonempty t
H : s ⊆ s₁ ∧ t ⊆ t₁
⊢ s ×ˢ t ⊆ s₁ ×ˢ t₁
[PROOFSTEP]
exact prod_mono H.1 H.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s₁ ×ˢ t₁ → s = s₁ ∧ t = t₁
[PROOFSTEP]
intro heq
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ s = s₁ ∧ t = t₁
[PROOFSTEP]
have h₁ : (s₁ ×ˢ t₁ : Set _).Nonempty := by rwa [← heq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
⊢ Set.Nonempty (s₁ ×ˢ t₁)
[PROOFSTEP]
rwa [← heq]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty (s₁ ×ˢ t₁)
⊢ s = s₁ ∧ t = t₁
[PROOFSTEP]
rw [prod_nonempty_iff] at h h₁
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty s ∧ Set.Nonempty t
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : Set.Nonempty s₁ ∧ Set.Nonempty t₁
⊢ s = s₁ ∧ t = t₁
[PROOFSTEP]
rw [← fst_image_prod s h.2, ← fst_image_prod s₁ h₁.2, heq, eq_self_iff_true, true_and_iff, ← snd_image_prod h.1 t, ←
  snd_image_prod h₁.1 t₁, heq]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ → s ×ˢ t = s₁ ×ˢ t₁
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s ×ˢ t = s ×ˢ t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
[PROOFSTEP]
cases' eq_empty_or_nonempty (s ×ˢ t) with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
[PROOFSTEP]
simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and_iff, or_iff_right_iff_imp]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case inl.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₂ : Set α
t t₂ : Set β
a : α
b : β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅
[PROOFSTEP]
exact prod_eq_empty_iff.mp h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁
[PROOFSTEP]
rw [prod_eq_prod_iff_of_nonempty h]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : Set.Nonempty (s ×ˢ t)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
[PROOFSTEP]
rw [nonempty_iff_ne_empty, Ne.def, prod_eq_empty_iff] at h
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
[PROOFSTEP]
simp_rw [h, false_and_iff, or_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
[PROOFSTEP]
simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true_iff, or_iff_left_iff_imp, or_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
ht : Set.Nonempty t
⊢ ∅ = ∅
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s t : Set α
x : α
⊢ (x, x) ∈ diagonal α
[PROOFSTEP]
simp [diagonal]
[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' diagonal α = diagonal ↑s
[PROOFSTEP]
ext ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
[GOAL]
case h.mk.mk.mk
α : Type u_1
s✝ t s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ({ val := x, property := hx }, { val := y, property := hy }) ∈ (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' diagonal α ↔
    ({ val := x, property := hx }, { val := y, property := hy }) ∈ diagonal ↑s
[PROOFSTEP]
simp [Set.diagonal]
[GOAL]
α : Type u_1
s t : Set α
⊢ (range fun x => (x, x)) = diagonal α
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case h.mk
α : Type u_1
s t : Set α
x y : α
⊢ ((x, y) ∈ range fun x => (x, x)) ↔ (x, y) ∈ diagonal α
[PROOFSTEP]
simp [diagonal, eq_comm]
[GOAL]
α : Type u_1
s✝ t : Set α
s : Set (α × α)
⊢ diagonal α ⊆ s ↔ ∀ (x : α), (x, x) ∈ s
[PROOFSTEP]
rw [← range_diag, range_subset_iff]
[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s ↔ x ∈ diagonal α ∩ s ×ˢ s
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ (fun x => (x, x)) '' s → x ∈ diagonal α ∩ s ×ˢ s
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
s✝ t s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (x, x)) x ∈ diagonal α ∩ s ×ˢ s
[PROOFSTEP]
exact ⟨rfl, hx, hx⟩
[GOAL]
case h.mpr
α : Type u_1
s✝ t s : Set α
x : α × α
⊢ x ∈ diagonal α ∩ s ×ˢ s → x ∈ (fun x => (x, x)) '' s
[PROOFSTEP]
obtain ⟨x, y⟩ := x
[GOAL]
case h.mpr.mk
α : Type u_1
s✝ t s : Set α
x y : α
⊢ (x, y) ∈ diagonal α ∩ s ×ˢ s → (x, y) ∈ (fun x => (x, x)) '' s
[PROOFSTEP]
rintro ⟨rfl : x = y, h2x⟩
[GOAL]
case h.mpr.mk.intro
α : Type u_1
s✝ t s : Set α
x : α
h2x : (x, x) ∈ s ×ˢ s
⊢ (x, x) ∈ (fun x => (x, x)) '' s
[PROOFSTEP]
exact mem_image_of_mem _ h2x.1
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
⊢ Set.Nonempty (offDiag s) ↔ Set.Nontrivial s
[PROOFSTEP]
simp [offDiag, Set.Nonempty, Set.Nontrivial]
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
⊢ offDiag s = ∅ ↔ Set.Subsingleton s
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, ← not_nontrivial_iff, offDiag_nonempty.not]
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
⊢ offDiag ∅ = ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a✝ a : α
⊢ offDiag {a} = ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
⊢ ∀ (x : α × α), x ∈ offDiag univ ↔ x ∈ (diagonal α)ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
x✝ : α × α
a : α
x : α × α
⊢ x ∈ offDiag (s ∩ t) ↔ x ∈ offDiag s ∩ offDiag t
[PROOFSTEP]
simp only [mem_offDiag, mem_inter_iff]
[GOAL]
α : Type u_1
s t : Set α
x✝ : α × α
a : α
x : α × α
⊢ (x.fst ∈ s ∧ x.fst ∈ t) ∧ (x.snd ∈ s ∧ x.snd ∈ t) ∧ x.fst ≠ x.snd ↔
    (x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd) ∧ x.fst ∈ t ∧ x.snd ∈ t ∧ x.fst ≠ x.snd
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
h : Disjoint s t
⊢ offDiag (s ∪ t) = offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ x ∈ offDiag (s ∪ t) ↔ x ∈ offDiag s ∪ offDiag t ∪ s ×ˢ t ∪ t ×ˢ s
[PROOFSTEP]
simp only [mem_offDiag, mem_union, ne_eq, mem_prod]
[GOAL]
case h
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd ↔
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd →
    ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
rintro ⟨h0 | h0, h1 | h1, h2⟩
[GOAL]
case h.mp.intro.inl.intro.inl
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h2 : ¬x.fst = x.snd
h1 : x.snd ∈ s
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
    x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
simp [h0, h1, h2]
[GOAL]
case h.mp.intro.inl.intro.inr
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h2 : ¬x.fst = x.snd
h1 : x.snd ∈ t
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
    x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
simp [h0, h1, h2]
[GOAL]
case h.mp.intro.inr.intro.inl
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h2 : ¬x.fst = x.snd
h1 : x.snd ∈ s
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
    x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
simp [h0, h1, h2]
[GOAL]
case h.mp.intro.inr.intro.inr
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h2 : ¬x.fst = x.snd
h1 : x.snd ∈ t
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
    x.fst ∈ t ∧ x.snd ∈ s
[PROOFSTEP]
simp [h0, h1, h2]
[GOAL]
case h.mpr
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
⊢ ((x.fst ∈ s ∧ x.snd ∈ s ∧ ¬x.fst = x.snd ∨ x.fst ∈ t ∧ x.snd ∈ t ∧ ¬x.fst = x.snd) ∨ x.fst ∈ s ∧ x.snd ∈ t) ∨
      x.fst ∈ t ∧ x.snd ∈ s →
    (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
[PROOFSTEP]
rintro (((⟨h0, h1, h2⟩ | ⟨h0, h1, h2⟩) | ⟨h0, h1⟩) | ⟨h0, h1⟩)
[GOAL]
case h.mpr.inl.inl.inl.intro.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ s
h2 : ¬x.fst = x.snd
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
[PROOFSTEP]
simp [*]
[GOAL]
case h.mpr.inl.inl.inr.intro.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ t
h2 : ¬x.fst = x.snd
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
[PROOFSTEP]
simp [*]
[GOAL]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
[PROOFSTEP]
simp [*]
[GOAL]
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
⊢ (x.fst ∈ s ∨ x.fst ∈ t) ∧ (x.snd ∈ s ∨ x.snd ∈ t) ∧ ¬x.fst = x.snd
[PROOFSTEP]
simp [*]
[GOAL]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
⊢ ¬x.fst = x.snd
[PROOFSTEP]
rintro h3
[GOAL]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
[PROOFSTEP]
rw [h3] at h0
[GOAL]
case h.mpr.inl.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ s
h1 : x.snd ∈ t
h3 : x.fst = x.snd
⊢ False
[PROOFSTEP]
exact (Set.disjoint_left.mp h h0 h1)
[GOAL]
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
⊢ ¬x.fst = x.snd
[PROOFSTEP]
rintro h3
[GOAL]
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.fst ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
[PROOFSTEP]
rw [h3] at h0
[GOAL]
case h.mpr.inr.intro
α : Type u_1
s t : Set α
x✝ : α × α
a : α
h : Disjoint s t
x : α × α
h0 : x.snd ∈ t
h1 : x.snd ∈ s
h3 : x.fst = x.snd
⊢ False
[PROOFSTEP]
exact (Set.disjoint_right.mp h h0 h1).elim
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ offDiag (insert a s) = offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}
[PROOFSTEP]
rw [insert_eq, union_comm, offDiag_union, offDiag_singleton, union_empty, union_right_comm]
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ Disjoint s {a}
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
α : Type u_1
s t : Set α
x : α × α
a : α
ha : ¬a ∈ s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ s → ¬a_1 ∈ {a}
[PROOFSTEP]
rintro b hb (rfl : b = a)
[GOAL]
α : Type u_1
s t : Set α
x : α × α
b : α
hb : b ∈ s
ha : ¬b ∈ s
⊢ False
[PROOFSTEP]
exact ha hb
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
⊢ f ∈ pi univ t ↔ ∀ (i : ι), f i ∈ t i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : (i : ι) → Set (α i)
⊢ pi ∅ s = univ
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ pi ∅ s ↔ x✝ ∈ univ
[PROOFSTEP]
simp [pi]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
x : (i : ι) → α i
⊢ (x ∈ pi s fun i => t i ∩ t₁ i) ↔ x ∈ pi s t ∩ pi s t₁
[PROOFSTEP]
simp only [forall_and, mem_pi, mem_inter_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
⊢ pi s t = ∅
[PROOFSTEP]
ext f
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ f ∈ pi s t ↔ f ∈ ∅
[PROOFSTEP]
simp only [mem_empty_iff_false, not_forall, iff_false_iff, mem_pi, not_imp]
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ∃ x, x ∈ s ∧ ¬f x ∈ t x
[PROOFSTEP]
exact ⟨i, hs, by simp [ht]⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
hs : i ∈ s
ht : t i = ∅
f : (i : ι) → α i
⊢ ¬f i ∈ t i
[PROOFSTEP]
simp [ht]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ Set.Nonempty (pi s t) ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ t i
[PROOFSTEP]
simp [Classical.skolem, Set.Nonempty]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ Set.Nonempty (pi univ t) ↔ ∀ (i : ι), Set.Nonempty (t i)
[PROOFSTEP]
simp [Classical.skolem, Set.Nonempty]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi s t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
refine' exists_congr fun i => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
cases isEmpty_or_nonempty (α i)
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
h✝ : IsEmpty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
simp [*, forall_and, eq_empty_iff_forall_not_mem]
[GOAL]
case inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
h✝ : Nonempty (α i)
⊢ (∀ (x : α i), i ∈ s ∧ ¬x ∈ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
[PROOFSTEP]
simp [*, forall_and, eq_empty_iff_forall_not_mem]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi univ t = ∅ ↔ ∃ i, t i = ∅
[PROOFSTEP]
simp [← not_nonempty_iff_eq_empty, univ_pi_nonempty_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ Disjoint (pi univ t₁) (pi univ t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)
[PROOFSTEP]
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, univ_pi_eq_empty_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ pi s t = ∅ ↔ ∃ i, i ∈ s ∧ t i = ∅
[PROOFSTEP]
simp [pi_eq_empty_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Disjoint (pi s t₁) (pi s t₂) ↔ ∃ i, i ∈ s ∧ Disjoint (t₁ i) (t₂ i)
[PROOFSTEP]
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
⊢ (range fun g i => f i (g i)) = pi univ fun i => range (f i)
[PROOFSTEP]
refine Subset.antisymm ?_ fun x hx => ?_
[GOAL]
case refine_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
⊢ (range fun g i => f i (g i)) ⊆ pi univ fun i => range (f i)
[PROOFSTEP]
rintro _ ⟨x, rfl⟩ i -
[GOAL]
case refine_1.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
f : (i : ι) → α i → β i
x : (i : ι) → α i
i : ι
⊢ (fun g i => f i (g i)) x i ∈ (fun i => range (f i)) i
[PROOFSTEP]
exact ⟨x i, rfl⟩
[GOAL]
case refine_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
hx : x ∈ pi univ fun i => range (f i)
⊢ x ∈ range fun g i => f i (g i)
[PROOFSTEP]
choose y hy using hx
[GOAL]
case refine_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
y : (i : ι) → i ∈ univ → α i
hy : ∀ (i : ι) (a : i ∈ univ), f i (y i a) = x i
⊢ x ∈ range fun g i => f i (g i)
[PROOFSTEP]
exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
s : Set ι
t : (i : ι) → Set (α i)
⊢ pi (insert i s) t = eval i ⁻¹' t i ∩ pi s t
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
s : Set ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ pi (insert i s) t ↔ x✝ ∈ eval i ⁻¹' t i ∩ pi s t
[PROOFSTEP]
simp [pi, or_imp, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
t : (i : ι) → Set (α i)
⊢ pi {i} t = eval i ⁻¹' t i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ x✝ ∈ pi {i} t ↔ x✝ ∈ eval i ⁻¹' t i
[PROOFSTEP]
simp [pi]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f g : (i : ι) → α i
⊢ (g ∈ pi univ fun i => {f i}) ↔ g ∈ {f}
[PROOFSTEP]
simp [funext_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (pi s fun i => if p i then t₁ i else t₂ i) = pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
[PROOFSTEP]
ext f
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ pi s fun i => if p i then t₁ i else t₂ i) ↔ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
[PROOFSTEP]
constructor
[GOAL]
case h.refine'_1.left
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁
[PROOFSTEP]
rintro i ⟨his, hpi⟩
[GOAL]
case h.refine'_1.left.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : p i
⊢ f i ∈ t₁ i
[PROOFSTEP]
simpa [*] using h i
[GOAL]
case h.refine'_1.right
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
⊢ f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
[PROOFSTEP]
rintro i ⟨his, hpi⟩
[GOAL]
case h.refine'_1.right.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i
[PROOFSTEP]
simpa [*] using h i
[GOAL]
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂ → f ∈ pi s fun i => if p i then t₁ i else t₂ i
[PROOFSTEP]
rintro ⟨ht₁, ht₂⟩ i his
[GOAL]
case h.refine'_2.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
[PROOFSTEP]
by_cases p i
[GOAL]
case h.refine'_2.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
[PROOFSTEP]
by_cases p i
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
h : p i
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
[PROOFSTEP]
simp_all
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
h : ¬p i
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
[PROOFSTEP]
simp_all
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi (s₁ ∪ s₂) t = pi s₁ t ∩ pi s₂ t
[PROOFSTEP]
simp [pi, or_imp, forall_and, setOf_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : Set ι
⊢ pi s t ∩ pi sᶜ t = pi univ t
[PROOFSTEP]
rw [← union_pi, union_compl_self]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ t j (update f i a j) = t j (f j)
[PROOFSTEP]
rw [update_noteq]
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : ¬i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i
[PROOFSTEP]
exact fun h => hi (h ▸ hj)
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi s fun j => t j (update f i a j)) = pi ({i} ∪ s \ {i}) fun j => t j (update f i a j)
[PROOFSTEP]
rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi ({i} ∪ s \ {i}) fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi (s \ {i}) fun j => t j (f j)
[PROOFSTEP]
rw [union_pi, singleton_pi', update_same, pi_update_of_not_mem]
[GOAL]
case hi
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
β✝ : ι → Type u_3
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
inst✝ : DecidableEq ι
β : ι → Type u_4
i : ι
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi univ fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi {i}ᶜ fun j => t j (f j)
[PROOFSTEP]
rw [compl_eq_univ_diff, ← pi_update_of_mem (mem_univ _)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ pi univ (update (fun j => univ) i s) = eval i ⁻¹' s
[PROOFSTEP]
rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
ht : Set.Nonempty (pi s t)
i : ι
⊢ t i ⊆ eval i '' pi s t
[PROOFSTEP]
classical
obtain ⟨f, hf⟩ := ht
refine' fun y hy => ⟨update f i y, fun j hj => _, update_same _ _ _⟩
obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
ht : Set.Nonempty (pi s t)
i : ι
⊢ t i ⊆ eval i '' pi s t
[PROOFSTEP]
obtain ⟨f, hf⟩ := ht
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
f : (i : ι) → α i
hf : f ∈ pi s t
⊢ t i ⊆ eval i '' pi s t
[PROOFSTEP]
refine' fun y hy => ⟨update f i y, fun j hj => _, update_same _ _ _⟩
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
f : (i : ι) → α i
hf : f ∈ pi s t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
⊢ update f i y j ∈ t j
[PROOFSTEP]
obtain rfl | hji := eq_or_ne j i
[GOAL]
case intro.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i
hf : f ∈ pi s t
j : ι
hj : j ∈ s
y : α j
hy : y ∈ t j
⊢ update f j y j ∈ t j
[PROOFSTEP]
simp [*, hf _ hj]
[GOAL]
case intro.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ i : ι
f : (i : ι) → α i
hf : f ∈ pi s t
y : α i
hy : y ∈ t i
j : ι
hj : j ∈ s
hji : j ≠ i
⊢ update f i y j ∈ t j
[PROOFSTEP]
simp [*, hf _ hj]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi s t₁ ⊆ pi s t₂ ↔ (∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i) ∨ pi s t₁ = ∅
[PROOFSTEP]
refine' ⟨fun h => or_iff_not_imp_right.2 _, fun h => h.elim pi_mono fun h' => h'.symm ▸ empty_subset _⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ ¬pi s t₁ = ∅ → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
[PROOFSTEP]
rw [← Ne.def, ← nonempty_iff_ne_empty]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
h : pi s t₁ ⊆ pi s t₂
⊢ Set.Nonempty (pi s t₁) → ∀ (i : ι), i ∈ s → t₁ i ⊆ t₂ i
[PROOFSTEP]
intro hne i hi
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
h : pi s t₁ ⊆ pi s t₂
hne : Set.Nonempty (pi s t₁)
i : ι
hi : i ∈ s
⊢ t₁ i ⊆ t₂ i
[PROOFSTEP]
simpa only [eval_image_pi hi hne, eval_image_pi hi (hne.mono h)] using image_subset (fun f : ∀ i, α i => f i) h
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
⊢ pi univ t₁ ⊆ pi univ t₂ ↔ (∀ (i : ι), t₁ i ⊆ t₂ i) ∨ ∃ i, t₁ i = ∅
[PROOFSTEP]
simp [pi_subset_pi_iff]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = pi univ (update (fun i => univ) i s)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x : (x : ι) → α x
⊢ x ∈ eval i ⁻¹' s ↔ x ∈ pi univ (update (fun i => univ) i s)
[PROOFSTEP]
simp [@forall_update_iff _ (fun i => Set (α i)) _ _ _ _ fun i' y => x i' ∈ y]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
⊢ eval i ⁻¹' s = pi {i} (update (fun i => univ) i s)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
s : Set (α i)
x✝ : (x : ι) → α x
⊢ x✝ ∈ eval i ⁻¹' s ↔ x✝ ∈ pi {i} (update (fun i => univ) i s)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' pi s t = t i
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
⊢ x ∈ update f i ⁻¹' pi s t ↔ x ∈ t i
[PROOFSTEP]
refine' ⟨fun h => _, fun hx j hj => _⟩
[GOAL]
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x ∈ t i
[PROOFSTEP]
convert h i hi
[GOAL]
case h.e'_4
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x = update f i x i
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
⊢ update f i x j ∈ t j
[PROOFSTEP]
obtain rfl | h := eq_or_ne j i
[GOAL]
case h.refine'_2.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
j : ι
hj hi : j ∈ s
hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1
x : α j
hx : x ∈ t j
⊢ update f j x j ∈ t j
[PROOFSTEP]
simpa
[GOAL]
case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j
[PROOFSTEP]
rw [update_noteq h]
[GOAL]
case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j
[PROOFSTEP]
exact hf j hj h
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
⊢ (pi univ fun i => if i ∈ s then t i else univ) = pi s t
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (x✝ ∈ pi univ fun i => if i ∈ s then t i else univ) ↔ x✝ ∈ pi s t
[PROOFSTEP]
simp_rw [mem_univ_pi]
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
⊢ (∀ (i : ι), x✝ i ∈ if i ∈ s then t i else univ) ↔ x✝ ∈ pi s t
[PROOFSTEP]
refine' forall_congr' fun i => _
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
⊢ (x✝ i ∈ if i ∈ s then t i else univ) ↔ i ∈ s → x✝ i ∈ t i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
h : i ∈ s
⊢ x✝ i ∈ t i ↔ i ∈ s → x✝ i ∈ t i
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s✝ s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
s : Set ι
inst✝ : DecidablePred fun x => x ∈ s
t : (i : ι) → Set (α i)
x✝ : (i : ι) → α i
i : ι
h : ¬i ∈ s
⊢ x✝ i ∈ univ ↔ i ∈ s → x✝ i ∈ t i
[PROOFSTEP]
simp [h]


[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ range some = Iio ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤
[PROOFSTEP]
rw [mem_Iio, lt_top_iff_ne_top, mem_range, ← none_eq_top, Option.ne_none_iff_exists]
[GOAL]
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ (∃ y, ↑y = x) ↔ ∃ x_1, Option.some x_1 = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Iio ⊤ = univ
[PROOFSTEP]
rw [← range_coe, preimage_range]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ⊤ = Ioi a
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioi a = Ioo ↑a ⊤
[PROOFSTEP]
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ici a = Ico ↑a ⊤
[PROOFSTEP]
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iio a = Iio ↑a
[PROOFSTEP]
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iic a = Iic ↑a
[PROOFSTEP]
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioi ⊥ = univ
[PROOFSTEP]
rw [← range_coe, preimage_range]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ⊥ ↑a = Iic a
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ⊥ ↑a = Iio a
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iio a = Ioo ⊥ ↑a
[PROOFSTEP]
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iic a = Ioc ⊥ ↑a
[PROOFSTEP]
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioi a = Ioi ↑a
[PROOFSTEP]
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ici a = Ici ↑a
[PROOFSTEP]
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ico_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]


[GOAL]
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ boolIndicator s x = true
[PROOFSTEP]
unfold boolIndicator
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ boolIndicator s x = false
[PROOFSTEP]
unfold boolIndicator
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ boolIndicator s ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ x ∈ boolIndicator s ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
simp only [boolIndicator, mem_preimage]
[GOAL]
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ boolIndicator s ⁻¹' t = univ ∨ boolIndicator s ⁻¹' t = s ∨ boolIndicator s ⁻¹' t = sᶜ ∨ boolIndicator s ⁻¹' t = ∅
[PROOFSTEP]
simp only [preimage_boolIndicator_eq_union]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅
[PROOFSTEP]
simp [s.union_compl_self]


[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⟩