[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋃ (i : ι) (j : κ i), s i j ↔ ∃ i j, x ∈ s i j
[PROOFSTEP]
simp_rw [mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
x : γ
s : (i : ι) → κ i → Set γ
⊢ x ∈ ⋂ (i : ι) (j : κ i), s i j ↔ ∀ (i : ι) (j : κ i), x ∈ s i j
[PROOFSTEP]
simp_rw [mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
src✝ : BooleanAlgebra (Set α) := instBooleanAlgebraSet
⊢ ∀ {ι : Type u_1} {κ : ι → Type u_1} (f : (a : ι) → κ a → Set α),
    ⨅ (a : ι), ⨆ (b : κ a), f a b = ⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a)
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
src✝ : BooleanAlgebra (Set α) := instBooleanAlgebraSet
ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
⊢ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f✝ a b = ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f✝ a (g a)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
src✝ : BooleanAlgebra (Set α) := instBooleanAlgebraSet
ι✝ : Type u_1
κ✝ : ι✝ → Type u_1
f✝ : (a : ι✝) → κ✝ a → Set α
x✝ : α
⊢ x✝ ∈ ⨅ (a : ι✝), ⨆ (b : κ✝ a), f✝ a b ↔ x✝ ∈ ⨆ (g : (a : ι✝) → κ✝ a), ⨅ (a : ι✝), f✝ a (g a)
[PROOFSTEP]
simp [Classical.skolem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
⊢ kernImage f sᶜ = (f '' s)ᶜ
[PROOFSTEP]
rw [kernImage_eq_compl, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ
[PROOFSTEP]
rw [kernImage_eq_compl, compl_empty, image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
[PROOFSTEP]
rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff, compl_subset_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s
[PROOFSTEP]
rw [← kernImage_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s
[PROOFSTEP]
exact kernImage_mono (empty_subset _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
[PROOFSTEP]
rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage, compl_inter,
  compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
t : Set β
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s
[PROOFSTEP]
rw [union_comm, kernImage_union_preimage, union_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
⊢ ∀ (a : Set α), a ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
t : Set ι
s : ι → Set β
w : ⋃ (i : ι) (_ : i ∈ t), s i = ⊤
x : β
⊢ ∃ i, i ∈ t ∧ x ∈ s i
[PROOFSTEP]
have p : x ∈ ⊤ := Set.mem_univ x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
t : Set ι
s : ι → Set β
w : ⋃ (i : ι) (_ : i ∈ t), s i = ⊤
x : β
p : x ∈ ⊤
⊢ ∃ i, i ∈ t ∧ x ∈ s i
[PROOFSTEP]
rw [← w, Set.mem_iUnion] at p 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
t : Set ι
s : ι → Set β
w : ⋃ (i : ι) (_ : i ∈ t), s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i, i ∈ t ∧ x ∈ s i
[PROOFSTEP]
simpa using p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ (i : ι) (_ : i ∈ t), s i = ⊤
⊢ Set.Nonempty t
[PROOFSTEP]
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ (i : ι) (_ : i ∈ t), s i = ⊤
x : ι
m : x ∈ t
⊢ Set.Nonempty t
[PROOFSTEP]
exact ⟨x, m⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
h_Union : Set.Nonempty (⋃ (i : ι), s i)
⊢ Nonempty ι
[PROOFSTEP]
obtain ⟨x, hx⟩ := h_Union
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
x : α
hx : x ∈ ⋃ (i : ι), s i
⊢ Nonempty ι
[PROOFSTEP]
exact ⟨Classical.choose $ mem_iUnion.mp hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
inst✝ : Nonempty α
h_Union : ⋃ (i : ι), s i = univ
⊢ Set.Nonempty (⋃ (i : ι), s i)
[PROOFSTEP]
simpa only [h_Union] using univ_nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
t : Set α
⊢ ⋃ (i : ι) (j : κ i), s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
[PROOFSTEP]
simp_rw [iUnion_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ⊆ ⋂ (i : ι) (j : κ i), t i j ↔ ∀ (i : ι) (j : κ i), s ⊆ t i j
[PROOFSTEP]
simp_rw [subset_iInter_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
P : ι → α → Prop
⊢ ⋃ (i : ι), {x | P i x} = {x | ∃ i, P i x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋃ (i : ι), {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}
[PROOFSTEP]
exact mem_iUnion
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
P : ι → α → Prop
⊢ ⋂ (i : ι), {x | P i x} = {x | ∀ (i : ι), P i x}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
P : ι → α → Prop
x✝ : α
⊢ x✝ ∈ ⋂ (i : ι), {x | P i x} ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
[PROOFSTEP]
exact mem_iInter
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
⊢ (⋃ (i : ι) (j : κ i), s i j)ᶜ = ⋂ (i : ι) (j : κ i), (s i j)ᶜ
[PROOFSTEP]
simp_rw [compl_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
⊢ (⋂ (i : ι) (j : κ i), s i j)ᶜ = ⋃ (i : ι) (j : κ i), (s i j)ᶜ
[PROOFSTEP]
simp_rw [compl_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set β
⊢ ⋃ (i : ι), s i = (⋂ (i : ι), (s i)ᶜ)ᶜ
[PROOFSTEP]
simp only [compl_iInter, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set β
⊢ ⋂ (i : ι), s i = (⋃ (i : ι), (s i)ᶜ)ᶜ
[PROOFSTEP]
simp only [compl_iUnion, compl_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ s \ ⋃ (i : ι), t i = ⋂ (i : ι), s \ t i
[PROOFSTEP]
rw [diff_eq, compl_iUnion, inter_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ ⋂ (i : ι), s ∩ (t i)ᶜ = ⋂ (i : ι), s \ t i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
t : ι → Set β
⊢ s \ ⋂ (i : ι), t i = ⋃ (i : ι), s \ t i
[PROOFSTEP]
rw [diff_eq, compl_iInter, inter_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
t : ι → Set β
⊢ ⋃ (i : ι), s ∩ (t i)ᶜ = ⋃ (i : ι), s \ t i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ DirectedOn r (⋃ (x : ι), f x)
[PROOFSTEP]
simp only [DirectedOn, exists_prop, mem_iUnion, exists_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
[PROOFSTEP]
exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
  let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
  let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
  ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k = v i
[PROOFSTEP]
classical
apply Subset.antisymm
· simp [iInter_subset]
· intro y y_in
  simp only [mem_image, mem_iInter, mem_preimage]
  rcases hv with ⟨z, hz⟩
  refine' ⟨Function.update z i y, _, update_same i y z⟩
  rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
  exact ⟨y_in, fun j _ => by simpa using hz j⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k = v i
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k ⊆ v i
[PROOFSTEP]
simp [iInter_subset]
[GOAL]
case h₂
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ v i ⊆ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
[PROOFSTEP]
intro y y_in
[GOAL]
case h₂
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
[PROOFSTEP]
simp only [mem_image, mem_iInter, mem_preimage]
[GOAL]
case h₂
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
[PROOFSTEP]
rcases hv with ⟨z, hz⟩
[GOAL]
case h₂.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
[PROOFSTEP]
refine' ⟨Function.update z i y, _, update_same i y z⟩
[GOAL]
case h₂.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1
[PROOFSTEP]
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
[GOAL]
case h₂.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
[PROOFSTEP]
exact ⟨y_in, fun j _ => by simpa using hz j⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : ι → Type u_12
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j
[PROOFSTEP]
simpa using hz j
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
⊢ Set.Nonempty (⋃ (i : ι), s i) ↔ ∃ i, Set.Nonempty (s i)
[PROOFSTEP]
simp [nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s✝ : ι → Set α
t : Set α
s : α → Set β
⊢ Set.Nonempty (⋃ (i : α) (_ : i ∈ t), s i) ↔ ∃ i, i ∈ t ∧ Set.Nonempty (s i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ ⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋃ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y (_ : p x ∧ q x y)
[PROOFSTEP]
simp only [iUnion_and, @iUnion_comm _ ι']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋃ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h = ⋃ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y (_ : p y ∧ q x y)
[PROOFSTEP]
simp only [iUnion_and, @iUnion_comm _ ι]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ ⋂ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h = ⋂ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y (_ : p x ∧ q x y)
[PROOFSTEP]
simp only [iInter_and, @iInter_comm _ ι']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι' → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p y ∧ q x y → Set α
⊢ ⋂ (x : ι) (y : ι') (h : p y ∧ q x y), s x y h = ⋂ (y : ι') (hy : p y) (x : ι) (hx : q x y), s x y (_ : p y ∧ q x y)
[PROOFSTEP]
simp only [iInter_and, @iInter_comm _ ι]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋃ (x : β) (h : x = b ∨ p x), s x h = s b (_ : b = b ∨ p b) ∪ ⋃ (x : β) (h : p x), s x (_ : x = b ∨ p x)
[PROOFSTEP]
simp only [iUnion_or, iUnion_union_distrib, iUnion_iUnion_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋂ (x : β) (h : x = b ∨ p x), s x h = s b (_ : b = b ∨ p b) ∩ ⋂ (x : β) (h : p x), s x (_ : x = b ∨ p x)
[PROOFSTEP]
simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
⊢ ⋃ (_ : Set.Nonempty s), s = s
[PROOFSTEP]
rw [iUnion_nonempty_index, biUnion_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
a : α
s : Set α
t : α → Set β
⊢ ⋂ (x : α) (_ : x ∈ insert a s), t x = t a ∩ ⋂ (x : α) (_ : x ∈ s), t x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
a b : α
s : α → Set β
⊢ ⋂ (x : α) (_ : x ∈ {a, b}), s x = s a ∩ s b
[PROOFSTEP]
rw [biInter_insert, biInter_singleton]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : Type u_12
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ ⋂ (i : ι) (_ : i ∈ s), f i ∩ t = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t
[PROOFSTEP]
haveI : Nonempty s := hs.to_subtype
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : Type u_12
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
this : Nonempty ↑s
⊢ ⋂ (i : ι) (_ : i ∈ s), f i ∩ t = (⋂ (i : ι) (_ : i ∈ s), f i) ∩ t
[PROOFSTEP]
simp [biInter_eq_iInter, ← iInter_inter]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : Type u_12
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ ⋂ (i : ι) (_ : i ∈ s), t ∩ f i = t ∩ ⋂ (i : ι) (_ : i ∈ s), f i
[PROOFSTEP]
rw [inter_comm, ← biInter_inter hs]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
α : Type u_12
s : Set ι
hs : Set.Nonempty s
f : ι → Set α
t : Set α
⊢ ⋂ (i : ι) (_ : i ∈ s), t ∩ f i = ⋂ (i : ι) (_ : i ∈ s), f i ∩ t
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
⊢ ∀ (x : α), x ∈ ⋃ (x : α) (_ : x ∈ s), {x} ↔ x ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
a : α
s : Set α
t : α → Set β
⊢ ⋃ (x : α) (_ : x ∈ insert a s), t x = t a ∪ ⋃ (x : α) (_ : x ∈ s), t x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
a b : α
s : α → Set β
⊢ ⋃ (x : α) (_ : x ∈ {a, b}), s x = s a ∪ s b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∩ ⋃ (i : ι) (j : κ i), t i j = ⋃ (i : ι) (j : κ i), s ∩ t i j
[PROOFSTEP]
simp only [inter_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋃ (i : ι) (j : κ i), s i j) ∩ t = ⋃ (i : ι) (j : κ i), s i j ∩ t
[PROOFSTEP]
simp_rw [iUnion_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ (i : ι) (j : κ i), t i j = ⋂ (i : ι) (j : κ i), s ∪ t i j
[PROOFSTEP]
simp_rw [union_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι) (j : κ i), s i j) ∪ t = ⋂ (i : ι) (j : κ i), s i j ∪ t
[PROOFSTEP]
simp_rw [iInter_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}
[PROOFSTEP]
simp only [mem_insert_iff, mem_singleton_iff, or_iff_not_imp_left, sUnion_eq_empty, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ (∃ x x_1, ¬x = ∅) → ⋃₀ S = univ
[PROOFSTEP]
rintro ⟨s, hs, hne⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
h : S ⊆ {∅, univ}
s : Set α
hs : s ∈ S
hne : ¬s = ∅
⊢ ⋃₀ S = univ
[PROOFSTEP]
obtain rfl : s = univ := (h hs).resolve_left hne
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
h : S ⊆ {∅, univ}
hs : univ ∈ S
hne : ¬univ = ∅
⊢ ⋃₀ S = univ
[PROOFSTEP]
exact univ_subset_iff.1 <| subset_sUnion_of_mem hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
⊢ Set.Nonempty (⋃₀ S) ↔ ∃ s, s ∈ S ∧ Set.Nonempty s
[PROOFSTEP]
simp [nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : ι → Set α
⊢ ⋃ (i : ι), f i = univ ↔ ∀ (x : α), ∃ i, x ∈ f i
[PROOFSTEP]
simp only [eq_univ_iff_forall, mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
⊢ ⋃ (i : ι) (j : κ i), s i j = univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
[PROOFSTEP]
simp only [iUnion_eq_univ_iff, mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
c : Set (Set α)
⊢ ⋃₀ c = univ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ a ∈ b
[PROOFSTEP]
simp only [eq_univ_iff_forall, mem_sUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : ι → Set α
⊢ ⋂ (i : ι), f i = ∅ ↔ ∀ (x : α), ∃ i, ¬x ∈ f i
[PROOFSTEP]
simp [Set.eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
⊢ ⋂ (i : ι) (j : κ i), s i j = ∅ ↔ ∀ (a : α), ∃ i j, ¬a ∈ s i j
[PROOFSTEP]
simp only [eq_empty_iff_forall_not_mem, mem_iInter, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b, b ∈ c ∧ ¬a ∈ b
[PROOFSTEP]
simp [Set.eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : ι → Set α
⊢ Set.Nonempty (⋂ (i : ι), f i) ↔ ∃ x, ∀ (i : ι), x ∈ f i
[PROOFSTEP]
simp [nonempty_iff_ne_empty, iInter_eq_empty_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
⊢ Set.Nonempty (⋂ (i : ι) (j : κ i), s i j) ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
c : Set (Set α)
⊢ Set.Nonempty (⋂₀ c) ↔ ∃ a, ∀ (b : Set α), b ∈ c → a ∈ b
[PROOFSTEP]
simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
x : α
⊢ x ∈ (⋃₀ S)ᶜ ↔ x ∈ ⋂₀ (compl '' S)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
⊢ ⋃₀ S = (⋂₀ (compl '' S))ᶜ
[PROOFSTEP]
rw [← compl_compl (⋃₀ S), compl_sUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)
[PROOFSTEP]
rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ
[PROOFSTEP]
rw [← compl_compl (⋂₀ S), compl_sInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
[PROOFSTEP]
exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
γ : α → Type u_11
f : Sigma γ → β
⊢ ∀ (x : β), x ∈ range f ↔ x ∈ ⋃ (a : α), range fun b => f { fst := a, snd := b }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : α → Set β
⊢ ⋃ (i : α), s i = range fun a => ↑a.snd
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set β
⊢ ⋃ (i : ι), s i = range fun a => ↑a.snd
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
⊢ ⋃ (i : ι), Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ ⋃ (i : ι), Sigma.mk i '' (Sigma.mk i ⁻¹' s) ↔ x ∈ s
[PROOFSTEP]
simp only [mem_iUnion, mem_image, mem_preimage]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) ↔ x ∈ s
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ (∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x) → x ∈ s
[PROOFSTEP]
rintro ⟨i, a, h, rfl⟩
[GOAL]
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ { fst := i, snd := a } ∈ s
[PROOFSTEP]
exact h
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
x : (i : ι) × σ i
⊢ x ∈ s → ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
x : (i : ι) × σ i
h : x ∈ s
⊢ ∃ i x_1, { fst := i, snd := x_1 } ∈ s ∧ { fst := i, snd := x_1 } = x
[PROOFSTEP]
cases' x with i a
[GOAL]
case h.mpr.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Type u_11
σ : ι → Type u_12
s : Set (Sigma σ)
i : ι
a : σ i
h : { fst := i, snd := a } ∈ s
⊢ ∃ i_1 x, { fst := i_1, snd := x } ∈ s ∧ { fst := i_1, snd := x } = { fst := i, snd := a }
[PROOFSTEP]
exact ⟨i, a, h, rfl⟩
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
f : α → β
⊢ ⋃ (x : α), {f x} = range f
[PROOFSTEP]
ext x
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
f : α → β
x : β
⊢ x ∈ ⋃ (x : α), {f x} ↔ x ∈ range f
[PROOFSTEP]
simp [@eq_comm _ x]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
⊢ ⋃ (x : α), {x} = univ
[PROOFSTEP]
simp [Set.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
⊢ ⋃ (i : ↑s), {↑i} = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (Set α)
⊢ ⋃₀ s = ⋃ (i : Set α) (_ : i ∈ s), i
[PROOFSTEP]
rw [← sUnion_image, image_id']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (Set α)
⊢ ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i
[PROOFSTEP]
rw [← sInter_image, image_id']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (Set α)
⊢ ⋃₀ s = ⋃ (i : ↑s), ↑i
[PROOFSTEP]
simp only [← sUnion_range, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (Set α)
⊢ ⋂₀ s = ⋂ (i : ↑s), ↑i
[PROOFSTEP]
simp only [← sInter_range, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
t : α → Set β
⊢ ⋃ (x : α) (_ : x ∈ ⋃ (i : ι), s i), t x = ⋃ (i : ι) (x : α) (_ : x ∈ s i), t x
[PROOFSTEP]
simp [@iUnion_comm _ ι]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
t : α → Set β
⊢ ⋂ (x : α) (_ : x ∈ ⋃ (i : ι), s i), t x = ⋂ (i : ι) (x : α) (_ : x ∈ s i), t x
[PROOFSTEP]
simp [@iInter_comm _ ι]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set (Set α)
⊢ ⋃₀ ⋃ (i : ι), s i = ⋃ (i : ι), ⋃₀ s i
[PROOFSTEP]
simp only [sUnion_eq_biUnion, biUnion_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set (Set α)
⊢ ⋂₀ ⋃ (i : ι), s i = ⋂ (i : ι), ⋂₀ s i
[PROOFSTEP]
simp only [sInter_eq_biInter, biInter_iUnion]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
⊢ (⋃ (y : β), range fun s => ↑(f s y)) = ⋃₀ C
[PROOFSTEP]
ext x
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) ↔ x ∈ ⋃₀ C
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ (x ∈ ⋃ (y : β), range fun s => ↑(f s y)) → x ∈ ⋃₀ C
[PROOFSTEP]
rintro ⟨s, ⟨y, rfl⟩, ⟨s, hs⟩, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro.mk
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ ⋃₀ C
[PROOFSTEP]
refine' ⟨_, hs, _⟩
[GOAL]
case h.mp.intro.intro.intro.intro.mk
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s => ↑(f s y)) { val := s, property := hs } ∈ s
[PROOFSTEP]
exact (f ⟨s, hs⟩ y).2
[GOAL]
case h.mpr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
⊢ x ∈ ⋃₀ C → x ∈ ⋃ (y : β), range fun s => ↑(f s y)
[PROOFSTEP]
rintro ⟨s, hs, hx⟩
[GOAL]
case h.mpr.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
[PROOFSTEP]
cases' hf ⟨s, hs⟩ ⟨x, hx⟩ with y hy
[GOAL]
case h.mpr.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ x ∈ ⋃ (y : β), range fun s => ↑(f s y)
[PROOFSTEP]
refine' ⟨_, ⟨y, rfl⟩, ⟨s, hs⟩, _⟩
[GOAL]
case h.mpr.intro.intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
α : Type u_11
β : Type u_12
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
x : α
s : Set α
hs : s ∈ C
hx : x ∈ s
y : β
hy : f { val := s, property := hs } y = { val := x, property := hx }
⊢ (fun s => ↑(f s y)) { val := s, property := hs } = x
[PROOFSTEP]
exact congr_arg Subtype.val hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
⊢ (⋃ (y : β), range fun x => ↑(f x y)) = ⋃ (x : ι), C x
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (x ∈ ⋃ (y : β), range fun x => ↑(f x y)) ↔ x ∈ ⋃ (x : ι), C x
[PROOFSTEP]
rw [mem_iUnion, mem_iUnion]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) ↔ ∃ i, x ∈ C i
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x => ↑(f x i)) → ∃ i, x ∈ C i
[PROOFSTEP]
rintro ⟨y, i, rfl⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ i_1, (fun x => ↑(f x y)) i ∈ C i_1
[PROOFSTEP]
exact ⟨i, (f i y).2⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ C i) → ∃ i, x ∈ range fun x => ↑(f x i)
[PROOFSTEP]
rintro ⟨i, hx⟩
[GOAL]
case h.mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
[PROOFSTEP]
cases' hf i ⟨x, hx⟩ with y hy
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
i : ι
hx : x ∈ C i
y : β
hy : f i y = { val := x, property := hx }
⊢ ∃ i, x ∈ range fun x => ↑(f x i)
[PROOFSTEP]
exact ⟨y, i, congr_arg Subtype.val hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ (i : ι) (j : κ i), t i j = ⋂ (i : ι) (j : κ i), s ∪ t i j
[PROOFSTEP]
simp_rw [union_distrib_iInter_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι) (j : κ i), s i j) ∪ t = ⋂ (i : ι) (j : κ i), s i j ∪ t
[PROOFSTEP]
simp_rw [union_distrib_iInter_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ (s : Set α) (_ : s ∈ S), f '' s
[PROOFSTEP]
rw [sInter_eq_biInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
f : α → β
⊢ f '' ⋂ (i : Set α) (_ : i ∈ S), i ⊆ ⋂ (s : Set α) (_ : s ∈ S), f '' s
[PROOFSTEP]
apply image_iInter₂_subset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective (restrictPreimage (U i) f)
[PROOFSTEP]
refine' ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ x = y
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (show f x ∈ Set.iUnion U by rw [hU]; triv)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U
[PROOFSTEP]
rw [hU]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
⊢ f x ∈ univ
[PROOFSTEP]
triv
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective (restrictPreimage (U i) f)
x y : α
e : f x = f y
i : ι
hi : f x ∈ U i
⊢ x = y
[PROOFSTEP]
injection @H i ⟨x, hi⟩ ⟨y, show f y ∈ U i from e ▸ hi⟩ (Subtype.ext e)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective (restrictPreimage (U i) f)
[PROOFSTEP]
refine' ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ ∃ a, f a = x
[PROOFSTEP]
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (show x ∈ Set.iUnion U by rw [hU]; triv)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ x ∈ iUnion U
[PROOFSTEP]
rw [hU]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
⊢ x ∈ univ
[PROOFSTEP]
triv
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective (restrictPreimage (U i) f)
x : β
i : ι
hi : x ∈ U i
⊢ ∃ a, f a = x
[PROOFSTEP]
exact ⟨_, congr_arg Subtype.val (H i ⟨x, hi⟩).choose_spec⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective (restrictPreimage (U i) f)
[PROOFSTEP]
rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU, surjective_iff_surjective_of_iUnion_eq_univ hU]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set β
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective (restrictPreimage (U i) f)) ∧ ∀ (i : ι), Surjective (restrictPreimage (U i) f)) ↔
    ∀ (i : ι), Bijective (restrictPreimage (U i) f)
[PROOFSTEP]
simp [Bijective, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
[PROOFSTEP]
inhabit ι
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
[PROOFSTEP]
refine' Subset.antisymm (image_iInter_subset s f) fun y hy => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : y ∈ ⋂ (i : ι), f '' s i
⊢ y ∈ f '' ⋂ (i : ι), s i
[PROOFSTEP]
simp only [mem_iInter, mem_image_iff_bex] at hy 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x x_1, f x = y
⊢ y ∈ f '' ⋂ (i : ι), s i
[PROOFSTEP]
choose x hx hy using hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ (i : ι), s i
[PROOFSTEP]
refine' ⟨x default, mem_iInter.2 fun i => _, hy _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default ∈ s i
[PROOFSTEP]
suffices x default = x i by
  rw [this]
  apply hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i
[PROOFSTEP]
apply hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default = x i
[PROOFSTEP]
replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ x default = x i
[PROOFSTEP]
apply h (hx _) (hx _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), x i ∈ ⋃ (j : ι), s j
⊢ f (x default) = f (x i)
[PROOFSTEP]
simp only [hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
⊢ f '' ⋂ (i : ι) (hi : p i), s i hi = ⋂ (i : ι) (hi : p i), f '' s i hi
[PROOFSTEP]
simp only [iInter, iInf_subtype']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
⊢ f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
[PROOFSTEP]
haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ f '' ⨅ (x : { i // p i }), s ↑x (_ : p ↑x) = ⨅ (x : { i // p i }), f '' s ↑x (_ : p ↑x)
[PROOFSTEP]
apply InjOn.image_iInter_eq
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ (i : ι) (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ (i : { i // p i }), s ↑i (_ : p ↑i))
[PROOFSTEP]
simpa only [iUnion, iSup_subtype'] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
hf : Bijective f
s : ι → Set α
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
[PROOFSTEP]
simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : Nonempty ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
[PROOFSTEP]
exact (hf.injective.injOn _).image_iInter_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
hf : Bijective f
s : (i : ι) → κ i → Set α
⊢ f '' ⋂ (i : ι) (j : κ i), s i j = ⋂ (i : ι) (j : κ i), f '' s i j
[PROOFSTEP]
simp_rw [image_iInter hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ (i : ι), s i)
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
rcases mem_iUnion.1 hx with ⟨i, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y
[PROOFSTEP]
rcases mem_iUnion.1 hy with ⟨j, hy⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
[PROOFSTEP]
rcases hs i j with ⟨k, hi, hj⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
hs : Directed (fun x x_1 => x ⊆ x_1) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ (i : ι), s i
y : α
hy✝ : y ∈ ⋃ (i : ι), s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y
[PROOFSTEP]
exact hf k (hi hx) (hj hy) hxy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
⊢ SurjOn f (⋂ (i : ι), s i) t
[PROOFSTEP]
intro y hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ (i : ι), s i
[PROOFSTEP]
rw [Hinj.image_iInter_eq, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i
[PROOFSTEP]
exact fun i => H i hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set α
⊢ f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set α
x : β
⊢ x ∈ f '' ⋃ (i : ι), s i ↔ x ∈ ⋃ (i : ι), f '' s i
[PROOFSTEP]
simp only [mem_image, mem_iUnion, ← exists_and_right, ← exists_and_left]
  --Porting note: `exists_swap` causes a `simp` loop in Lean4 so we use `rw` instead.
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set α
x : β
⊢ (∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i x_1, x_1 ∈ s i ∧ f x_1 = x
[PROOFSTEP]
rw [exists_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ (i : ι) (j : κ i), s i j = ⋃ (i : ι) (j : κ i), f '' s i j
[PROOFSTEP]
simp_rw [image_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ { val := x, property := h } ∈ univ ↔ { val := x, property := h } ∈ ⋃ (x : α) (h : p x), {{ val := x, property := h }}
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι' → Sort u_10
ι : Sort u_11
f : ι → α
a : α
⊢ a ∈ range f ↔ a ∈ ⋃ (i : ι), {f i}
[PROOFSTEP]
simp [@eq_comm α a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ b ∈ ⋃ (i : α) (_ : i ∈ s), {f i}
[PROOFSTEP]
simp [@eq_comm β b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : ι → α
g : α → Set β
⊢ ⋃ (x : α) (y : ι) (_ : f y = x), g x = ⋃ (y : ι), g (f y)
[PROOFSTEP]
simpa using biUnion_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : ι → α
g : α → Set β
⊢ ⋂ (x : α) (y : ι) (_ : f y = x), g x = ⋂ (y : ι), g (f y)
[PROOFSTEP]
simpa using biInter_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set β
⊢ ∀ (x : α), x ∈ f ⁻¹' ⋃ (i : ι), s i ↔ x ∈ ⋃ (i : ι), f ⁻¹' s i
[PROOFSTEP]
simp [preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ (i : ι) (j : κ i), s i j = ⋃ (i : ι) (j : κ i), f ⁻¹' s i j
[PROOFSTEP]
simp_rw [preimage_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ (t : Set β) (_ : t ∈ s), f ⁻¹' t
[PROOFSTEP]
rw [sUnion_eq_biUnion, preimage_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ (i : ι), s i = ⋂ (i : ι), f ⁻¹' s i
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ (i : ι), s i ↔ x✝ ∈ ⋂ (i : ι), f ⁻¹' s i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋂ (i : ι) (j : κ i), s i j = ⋂ (i : ι) (j : κ i), f ⁻¹' s i j
[PROOFSTEP]
simp_rw [preimage_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋂₀ s = ⋂ (t : Set β) (_ : t ∈ s), f ⁻¹' t
[PROOFSTEP]
rw [sInter_eq_biInter, preimage_iInter₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
s : Set β
⊢ ⋃ (y : β) (_ : y ∈ s), f ⁻¹' {y} = f ⁻¹' s
[PROOFSTEP]
rw [← preimage_iUnion₂, biUnion_of_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
⊢ ⋃ (y : β) (_ : y ∈ range f), f ⁻¹' {y} = univ
[PROOFSTEP]
rw [biUnion_preimage_singleton, preimage_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : ι → Set β
⊢ s ×ˢ ⋃ (i : ι), t i = ⋃ (i : ι), s ×ˢ t i
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : ι → Set β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ⋃ (i : ι), t i ↔ x✝ ∈ ⋃ (i : ι), s ×ˢ t i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : (i : ι) → κ i → Set β
⊢ s ×ˢ ⋃ (i : ι) (j : κ i), t i j = ⋃ (i : ι) (j : κ i), s ×ˢ t i j
[PROOFSTEP]
simp_rw [prod_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
[PROOFSTEP]
simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
t : Set β
⊢ (⋃ (i : ι), s i) ×ˢ t = ⋃ (i : ι), s i ×ˢ t
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ (i : ι), s i) ×ˢ t ↔ x✝ ∈ ⋃ (i : ι), s i ×ˢ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : (i : ι) → κ i → Set α
t : Set β
⊢ (⋃ (i : ι) (j : κ i), s i j) ×ˢ t = ⋃ (i : ι) (j : κ i), s i j ×ˢ t
[PROOFSTEP]
simp_rw [iUnion_prod_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun s => s ×ˢ t) '' C)
[PROOFSTEP]
simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι'✝ : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι'✝ → Sort u_10
ι : Type u_11
ι' : Type u_12
α : Type u_13
β : Type u_14
s : ι → Set α
t : ι' → Set β
⊢ ⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
[PROOFSTEP]
ext
[GOAL]
case h
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι'✝ : Sort u_5
ι₂ : Sort u_6
κ : ι✝ → Sort u_7
κ₁ : ι✝ → Sort u_8
κ₂ : ι✝ → Sort u_9
κ' : ι'✝ → Sort u_10
ι : Type u_11
ι' : Type u_12
α : Type u_13
β : Type u_14
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ x✝ ∈ ⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd ↔ x✝ ∈ (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
⊢ ⋃ (x : α), s x ×ˢ t x = (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
[PROOFSTEP]
ext ⟨z, w⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (z, w) ∈ ⋃ (x : α), s x ×ˢ t x ↔ (z, w) ∈ (⋃ (x : α), s x) ×ˢ ⋃ (x : α), t x
[PROOFSTEP]
simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ (∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i) ∧
    ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
[PROOFSTEP]
constructor
[GOAL]
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → w ∈ t x → (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
[PROOFSTEP]
intro x hz hw
[GOAL]
case h.mk.left
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i
[PROOFSTEP]
exact ⟨⟨x, hz⟩, x, hw⟩
[GOAL]
case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
⊢ ∀ (x : α), z ∈ s x → ∀ (x : α), w ∈ t x → ∃ i, z ∈ s i ∧ w ∈ t i
[PROOFSTEP]
intro x hz x' hw
[GOAL]
case h.mk.right
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
x' : α
hw : w ∈ t x'
⊢ ∃ i, z ∈ s i ∧ w ∈ t i
[PROOFSTEP]
exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
T : Set (Set β)
hS : Set.Nonempty S
hT : Set.Nonempty T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
[PROOFSTEP]
obtain ⟨s₁, h₁⟩ := hS
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
T : Set (Set β)
hT : Set.Nonempty T
s₁ : Set α
h₁ : s₁ ∈ S
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
[PROOFSTEP]
obtain ⟨s₂, h₂⟩ := hT
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
⊢ ⋂₀ S ×ˢ ⋂₀ T = ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
[PROOFSTEP]
refine' Set.Subset.antisymm (sInter_prod_sInter_subset S T) fun x hx => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : x ∈ ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ T), r.fst ×ˢ r.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
[PROOFSTEP]
rw [mem_iInter₂] at hx 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
T : Set (Set β)
s₁ : Set α
h₁ : s₁ ∈ S
s₂ : Set β
h₂ : s₂ ∈ T
x : α × β
hx : ∀ (i : Set α × Set β), i ∈ S ×ˢ T → x ∈ i.fst ×ˢ i.snd
⊢ x ∈ ⋂₀ S ×ˢ ⋂₀ T
[PROOFSTEP]
exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
hS : Set.Nonempty S
t : Set β
⊢ ⋂₀ S ×ˢ t = ⋂ (s : Set α) (_ : s ∈ S), s ×ˢ t
[PROOFSTEP]
rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
S : Set (Set α)
hS : Set.Nonempty S
t : Set β
⊢ ⋂ (r : Set α × Set β) (_ : r ∈ S ×ˢ {t}), r.fst ×ˢ r.snd = ⋂ (s : Set α) (_ : s ∈ S), s ×ˢ t
[PROOFSTEP]
simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
T : Set (Set β)
hT : Set.Nonempty T
s : Set α
⊢ s ×ˢ ⋂₀ T = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t
[PROOFSTEP]
rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
T : Set (Set β)
hT : Set.Nonempty T
s : Set α
⊢ ⋂ (r : Set α × Set β) (_ : r ∈ {s} ×ˢ T), r.fst ×ˢ r.snd = ⋂ (t : Set β) (_ : t ∈ T), s ×ˢ t
[PROOFSTEP]
simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ (a : α) (_ : a ∈ s), f a '' t = image2 f s t
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ ⋃ (a : α) (_ : a ∈ s), f a '' t ↔ y ∈ image2 f s t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ ⋃ (a : α) (_ : a ∈ s), f a '' t → y ∈ image2 f s t
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ image2 f s t → y ∈ ⋃ (a : α) (_ : a ∈ s), f a '' t
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (∃ i i_1, y ∈ f i '' t) → y ∈ image2 f s t
[PROOFSTEP]
rintro ⟨a, ha, x, hx, ax⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ image2 f s t → ∃ i i_1, y ∈ f i '' t
[PROOFSTEP]
rintro ⟨a, ha, x, hx, ax⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
ha : a ∈ s
x : β
hx : x ∈ t
ax : f a x = y
⊢ y ∈ image2 f s t
[PROOFSTEP]
exact ⟨a, x, ha, hx, ax⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
ha : β
x : a ∈ s
hx : ha ∈ t
ax : f a ha = y
⊢ ∃ i i_1, y ∈ f i '' t
[PROOFSTEP]
exact ⟨a, x, ha, hx, ax⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
⊢ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s = image2 f s t
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s ↔ y ∈ image2 f s t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s → y ∈ image2 f s t
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ image2 f s t → y ∈ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (∃ i i_1, y ∈ (fun a => f a i) '' s) → y ∈ image2 f s t
[PROOFSTEP]
rintro ⟨a, b, c, d, e⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ y ∈ image2 f s t → ∃ i i_1, y ∈ (fun a => f a i) '' s
[PROOFSTEP]
rintro ⟨a, b, c, d, e⟩
[GOAL]
case h.mp.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
a : β
b : a ∈ t
c : α
d : c ∈ s
e : (fun a_1 => f a_1 a) c = y
⊢ y ∈ image2 f s t
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
[PROOFSTEP]
exact ⟨c, a, d, b, e⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
[PROOFSTEP]
exact ⟨b, d, a, c, e⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ image2 f (⋃ (i : ι), s i) t = ⋃ (i : ι), image2 f (s i) t
[PROOFSTEP]
simp only [← image_prod, iUnion_prod_const, image_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : ι → Set β
⊢ image2 f s (⋃ (i : ι), t i) = ⋃ (i : ι), image2 f s (t i)
[PROOFSTEP]
simp only [← image_prod, prod_iUnion, image_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ (i : ι) (j : κ i), s i j) t = ⋃ (i : ι) (j : κ i), image2 f (s i j) t
[PROOFSTEP]
simp_rw [image2_iUnion_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋃ (i : ι) (j : κ i), t i j) = ⋃ (i : ι) (j : κ i), image2 f s (t i j)
[PROOFSTEP]
simp_rw [image2_iUnion_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ image2 f (⋂ (i : ι), s i) t ⊆ ⋂ (i : ι), image2 f (s i) t
[PROOFSTEP]
simp_rw [image2_subset_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : ι → Set α
t : Set β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ (y : β), y ∈ t → ∀ (i : ι), f x y ∈ image2 f (s i) t
[PROOFSTEP]
exact fun x hx y hy i => mem_image2_of_mem (hx _) hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : ι → Set β
⊢ image2 f s (⋂ (i : ι), t i) ⊆ ⋂ (i : ι), image2 f s (t i)
[PROOFSTEP]
simp_rw [image2_subset_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : ι → Set β
⊢ ∀ (x : α), x ∈ s → ∀ (y : β), (∀ (i : ι), y ∈ t i) → ∀ (i : ι), f x y ∈ image2 f s (t i)
[PROOFSTEP]
exact fun x hx y hy i => mem_image2_of_mem hx (hy _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ (i : ι) (j : κ i), s i j) t ⊆ ⋂ (i : ι) (j : κ i), image2 f (s i j) t
[PROOFSTEP]
simp_rw [image2_subset_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : (i : ι) → κ i → Set α
t : Set β
⊢ ∀ (x : α),
    (∀ (i : ι) (i_1 : κ i), x ∈ s i i_1) → ∀ (y : β), y ∈ t → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f (s i i_1) t
[PROOFSTEP]
exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ image2 f s (⋂ (i : ι) (j : κ i), t i j) ⊆ ⋂ (i : ι) (j : κ i), image2 f s (t i j)
[PROOFSTEP]
simp_rw [image2_subset_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : (i : ι) → κ i → Set β
⊢ ∀ (x : α),
    x ∈ s → ∀ (y : β), (∀ (i : ι) (i_1 : κ i), y ∈ t i i_1) → ∀ (i : ι) (i_1 : κ i), f x y ∈ image2 f s (t i i_1)
[PROOFSTEP]
exact fun x hx y hy i j => mem_image2_of_mem hx (hy _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s✝ : Set α
t✝ : Set β
s : Set α
t : Set β
⊢ image2 f s t = ⋃ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), {f i j}
[PROOFSTEP]
simp_rw [← image_eq_iUnion, iUnion_image_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ (a : α) (_ : a ∈ s), (fun b => (a, b)) '' t
[PROOFSTEP]
rw [iUnion_image_left, image2_mk_eq_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ (b : β) (_ : b ∈ t), (fun a => (a, b)) '' s
[PROOFSTEP]
rw [iUnion_image_right, image2_mk_eq_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (α → β)
t : Set α
⊢ ∀ (x : β), x ∈ seq s t ↔ x ∈ ⋃ (f : α → β) (_ : f ∈ s), f '' t
[PROOFSTEP]
simp [seq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β
t : Set α
⊢ ∀ (x : β), x ∈ seq {f} t ↔ x ∈ f '' t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (α → β)
a : α
⊢ ∀ (x : β), x ∈ seq s {a} ↔ x ∈ (fun f => f a) '' s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ seq s (seq t u) = seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
[PROOFSTEP]
refine' Set.ext fun c => Iff.intro _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq s (seq t u) → c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
[PROOFSTEP]
rintro ⟨f, hfs, b, ⟨g, hg, a, hau, rfl⟩, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (β → γ)
t : Set (α → β)
u : Set α
f : β → γ
hfs : f ∈ s
g : α → β
hg : g ∈ t
a : α
hau : a ∈ u
⊢ f (g a) ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u
[PROOFSTEP]
exact ⟨f ∘ g, ⟨(· ∘ ·) f, mem_image_of_mem _ hfs, g, hg, rfl⟩, a, hau, rfl⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (β → γ)
t : Set (α → β)
u : Set α
c : γ
⊢ c ∈ seq (seq ((fun x x_1 => x ∘ x_1) '' s) t) u → c ∈ seq s (seq t u)
[PROOFSTEP]
rintro ⟨fg, ⟨fc, ⟨f, hfs, rfl⟩, g, hgt, rfl⟩, a, ha, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set (β → γ)
t : Set (α → β)
u : Set α
f : β → γ
hfs : f ∈ s
g : α → β
hgt : g ∈ t
a : α
ha : a ∈ u
⊢ (fun x x_1 => x ∘ x_1) f g a ∈ seq s (seq t u)
[PROOFSTEP]
exact ⟨f, hfs, g a, ⟨g, hgt, a, ha, rfl⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' seq s t = seq ((fun x x_1 => x ∘ x_1) f '' s) t
[PROOFSTEP]
rw [← singleton_seq, ← singleton_seq, seq_seq, image_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
⊢ s ×ˢ t = seq (Prod.mk '' s) t
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t ↔ (a, b) ∈ seq (Prod.mk '' s) t
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ s ×ˢ t → (a, b) ∈ seq (Prod.mk '' s) t
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
ha : (a, b).fst ∈ s
hb : (a, b).snd ∈ t
⊢ (a, b) ∈ seq (Prod.mk '' s) t
[PROOFSTEP]
exact ⟨Prod.mk a, ⟨a, ha, rfl⟩, b, hb, rfl⟩
[GOAL]
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
⊢ (a, b) ∈ seq (Prod.mk '' s) t → (a, b) ∈ s ×ˢ t
[PROOFSTEP]
rintro ⟨f, ⟨x, hx, rfl⟩, y, hy, eq⟩
[GOAL]
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (a, b) ∈ s ×ˢ t
[PROOFSTEP]
rw [← eq]
[GOAL]
case h.mk.mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
a : α
b : β
x : α
hx : x ∈ s
y : β
hy : y ∈ t
eq : (x, y) = (a, b)
⊢ (x, y) ∈ s ×ˢ t
[PROOFSTEP]
exact ⟨hx, hy⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
⊢ seq (Prod.mk '' s) t = seq ((fun b a => (a, b)) '' t) s
[PROOFSTEP]
rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
s : Set α
t : Set β
⊢ seq ((fun x x_1 => x ∘ x_1) Prod.swap ∘ Prod.mk '' t) s = seq ((fun b a => (a, b)) '' t) s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = seq (f '' s) t
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
f : α → β → γ
s : Set α
t : Set β
x✝ : γ
⊢ x✝ ∈ image2 f s t ↔ x✝ ∈ seq (f '' s) t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
i : Set α
s : (a : α) → Set (π a)
⊢ pi i s = ⋂ (a : α) (_ : a ∈ i), eval a ⁻¹' s a
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ pi i s ↔ x✝ ∈ ⋂ (a : α) (_ : a ∈ i), eval a ⁻¹' s a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
t : (i : α) → Set (π i)
⊢ pi univ t = ⋂ (i : α), eval i ⁻¹' t i
[PROOFSTEP]
simp only [pi_def, iInter_true, mem_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
i : Set α
s t : (a : α) → Set (π a)
⊢ pi i s \ pi i t ⊆ ⋃ (a : α) (_ : a ∈ i), eval a ⁻¹' (s a \ t a)
[PROOFSTEP]
refine' diff_subset_comm.2 fun x hx a ha => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ pi i s \ ⋃ (a : α) (_ : a ∈ i), eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a
[PROOFSTEP]
simp only [mem_diff, mem_pi, mem_iUnion, not_exists, mem_preimage, not_and, not_not, eval_apply] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
a : α
ha : a ∈ i
hx : (∀ (i_1 : α), i_1 ∈ i → x i_1 ∈ s i_1) ∧ ∀ (x_1 : α), x_1 ∈ i → eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1
⊢ x a ∈ t a
[PROOFSTEP]
exact hx.2 _ ha (hx.1 _ ha)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
t : (i : α) → ι → Set (π i)
⊢ (⋃ (x : α → ι), pi univ fun i => t i (x i)) = pi univ fun i => ⋃ (j : ι), t i j
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
π : α → Type u_11
t : (i : α) → ι → Set (π i)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ (x : α → ι), pi univ fun i => t i (x i)) ↔ x✝ ∈ pi univ fun i => ⋃ (j : ι), t i j
[PROOFSTEP]
simp [Classical.skolem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Ici (⨆ (i : ι), f i) ↔ x✝ ∈ ⋂ (i : ι), Ici (f i)
[PROOFSTEP]
simp only [mem_Ici, iSup_le_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
f : ι → α
x✝ : α
⊢ x✝ ∈ Iic (⨅ (i : ι), f i) ↔ x✝ ∈ ⋂ (i : ι), Iic (f i)
[PROOFSTEP]
simp only [mem_Iic, le_iInf_iff, mem_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), Ici (f i j)
[PROOFSTEP]
simp_rw [Ici_iSup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Iic (⨅ (i : ι) (j : κ i), f i j) = ⋂ (i : ι) (j : κ i), Iic (f i j)
[PROOFSTEP]
simp_rw [Iic_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
s : Set α
⊢ Ici (sSup s) = ⋂ (a : α) (_ : a ∈ s), Ici a
[PROOFSTEP]
rw [sSup_eq_iSup, Ici_iSup₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ (a : α) (_ : a ∈ s), Iic a
[PROOFSTEP]
rw [sInf_eq_iInf, Iic_iInf₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ (x : α) (_ : x ∈ s₁), t x) \ ⋃ (x : α) (_ : x ∈ s₂), t x ⊆ ⋃ (x : α) (_ : x ∈ s₁ \ s₂), t x
[PROOFSTEP]
simp only [diff_subset_iff, ← biUnion_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
s₁ s₂ : Set α
⊢ ⋃ (x : α) (_ : x ∈ s₁), t x ⊆ ⋃ (x : α) (_ : x ∈ s₂ ∪ s₁ \ s₂), t x
[PROOFSTEP]
apply biUnion_subset_biUnion_left
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
[PROOFSTEP]
rw [union_diff_self]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁
[PROOFSTEP]
apply subset_union_right
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
b : β
hb : b ∈ ⋃ (i : α), t i
⊢ ∃ a, b ∈ t a
[PROOFSTEP]
simpa using hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
b₂ : β
h₂ : b₂ ∈ t a₂
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₂, snd := { val := b₂, property := h₂ } }
b_eq : b₁ = b₂
a_eq : a₁ = a₂
⊢ ↑(Eq.recOn a_eq { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₂, snd := { val := b₂, property := h₂ } }.snd
[PROOFSTEP]
subst b_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₂, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn a_eq { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₂, snd := { val := b₁, property := h₂ } }.snd
[PROOFSTEP]
subst a_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
t : α → Set β
h : ∀ (i j : α), i ≠ j → Disjoint (t i) (t j)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq :
  sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₁ } } =
    sigmaToiUnion t { fst := a₁, snd := { val := b₁, property := h₂ } }
⊢ ↑(Eq.recOn (_ : a₁ = a₁) { fst := a₁, snd := { val := b₁, property := h₁ } }.snd) =
    ↑{ fst := a₁, snd := { val := b₁, property := h₂ } }.snd
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a = ⨆ (i : ι) (a : α) (_ : a ∈ s i), f a
[PROOFSTEP]
rw [iSup_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ (a : α) (_ : a ∈ ⋃ (i : ι), s i), f a = ⨆ (j : α) (i : ι) (_ : j ∈ s i), f j
[PROOFSTEP]
simp_rw [mem_iUnion, iSup_exists]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ (t : Set β) (_ : t ∈ s), sSup t
[PROOFSTEP]
simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ (x : α) (_ : x ∈ ⋃₀ S), f x = ⨆ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), f x
[PROOFSTEP]
rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ (x : α) (_ : x ∈ ⋃₀ S), f x = ⨅ (s : Set α) (_ : s ∈ S) (x : α) (_ : x ∈ s), f x
[PROOFSTEP]
rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
S : Set (Set α)
p : α → Prop
⊢ (∀ (x : α), x ∈ ⋃₀ S → p x) ↔ ∀ (s : Set α), s ∈ S → ∀ (x : α), x ∈ s → p x
[PROOFSTEP]
simp_rw [← iInf_Prop_eq, iInf_sUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
ι₂ : Sort u_6
κ : ι → Sort u_7
κ₁ : ι → Sort u_8
κ₂ : ι → Sort u_9
κ' : ι' → Sort u_10
inst✝ : CompleteLattice β
S : Set (Set α)
p : α → Prop
⊢ (∃ x, x ∈ ⋃₀ S ∧ p x) ↔ ∃ s, s ∈ S ∧ ∃ x, x ∈ s ∧ p x
[PROOFSTEP]
simp_rw [← exists_prop, ← iSup_Prop_eq, iSup_sUnion]
