[GOAL]
α : Type u_1
s t : Set α
h₁ : s = t
x✝ : α
h₂ : x✝ ∈ s
⊢ x✝ ∈ t
[PROOFSTEP]
rw [← h₁]
[GOAL]
α : Type u_1
s t : Set α
h₁ : s = t
x✝ : α
h₂ : x✝ ∈ s
⊢ x✝ ∈ s
[PROOFSTEP]
exact h₂
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
h : s = t
x : α
⊢ x ∈ s ↔ x ∈ t
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p : α → β → Prop
⊢ (∀ (a : α), a ∈ s → ∀ (b : β), p a b) ↔ ∀ (b : β) (a : α), a ∈ s → p a b
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsRefl (Set α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsTrans (Set α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun x x_1 => x ≤ x_1) (fun x x_1 => x ≤ x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsAntisymm (Set α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsIrrefl (Set α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsTrans (Set α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun x x_1 => x < x_1) (fun x x_1 => x ≤ x_1) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Trans (fun x x_1 => x ≤ x_1) (fun x x_1 => x < x_1) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ IsAsymm (Set α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ ¬s ⊆ t ↔ ∃ a, a ∈ s ∧ ¬a ∈ t
[PROOFSTEP]
simp only [subset_def, not_forall, exists_prop]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Set.Nonempty (s ∩ t) ↔ ∃ x, x ∈ s ∧ x ∈ t
[PROOFSTEP]
simp_rw [inter_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Set.Nonempty (s ∩ t) ↔ ∃ x, x ∈ t ∧ x ∈ s
[PROOFSTEP]
simp_rw [inter_nonempty, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ ¬Set.Nonempty s ↔ s = ∅
[PROOFSTEP]
simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ ¬Nonempty ↑s ↔ s = ∅
[PROOFSTEP]
rw [nonempty_subtype, not_exists, eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ ¬IsEmpty ↑s ↔ ¬s = ∅
[PROOFSTEP]
simpa using nonempty_iff_ne_empty
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Subsingleton α
⊢ Set.Nonempty s → s = univ
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
[PROOFSTEP]
refine' eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s
[PROOFSTEP]
rwa [Subsingleton.elim y x]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α✝
s✝ s₁ s₂ t t₁ t₂ u : Set α✝
α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ∃ a, ¬a ∈ s
[PROOFSTEP]
rw [← not_forall, ← eq_univ_iff_forall]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α✝
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α✝
α : Type u_1
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t
[PROOFSTEP]
simp [subset_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅
[PROOFSTEP]
simp only [← subset_empty_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
[PROOFSTEP]
exact union_subset_iff
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
[PROOFSTEP]
simp only [subset_def, mem_insert_iff, or_imp, forall_and, forall_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t
[PROOFSTEP]
refine' ⟨fun h x hx => _, insert_subset_insert⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
⊢ x ∈ t
[PROOFSTEP]
rcases h (subset_insert _ _ hx) with (rfl | hxt)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hx : x ∈ s
ha : ¬x ∈ s
h : insert x s ⊆ insert x t
⊢ x ∈ t
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : ¬a ∈ s
h : insert a s ⊆ insert a t
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ t
[PROOFSTEP]
exacts [(ha hx).elim, hxt]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s ⊂ t ↔ ∃ a x, insert a s ⊆ t
[PROOFSTEP]
simp only [insert_subset_iff, exists_and_right, ssubset_def, not_subset]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ (s ⊆ t ∧ ∃ a, a ∈ t ∧ ¬a ∈ s) ↔ (∃ x x_1, x ∈ t) ∧ s ⊆ t
[PROOFSTEP]
simp only [exists_prop, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
P : α → Prop
a : α
s : Set α
⊢ (∃ x, x ∈ insert a s ∧ P x) ↔ P a ∨ ∃ x, x ∈ s ∧ P x
[PROOFSTEP]
simp [mem_insert_iff, or_and_right, exists_and_left, exists_or]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s s₁ s₂ t t₁ t₂ u : Set α
x a : α
⊢ a ∈ insert x ∅ ↔ a ∈ {x}
[PROOFSTEP]
simp only [mem_empty_iff_false, mem_insert_iff, or_false]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s s₁ s₂ t t₁ t₂ u : Set α
x a : α
⊢ a = x ↔ a ∈ {x}
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ {a} ⊆ {b} ↔ a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Set.Nonempty ({a} ∩ s) ↔ a ∈ s
[PROOFSTEP]
simp only [Set.Nonempty, mem_inter_iff, mem_singleton_iff, exists_eq_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Set.Nonempty (s ∩ {a}) ↔ a ∈ s
[PROOFSTEP]
rw [inter_comm, singleton_inter_nonempty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ s ∩ {a} = ∅ ↔ ¬a ∈ s
[PROOFSTEP]
rw [inter_comm, singleton_inter_eq_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y z w : α
⊢ {x, y} = {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
simp only [Set.Subset.antisymm_iff, Set.insert_subset_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
  Set.singleton_subset_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y z w : α
⊢ ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) → x = z ∧ y = w ∨ x = w ∧ y = z
[PROOFSTEP]
rintro ⟨⟨rfl | rfl, rfl | rfl⟩, ⟨h₁, h₂⟩⟩
[GOAL]
case mp.intro.intro.inl.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
y w : α
h₁ : y = y ∨ y = y
h₂ : w = y ∨ w = y
⊢ y = y ∧ y = w ∨ y = w ∧ y = y
[PROOFSTEP]
simp [h₁, h₂] at *
[GOAL]
case mp.intro.intro.inl.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y : α
h₁ : x = x ∨ x = y
h₂ : y = x ∨ y = y
⊢ x = x ∧ y = y ∨ x = y ∧ y = x
[PROOFSTEP]
simp [h₁, h₂] at *
[GOAL]
case mp.intro.intro.inr.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y : α
h₁ : y = x ∨ y = y
h₂ : x = x ∨ x = y
⊢ x = y ∧ y = x ∨ x = x ∧ y = y
[PROOFSTEP]
simp [h₁, h₂] at *
[GOAL]
case mp.intro.intro.inr.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
y z : α
h₁ : z = y ∨ z = y
h₂ : y = y ∨ y = y
⊢ y = z ∧ y = y ∨ y = y ∧ y = z
[PROOFSTEP]
simp [h₁, h₂] at *
[GOAL]
case mp.intro.intro.inl.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
y w : α
h₁ : True
h₂ : w = y
⊢ y = w
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case mp.intro.intro.inr.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
y z : α
h₁ : z = y
h₂ : True
⊢ y = z
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y z w : α
⊢ x = z ∧ y = w ∨ x = w ∧ y = z → ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y)
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case mpr.inl.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y : α
⊢ ((x = x ∨ x = y) ∧ (y = x ∨ y = y)) ∧ (x = x ∨ x = y) ∧ (y = x ∨ y = y)
[PROOFSTEP]
simp
[GOAL]
case mpr.inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x y : α
⊢ ((x = y ∨ x = x) ∧ (y = y ∨ y = x)) ∧ (y = x ∨ y = y) ∧ (x = x ∨ x = y)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p q : α → Prop
x : α
⊢ {x | x ∈ s ∧ p x} = {x | x ∈ s ∧ q x} ↔ ∀ (x : α), x ∈ s → (p x ↔ q x)
[PROOFSTEP]
simp_rw [ext_iff, mem_sep_iff, and_congr_right_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p q : α → Prop
x : α
⊢ {x | x ∈ s ∧ p x} = s ↔ ∀ (x : α), x ∈ s → p x
[PROOFSTEP]
simp_rw [ext_iff, mem_sep_iff, and_iff_left_iff_imp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p q : α → Prop
x : α
⊢ {x | x ∈ s ∧ p x} = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
[PROOFSTEP]
simp_rw [ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false_iff, not_and]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
⊢ ∅ ⊆ {x} ↔ ∅ = ∅ ∨ ∅ = {x}
[PROOFSTEP]
exact ⟨fun _ => Or.inl rfl, fun _ => empty_subset _⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hs : Set.Nonempty s
⊢ s ⊆ {x} ↔ s = ∅ ∨ s = {x}
[PROOFSTEP]
simp [eq_singleton_iff_nonempty_unique_mem, hs, hs.ne_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅
[PROOFSTEP]
rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false_iff, and_iff_left_iff_imp]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
⊢ s = ∅ → s ≠ {x}
[PROOFSTEP]
exact fun h => h ▸ (singleton_ne_empty _).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
[PROOFSTEP]
rw [disjoint_comm, disjoint_left]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
[PROOFSTEP]
simp only [Ne.def, disjoint_left, @imp_not_comm _ (_ = _), forall_eq']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Disjoint {a} s ↔ ¬a ∈ s
[PROOFSTEP]
simp [Set.disjoint_iff, subset_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ Disjoint {a} {b} ↔ a ≠ b
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Nontrivial α
x : α
⊢ Set.Nonempty {x}ᶜ
[PROOFSTEP]
obtain ⟨y, hy⟩ := exists_ne x
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Nontrivial α
x y : α
hy : y ≠ x
⊢ Set.Nonempty {x}ᶜ
[PROOFSTEP]
exact ⟨y, by simp [hy]⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Nontrivial α
x y : α
hy : y ≠ x
⊢ y ∈ {x}ᶜ
[PROOFSTEP]
simp [hy]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ sᶜ ∪ s = univ
[PROOFSTEP]
rw [union_comm, union_compl_self]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
x : α
⊢ x ∈ s ∧ ¬x ∈ t ↔ x ∈ s ∩ tᶜ
[PROOFSTEP]
simp [mem_compl]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s \ t = tᶜ ∩ s
[PROOFSTEP]
rw [diff_eq, inter_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s \ t ∪ s ∩ t = s
[PROOFSTEP]
rw [union_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ s ∩ t ∪ s \ t = s
[PROOFSTEP]
exact sup_inf_sdiff _ _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ insert x t
[PROOFSTEP]
rw [← union_singleton, union_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
x : α
s t : Set α
⊢ s \ {x} ⊆ t ↔ s ⊆ {x} ∪ t
[PROOFSTEP]
apply diff_subset_iff
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
x : α
s : Set α
⊢ s ⊆ insert x (s \ {x})
[PROOFSTEP]
rw [← diff_singleton_subset_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : a ∈ t
⊢ insert a s \ t = s \ t
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : a ∈ t
x✝ : α
⊢ x✝ ∈ insert a s \ t ↔ x✝ ∈ s \ t
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : a ∈ t
x✝ : α
⊢ x✝ ∈ insert a s \ t → x✝ ∈ s \ t
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, h]
[GOAL]
case h.mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : a ∈ t
x✝ : α
⊢ x✝ ∈ s \ t → x✝ ∈ insert a s \ t
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
⊢ insert a s \ t = insert a (s \ t)
[PROOFSTEP]
classical
ext x
by_cases h' : x ∈ t
· have : x ≠ a := by
    intro H
    rw [H] at h' 
    exact h h'
  simp [h, h', this]
· simp [h, h']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
⊢ insert a s \ t = insert a (s \ t)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
[PROOFSTEP]
by_cases h' : x ∈ t
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
[PROOFSTEP]
have : x ≠ a := by
  intro H
  rw [H] at h' 
  exact h h'
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
⊢ x ≠ a
[PROOFSTEP]
intro H
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
H : x = a
⊢ False
[PROOFSTEP]
rw [H] at h' 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : a ∈ t
H : x = a
⊢ False
[PROOFSTEP]
exact h h'
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : x ∈ t
this : x ≠ a
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
[PROOFSTEP]
simp [h, h', this]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : ¬a ∈ t
x : α
h' : ¬x ∈ t
⊢ x ∈ insert a s \ t ↔ x ∈ insert a (s \ t)
[PROOFSTEP]
simp [h, h']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
⊢ insert a s \ {a} = s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s
[PROOFSTEP]
simp [and_iff_left_of_imp fun hx : x ∈ s => show x ≠ a from fun hxa => h <| hxa ▸ hx]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
⊢ insert a s \ s = {a}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
x✝ : α
⊢ x✝ ∈ insert a s \ s ↔ x✝ ∈ {a}
[PROOFSTEP]
rw [Set.mem_diff, Set.mem_insert_iff, Set.mem_singleton_iff, or_and_right, and_not_self_iff, or_false_iff,
  and_iff_left_iff_imp]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
x✝ : α
⊢ x✝ = a → ¬x✝ ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x✝ : α
h : ¬x✝ ∈ s
⊢ ¬x✝ ∈ s
[PROOFSTEP]
exact h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
h : a ∈ s
⊢ s ∩ insert a t = insert a (s ∩ t)
[PROOFSTEP]
rw [insert_inter_distrib, insert_eq_of_mem h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
h : a ∈ t
⊢ insert a s ∩ t = insert a (s ∩ t)
[PROOFSTEP]
rw [insert_inter_distrib, insert_eq_of_mem h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
h : ¬a ∈ s
⊢ Disjoint {a} s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
a : α
⊢ ¬Disjoint s {a} ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
a : α
s : Set α
⊢ insert a (s \ {a}) = insert a s
[PROOFSTEP]
simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
hab : a ≠ b
s : Set α
⊢ insert a (s \ {b}) = insert a s \ {b}
[PROOFSTEP]
simp_rw [← union_singleton, union_diff_distrib, diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
⊢ 𝒫{x} = {∅, {x}}
[PROOFSTEP]
ext y
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
y : Set α
⊢ y ∈ 𝒫{x} ↔ y ∈ {∅, {x}}
[PROOFSTEP]
rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then s h else t h) ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
[PROOFSTEP]
split_ifs with hp
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : p
⊢ x ∈ s hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
[PROOFSTEP]
exact ⟨fun hx => ⟨fun _ => hx, fun hnp => (hnp hp).elim⟩, fun hx => hx.1 hp⟩
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
s : p → Set α
t : ¬p → Set α
x : α
hp : ¬p
⊢ x ∈ t hp ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h
[PROOFSTEP]
exact
  ⟨fun hx => ⟨fun h => (hp h).elim, fun _ => hx⟩, fun hx => hx.2 hp⟩
    --Porting note: Old proof was `split_ifs; simp [h]`
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else univ) ↔ ∀ (h : p), x ∈ t h
[PROOFSTEP]
simp [mem_dite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then univ else t h) ↔ ∀ (h : ¬p), x ∈ t h
[PROOFSTEP]
simp [mem_dite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else ∅) ↔ ∃ h, x ∈ t h
[PROOFSTEP]
simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ h, x ∈ t h
[PROOFSTEP]
exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : Set α
x : α
⊢ (∃ h, x ∈ t) ↔ p ∧ x ∈ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then ∅ else t h) ↔ ∃ h, x ∈ t h
[PROOFSTEP]
simp only [mem_dite, mem_empty_iff_false, imp_false]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (¬p ∧ ∀ (h : ¬p), x ∈ t h) ↔ ∃ h, x ∈ t h
[PROOFSTEP]
exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : Set α
x : α
⊢ (∃ h, x ∈ t) ↔ ¬p ∧ x ∈ t
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α
⊢ Set.ite t s s' ∩ t = s ∩ t
[PROOFSTEP]
rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α
⊢ Set.ite tᶜ s s' = Set.ite t s' s
[PROOFSTEP]
rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α
⊢ Set.ite t s s' ∩ tᶜ = s' ∩ tᶜ
[PROOFSTEP]
rw [← ite_compl, ite_inter_self]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ Set.ite s s t = s ∪ t
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α
⊢ Set.ite s t s = t ∩ s
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s s' : Set α
⊢ Set.ite ∅ s s' = s'
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s s' : Set α
⊢ Set.ite univ s s' = s
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u t s : Set α
⊢ Set.ite t ∅ s = s \ t
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u t s : Set α
⊢ Set.ite t s ∅ = s ∩ t
[PROOFSTEP]
simp [Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s₁' s₂' : Set α
⊢ Set.ite t (s₁ ∩ s₂) (s₁' ∩ s₂') = Set.ite t s₁ s₁' ∩ Set.ite t s₂ s₂'
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ x ∈ Set.ite t (s₁ ∩ s₂) (s₁' ∩ s₂') ↔ x ∈ Set.ite t s₁ s₁' ∩ Set.ite t s₂ s₂'
[PROOFSTEP]
simp only [Set.ite, Set.mem_inter_iff, Set.mem_diff, Set.mem_union]
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s₁' s₂' : Set α
x : α
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
[PROOFSTEP]
tauto
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s : Set α
⊢ Set.ite t (s₁ ∩ s) (s₂ ∩ s) = Set.ite t s₁ s₂ ∩ s
[PROOFSTEP]
rw [ite_inter_inter, ite_same]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁✝ s₂✝ t✝ t₁ t₂ u t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ Set.ite t s₁ s₂ ∩ s = s₁ ∩ s
[PROOFSTEP]
rw [← ite_inter, ← h, ite_same]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
⊢ u ⊆ Set.ite t s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
[PROOFSTEP]
simp only [subset_def, ← forall_and]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ Set.ite t s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
[PROOFSTEP]
refine' forall_congr' fun x => _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ Set.ite t s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
[PROOFSTEP]
by_cases hx : x ∈ t
[GOAL]
case pos
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
x : α
hx : x ∈ t
⊢ x ∈ u → x ∈ Set.ite t s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
[PROOFSTEP]
simp [*, Set.ite]
[GOAL]
case neg
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ t s s' u : Set α
x : α
hx : ¬x ∈ t
⊢ x ∈ u → x ∈ Set.ite t s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
[PROOFSTEP]
simp [*, Set.ite]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
p : Set α → Prop
hs : Set.Subsingleton s
he : p ∅
h₁ : ∀ (x : α), p {x}
⊢ p s
[PROOFSTEP]
rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s₁ s₂ t t₁ t₂ u : Set α
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
hs : Set.Subsingleton ∅
⊢ p ∅
case inr.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s₁ s₂ t t₁ t₂ u : Set α
p : Set α → Prop
he : p ∅
h₁ : ∀ (x : α), p {x}
x : α
hs : Set.Subsingleton {x}
⊢ p {x}
[PROOFSTEP]
exacts [he, h₁ _]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ (∃ a, s = {a}) ↔ Set.Nonempty s ∧ Set.Subsingleton s
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ (∃ a, s = {a}) → Set.Nonempty s ∧ Set.Subsingleton s
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case refine'_1.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b : α
s₁ s₂ t t₁ t₂ u : Set α
a : α
⊢ Set.Nonempty {a} ∧ Set.Subsingleton {a}
[PROOFSTEP]
exact ⟨singleton_nonempty a, subsingleton_singleton⟩
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
h : Set.Nonempty s ∧ Set.Subsingleton s
⊢ ∃ a, s = {a}
[PROOFSTEP]
exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Subsingleton ↑s ↔ Set.Subsingleton s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Subsingleton ↑s → Set.Subsingleton s
[PROOFSTEP]
refine' fun h => fun a ha b hb => _
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a✝ b✝ : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
h : Subsingleton ↑s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
[PROOFSTEP]
exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Set.Subsingleton s → Subsingleton ↑s
[PROOFSTEP]
exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Subsingleton α
s : Set α
⊢ Subsingleton ↑s
[PROOFSTEP]
rw [s.subsingleton_coe]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u : Set α
inst✝ : Subsingleton α
s : Set α
⊢ Set.Subsingleton s
[PROOFSTEP]
exact subsingleton_of_subsingleton
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
hs : Set.Nontrivial s
z : α
⊢ ∃ x, x ∈ s ∧ x ≠ z
[PROOFSTEP]
by_contra' H
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
hs : Set.Nontrivial s
z : α
H : ∀ (x : α), x ∈ s → x = z
⊢ False
[PROOFSTEP]
rcases hs with ⟨x, hx, y, hy, hxy⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ False
[PROOFSTEP]
rw [H x hx, H y hy] at hxy 
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
z : α
H : ∀ (x : α), x ∈ s → x = z
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : z ≠ z
⊢ False
[PROOFSTEP]
exact hxy rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : Set.Nontrivial {x}
⊢ False
[PROOFSTEP]
rw [nontrivial_iff_exists_ne (mem_singleton x)] at H 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
⊢ False
[PROOFSTEP]
let ⟨y, hy, hya⟩ := H
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
H : ∃ y, y ∈ {x} ∧ y ≠ x
y : α
hy : y ∈ {x}
hya : y ≠ x
⊢ False
[PROOFSTEP]
exact hya (mem_singleton_iff.1 hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hs : Set.Nontrivial s
H : s = {x}
⊢ False
[PROOFSTEP]
rw [H] at hs 
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : α
hs : Set.Nontrivial {x}
H : s = {x}
⊢ False
[PROOFSTEP]
exact not_nontrivial_singleton hs
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Nontrivial ↑s ↔ Set.Nontrivial s
[PROOFSTEP]
rw [← nontrivial_univ_iff, Set.Nontrivial, Set.Nontrivial]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) ↔ ∃ x x_1 y x_2, x ≠ y
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y
[PROOFSTEP]
rintro ⟨x, _, y, _, hxy⟩
[GOAL]
case mp.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : ↑s
w✝¹ : x ∈ univ
y : ↑s
w✝ : y ∈ univ
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
[PROOFSTEP]
exact ⟨x, Subtype.prop x, y, Subtype.prop y, fun h => hxy (Subtype.coe_injective h)⟩
[GOAL]
case mpr
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ (∃ x x_1 y x_2, x ≠ y) → ∃ x x_1 y x_2, x ≠ y
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hxy⟩
[GOAL]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ x x_1 y x_2, x ≠ y
[PROOFSTEP]
exact ⟨⟨x, hx⟩, mem_univ _, ⟨y, hy⟩, mem_univ _, Subtype.mk_eq_mk.not.mpr hxy⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
⊢ ¬Set.Subsingleton s ↔ Set.Nontrivial s
[PROOFSTEP]
simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s✝ s₁ s₂ t t₁ t₂ u s : Set α
⊢ Set.Subsingleton s ∨ Set.Nontrivial s
[PROOFSTEP]
simp [or_iff_not_imp_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : a ∈ s
⊢ s = {a} ∨ Set.Nontrivial s
[PROOFSTEP]
rw [← subsingleton_iff_singleton ha]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
ha : a ∈ s
⊢ Set.Subsingleton s ∨ Set.Nontrivial s
[PROOFSTEP]
exact s.subsingleton_or_nontrivial
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : Prop
⊢ x ∈ {True, False}
[PROOFSTEP]
rw [mem_insert_iff, mem_singleton_iff]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
x : Prop
⊢ x = True ∨ x = False
[PROOFSTEP]
exact Classical.propComplete x
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ MonotoneOn f s ↔ Monotone fun a => f ↑a
[PROOFSTEP]
simp [Monotone, MonotoneOn]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ AntitoneOn f s ↔ Antitone fun a => f ↑a
[PROOFSTEP]
simp [Antitone, AntitoneOn]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMonoOn f s ↔ StrictMono fun a => f ↑a
[PROOFSTEP]
simp [StrictMono, StrictMonoOn]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAntiOn f s ↔ StrictAnti fun a => f ↑a
[PROOFSTEP]
simp [StrictAnti, StrictAntiOn]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a x b x c x, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
  not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t t₁ t₂ u : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔ ∃ a x b x c x, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
[PROOFSTEP]
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
  not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
f✝ : α → β
f : Set α → Set β
hf : Injective f
h2 : f ∅ = ∅
s : Set α
⊢ Set.Nonempty (f s) ↔ Set.Nonempty s
[PROOFSTEP]
rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]
[GOAL]
α : Type u_1
s t u : Set α
x : ↑s
⊢ inclusion (_ : s ⊆ s) x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
s t u : Set α
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion (_ : s ⊆ s) { val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s t u : Set α
h : s ⊆ t
x : ↑t
m : ↑x ∈ s
⊢ inclusion h { val := ↑x, property := m } = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
s t u : Set α
h : s ⊆ t
val✝ : α
property✝ : val✝ ∈ t
m : ↑{ val := val✝, property := property✝ } ∈ s
⊢ inclusion h { val := ↑{ val := val✝, property := property✝ }, property := m } = { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
x : ↑s
⊢ inclusion htu (inclusion hst x) = inclusion (_ : s ⊆ u) x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion htu (inclusion hst { val := val✝, property := property✝ }) =
    inclusion (_ : s ⊆ u) { val := val✝, property := property✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s✝ t✝ u s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
⊢ s = t
[PROOFSTEP]
refine' Set.Subset.antisymm h (fun x hx => _)
[GOAL]
α : Type u_1
s✝ t✝ u s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
⊢ x ∈ s
[PROOFSTEP]
obtain ⟨y, hy⟩ := h_surj ⟨x, hx⟩
[GOAL]
case intro
α : Type u_1
s✝ t✝ u s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
y : ↑s
hy : inclusion h y = { val := x, property := hx }
⊢ x ∈ s
[PROOFSTEP]
exact mem_of_eq_of_mem (congr_arg Subtype.val hy).symm y.prop
[GOAL]
α : Type u
s t : Set α
a : α
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (a ∈ t)
⊢ Decidable (a ∈ s ∧ ¬a ∈ t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
s t : Set α
a : α
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (a ∈ t)
⊢ Decidable (a ∈ s ∧ a ∈ t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
s t : Set α
a : α
inst✝¹ : Decidable (a ∈ s)
inst✝ : Decidable (a ∈ t)
⊢ Decidable (a ∈ s ∨ a ∈ t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
s t : Set α
a : α
inst✝ : Decidable (a ∈ s)
⊢ Decidable ¬a ∈ s
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
s t : Set α
a x✝ : α
⊢ ¬(fun x => x ∈ ∅) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
s t : Set α
a x✝ : α
⊢ (fun x => x ∈ univ) x✝
[PROOFSTEP]
simp
[GOAL]
α : Type u
s t : Set α
a : α
p : α → Prop
inst✝ : Decidable (p a)
⊢ Decidable (a ∈ {a | p a})
[PROOFSTEP]
assumption
