[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
g✝ : β → γ
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
⊢ f ⁻¹' s = g ⁻¹' s
[PROOFSTEP]
congr with x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
g✝ : β → γ
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
x : α
⊢ x ∈ f ⁻¹' s ↔ x ∈ g ⁻¹' s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x => b) ⁻¹' s = if b ∈ s then univ else ∅
[PROOFSTEP]
split_ifs with hb
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∈ s
⊢ (fun x => b) ⁻¹' s = univ
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : ¬b ∈ s
⊢ (fun x => b) ⁻¹' s = ∅
[PROOFSTEP]
exacts [preimage_const_of_mem hb, preimage_const_of_not_mem hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
g : β → γ
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
g : β → γ
f : α → α
⊢ preimage f^[Nat.zero] = (preimage f)^[Nat.zero]
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
g : β → γ
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[Nat.succ n] = (preimage f)^[Nat.succ n]
[PROOFSTEP]
rw [iterate_succ, iterate_succ', Set.preimage_comp_eq, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ { val := x, property := h } ∈ s ↔ x ∈ t
[PROOFSTEP]
rw [s_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
s_eq : s = Subtype.val ⁻¹' t
x : α
h : p x
⊢ { val := x, property := h } ∈ Subtype.val ⁻¹' t ↔ x ∈ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
g : β → γ
p : α → Prop
s : Set (Subtype p)
t : Set α
h : ∀ (x : α) (h : p x), { val := x, property := h } ∈ s ↔ x ∈ t
x✝ : Subtype p
x : α
hx : p x
⊢ { val := x, property := hx } ∈ s ↔ { val := x, property := hx } ∈ Subtype.val ⁻¹' t
[PROOFSTEP]
simp [h]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ
[PROOFSTEP]
ext ⟨x, x_in_s⟩
[GOAL]
case h.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u ↔ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
[PROOFSTEP]
constructor
[GOAL]
case h.mk.mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u → { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
[PROOFSTEP]
intro x_in_u x_in_v
[GOAL]
case h.mk.mp
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
x_in_v : { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' v
⊢ False
[PROOFSTEP]
exact eq_empty_iff_forall_not_mem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩
[GOAL]
case h.mk.mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ → { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
[PROOFSTEP]
intro hx
[GOAL]
case h.mk.mpr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α✝ → β
g : β → γ
α : Type u_6
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
hx : { val := x, property := x_in_s } ∈ (Subtype.val ⁻¹' v)ᶜ
⊢ { val := x, property := x_in_s } ∈ Subtype.val ⁻¹' u
[PROOFSTEP]
exact Or.elim (hsuv x_in_s) id fun hx' => hx.elim hx'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
p : β → Prop
⊢ (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ (x : α), x ∈ s → p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
p : β → Prop
⊢ (∃ y, y ∈ f '' s ∧ p y) ↔ ∃ x, x ∈ s ∧ p (f x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ x ∈ f '' s ↔ x ∈ g '' s
[PROOFSTEP]
rw [mem_image, mem_image]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ f x_1 = x) ↔ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
[PROOFSTEP]
exact
  {
    mp := by
      rintro ⟨a, ha1, ha2⟩
      exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩,
    mpr := by
      rintro ⟨a, ha1, ha2⟩
      exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩ }
    -- safe [ext_iff, iff_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ f x_1 = x) → ∃ x_1, x_1 ∈ s ∧ g x_1 = x
[PROOFSTEP]
rintro ⟨a, ha1, ha2⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : f a = x
⊢ ∃ x_1, x_1 ∈ s ∧ g x_1 = x
[PROOFSTEP]
exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
⊢ (∃ x_1, x_1 ∈ s ∧ g x_1 = x) → ∃ x_1, x_1 ∈ s ∧ f x_1 = x
[PROOFSTEP]
rintro ⟨a, ha1, ha2⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
x : β
a : α
ha1 : a ∈ s
ha2 : g a = x
⊢ ∃ x_1, x_1 ∈ s ∧ f x_1 = x
[PROOFSTEP]
exact ⟨a, ⟨ha1, (h a ha1) ▸ ha2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
β' : Type u_6
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' (g '' s) = g' '' (f' '' s)
[PROOFSTEP]
simp_rw [image_image, h_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t a b : Set α
f : α → β
h : a ⊆ b
⊢ f '' a ⊆ f '' b
[PROOFSTEP]
simp only [subset_def, mem_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t a b : Set α
f : α → β
h : a ⊆ b
⊢ ∀ (x : β), (∃ x_1, x_1 ∈ a ∧ f x_1 = x) → ∃ x_1, x_1 ∈ b ∧ f x_1 = x
[PROOFSTEP]
exact fun x => fun ⟨w, h1, h2⟩ => ⟨w, h h1, h2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' (s ∪ t) → x ∈ f '' s ∪ f '' t
[PROOFSTEP]
rintro ⟨a, h | h, rfl⟩ <;> [left; right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' (s ∪ t) → x ∈ f '' s ∪ f '' t
[PROOFSTEP]
rintro ⟨a, h | h, rfl⟩
[GOAL]
case intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ f a ∈ f '' s ∪ f '' t
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ f a ∈ f '' s ∪ f '' t
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ f a ∈ f '' s
[PROOFSTEP]
exact ⟨_, h, rfl⟩
[GOAL]
case intro.intro.inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ f a ∈ f '' t
[PROOFSTEP]
exact ⟨_, h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' s ∪ f '' t → x ∈ f '' (s ∪ t)
[PROOFSTEP]
rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩) <;> refine' ⟨_, _, rfl⟩ <;> [left; right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
x : β
⊢ x ∈ f '' s ∪ f '' t → x ∈ f '' (s ∪ t)
[PROOFSTEP]
rintro (⟨a, h, rfl⟩ | ⟨a, h, rfl⟩)
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ f a ∈ f '' (s ∪ t)
[PROOFSTEP]
refine' ⟨_, _, rfl⟩
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ f a ∈ f '' (s ∪ t)
[PROOFSTEP]
refine' ⟨_, _, rfl⟩
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ a ∈ s ∪ t
[PROOFSTEP]
left
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ a ∈ s ∪ t
[PROOFSTEP]
right
[GOAL]
case inl.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ s
⊢ a ∈ s
[PROOFSTEP]
exact h
[GOAL]
case inr.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
a : α
h : a ∈ t
⊢ a ∈ t
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
⊢ f '' ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y
b : β
x✝ : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
ι : Type u_6
f : ι → β
H : Surjective f
⊢ ∀ (x : β), x ∈ f '' univ
[PROOFSTEP]
simpa [image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
a : α
⊢ f '' {a} = {f a}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
a : α
x✝ : β
⊢ x✝ ∈ f '' {a} ↔ x✝ ∈ {f a}
[PROOFSTEP]
simp [image, eq_comm]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α✝ → β✝
s✝ t : Set α✝
α : Type u_6
β : Type u_7
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅
[PROOFSTEP]
simp only [eq_empty_iff_forall_not_mem]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α✝ → β✝
s✝ t : Set α✝
α : Type u_6
β : Type u_7
f : α → β
s : Set α
⊢ (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s
[PROOFSTEP]
exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s t✝ : Set α
inst✝ : BooleanAlgebra α
t : α
S : Set α
⊢ t ∈ compl '' S ↔ tᶜ ∈ S
[PROOFSTEP]
simp [← preimage_compl_eq_image_compl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
⊢ (fun x => x) '' s = s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
x✝ : α
⊢ x✝ ∈ (fun x => x) '' s ↔ x✝ ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
⊢ id '' s = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s t : Set α
inst✝ : BooleanAlgebra α
S : Set α
⊢ compl '' (compl '' S) = S
[PROOFSTEP]
rw [← image_comp, compl_comp_compl, image_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
a : α
s : Set α
x✝ : β
⊢ x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)
[PROOFSTEP]
simp [and_or_left, exists_or, eq_comm, or_comm, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
a b : α
⊢ f '' {a, b} = {f a, f b}
[PROOFSTEP]
simp only [image_insert_eq, image_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : Function.RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s
[PROOFSTEP]
rw [image_eq_preimage_of_inverse h₁ h₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : Function.RightInverse g f
⊢ b ∈ g ⁻¹' s ↔ g b ∈ s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)
[PROOFSTEP]
simp [disjoint_iff_inf_le, ← image_inter H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Surjective f
⊢ f '' s ∪ f '' sᶜ = univ
[PROOFSTEP]
rw [← image_union]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t : Set α
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ
[PROOFSTEP]
simp [image_univ_of_surjective H]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)
[PROOFSTEP]
rw [diff_subset_iff, ← image_union, union_diff_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)
[PROOFSTEP]
exact image_subset f (subset_union_right t s)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t✝ : Set α
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)
[PROOFSTEP]
simp_rw [Set.symmDiff_def, image_union, image_diff hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : β → α
hf : Surjective f
eq : f ⁻¹' s = f ⁻¹' t
⊢ s = t
[PROOFSTEP]
rw [← image_preimage_eq s hf, ← image_preimage_eq t hf, eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ t
[PROOFSTEP]
calc
  f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ f '' (f ⁻¹' t) := image_inter_subset _ _ _
  _ ⊆ f '' s ∩ t := inter_subset_inter_right _ (image_preimage_subset f t)
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t ⊆ f '' (s ∩ f ⁻¹' t)
[PROOFSTEP]
rintro _ ⟨⟨x, h', rfl⟩, h⟩
[GOAL]
case h₂.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
x : α
h' : x ∈ s
h : f x ∈ t
⊢ f x ∈ f '' (s ∩ f ⁻¹' t)
[PROOFSTEP]
exact ⟨x, ⟨h', h⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
[PROOFSTEP]
simp only [inter_comm, image_inter_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ Set.Nonempty (f '' s ∩ t) ↔ Set.Nonempty (s ∩ f ⁻¹' t)
[PROOFSTEP]
rw [← image_inter_preimage, nonempty_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t
[PROOFSTEP]
simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ s = t
[PROOFSTEP]
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
hf : Injective f
⊢ f '' s ⊆ f '' t ↔ s ⊆ t
[PROOFSTEP]
refine' Iff.symm <| (Iff.intro (image_subset f)) fun h => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ s ⊆ t
[PROOFSTEP]
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : α → β
s t : Set α
f : α → β
hf : Injective f
h : f '' s ⊆ f '' t
⊢ f ⁻¹' (f '' s) ⊆ f ⁻¹' (f '' t)
[PROOFSTEP]
exact preimage_mono h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
⊢ ↑σ '' s = s
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ↑σ '' s ↔ i ∈ s
[PROOFSTEP]
obtain hi | hi := eq_or_ne (σ i) i
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s ↔ i ∈ s
[PROOFSTEP]
refine' ⟨_, fun h => ⟨i, h, hi⟩⟩
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
⊢ i ∈ ↑σ '' s → i ∈ s
[PROOFSTEP]
rintro ⟨j, hj, h⟩
[GOAL]
case h.inl.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i = i
j : α
hj : j ∈ s
h : ↑σ j = i
⊢ i ∈ s
[PROOFSTEP]
rwa [σ.injective (hi.trans h.symm)]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
⊢ i ∈ ↑σ '' s ↔ i ∈ s
[PROOFSTEP]
refine' iff_of_true ⟨σ.symm i, hs fun h => hi _, σ.apply_symm_apply _⟩ (hs hi)
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
h : ↑σ (↑σ.symm i) = ↑σ.symm i
⊢ ↑σ i = i
[PROOFSTEP]
convert congr_arg σ h
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
h : ↑σ (↑σ.symm i) = ↑σ.symm i
⊢ i = ↑σ (↑σ.symm i)
[PROOFSTEP]
exact (σ.apply_symm_apply _).symm
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : α → β
s✝ t s : Set α
σ : Equiv.Perm α
hs : {a | ↑σ a ≠ a} ⊆ s
i : α
hi : ↑σ i ≠ i
h : ↑σ (↑σ.symm i) = ↑σ.symm i
⊢ i = ↑σ (↑σ.symm i)
[PROOFSTEP]
exact (σ.apply_symm_apply _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s
[PROOFSTEP]
ext t
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
[PROOFSTEP]
simp_rw [mem_union, mem_image, mem_powerset_iff]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s ↔ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
⊢ t ⊆ insert a s → t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
intro h
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
by_cases hs : a ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
right
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
refine' ⟨t \ { a }, _, _⟩
[GOAL]
case pos.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t \ {a} ⊆ s
[PROOFSTEP]
rw [diff_singleton_subset_iff]
[GOAL]
case pos.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ t ⊆ insert a s
[PROOFSTEP]
assumption
[GOAL]
case pos.h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : a ∈ t
⊢ insert a (t \ {a}) = t
[PROOFSTEP]
rw [insert_diff_singleton, insert_eq_of_mem hs]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t
[PROOFSTEP]
left
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ insert a s
hs : ¬a ∈ t
⊢ t ⊆ s
[PROOFSTEP]
exact (subset_insert_iff_of_not_mem hs).mp h
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
⊢ (t ⊆ s ∨ ∃ x, x ⊆ s ∧ insert a x = t) → t ⊆ insert a s
[PROOFSTEP]
rintro (h | ⟨s', h₁, rfl⟩)
[GOAL]
case h.mpr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
t : Set α
h : t ⊆ s
⊢ t ⊆ insert a s
[PROOFSTEP]
exact subset_trans h (subset_insert a s)
[GOAL]
case h.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s : Set α
a : α
s' : Set α
h₁ : s' ⊆ s
⊢ insert a s' ⊆ insert a s
[PROOFSTEP]
exact insert_subset_insert h₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : α → Prop
⊢ (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : ↑(range f) → Prop
H : ∀ (i : ι), p { val := f i, property := (_ : f i ∈ range f) }
x✝ : ↑(range f)
y : α
i : ι
hi : f i = y
⊢ p { val := y, property := (_ : ∃ y_1, f y_1 = y) }
[PROOFSTEP]
subst hi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : ↑(range f) → Prop
H : ∀ (i : ι), p { val := f i, property := (_ : f i ∈ range f) }
x✝ : ↑(range f)
i : ι
⊢ p { val := f i, property := (_ : ∃ y, f y = f i) }
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : α → Prop
⊢ (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : α → Prop
⊢ (∃ a, a ∈ range f ∧ p a) ↔ ∃ i, p (f i)
[PROOFSTEP]
simpa only [exists_prop] using exists_range_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
a : α
i : ι
hi : f i = a
ha : p { val := a, property := (_ : ∃ y, f y = a) }
⊢ ∃ i, p { val := f i, property := (_ : f i ∈ range f) }
[PROOFSTEP]
subst a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
i : ι
ha : p { val := f i, property := (_ : ∃ y, f y = f i) }
⊢ ∃ i, p { val := f i, property := (_ : f i ∈ range f) }
[PROOFSTEP]
exact ⟨i, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
⊢ f '' univ = range f
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x✝ : β
⊢ x✝ ∈ f '' univ ↔ x✝ ∈ range f
[PROOFSTEP]
simp [image, range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s ⊆ range f
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
[PROOFSTEP]
exact image_subset _ (subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
i : ℕ
⊢ i ∈ range Nat.succ → 0 < i
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
n : ℕ
⊢ 0 < Nat.succ n
[PROOFSTEP]
exact Nat.succ_pos n
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → γ
g : β → γ
⊢ range f ⊆ range g ↔ ∃ h, f = g ∘ h
[PROOFSTEP]
simp only [range_subset_iff, mem_range, Classical.skolem, Function.funext_iff, (· ∘ ·), eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ (b : β), b ∈ s → ∃ a, f a = b
[PROOFSTEP]
rw [← range_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ range f = s ↔ (range fun a => f a) ⊆ s ∧ ∀ (b : β), b ∈ s → ∃ a, f a = b
[PROOFSTEP]
exact le_antisymm_iff
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
g : β → γ
⊢ range (g ∘ f) ⊆ range g
[PROOFSTEP]
rw [range_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
g : β → γ
⊢ g '' range f ⊆ range g
[PROOFSTEP]
apply image_subset_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι
[PROOFSTEP]
rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
⊢ f '' s ∪ f '' sᶜ = range f
[PROOFSTEP]
rw [← image_union, ← image_univ, ← union_compl_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ y ∈ insert (f x) (f '' {x}ᶜ) ↔ y ∈ range f
[PROOFSTEP]
rw [mem_range, mem_insert_iff, mem_image]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) ↔ ∃ y_1, f y_1 = y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y) → ∃ y_1, f y_1 = y
[PROOFSTEP]
rintro (h | ⟨x', _, h⟩)
[GOAL]
case h.mp.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
h : y = f x
⊢ ∃ y_1, f y_1 = y
[PROOFSTEP]
exact ⟨x, h.symm⟩
[GOAL]
case h.mp.inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
left✝ : x' ∈ {x}ᶜ
h : f x' = y
⊢ ∃ y_1, f y_1 = y
[PROOFSTEP]
exact ⟨x', h⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
⊢ (∃ y_1, f y_1 = y) → y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
[PROOFSTEP]
rintro ⟨x', h⟩
[GOAL]
case h.mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
[PROOFSTEP]
by_cases hx : x' = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
[PROOFSTEP]
left
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : x' = x
⊢ y = f x
[PROOFSTEP]
rw [← h, hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ y = f x ∨ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
[PROOFSTEP]
right
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ ∃ x_1, x_1 ∈ {x}ᶜ ∧ f x_1 = y
[PROOFSTEP]
refine' ⟨_, _, h⟩
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ∈ {x}ᶜ
[PROOFSTEP]
rw [mem_compl_singleton_iff]
[GOAL]
case neg.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : α
y : β
x' : α
h : f x' = y
hx : ¬x' = x
⊢ x' ≠ x
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t✝ : Set α
f : α → β
t : Set β
x : β
x✝ : x ∈ t ∩ range f
hx : x ∈ t
y : α
h_eq : f y = x
⊢ y ∈ f ⁻¹' t
[PROOFSTEP]
rw [preimage, mem_setOf, h_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t✝ : Set α
f : α → β
t : Set β
x : β
x✝ : x ∈ t ∩ range f
hx : x ∈ t
y : α
h_eq : f y = x
⊢ x ∈ t
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
hs : s ⊆ range f
⊢ f '' (f ⁻¹' s) = s
[PROOFSTEP]
rw [image_preimage_eq_inter_range, inter_eq_self_of_subset_left hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s) = s → s ⊆ range f
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ s ⊆ range f
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
h : f '' (f ⁻¹' s) = s
⊢ f '' (f ⁻¹' s) ⊆ range f
[PROOFSTEP]
apply image_subset_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s)
[PROOFSTEP]
rw [← exists_range_iff, range_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s, s ⊆ range f ∧ p s) ↔ ∃ a, a ∈ 𝒫 range f ∧ p a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∃ s x, p s) ↔ ∃ s, p (f '' s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (s : Set α), p (f '' s)
[PROOFSTEP]
rw [← forall_range_iff, range_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t
[PROOFSTEP]
intro h x hx
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases hs hx with ⟨y, rfl⟩
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t
[PROOFSTEP]
exact h hx
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
[PROOFSTEP]
intro h x
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case mp.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t
[PROOFSTEP]
rw [← preimage_subset_preimage_iff hs, h]
[GOAL]
case mp.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
[PROOFSTEP]
rw [← preimage_subset_preimage_iff ht, h]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s
[PROOFSTEP]
rw [inter_comm, preimage_inter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ f ⁻¹' (f '' (f ⁻¹' s)) = f ⁻¹' s
[PROOFSTEP]
rw [image_preimage_eq_inter_range, preimage_inter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ range Sum.inl = {x | Sum.isLeft x = true}
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inl ↔ Sum.inl val✝ ∈ {x | Sum.isLeft x = true}
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inl ↔ Sum.inr val✝ ∈ {x | Sum.isLeft x = true}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ range Sum.inr = {x | Sum.isRight x = true}
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
val✝ : α
⊢ Sum.inl val✝ ∈ range Sum.inr ↔ Sum.inl val✝ ∈ {x | Sum.isRight x = true}
[PROOFSTEP]
simp
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
val✝ : β
⊢ Sum.inr val✝ ∈ range Sum.inr ↔ Sum.inr val✝ ∈ {x | Sum.isRight x = true}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ range Sum.inl ⊓ range Sum.inr ≤ ⊥
[PROOFSTEP]
rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥
[PROOFSTEP]
exact Sum.noConfusion h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ ⊤ ≤ range Sum.inl ⊔ range Sum.inr
[PROOFSTEP]
rintro (x | y) - <;> [left; right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ ⊤ ≤ range Sum.inl ⊔ range Sum.inr
[PROOFSTEP]
rintro (x | y) -
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
x : α
⊢ Sum.inl x ∈ range Sum.inl ⊔ range Sum.inr
[PROOFSTEP]
left
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
y : β
⊢ Sum.inr y ∈ range Sum.inl ⊔ range Sum.inr
[PROOFSTEP]
right
[GOAL]
case inl.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
x : α
⊢ Sum.inl x ∈ range Sum.inl
[PROOFSTEP]
exact mem_range_self _
[GOAL]
case inr.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
y : β
⊢ Sum.inr y ∈ range Sum.inr
[PROOFSTEP]
exact mem_range_self _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s✝ t : Set α
s : Set β
⊢ Sum.inl ⁻¹' (Sum.inr '' s) = ∅
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s✝ t : Set α
s : Set β
x✝ : α
⊢ x✝ ∈ Sum.inl ⁻¹' (Sum.inr '' s) ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s✝ t s : Set α
⊢ Sum.inr ⁻¹' (Sum.inl '' s) = ∅
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s✝ t s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' (Sum.inl '' s) ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ Sum.inl ⁻¹' range Sum.inr = ∅
[PROOFSTEP]
rw [← image_univ, preimage_inl_image_inr]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
⊢ Sum.inr ⁻¹' range Sum.inl = ∅
[PROOFSTEP]
rw [← image_univ, preimage_inr_image_inl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s✝ t : Set α
s : Set (α ⊕ β)
⊢ Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s
[PROOFSTEP]
rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_distrib_left, range_inl_union_range_inr,
  inter_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x | p x})
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ { val := x, property := hx } ∈ range (Subtype.map f h) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' {x | p x})
[PROOFSTEP]
rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.coe_mk]
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) ↔
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
[PROOFSTEP]
apply Iff.intro
[GOAL]
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) →
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
[PROOFSTEP]
rintro ⟨a, b, hab⟩
[GOAL]
case h.mk.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : Subtype.map f h { val := a, property := b } = { val := x, property := hx }
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
[PROOFSTEP]
rw [Subtype.map, Subtype.mk.injEq] at hab
[GOAL]
case h.mk.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ a ∈ {x | p x} ∧ f a = x
[PROOFSTEP]
trivial
[GOAL]
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
[PROOFSTEP]
rintro ⟨a, b, hab⟩
[GOAL]
case h.mk.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
[PROOFSTEP]
use a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ Subtype.map f h { val := a, property := b } = { val := x, property := hx }
[PROOFSTEP]
rw [Subtype.map, Subtype.mk.injEq]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ f ↑{ val := a, property := b } = x
[PROOFSTEP]
exact hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x
[PROOFSTEP]
simp [range_subset_iff, funext_iff, mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s
[PROOFSTEP]
rw [compl_eq_univ_diff, image_diff_preimage, image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s = range fun x => f ↑x
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x => f ↑x
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x => f ↑x
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
[PROOFSTEP]
rintro ⟨x, h1, h2⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x => f ↑x
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
[PROOFSTEP]
exact ⟨⟨x, h1⟩, h2⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
[PROOFSTEP]
rintro ⟨⟨x, h1⟩, h2⟩
[GOAL]
case h.mpr.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x => f ↑x) { val := x, property := h1 } = x✝
⊢ x✝ ∈ f '' s
[PROOFSTEP]
exact ⟨x, h1, h2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g
[PROOFSTEP]
by_cases h : p
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range (if p then f else g) ⊆ range f ∪ range g
[PROOFSTEP]
rw [if_pos h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : p
⊢ range f ⊆ range f ∪ range g
[PROOFSTEP]
exact subset_union_left _ _
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range (if p then f else g) ⊆ range f ∪ range g
[PROOFSTEP]
rw [if_neg h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : Prop
inst✝ : Decidable p
f g : α → β
h : ¬p
⊢ range g ⊆ range f ∪ range g
[PROOFSTEP]
exact subset_union_right _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ (range fun x => if p x then f x else g x) ⊆ range f ∪ range g
[PROOFSTEP]
rw [range_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
⊢ ∀ (y : α), (if p y then f y else g y) ∈ range f ∪ range g
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
⊢ (if p x then f x else g x) ∈ range f ∪ range g
[PROOFSTEP]
by_cases h : p x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
[PROOFSTEP]
simp [if_pos h, mem_union, mem_range_self]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
f g : α → β
x : α
h : ¬p x
⊢ (if p x then f x else g x) ∈ range f ∪ range g
[PROOFSTEP]
simp [if_neg h, mem_union, mem_range_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
⊢ range f = {f default}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
⊢ x ∈ range f ↔ x ∈ {f default}
[PROOFSTEP]
rw [mem_range]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
⊢ (∃ y, f y = x) ↔ x ∈ {f default}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
⊢ (∃ y, f y = x) → x ∈ {f default}
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
i : ι
hi : f i = x
⊢ x ∈ {f default}
[PROOFSTEP]
rw [h.uniq i] at hi
[GOAL]
case h.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
i : ι
hi : f default = x
⊢ x ∈ {f default}
[PROOFSTEP]
exact hi ▸ mem_singleton _
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : Unique ι
x : α
⊢ x ∈ {f default} → ∃ y, f y = x
[PROOFSTEP]
exact fun h => ⟨default, h.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}
[PROOFSTEP]
ext
  ⟨x, hx⟩
      -- Porting note: `simp [inclusion]` doesn't solve goal
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) ↔ { val := x, property := hx } ∈ {x | ↑x ∈ s}
[PROOFSTEP]
apply Iff.intro
[GOAL]
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) → { val := x, property := hx } ∈ {x | ↑x ∈ s}
[PROOFSTEP]
rw [mem_range]
[GOAL]
case h.mk.mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ (∃ y, inclusion h y = { val := x, property := hx }) → { val := x, property := hx } ∈ {x | ↑x ∈ s}
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : inclusion h a = { val := x, property := hx }
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
[PROOFSTEP]
rw [inclusion, Subtype.mk.injEq] at ha
[GOAL]
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
[PROOFSTEP]
rw [mem_setOf, Subtype.coe_mk, ← ha]
[GOAL]
case h.mk.mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ ↑a ∈ s
[PROOFSTEP]
exact Subtype.coe_prop _
[GOAL]
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
[PROOFSTEP]
rw [mem_setOf, Subtype.coe_mk, mem_range]
[GOAL]
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ x ∈ s → ∃ y, inclusion h y = { val := x, property := hx }
[PROOFSTEP]
intro hx'
[GOAL]
case h.mk.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ ∃ y, inclusion h y = { val := x, property := hx }
[PROOFSTEP]
use⟨x, hx'⟩
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ inclusion h { val := x, property := hx' } = { val := x, property := hx }
[PROOFSTEP]
trivial
  -- simp_rw [inclusion, mem_range, Subtype.mk_eq_mk]
    -- rw [SetCoe.exists, Subtype.coe_mk, exists_prop, exists_eq_right, mem_set_of, Subtype.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
⊢ f ∘ rangeSplitting f = Subtype.val
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x✝ : ↑(range f)
⊢ (f ∘ rangeSplitting f) x✝ = ↑x✝
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x✝ : ↑(range f)
⊢ f (rangeSplitting f x✝) = ↑x✝
[PROOFSTEP]
apply apply_rangeSplitting
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ rangeFactorization f (rangeSplitting f x) = x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ ↑(rangeFactorization f (rangeSplitting f x)) = ↑x
[PROOFSTEP]
simp only [rangeFactorization_coe]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
f✝ : ι → α
s t : Set α
f : α → β
x : ↑(range f)
⊢ f (rangeSplitting f x) = ↑x
[PROOFSTEP]
apply apply_rangeSplitting
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s✝ : Set α✝
α : Type u_6
β : Type u_7
f : α → β
hf : Surjective f
s : Set β
hs : Set.Subsingleton (f ⁻¹' s)
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
⊢ fx = fy
[PROOFSTEP]
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s✝ : Set α✝
α : Type u_6
β : Type u_7
f : α → β
hf : Surjective f
s : Set β
hs : Set.Subsingleton (f ⁻¹' s)
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y
[PROOFSTEP]
exact congr_arg f (hs hx hy)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s✝ : Set α
s : Set β
hs : Set.Nontrivial s
f : α → β
hf : Surjective f
⊢ Set.Nontrivial (f ⁻¹' s)
[PROOFSTEP]
rcases hs with ⟨fx, hx, fy, hy, hxy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ Set.Nontrivial (f ⁻¹' s)
[PROOFSTEP]
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ Set.Nontrivial (f ⁻¹' s)
[PROOFSTEP]
exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
⊢ Surjective (preimage f)
[PROOFSTEP]
intro s
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
⊢ ∃ a, f ⁻¹' a = s
[PROOFSTEP]
use f '' s
[GOAL]
case h
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
⊢ f ⁻¹' (f '' s) = s
[PROOFSTEP]
rw [hf.preimage_image]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Surjective f
⊢ Surjective (image f)
[PROOFSTEP]
intro s
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s
[PROOFSTEP]
use f ⁻¹' s
[GOAL]
case h
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Surjective f
s : Set β
⊢ f '' (f ⁻¹' s) = s
[PROOFSTEP]
rw [hf.image_preimage]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Surjective f
s : Set β
⊢ Set.Nonempty (f ⁻¹' s) ↔ Set.Nonempty s
[PROOFSTEP]
rw [← nonempty_image_iff, hf.image_preimage]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
⊢ Injective (image f)
[PROOFSTEP]
intro s t h
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
[PROOFSTEP]
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
[PROOFSTEP]
apply Set.preimage_subset_preimage_iff
[GOAL]
case hs
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
[PROOFSTEP]
rw [Function.Surjective.range_eq hf]
[GOAL]
case hs
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ
[PROOFSTEP]
apply subset_univ
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
y : β
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ
[PROOFSTEP]
rcases em (y ∈ range f) with (⟨x, rfl⟩ | hx)
[GOAL]
case h.inl.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
x : α
⊢ f x ∈ (f '' s)ᶜ ↔ f x ∈ f '' sᶜ ∪ (range f)ᶜ
[PROOFSTEP]
simp [hf.eq_iff]
[GOAL]
case h.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
y : β
hx : ¬y ∈ range f
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ
[PROOFSTEP]
rw [mem_range, not_exists] at hx
[GOAL]
case h.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
hf : Injective f
s : Set α
y : β
hx : ∀ (x : α), ¬f x = y
⊢ y ∈ (f '' s)ᶜ ↔ y ∈ f '' sᶜ ∪ (range f)ᶜ
[PROOFSTEP]
simp [hx]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' (f '' s) = s
[PROOFSTEP]
rw [← image_comp, h.comp_eq_id, image_id]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' (g ⁻¹' s) = s
[PROOFSTEP]
rw [← preimage_comp, h.comp_eq_id, preimage_id]
[GOAL]
α : Type u_1
s t : Set α
h : t ⊆ s
⊢ val '' {x | ↑x ∈ t} = t
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t
[PROOFSTEP]
rw [Set.mem_image]
[GOAL]
case h
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t
[PROOFSTEP]
exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩
[GOAL]
α : Type u_1
s : Set α
⊢ range val = s
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
α : Type u_1
s : Set α
⊢ val '' univ = s
[PROOFSTEP]
simp [-Set.image_univ, coe_image]
[GOAL]
α : Type u_1
s : Set α
⊢ val ⁻¹' s = univ
[PROOFSTEP]
rw [← preimage_range, range_coe]
[GOAL]
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ x ∈ s
[PROOFSTEP]
rw [← yvaleq]
[GOAL]
α : Type u_1
s : Set α
t : Set ↑s
x : α
x✝ : x ∈ val '' t
y : { x // x ∈ s }
left✝ : y ∈ t
yvaleq : ↑y = x
⊢ ↑y ∈ s
[PROOFSTEP]
exact y.property
[GOAL]
α : Type u_1
s t u : Set α
⊢ val ⁻¹' t = val ⁻¹' u ↔ t ∩ s = u ∩ s
[PROOFSTEP]
rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]
[GOAL]
α : Type u_1
s t : Set α
⊢ val ⁻¹' (t ∩ s) = val ⁻¹' t
[PROOFSTEP]
rw [preimage_coe_eq_preimage_coe_iff, inter_assoc, inter_self]
[GOAL]
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ s, p (val '' s)) ↔ ∃ s, s ⊆ t ∧ p s
[PROOFSTEP]
rw [← exists_subset_range_and_iff, range_coe]
[GOAL]
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set ↑t), p (val '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s
[PROOFSTEP]
rw [← forall_subset_range_iff, range_coe]
[GOAL]
α : Type u_1
s t : Set α
⊢ Set.Nonempty (val ⁻¹' t) ↔ Set.Nonempty (s ∩ t)
[PROOFSTEP]
rw [inter_comm, ← image_preimage_coe, nonempty_image_iff]
[GOAL]
α : Type u_1
s t : Set α
⊢ val ⁻¹' t = ∅ ↔ s ∩ t = ∅
[PROOFSTEP]
simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)
[PROOFSTEP]
simp only [mem_range, not_exists, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ (Injective fun x => f (some x)) ∧ ∀ (x : α), ¬f (some x) = f none
[PROOFSTEP]
refine' ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, _⟩
[GOAL]
α : Type u_1
β : Type u_2
f : Option α → β
⊢ ((Injective fun x => f (some x)) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
[PROOFSTEP]
rintro ⟨h_some, h_none⟩ (_ | a) (_ | b) hab
[GOAL]
case intro.none.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective fun x => f (some x)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ none = none
case intro.none.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective fun x => f (some x)
h_none : ∀ (x : α), ¬f (some x) = f none
b : α
hab : f none = f (some b)
⊢ none = some b
case intro.some.none
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective fun x => f (some x)
h_none : ∀ (x : α), ¬f (some x) = f none
a : α
hab : f (some a) = f none
⊢ some a = none
case intro.some.some
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective fun x => f (some x)
h_none : ∀ (x : α), ¬f (some x) = f none
a b : α
hab : f (some a) = f (some b)
⊢ some a = some b
[PROOFSTEP]
exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]
[GOAL]
α : Type u
β : Type v
f : α → β
⊢ Injective (preimage f) ↔ Surjective f
[PROOFSTEP]
refine' ⟨fun h y => _, Surjective.preimage_injective⟩
[GOAL]
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ ∃ a, f a = y
[PROOFSTEP]
obtain ⟨x, hx⟩ : (f ⁻¹' { y }).Nonempty :=
  by
  rw [h.nonempty_apply_iff preimage_empty]
  apply singleton_nonempty
[GOAL]
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ Set.Nonempty (f ⁻¹' {y})
[PROOFSTEP]
rw [h.nonempty_apply_iff preimage_empty]
[GOAL]
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ Set.Nonempty {y}
[PROOFSTEP]
apply singleton_nonempty
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
x : α
hx : x ∈ f ⁻¹' {y}
⊢ ∃ a, f a = y
[PROOFSTEP]
exact ⟨x, hx⟩
[GOAL]
α : Type u
β : Type v
f : α → β
⊢ Surjective (preimage f) ↔ Injective f
[PROOFSTEP]
refine' ⟨fun h x x' hx => _, Injective.preimage_surjective⟩
[GOAL]
α : Type u
β : Type v
f : α → β
h : Surjective (preimage f)
x x' : α
hx : f x = f x'
⊢ x = x'
[PROOFSTEP]
cases' h { x } with s hs
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (preimage f)
x x' : α
hx : f x = f x'
s : Set β
hs : f ⁻¹' s = {x}
⊢ x = x'
[PROOFSTEP]
have := mem_singleton x
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (preimage f)
x x' : α
hx : f x = f x'
s : Set β
hs : f ⁻¹' s = {x}
this : x ∈ {x}
⊢ x = x'
[PROOFSTEP]
rwa [← hs, mem_preimage, hx, ← mem_preimage, hs, mem_singleton_iff, eq_comm] at this
[GOAL]
α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f
[PROOFSTEP]
refine' ⟨fun h y => _, Surjective.image_surjective⟩
[GOAL]
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
⊢ ∃ a, f a = y
[PROOFSTEP]
cases' h { y } with s hs
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ ∃ a, f a = y
[PROOFSTEP]
have := mem_singleton y
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ {y}
⊢ ∃ a, f a = y
[PROOFSTEP]
rw [← hs] at this
[GOAL]
case intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ a, f a = y
[PROOFSTEP]
rcases this with ⟨x, _, hx⟩
[GOAL]
case intro.intro.intro
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left✝ : x ∈ s
hx : f x = y
⊢ ∃ a, f a = y
[PROOFSTEP]
exact ⟨x, hx⟩
[GOAL]
α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f
[PROOFSTEP]
refine' ⟨fun h x x' hx => _, Injective.image_injective⟩
[GOAL]
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'
[PROOFSTEP]
rw [← singleton_eq_singleton_iff]
[GOAL]
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}
[PROOFSTEP]
apply h
[GOAL]
case a
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}
[PROOFSTEP]
rw [image_singleton, image_singleton, hx]
[GOAL]
α : Type u
β : Type v
f✝ f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f ⁻¹' s = t ↔ s = f '' t
[PROOFSTEP]
rw [← image_eq_image hf.1, hf.2.image_preimage]
[GOAL]
α : Type u
β : Type v
f✝ f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ s = f ⁻¹' t ↔ f '' s = t
[PROOFSTEP]
rw [← image_eq_image hf.1, hf.2.image_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β
s✝ t✝ : Set α
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
⊢ f '' s ⊓ g '' t ≤ ⊥
[PROOFSTEP]
rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f✝ : α → β
s✝ t✝ : Set α
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ g c ∈ ⊥
[PROOFSTEP]
exact h b hb c hc eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t✝ : Set α
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint s t
[PROOFSTEP]
rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq, image_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t : Set α
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅
[PROOFSTEP]
simpa using h.preimage f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t : Set α
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)
[PROOFSTEP]
simp only [eq_empty_iff_forall_not_mem, disjoint_iff_inter_eq_empty, not_exists, mem_inter_iff, not_and, mem_range,
  mem_preimage] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ ∀ (x : β), x ∈ s → ∀ (x_1 : α), ¬f x_1 = x
[PROOFSTEP]
intro y hy x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ False
[PROOFSTEP]
rw [← hx] at hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s✝ t : Set α
s : Set β
h : ∀ (x : α), ¬f x ∈ s
y : β
x : α
hy : f x ∈ s
hx : f x = y
⊢ False
[PROOFSTEP]
exact h x hy
[GOAL]
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' (Sigma.mk i '' s) = ∅
[PROOFSTEP]
change Sigma.mk j ⁻¹' {⟨i, u⟩ | u ∈ s} = ∅
[GOAL]
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
h : i ≠ j
⊢ Sigma.mk j ⁻¹' {x | ∃ u, u ∈ s ∧ { fst := i, snd := u } = x} = ∅
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
⊢ Sigma.mk i ⁻¹' (Sigma.mk i '' s) = s
[PROOFSTEP]
change Sigma.mk i ⁻¹' {⟨i, u⟩ | u ∈ s} = s
[GOAL]
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
⊢ Sigma.mk i ⁻¹' {x | ∃ u, u ∈ s ∧ { fst := i, snd := u } = x} = s
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}
[PROOFSTEP]
refine' antisymm (range_subset_iff.2 fun l => forall_mem_map_iff.2 fun y _ => mem_range_self _) fun l hl => _
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
f : α → β
l : List β
hl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ l ∈ range (map f)
[PROOFSTEP]
induction' l with a l ihl
[GOAL]
case nil
α : Type u_1
β : Type u_2
l✝ : List α
f : α → β
l : List β
hl✝ : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
hl : [] ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ [] ∈ range (map f)
[PROOFSTEP]
exact ⟨[], rfl⟩
[GOAL]
case cons
α : Type u_1
β : Type u_2
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List β
ihl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: l ∈ range (map f)
[PROOFSTEP]
rcases ihl fun x hx => hl x <| subset_cons _ _ hx with ⟨l, rfl⟩
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: map f l ∈ range (map f)
[PROOFSTEP]
rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
[GOAL]
case cons.intro.intro
α : Type u_1
β : Type u_2
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ f a :: map f l ∈ range (map f)
[PROOFSTEP]
exact ⟨a :: l, map_cons _ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
l : List α
s : Set α
⊢ range (map Subtype.val) = {l | ∀ (x : α), x ∈ l → x ∈ s}
[PROOFSTEP]
rw [range_list_map, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ (range fun k => nthLe l ↑k (_ : ↑k < length l)) = {x | x ∈ l}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ x ∈ {x | x ∈ l}
[PROOFSTEP]
rw [mem_setOf_eq, mem_iff_get]
[GOAL]
case h
α : Type u_1
β : Type u_2
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ ∃ n, List.get l n = x
[PROOFSTEP]
exact ⟨fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩, fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ range (get? l) = insert none (some '' {x | x ∈ l})
[PROOFSTEP]
rw [← range_list_nthLe, ← range_comp]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ range (get? l) = insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
[PROOFSTEP]
refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset_iff.2 ⟨_, _⟩)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : List α
n : ℕ
⊢ get? l n ∈ insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
case refine'_2
α : Type u_1
β : Type u_2
l : List α
⊢ none ∈ range (get? l)
case refine'_3
α : Type u_1
β : Type u_2
l : List α
⊢ range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)) ⊆ range (get? l)
[PROOFSTEP]
exacts [(le_or_lt l.length n).imp get?_eq_none.2 (fun hlt => ⟨⟨_, hlt⟩, (get?_eq_get hlt).symm⟩),
  ⟨_, get?_eq_none.2 le_rfl⟩, range_subset_iff.2 <| fun k => ⟨_, get?_eq_get _⟩]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
d : α
⊢ (range fun n => getD l n d) = (fun o => Option.getD o d) '' range (get? l)
[PROOFSTEP]
simp only [← range_comp, (· ∘ ·), getD_eq_getD_get?]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
d : α
⊢ (fun o => Option.getD o d) '' range (get? l) = insert d {x | x ∈ l}
[PROOFSTEP]
simp only [range_list_get?, image_insert_eq, Option.getD, image_image, image_id']
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ ∃ y, map c y = l
[PROOFSTEP]
rw [← Set.mem_range, Set.range_list_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}
[PROOFSTEP]
exact fun a ha => CanLift.prf a (H a ha)


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : κ), f n) r ↔ ∀ (n : κ), Set.Pairwise (f n) r
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ Set.Pairwise (⋃ (n : κ), f n) r → ∀ (n : κ), Set.Pairwise (f n) r
[PROOFSTEP]
intro H n
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : Set.Pairwise (⋃ (n : κ), f n) r
n : κ
⊢ Set.Pairwise (f n) r
[PROOFSTEP]
exact Pairwise.mono (subset_iUnion _ _) H
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
⊢ (∀ (n : κ), Set.Pairwise (f n) r) → Set.Pairwise (⋃ (n : κ), f n) r
[PROOFSTEP]
intro H i hi j hj hij
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
⊢ r i j
[PROOFSTEP]
rcases mem_iUnion.1 hi with ⟨m, hm⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j
[PROOFSTEP]
rcases mem_iUnion.1 hj with ⟨n, hn⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j
[PROOFSTEP]
rcases h m n with ⟨p, mp, np⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p✝ q : α → α → Prop
f✝ g : ι → α
s t u : Set α
a b : α
f : κ → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
H : ∀ (n : κ), Set.Pairwise (f n) r
i : α
hi : i ∈ ⋃ (n : κ), f n
j : α
hj : j ∈ ⋃ (n : κ), f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j
[PROOFSTEP]
exact H p (mp hm) (np hn) hij
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r✝ p q : α → α → Prop
f g : ι → α
s✝ t u : Set α
a b : α
r : α → α → Prop
s : Set (Set α)
h : DirectedOn (fun x x_1 => x ⊆ x_1) s
⊢ Set.Pairwise (⋃₀ s) r ↔ ∀ (a : Set α), a ∈ s → Set.Pairwise a r
[PROOFSTEP]
rw [sUnion_eq_iUnion, pairwise_iUnion h.directed_val, SetCoe.forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
⊢ PairwiseDisjoint (⋃ (i : ι') (_ : i ∈ s), g i) f
[PROOFSTEP]
rintro a ha b hb hab
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a : ι
ha : a ∈ ⋃ (i : ι') (_ : i ∈ s), g i
b : ι
hb : b ∈ ⋃ (i : ι') (_ : i ∈ s), g i
hab : a ≠ b
⊢ (Disjoint on f) a b
[PROOFSTEP]
simp_rw [Set.mem_iUnion] at ha hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a b : ι
hab : a ≠ b
ha : ∃ i i_1, a ∈ g i
hb : ∃ i i_1, b ∈ g i
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain ⟨c, hc, ha⟩ := ha
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a b : ι
hab : a ≠ b
hb : ∃ i i_1, b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain ⟨d, hd, hb⟩ := hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b
[PROOFSTEP]
obtain hcd | hcd := eq_or_ne (g c) (g d)
[GOAL]
case intro.intro.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact hg d hd (hcd.subst ha) hb hab
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s✝ : Set ι
t s : Set ι'
g : ι' → Set ι
f : ι → α
hs : PairwiseDisjoint s fun i' => ⨆ (i : ι) (_ : i ∈ g i'), f i
hg : ∀ (i : ι'), i ∈ s → PairwiseDisjoint (g i) f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b
[PROOFSTEP]
exact
  (hs hc hd <| ne_of_apply_ne _ hcd).mono (le_iSup₂ (f := fun i (_ : i ∈ g c) => f i) a ha)
    (le_iSup₂ (f := fun i (_ : i ∈ g d) => f i) b hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
⊢ PairwiseDisjoint (s ×ˢ t) f
[PROOFSTEP]
rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
rw [mem_prod] at hi hj
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')
[PROOFSTEP]
refine' (ht hi.2 hj.2 <| (Prod.mk.inj_left _).ne_iff.1 h).mono _ _
[GOAL]
case mk.mk.inl.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) (i, i').snd
[PROOFSTEP]
convert le_iSup₂ (α := α) i hi.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') = f (i, (i, i').snd)
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) (i, j').snd
[PROOFSTEP]
convert le_iSup₂ (α := α) i hj.1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j' : ι'
hj : (i, j').fst ∈ s ∧ (i, j').snd ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') = f (i, (i, j').snd)
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')
[PROOFSTEP]
refine' (hs hi.1 hj.1 hij).mono _ _
[GOAL]
case mk.mk.inr.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) (i, i').fst
[PROOFSTEP]
convert le_iSup₂ (α := α) i' hi.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') = f ((i, i').fst, i')
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) (j, j').fst
[PROOFSTEP]
convert le_iSup₂ (α := α) j' hj.2
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')
ht : PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
i : ι
i' : ι'
hi : (i, i').fst ∈ s ∧ (i, i').snd ∈ t
j : ι
j' : ι'
hj : (j, j').fst ∈ s ∧ (j, j').snd ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') = f ((j, j').fst, j')
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ PairwiseDisjoint (s ×ˢ t) f ↔
    (PairwiseDisjoint s fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) ∧
      PairwiseDisjoint t fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')
[PROOFSTEP]
refine' ⟨fun h => ⟨fun i hi j hj hij => _, fun i hi j hj hij => _⟩, fun h => h.1.prod_left h.2⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ (Disjoint on fun i => ⨆ (i' : ι') (_ : i' ∈ t), f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ (Disjoint on fun i' => ⨆ (i : ι) (_ : i ∈ s), f (i, i')) i j
[PROOFSTEP]
simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ (i_1 : ι'), i_1 ∈ t → ∀ (i_3 : ι'), i_3 ∈ t → Disjoint (f (i, i_1)) (f (j, i_3))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ (i_1 : ι), i_1 ∈ s → ∀ (i_3 : ι), i_3 ∈ s → Disjoint (f (i_1, i)) (f (i_3, j))
[PROOFSTEP]
intro i' hi' j' hj'
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))
[PROOFSTEP]
exact h (mk_mem_prod hi hi') (mk_mem_prod hj hj') (ne_of_apply_ne Prod.fst hij)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : PairwiseDisjoint (s ×ˢ t) f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))
[PROOFSTEP]
exact h (mk_mem_prod hi' hi) (mk_mem_prod hj' hj) (ne_of_apply_ne Prod.snd hij)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
⊢ (⋃ (i : ι) (_ : i ∈ s), f i) \ ⋃ (i : ι) (_ : i ∈ t), f i = ⋃ (i : ι) (_ : i ∈ s \ t), f i
[PROOFSTEP]
refine'
  (biUnion_diff_biUnion_subset f s t).antisymm (iUnion₂_subset fun i hi a ha => (mem_diff _).2 ⟨mem_biUnion hi.1 ha, _⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬a ∈ ⋃ (x : ι) (_ : x ∈ t), f x
[PROOFSTEP]
rw [mem_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
⊢ ¬∃ i j, a ∈ f i
[PROOFSTEP]
rintro ⟨j, hj, haj⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
s t : Set ι
f : ι → Set α
h : PairwiseDisjoint (s ∪ t) f
i : ι
hi : i ∈ s \ t
a : α
ha : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ False
[PROOFSTEP]
exact (h (Or.inl hi.1) (Or.inr hj) (ne_of_mem_of_not_mem hj hi.2).symm).le_bot ⟨ha, haj⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
⊢ s ⊆ t
[PROOFSTEP]
rintro i hi
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
⊢ i ∈ t
[PROOFSTEP]
obtain ⟨a, hai⟩ := h₁ i hi
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
⊢ i ∈ t
[PROOFSTEP]
obtain ⟨j, hj, haj⟩ := mem_iUnion₂.1 (h <| mem_iUnion₂_of_mem hi hai)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
κ : Sort u_6
r p q : α → α → Prop
f : ι → Set α
s t : Set ι
h₀ : PairwiseDisjoint (s ∪ t) f
h₁ : ∀ (i : ι), i ∈ s → Set.Nonempty (f i)
h : ⋃ (i : ι) (_ : i ∈ s), f i ⊆ ⋃ (i : ι) (_ : i ∈ t), f i
i : ι
hi : i ∈ s
a : α
hai : a ∈ f i
j : ι
hj : j ∈ t
haj : a ∈ f j
⊢ i ∈ t
[PROOFSTEP]
rwa [h₀.eq (subset_union_left _ _ hi) (subset_union_right _ _ hj) (not_disjoint_iff.2 ⟨a, hai, haj⟩)]


[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
refine' ⟨_, fun ⟨b, hb⟩ x y hx hy => (hb x hx).2.trans (add_le_add_right (hb y hy).1 _)⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u_1
β : Type u_2
f : α → ℕ
⊢ EquitableOn ∅ f → ∃ b, ∀ (a : α), a ∈ ∅ → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ EquitableOn s f → ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
intro hs
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
by_cases h : ∀ y ∈ s, f x ≤ f y
[GOAL]
case pos
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ∀ (y : α), y ∈ s → f x ≤ f y
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
exact ⟨f x, fun y hy => ⟨h _ hy, hs hy hx⟩⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ¬∀ (y : α), y ∈ s → f x ≤ f y
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
h : ∃ y, y ∈ s ∧ f y < f x
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
obtain ⟨w, hw, hwx⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
⊢ ∃ b, ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
refine' ⟨f w, fun y hy => ⟨Nat.le_of_succ_le_succ _, hs hy hw⟩⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ Nat.succ (f w) ≤ Nat.succ (f y)
[PROOFSTEP]
rw [(Nat.succ_le_of_lt hwx).antisymm (hs hx hw)]
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
hs : EquitableOn s f
w : α
hw : w ∈ s
hwx : f w < f x
y : α
hy : y ∈ s
⊢ f x ≤ Nat.succ (f y)
[PROOFSTEP]
exact hs hx hy
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, f '' s ⊆ Icc b (b + 1)
[PROOFSTEP]
simpa only [image_subset_iff] using equitableOn_iff_exists_le_le_add_one
[GOAL]
α : Type u_1
β : Type u_2
s : Set α
f : α → ℕ
⊢ EquitableOn s f ↔ ∃ b, ∀ (a : α), a ∈ s → f a = b ∨ f a = b + 1
[PROOFSTEP]
simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f i ≤ f j + 1
[PROOFSTEP]
rw [hs hi hj]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : OrderedSemiring β
s : Set α
hs : Set.Subsingleton s
f : α → β
i j : α
hi : i ∈ s
hj : j ∈ s
⊢ f j ≤ f j + 1
[PROOFSTEP]
exact le_add_of_nonneg_right zero_le_one
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
⊢ EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
rw [Set.equitableOn_iff_exists_le_le_add_one]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) ↔
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
refine' ⟨_, fun h => ⟨_, h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
⊢ (∃ b, ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1) →
    ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
rintro ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
by_cases h : ∀ a ∈ s, f a = b + 1
[GOAL]
case pos
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
intro a ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
[GOAL]
case pos
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a✝ : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∀ (a : α), a ∈ s → f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
[PROOFSTEP]
exact ⟨le_rfl, Nat.le_succ _⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ¬∀ (a : α), a ∈ s → f a = b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
h : ∃ a, a ∈ s ∧ f a ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ := h
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
suffices h : b = (∑ i in s, f i) / s.card
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → (∑ i in s, f i) / card s ≤ f a ∧ f a ≤ (∑ i in s, f i) / card s + 1
[PROOFSTEP]
simp_rw [← h]
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i in s, f i) / card s
⊢ ∀ (a : α), a ∈ s → b ≤ f a ∧ f a ≤ b + 1
[PROOFSTEP]
apply hb
[GOAL]
case h
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b = (∑ i in s, f i) / card s
[PROOFSTEP]
symm
[GOAL]
case h
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ (∑ i in s, f i) / card s = b
[PROOFSTEP]
refine'
  Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
    ((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le _)
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ b * card s ≤ ∑ i in s, b
[PROOFSTEP]
simp [mul_comm]
[GOAL]
case h
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i in s, (b + 1) ≤ Nat.succ b * card s
[PROOFSTEP]
rw [mul_comm, sum_const_nat]
[GOAL]
case h
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
b : ℕ
hb : ∀ (a : α), a ∈ ↑s → b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ (x : α), x ∈ s → b + 1 = Nat.succ b
[PROOFSTEP]
exact fun _ _ => rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
f : α → ℕ
a : α
⊢ EquitableOn (↑s) f ↔ ∀ (a : α), a ∈ s → f a = (∑ i in s, f i) / card s ∨ f a = (∑ i in s, f i) / card s + 1
[PROOFSTEP]
simp_rw [equitableOn_iff_le_le_add_one, Nat.le_and_le_add_one_iff]


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : LE α
x : α
z : β
⊢ z ∈ Accumulate s x ↔ ∃ y, y ≤ x ∧ z ∈ s y
[PROOFSTEP]
simp_rw [accumulate_def, mem_iUnion₂, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), Accumulate s y = ⋃ (y : α) (_ : y ≤ x), s y
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), Accumulate s y ⊆ ⋃ (y : α) (_ : y ≤ x), s y
[PROOFSTEP]
exact iUnion₂_subset fun y hy => monotone_accumulate hy
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
x : α
⊢ ⋃ (y : α) (_ : y ≤ x), s y ⊆ ⋃ (y : α) (_ : y ≤ x), Accumulate s y
[PROOFSTEP]
exact iUnion₂_mono fun y _ => subset_accumulate
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), Accumulate s x = ⋃ (x : α), s x
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), Accumulate s x ⊆ ⋃ (x : α), s x
[PROOFSTEP]
simp only [subset_def, mem_iUnion, exists_imp, mem_accumulate]
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ∀ (x : β) (x_1 x_2 : α), x_2 ≤ x_1 ∧ x ∈ s x_2 → ∃ i, x ∈ s i
[PROOFSTEP]
intro z x x' ⟨_, hz⟩
[GOAL]
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
z : β
x x' : α
left✝ : x' ≤ x
hz : z ∈ s x'
⊢ ∃ i, z ∈ s i
[PROOFSTEP]
exact ⟨x', hz⟩
[GOAL]
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
s : α → Set β
t : α → Set γ
inst✝ : Preorder α
⊢ ⋃ (x : α), s x ⊆ ⋃ (x : α), Accumulate s x
[PROOFSTEP]
exact iUnion_mono fun i => subset_accumulate