/-
Copyright (c) 2020 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
Ported by: Anatole Dedecker

! This file was ported from Lean 3 source module data.set.accumulate
! leanprover-community/mathlib commit 207cfac9fcd06138865b5d04f7091e46d9320432
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Lattice

/-!
# Accumulate

The function `Accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
-/


variable {
α: Type ?u.1105
α 
β: Type ?u.122
β 
γ: Type ?u.29
γ : 
Type _: Type (?u.8+1)
Type _} {
s: α → Set β
s : 
α: Type ?u.23
α → 
Set: Type ?u.219 → Type ?u.219
Set 
β: Type ?u.26
β} {
t: α → Set γ
t : 
α: Type ?u.23
α → 
Set: Type ?u.225 → Type ?u.225
Set 
γ: Type ?u.8
γ}

namespace Set

/-- `Accumulate s` is the union of `s y` for `y ≤ x`. -/
def 
Accumulate: [inst : LE α] → (α → Set β) → α → Set β
Accumulate [
LE: Type ?u.44 → Type ?u.44
LE 
α: Type ?u.23
α] (
s: α → Set β
s : 
α: Type ?u.23
α → 
Set: Type ?u.49 → Type ?u.49
Set 
β: Type ?u.26
β) (
x: α
x : 
α: Type ?u.23
α) : 
Set: Type ?u.55 → Type ?u.55
Set 
β: Type ?u.26
β :=
  ⋃ 
y: ?m.71
y ≤ 
x: α
x, 
s: α → Set β
s 
y: ?m.71
y
#align set.accumulate 
Set.Accumulate: {α : Type u_1} → {β : Type u_2} → [inst : LE α] → (α → Set β) → α → Set β
Set.Accumulate

theorem 
accumulate_def: ∀ [inst : LE α] {x : α}, Accumulate s x = iUnion fun y => iUnion fun h => s y
accumulate_def [
LE: Type ?u.140 → Type ?u.140
LE 
α: Type ?u.119
α] {
x: α
x : 
α: Type ?u.119
α} : 
Accumulate: {α : Type ?u.147} → {β : Type ?u.146} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s 
x: α
x = ⋃ 
y: ?m.167
y ≤ 
x: α
x, 
s: α → Set β
s 
y: ?m.167
y :=
  
rfl: ∀ {α : Sort ?u.194} {a : α}, a = a
rfl
#align set.accumulate_def 
Set.accumulate_def: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α},
  Accumulate s x = iUnion fun y => iUnion fun h => s y
Set.accumulate_def

@[simp]
theorem 
mem_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α} {z : β}, z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
mem_accumulate [
LE: Type ?u.229 → Type ?u.229
LE 
α: Type ?u.208
α] {
x: α
x : 
α: Type ?u.208
α} {
z: β
z : 
β: Type ?u.211
β} : 
z: β
z ∈ 
Accumulate: {α : Type ?u.242} → {β : Type ?u.241} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s 
x: α
x ↔ ∃ 
y: ?m.283
y ≤ 
x: α
x, 
z: β
z ∈ 
s: α → Set β
s 
y: ?m.283
y := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s ysimp_rw [
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
accumulate_def: ∀ {α : Type ?u.411} {β : Type ?u.412} {s : α → Set β} [inst : LE α] {x : α},
  Accumulate s x = iUnion fun y => iUnion fun h => s y
accumulate_def,
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

(z ∈ iUnion fun y => iUnion fun h => s y) ↔ ∃ y, y ≤ x ∧ z ∈ s y 
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
mem_iUnion₂: ∀ {γ : Type ?u.563} {ι : Sort ?u.564} {κ : ι → Sort ?u.565} {x : γ} {s : (i : ι) → κ i → Set γ},
  (x ∈ iUnion fun i => iUnion fun j => s i j) ↔ ∃ i j, x ∈ s i j
mem_iUnion₂,
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

(∃ i j, z ∈ s i) ↔ ∃ y, y ≤ x ∧ z ∈ s y 
α: Type u_1

β: Type u_2

γ: Type ?u.214

s: α → Set β

t: α → Set γ

inst✝: LE α

x: α

z: β

z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
exists_prop: ∀ {b a : Prop}, (∃ _h, b) ↔ a ∧ b
exists_prop
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align set.mem_accumulate 
Set.mem_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] {x : α} {z : β}, z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
Set.mem_accumulate

theorem 
subset_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] {x : α}, s x ⊆ Accumulate s x
subset_accumulate [
Preorder: Type ?u.1126 → Type ?u.1126
Preorder 
α: Type ?u.1105
α] {
x: α
x : 
α: Type ?u.1105
α} : 
s: α → Set β
s 
x: α
x ⊆ 
Accumulate: {α : Type ?u.1143} → {β : Type ?u.1142} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s 
x: α
x := fun 
_: ?m.1189
_ => 
mem_biUnion: ∀ {α : Type ?u.1191} {β : Type ?u.1192} {s : Set α} {t : α → Set β} {x : α} {y : β},
  x ∈ s → y ∈ t x → y ∈ iUnion fun x => iUnion fun h => t x
mem_biUnion 
le_rfl: ∀ {α : Type ?u.1224} [inst : Preorder α] {a : α}, a ≤ a
le_rfl
#align set.subset_accumulate 
Set.subset_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] {x : α}, s x ⊆ Accumulate s x
Set.subset_accumulate

theorem 
monotone_accumulate: ∀ [inst : Preorder α], Monotone (Accumulate s)
monotone_accumulate [
Preorder: Type ?u.1313 → Type ?u.1313
Preorder 
α: Type ?u.1292
α] : 
Monotone: {α : Type ?u.1317} → {β : Type ?u.1316} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone (
Accumulate: {α : Type ?u.1349} → {β : Type ?u.1348} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s) := fun 
_: ?m.1438
_ 
_: ?m.1441
_ 
hxy: ?m.1444
hxy =>
  
biUnion_subset_biUnion_left: ∀ {α : Type ?u.1446} {β : Type ?u.1447} {s s' : Set α} {t : α → Set β},
  s ⊆ s' → (iUnion fun x => iUnion fun h => t x) ⊆ iUnion fun x => iUnion fun h => t x
biUnion_subset_biUnion_left fun 
_: ?m.1487
_ 
hz: ?m.1490
hz => 
le_trans: ∀ {α : Type ?u.1492} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans 
hz: ?m.1490
hz 
hxy: ?m.1444
hxy
#align set.monotone_accumulate 
Set.monotone_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], Monotone (Accumulate s)
Set.monotone_accumulate

theorem 
biUnion_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] (x : α),
  (iUnion fun y => iUnion fun h => Accumulate s y) = iUnion fun y => iUnion fun h => s y
biUnion_accumulate [
Preorder: Type ?u.1611 → Type ?u.1611
Preorder 
α: Type ?u.1590
α] (
x: α
x : 
α: Type ?u.1590
α) : (⋃ 
y: ?m.1622
y ≤ 
x: α
x, 
Accumulate: {α : Type ?u.1647} → {β : Type ?u.1646} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s 
y: ?m.1622
y) = ⋃ 
y: ?m.1686
y ≤ 
x: α
x, 
s: α → Set β
s 
y: ?m.1686
y := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

(iUnion fun y => iUnion fun h => Accumulate s y) = iUnion fun y => iUnion fun h => s yapply 
Subset.antisymm: ∀ {α : Type ?u.1715} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Subset.antisymm
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₁
(iUnion fun y => iUnion fun h => Accumulate s y) ⊆ iUnion fun y => iUnion fun h => s y
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₂
(iUnion fun y => iUnion fun h => s y) ⊆ iUnion fun y => iUnion fun h => Accumulate s y
  
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

(iUnion fun y => iUnion fun h => Accumulate s y) = iUnion fun y => iUnion fun h => s y·
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₁
(iUnion fun y => iUnion fun h => Accumulate s y) ⊆ iUnion fun y => iUnion fun h => s y 
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₁
(iUnion fun y => iUnion fun h => Accumulate s y) ⊆ iUnion fun y => iUnion fun h => s y
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₂
(iUnion fun y => iUnion fun h => s y) ⊆ iUnion fun y => iUnion fun h => Accumulate s yexact 
iUnion₂_subset: ∀ {α : Type ?u.1730} {ι : Sort ?u.1731} {κ : ι → Sort ?u.1732} {s : (i : ι) → κ i → Set α} {t : Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t) → (iUnion fun i => iUnion fun j => s i j) ⊆ t
iUnion₂_subset fun 
y: ?m.1767
y 
hy: ?m.1770
hy => 
monotone_accumulate: ∀ {α : Type ?u.1772} {β : Type ?u.1773} {s : α → Set β} [inst : Preorder α], Monotone (Accumulate s)
monotone_accumulate 
hy: ?m.1770
hy
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

(iUnion fun y => iUnion fun h => Accumulate s y) = iUnion fun y => iUnion fun h => s y·
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₂
(iUnion fun y => iUnion fun h => s y) ⊆ iUnion fun y => iUnion fun h => Accumulate s y 
α: Type u_1

β: Type u_2

γ: Type ?u.1596

s: α → Set β

t: α → Set γ

inst✝: Preorder α

x: α

h₂
(iUnion fun y => iUnion fun h => s y) ⊆ iUnion fun y => iUnion fun h => Accumulate s yexact 
iUnion₂_mono: ∀ {α : Type ?u.1837} {ι : Sort ?u.1838} {κ : ι → Sort ?u.1839} {s t : (i : ι) → κ i → Set α},
  (∀ (i : ι) (j : κ i), s i j ⊆ t i j) → (iUnion fun i => iUnion fun j => s i j) ⊆ iUnion fun i => iUnion fun j => t i j
iUnion₂_mono fun 
y: ?m.1859
y 
_: ?m.1862
_ => 
subset_accumulate: ∀ {α : Type ?u.1864} {β : Type ?u.1865} {s : α → Set β} [inst : Preorder α] {x : α}, s x ⊆ Accumulate s x
subset_accumulate
Goals accomplished! 🐙
#align set.bUnion_accumulate 
Set.biUnion_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] (x : α),
  (iUnion fun y => iUnion fun h => Accumulate s y) = iUnion fun y => iUnion fun h => s y
Set.biUnion_accumulate

theorem 
iUnion_accumulate: ∀ [inst : Preorder α], (iUnion fun x => Accumulate s x) = iUnion fun x => s x
iUnion_accumulate [
Preorder: Type ?u.1932 → Type ?u.1932
Preorder 
α: Type ?u.1911
α] : (⋃ 
x: ?m.1941
x, 
Accumulate: {α : Type ?u.1944} → {β : Type ?u.1943} → [inst : LE α] → (α → Set β) → α → Set β
Accumulate 
s: α → Set β
s 
x: ?m.1941
x) = ⋃ 
x: ?m.1990
x, 
s: α → Set β
s 
x: ?m.1990
x := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

(iUnion fun x => Accumulate s x) = iUnion fun x => s xapply 
Subset.antisymm: ∀ {α : Type ?u.2003} {a b : Set α}, a ⊆ b → b ⊆ a → a = b
Subset.antisymm
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
(iUnion fun x => Accumulate s x) ⊆ iUnion fun x => s x
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₂
(iUnion fun x => s x) ⊆ iUnion fun x => Accumulate s x
  
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

(iUnion fun x => Accumulate s x) = iUnion fun x => s x·
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
(iUnion fun x => Accumulate s x) ⊆ iUnion fun x => s x 
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
(iUnion fun x => Accumulate s x) ⊆ iUnion fun x => s x
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₂
(iUnion fun x => s x) ⊆ iUnion fun x => Accumulate s xsimp only [
subset_def: ∀ {α : Type ?u.2029} {s t : Set α}, (s ⊆ t) = ∀ (x : α), x ∈ s → x ∈ t
subset_def, 
mem_iUnion: ∀ {α : Type ?u.2042} {ι : Sort ?u.2043} {x : α} {s : ι → Set α}, (x ∈ iUnion fun i => s i) ↔ ∃ i, x ∈ s i
mem_iUnion, 
exists_imp: ∀ {α : Sort ?u.2071} {p : α → Prop} {b : Prop}, (∃ x, p x) → b ↔ ∀ (x : α), p x → b
exists_imp, 
mem_accumulate: ∀ {α : Type ?u.2092} {β : Type ?u.2093} {s : α → Set β} [inst : LE α] {x : α} {z : β},
  z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
mem_accumulate]
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i
    
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
(iUnion fun x => Accumulate s x) ⊆ iUnion fun x => s xintro 
z: β
z 
x: α
x 
x': α
x' ⟨_, 
hz: z ∈ s x'
hz⟩
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

z: β

x, x': α

left✝: x' ≤ x

hz: z ∈ s x'

h₁
∃ i, z ∈ s i
    
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₁
(iUnion fun x => Accumulate s x) ⊆ iUnion fun x => s xexact ⟨
x': α
x', 
hz: z ∈ s x'
hz⟩
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

(iUnion fun x => Accumulate s x) = iUnion fun x => s x·
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₂
(iUnion fun x => s x) ⊆ iUnion fun x => Accumulate s x 
α: Type u_1

β: Type u_2

γ: Type ?u.1917

s: α → Set β

t: α → Set γ

inst✝: Preorder α

h₂
(iUnion fun x => s x) ⊆ iUnion fun x => Accumulate s xexact 
iUnion_mono: ∀ {α : Type ?u.2674} {ι : Sort ?u.2675} {s t : ι → Set α},
  (∀ (i : ι), s i ⊆ t i) → (iUnion fun i => s i) ⊆ iUnion fun i => t i
iUnion_mono fun 
i: ?m.2701
i => 
subset_accumulate: ∀ {α : Type ?u.2703} {β : Type ?u.2704} {s : α → Set β} [inst : Preorder α] {x : α}, s x ⊆ Accumulate s x
subset_accumulate
Goals accomplished! 🐙
#align set.Union_accumulate 
Set.iUnion_accumulate: ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α],
  (iUnion fun x => Accumulate s x) = iUnion fun x => s x
Set.iUnion_accumulate

end Set