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