[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


[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
cases' lt_or_le x y with h' h'
[GOAL]
case inl
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
use x
[GOAL]
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)
[PROOFSTEP]
simp [*, not_le.2 h']
[GOAL]
case inr
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
[PROOFSTEP]
use max x (x + dy)
[GOAL]
case property
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : y ≤ x
⊢ max x (x + dy) ∈ Ico x (x + dx) \ Ico y (y + dy)
[PROOFSTEP]
simp [*, le_refl]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioc (a * b ^ n) (a * b ^ (n + 1)))
[PROOFSTEP]
simp_rw [Function.onFun, Set.disjoint_iff]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ioc (a * b ^ x) (a * b ^ (x + 1)) ∩ Ioc (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
[PROOFSTEP]
intro m n hmn x hx
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
[PROOFSTEP]
apply hmn
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
[PROOFSTEP]
have hb : 1 < b := by
  have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
  rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
[PROOFSTEP]
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_le hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
[PROOFSTEP]
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
[PROOFSTEP]
have i1 := hx.1.1.trans_le hx.2.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
[PROOFSTEP]
have i2 := hx.2.1.trans_le hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
[PROOFSTEP]
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, Int.lt_add_one_iff] at i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n
[PROOFSTEP]
exact le_antisymm i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ico (a * b ^ n) (a * b ^ (n + 1)))
[PROOFSTEP]
simp_rw [Function.onFun, Set.disjoint_iff]
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise fun x y => Ico (a * b ^ x) (a * b ^ (x + 1)) ∩ Ico (a * b ^ y) (a * b ^ (y + 1)) ⊆ ∅
[PROOFSTEP]
intro m n hmn x hx
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
[PROOFSTEP]
apply hmn
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ m = n
[PROOFSTEP]
have hb : 1 < b := by
  have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
  rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b
[PROOFSTEP]
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
[PROOFSTEP]
rwa [mul_lt_mul_iff_left, ← mul_one (b ^ m), zpow_add_one, mul_lt_mul_iff_left] at this
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
⊢ m = n
[PROOFSTEP]
have i1 := hx.1.1.trans_lt hx.2.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
⊢ m = n
[PROOFSTEP]
have i2 := hx.2.1.trans_lt hx.1.2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : a * b ^ m < a * b ^ (n + 1)
i2 : a * b ^ n < a * b ^ (m + 1)
⊢ m = n
[PROOFSTEP]
rw [mul_lt_mul_iff_left, zpow_lt_zpow_iff hb, Int.lt_add_one_iff] at i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
hb : 1 < b
i1 : m ≤ n
i2 : n ≤ m
⊢ m = n
[PROOFSTEP]
exact le_antisymm i1 i2
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioc (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ico (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ico_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ Pairwise (Disjoint on fun n => Ioo (b ^ n) (b ^ (n + 1)))
[PROOFSTEP]
simpa only [one_mul] using pairwise_disjoint_Ioo_mul_zpow 1 b
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioc (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ioc_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ico (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ico_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (a + ↑n) (a + ↑n + 1))
[PROOFSTEP]
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using pairwise_disjoint_Ioo_add_zsmul a (1 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ico (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ico_add_int_cast (0 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioo (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ioo_add_int_cast (0 : α)
[GOAL]
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ioc (↑n) (↑n + 1))
[PROOFSTEP]
simpa only [zero_add] using pairwise_disjoint_Ioc_add_int_cast (0 : α)


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Ici (x i)) ↔ y ∈ Ici x
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Iic (x i)) ↔ y ∈ Iic x
[PROOFSTEP]
simp [Pi.le_def]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y✝ y : (i : ι) → α i
⊢ (y ∈ pi univ fun i => Icc (x i) (y✝ i)) ↔ y ∈ Icc x y✝
[PROOFSTEP]
simp [Pi.le_def, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ (pi univ fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
have : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc, inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
⊢ Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, ← inter_assoc, inter_eq_self_of_subset_left (Ioi_subset_Ioi hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (pi univ fun i => Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
simp_rw [univ_pi_update i₀ _ _ fun i z ↦ Ioc z (y i), ← pi_inter_compl ({ i₀ } : Set ι), singleton_pi', ← inter_assoc,
  this]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ (pi univ fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
have : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm, inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
⊢ Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_left_comm, inter_eq_self_of_subset_left (Iic_subset_Iic.2 hm)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (pi univ fun i => Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
simp_rw [univ_pi_update i₀ y m fun i z ↦ Ioc (x i) z, ← pi_inter_compl ({ i₀ } : Set ι), singleton_pi', ← inter_assoc,
  this]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ pi {i₀}ᶜ fun j => Ioc (x j) (y j)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ Disjoint (pi univ fun i => Ioc (x i) (update y i₀ m i)) (pi univ fun i => Ioc (update x i₀ m i) (y i))
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
⊢ ∀ ⦃a : (i : ι) → α i⦄,
    (a ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)) → ¬a ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
[PROOFSTEP]
rintro z h₁ h₂
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
⊢ False
[PROOFSTEP]
refine' (h₁ i₀ (mem_univ _)).2.not_lt _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
x✝ y✝ : (i : ι) → α i
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
z : (i : ι) → α i
h₁ : z ∈ pi univ fun i => Ioc (x i) (update y i₀ m i)
h₂ : z ∈ pi univ fun i => Ioc (update x i₀ m i) (y i)
⊢ update y i₀ m i₀ < z i₀
[PROOFSTEP]
simpa only [Function.update_same] using (h₂ i₀ (mem_univ _)).1
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Icc a b = Icc (update f i a) (update f i b)
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ Icc (update f i a) (update f i b)
[PROOFSTEP]
rw [← Set.pi_univ_Icc]
[GOAL]
case h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b ↔ x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
refine' ⟨_, fun h => ⟨x i, _, _⟩⟩
[GOAL]
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
⊢ x ∈ update f i '' Icc a b → x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
rintro ⟨c, hc, rfl⟩
[GOAL]
case h.refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b c : α i
hc : c ∈ Icc a b
⊢ update f i c ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
[PROOFSTEP]
simpa [update_le_update_iff]
[GOAL]
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b
[PROOFSTEP]
simpa only [Function.update_same] using h i (mem_univ i)
[GOAL]
case h.refine'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x
[PROOFSTEP]
ext j
[GOAL]
case h.refine'_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
j : ι
⊢ update f i (x i) j = x j
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case h.refine'_3.h.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) i = x i
[PROOFSTEP]
exact Function.update_same _ _ _
[GOAL]
case h.refine'_3.h.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ pi univ fun i_1 => Icc (update f i a i_1) (update f i b i_1)
j : ι
hij : i ≠ j
⊢ update f i (x i) j = x j
[PROOFSTEP]
simpa only [Function.update_noteq hij.symm, le_antisymm_iff] using h j (mem_univ j)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b = Ico (update f i a) (update f i b)
[PROOFSTEP]
rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton, image_update_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioc a b = Ioc (update f i a) (update f i b)
[PROOFSTEP]
rw [← Icc_diff_left, ← Icc_diff_left, image_diff (update_injective _ _), image_singleton, image_update_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)
[PROOFSTEP]
rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton, image_update_Ico]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Icc a (f i) = Icc (update f i a) f
[PROOFSTEP]
simpa using image_update_Icc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ico a (f i) = Ico (update f i a) f
[PROOFSTEP]
simpa using image_update_Ico f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioc a (f i) = Ioc (update f i a) f
[PROOFSTEP]
simpa using image_update_Ioc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioo a (f i) = Ioo (update f i a) f
[PROOFSTEP]
simpa using image_update_Ioo f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Icc (f i) b = Icc f (update f i b)
[PROOFSTEP]
simpa using image_update_Icc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ico (f i) b = Ico f (update f i b)
[PROOFSTEP]
simpa using image_update_Ico f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioc (f i) b = Ioc f (update f i b)
[PROOFSTEP]
simpa using image_update_Ioc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' Ioo (f i) b = Ioo f (update f i b)
[PROOFSTEP]
simpa using image_update_Ioo f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)
[PROOFSTEP]
simp_rw [uIcc, update_sup, update_inf]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' uIcc a (f i) = uIcc (update f i a) f
[PROOFSTEP]
simpa using image_update_uIcc f i a (f i)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
b : α i
⊢ update f i '' uIcc (f i) b = uIcc f (update f i b)
[PROOFSTEP]
simpa using image_update_uIcc f i (f i) b
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((pi univ fun i => Ioc (x i) (update y i₀ m i)) ∪ pi univ fun i => Ioc (update x i₀ m i) (y i)) =
    pi univ fun i => Ioc (x i) (y i)
[PROOFSTEP]
simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right, ← setOf_or, le_or_lt,
  setOf_true, univ_inter]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' : (i : ι) → α i
⊢ (Icc x y \ pi univ fun i => Ioo (x' i) (y' i)) ⊆
    (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
rintro a ⟨⟨hxa, hay⟩, ha'⟩
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
ha' : ¬a ∈ pi univ fun i => Ioo (x' i) (y' i)
hxa : x ≤ a
hay : a ≤ y
⊢ a ∈ (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
simp at ha'
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, x' x < a x → y' x ≤ a x
⊢ a ∈ (⋃ (i : ι), Icc x (update y i (x' i))) ∪ ⋃ (i : ι), Icc (update x i (y' i)) y
[PROOFSTEP]
simp [le_update_iff, update_le_iff, hxa, hay, hxa _, hay _, ← exists_or]
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ x, x' x < a x → y' x ≤ a x
⊢ ∃ x, a x ≤ x' x ∨ y' x ≤ a x
[PROOFSTEP]
rcases ha' with ⟨w, hw⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
⊢ ∃ x, a x ≤ x' x ∨ y' x ≤ a x
[PROOFSTEP]
apply Exists.intro w
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
cases lt_or_le (x' w) (a w)
[GOAL]
case intro.intro.intro.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
h✝ : x' w < a w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
simp_all
[GOAL]
case intro.intro.intro.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : x' w < a w → y' w ≤ a w
h✝ : a w ≤ x' w
⊢ a w ≤ x' w ∨ y' w ≤ a w
[PROOFSTEP]
simp_all
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ pi univ fun i => Ioc (y i) (z i)) ⊆ ⋃ (i : ι), Icc x (update z i (y i))
[PROOFSTEP]
rintro a ⟨⟨hax, haz⟩, hay⟩
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z a : (i : ι) → α i
hay : ¬a ∈ pi univ fun i => Ioc (y i) (z i)
hax : x ≤ a
haz : a ≤ z
⊢ a ∈ ⋃ (i : ι), Icc x (update z i (y i))
[PROOFSTEP]
simpa [not_and_or, hax, le_update_iff, haz _] using hay


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = { val := a, property := (_ : a ∈ Icc a b) }
[PROOFSTEP]
simp [projIcc, hx, hx.trans h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = { val := b, property := (_ : b ∈ Icc a b) }
[PROOFSTEP]
simp [projIcc, hx, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
⊢ projIci a x = { val := a, property := (_ : a ≤ a) } ↔ x ≤ a
[PROOFSTEP]
simp [projIci, Subtype.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
⊢ projIic b x = { val := b, property := (_ : b ≤ b) } ↔ b ≤ x
[PROOFSTEP]
simp [projIic, Subtype.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
⊢ projIcc a b (_ : a ≤ b) x = { val := a, property := (_ : a ∈ Icc a b) } ↔ x ≤ a
[PROOFSTEP]
simp [projIcc, Subtype.ext_iff, h.not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
x : α
h : a < b
⊢ projIcc a b (_ : a ≤ b) x = { val := b, property := (_ : b ∈ Icc a b) } ↔ b ≤ x
[PROOFSTEP]
simp [projIcc, Subtype.ext_iff, max_min_distrib_left, h.le, h.not_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Ici a
⊢ projIci a x = { val := x, property := hx }
[PROOFSTEP]
simpa [projIci]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Iic b
⊢ projIic b x = { val := x, property := hx }
[PROOFSTEP]
simpa [projIic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ projIcc a b h x = { val := x, property := hx }
[PROOFSTEP]
simp [projIcc, hx.1, hx.2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Ici a)
⊢ projIci a ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Ici a
⊢ projIci a ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIci_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Iic b)
⊢ projIic b ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Iic b
⊢ projIic b ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIic_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
x : ↑(Icc a b)
⊢ projIcc a b h ↑x = x
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x val✝ : α
property✝ : val✝ ∈ Icc a b
⊢ projIcc a b h ↑{ val := val✝, property := property✝ } = { val := val✝, property := property✝ }
[PROOFSTEP]
apply projIcc_of_mem
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ projIci a x < projIci a y
[PROOFSTEP]
simpa only [projIci_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Iic b
y : α
hy : y ∈ Iic b
hxy : x < y
⊢ projIic b x < projIic b y
[PROOFSTEP]
simpa only [projIic_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y
[PROOFSTEP]
simpa only [projIcc_of_mem, hx, hy]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Ici a) → β
⊢ range (IciExtend f) = range f
[PROOFSTEP]
simp only [IciExtend, range_comp f, range_projIci, range_id', image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Iic b) → β
⊢ range (IicExtend f) = range f
[PROOFSTEP]
simp only [IicExtend, range_comp f, range_projIic, range_id', image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : ↑(Icc a b) → β
⊢ range (IccExtend h f) = range f
[PROOFSTEP]
simp only [IccExtend, range_comp f, range_projIcc, image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
⊢ IccExtend h (f ∘ Subtype.val) = f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
cases' lt_or_le x a with hxa hax
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hxa : x < a
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
simp [IccExtend_of_le_left _ _ hxa.le, ha x hxa]
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
cases' le_or_lt x b with hxb hbx
[GOAL]
case h.inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
lift x to Icc a b using ⟨hax, hxb⟩
[GOAL]
case h.inr.inl.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x // x ∈ Icc a b }
hax : a ≤ ↑x
hxb : ↑x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) ↑x = f ↑x
[PROOFSTEP]
rw [IccExtend_val, comp_apply]
[GOAL]
case h.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x✝ : α
f : α → β
ha : ∀ (x : α), x < a → f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
[PROOFSTEP]
simp [IccExtend_of_right_le _ _ hbx.le, hb x hbx]


[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a) (Ici (a + d))
[PROOFSTEP]
refine' ⟨fun x h => add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).injOn _, fun _ h => _⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d x✝ : M
h : x✝ ∈ Ici (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h)
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a + d + c ∈ Ici (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a ≤ a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ici a
[PROOFSTEP]
exact ⟨a + c, h, by rw [add_right_comm]⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a ≤ a + c
⊢ (fun x => x + d) (a + c) = a + d + c
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a) (Ioi (a + d))
[PROOFSTEP]
refine' ⟨fun x h => add_lt_add_right (mem_Ioi.mp h) _, fun _ _ _ _ h => add_right_cancel h, fun _ h => _⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d x✝ : M
h : x✝ ∈ Ioi (a + d)
⊢ x✝ ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h
[GOAL]
case intro
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a < a + c
⊢ a + d + c ∈ (fun x => x + d) '' Ioi a
[PROOFSTEP]
exact ⟨a + c, h, by rw [add_right_comm]⟩
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c✝ d c : M
h : a < a + c
⊢ (fun x => x + d) (a + c) = a + d + c
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Icc a b) (Icc (a + d) (b + d))
[PROOFSTEP]
rw [← Ici_inter_Iic, ← Ici_inter_Iic]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
[PROOFSTEP]
exact (Ici_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx => le_of_add_le_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioo a b) (Ioo (a + d) (b + d))
[PROOFSTEP]
rw [← Ioi_inter_Iio, ← Ioi_inter_Iio]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iio b) (Ioi (a + d) ∩ Iio (b + d))
[PROOFSTEP]
exact (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx => lt_of_add_lt_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioc a b) (Ioc (a + d) (b + d))
[PROOFSTEP]
rw [← Ioi_inter_Iic, ← Ioi_inter_Iic]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ioi a ∩ Iic b) (Ioi (a + d) ∩ Iic (b + d))
[PROOFSTEP]
exact (Ioi_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx => le_of_add_le_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ico a b) (Ico (a + d) (b + d))
[PROOFSTEP]
rw [← Ici_inter_Iio, ← Ici_inter_Iio]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iio b) (Ici (a + d) ∩ Iio (b + d))
[PROOFSTEP]
exact (Ici_add_bij a d).inter_mapsTo (fun x hx => add_lt_add_right hx _) fun x hx => lt_of_add_lt_add_right hx.2
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ici b = Ici (a + b)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ici]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioi b = Ioi (a + b)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioi]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Icc b c = Icc (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Icc]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ico b c = Ico (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ico]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioc b c = Ioc (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioc]
[GOAL]
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b c d : M
⊢ (fun x => a + x) '' Ioo b c = Ioo (a + b) (a + c)
[PROOFSTEP]
simp only [add_comm a, image_add_const_Ioo]


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s✝ t : Set α
a✝ : α
m n : ℕ
a : α
s : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
induction' n with n ih generalizing a
[GOAL]
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n : ℕ
a✝ : α
s✝ : Fin n → Set α
a : α
s : Fin Nat.zero → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
simp_rw [List.ofFn_zero, List.prod_nil, Fin.exists_fin_zero_pi, eq_comm, Set.mem_one]
[GOAL]
case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s✝¹ t : Set α
a✝¹ : α
m n✝ : ℕ
a✝ : α
s✝ : Fin n✝ → Set α
n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
a : α
s : Fin (Nat.succ n) → Set α
⊢ a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
simp_rw [List.ofFn_succ, List.prod_cons, Fin.exists_fin_succ_pi, Fin.cons_zero, Fin.cons_succ, mem_mul, @ih,
  exists_and_left, exists_exists_eq_and, SetCoe.exists, exists_prop]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n : ℕ
l : List (Set α)
a : α
⊢ a ∈ List.prod l ↔ ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = l
[PROOFSTEP]
induction' l using List.ofFnRec with n f
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ a ∈ List.prod (List.ofFn f) ↔
    ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = List.ofFn f
[PROOFSTEP]
simp only [mem_prod_list_ofFn, List.exists_iff_exists_tuple, List.map_ofFn, Function.comp, List.ofFn_inj',
  Sigma.mk.inj_iff, and_left_comm, exists_and_left, exists_eq_left, heq_eq_eq]
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) ↔
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
constructor
[GOAL]
case h.mp
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a) →
    ∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
rintro ⟨fi, rfl⟩
[GOAL]
case h.mp.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
f : Fin n → Set α
fi : (i : Fin n) → ↑(f i)
⊢ ∃ x,
    List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = List.prod (List.ofFn fun i => ↑(fi i)) ∧
      (fun x_1 => (x x_1).fst) = f
[PROOFSTEP]
exact ⟨fun i ↦ ⟨_, fi i⟩, rfl, rfl⟩
[GOAL]
case h.mpr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
f : Fin n → Set α
⊢ (∃ x, List.prod (List.ofFn fun x_1 => ↑(x x_1).snd) = a ∧ (fun x_1 => (x x_1).fst) = f) →
    ∃ f_1, List.prod (List.ofFn fun i => ↑(f_1 i)) = a
[PROOFSTEP]
rintro ⟨fi, rfl, rfl⟩
[GOAL]
case h.mpr.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a : α
m n✝ n : ℕ
fi : Fin n → (s : Set α) × ↑s
⊢ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = List.prod (List.ofFn fun x => ↑(fi x).snd)
[PROOFSTEP]
exact ⟨fun i ↦ _, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Monoid α
s t : Set α
a✝ : α
m n✝ : ℕ
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a
[PROOFSTEP]
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]


[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 0 ↔ ↑x = 0
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 1 ↔ x = 1
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 1 ↔ ↑x = 1
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Icc 0 1
⊢ 1 - t ∈ Icc 0 1
[PROOFSTEP]
rw [mem_Icc] at *
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 ≤ t ∧ t ≤ 1
⊢ 0 ≤ 1 - t ∧ 1 - t ≤ 1
[PROOFSTEP]
exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 1 - ↑x ≤ 1
[PROOFSTEP]
simpa using x.2.1
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ioc 0 1)
⊢ ↑x = 1 ↔ x = 1
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ioc 0 1)
⊢ x = 1 ↔ ↑x = 1
[PROOFSTEP]
exact Subtype.ext_iff
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1
[PROOFSTEP]
rw [mem_Ioo] at *
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1
[PROOFSTEP]
refine' ⟨sub_pos.2 ht.2, _⟩
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1
[PROOFSTEP]
exact lt_of_le_of_ne ((sub_le_self_iff 1).2 ht.1.le) (mt sub_eq_self.mp ht.1.ne')
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 0 < 1 - ↑x
[PROOFSTEP]
simpa using x.2.2
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Ioo 0 1)
⊢ 1 - ↑x < 1
[PROOFSTEP]
simpa using x.2.1


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem, mem_support]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_mulSupport]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (support fun x => f (c⁻¹ • x)) = c • support f
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ support fun x => f (c⁻¹ • x)) ↔ x ∈ c • support f
[PROOFSTEP]
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_support]


[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ g • s = s
[PROOFSTEP]
suffices ∀ {g' : G} (_ : g' ^ n ^ j = 1), g' • s ⊆ s
  by
  refine' le_antisymm (this hg) _
  conv_lhs => rw [← smul_inv_smul g s]
  replace hg : g⁻¹ ^ n ^ j = 1
  · rw [inv_zpow, hg, inv_one]
  simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • s = s
[PROOFSTEP]
refine' le_antisymm (this hg) _
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ s ≤ g • s
[PROOFSTEP]
conv_lhs => rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
| s
[PROOFSTEP]
rw [← smul_inv_smul g s]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g • g⁻¹ • s ≤ g • s
[PROOFSTEP]
replace hg : g⁻¹ ^ n ^ j = 1
[GOAL]
case hg
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
⊢ g⁻¹ ^ n ^ j = 1
[PROOFSTEP]
rw [inv_zpow, hg, inv_one]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
this : ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
hg : g⁻¹ ^ n ^ j = 1
⊢ g • g⁻¹ • s ≤ g • s
[PROOFSTEP]
simpa only [le_eq_subset, set_smul_subset_set_smul_iff] using this hg
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • s ⊆ s
[PROOFSTEP]
rw [(IsFixedPt.preimage_iterate hs j : (zpowGroupHom n)^[j] ⁻¹' s = s).symm]
[GOAL]
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
⊢ ∀ {g' : G}, g' ^ n ^ j = 1 → g' • (fun x => x ^ n)^[j] ⁻¹' s ⊆ (fun x => x ^ n)^[j] ⁻¹' s
[PROOFSTEP]
rintro g' hg' - ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (fun x => g' • x) y ∈ (fun x => x ^ n)^[j] ⁻¹' s
[PROOFSTEP]
change (zpowGroupHom n)^[j] (g' * y) ∈ s
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (↑(zpowGroupHom n))^[j] (g' * y) ∈ s
[PROOFSTEP]
replace hg' : (zpowGroupHom n)^[j] g' = 1
[GOAL]
case hg'
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' : G
hg' : g' ^ n ^ j = 1
y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
⊢ (↑(zpowGroupHom n))^[j] g' = 1
[PROOFSTEP]
simpa [zpowGroupHom]
[GOAL]
case intro.intro
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x => x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun x => x ^ n)^[j] ⁻¹' s
hg' : (↑(zpowGroupHom n))^[j] g' = 1
⊢ (↑(zpowGroupHom n))^[j] (g' * y) ∈ s
[PROOFSTEP]
rwa [iterate_map_mul, hg', one_mul]