chore(order/basic): add le_update_iff and update_le_iff (#5080)

Other changes:

* add `update_eq_iff`, `eq_update_iff` and a more general lemma `rel_update_iff`;
* remove `@[simps]` attributes on `pi.*_lattice` instances.

src/data/set/intervals/pi.lean

@@ -51,17 +51,39 @@ lemma pi_univ_Ico_subset : pi univ (λ i, Ico (x i) (y i)) ⊆ Ico x y :=
 
 end pi_preorder
 
-lemma Icc_diff_pi_univ_Ioc_subset [decidable_eq ι] [Π i, linear_order (α i)] (x y z : Π i, α i) :
-  Icc x z \ pi univ (λ i, Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (function.update z i (y i)) :=
+variables [decidable_eq ι] [Π i, linear_order (α i)]
+
+open function (update)
+
+/-- If `x`, `y`, `x'`, and `y'` are functions `Π i : ι, α i`, then
+the set difference between the box `[x, y]` and the product of the open intervals `(x' i, y' i)`
+is covered by the union of the following boxes: for each `i : ι`, we take
+`[x, update y i (x' i)]` and `[update x i (y' i), y]`.
+
+E.g., if `x' = x` and `y' = y`, then this lemma states that the difference between a closed box
+`[x, y]` and the corresponding open box `{z | ∀ i, x i < z i < y i}` is covered by the union
+of the faces of `[x, y]`. -/
+lemma Icc_diff_pi_univ_Ioo_subset (x y x' y' : Π i, α i) :
+  Icc x y \ pi univ (λ i, Ioo (x' i) (y' i)) ⊆
+    (⋃ i : ι, Icc x (update y i (x' i))) ∪ ⋃ i : ι, Icc (update x i (y' i)) y :=
+begin
+  rintros a ⟨⟨hxa, hay⟩, ha'⟩,
+  simpa [le_update_iff, update_le_iff, hxa, hay, hxa _, hay _, ← exists_or_distrib,
+    not_and_distrib] using ha'
+end
+
+/-- If `x`, `y`, `z` are functions `Π i : ι, α i`, then
+the set difference between the box `[x, z]` and the product of the intervals `(y i, z i]`
+is covered by the union of the boxes `[x, update z i (y i)]`.
+
+E.g., if `x = y`, then this lemma states that the difference between a closed box
+`[x, y]` and the product of half-open intervals `{z | ∀ i, x i < z i ≤ y i}` is covered by the union
+of the faces of `[x, y]` adjacent to `x`. -/
+lemma Icc_diff_pi_univ_Ioc_subset (x y z : Π i, α i) :
+  Icc x z \ pi univ (λ i, Ioc (y i) (z i)) ⊆ ⋃ i : ι, Icc x (update z i (y i)) :=
 begin
   rintros a ⟨⟨hax, haz⟩, hay⟩,
-  simp only [mem_Ioc, mem_univ_pi, not_forall, not_and_distrib, not_lt] at hay,
-  rcases hay with ⟨i, hi⟩,
-  replace hi : a i ≤ y i := hi.elim id (λ h, (h $ haz i).elim),
-  refine mem_Union.2 ⟨i, ⟨hax, λ j, _⟩⟩,
-  by_cases hj : j = i,
-  { subst j, simpa },
-  { simp [hj, haz j] }
+  simpa [not_and_distrib, hax, le_update_iff, haz _] using hay
 end
 
 end set

src/logic/function/basic.lean

@@ -312,22 +312,30 @@ lemma update_injective (f : Πa, β a) (a' : α) : injective (update f a') :=
 @[simp] lemma update_noteq {a a' : α} (h : a ≠ a') (v : β a') (f : Πa, β a) : update f a' v a = f a :=
 dif_neg h
 
+lemma rel_update_iff {β' : α → Sort*} {a : α} {b : β a} {f : Π a, β a} {g : Π a, β' a}
+  (r : Π a, β a → β' a → Prop) :
+  (∀ x, r x (update f a b x) (g x)) ↔ r a b (g a) ∧ ∀ x ≠ a, r x (f x) (g x) :=
+calc (∀ x, r x (update f a b x) (g x)) ↔ ∀ x, (x = a ∨ x ≠ a) → r x (update f a b x) (g x) :
+  by simp only [ne.def, classical.em, forall_prop_of_true]
+... ↔ r a b (g a) ∧ ∀ x ≠ a, r x (update f a b x) (g x) :
+  by simp only [or_imp_distrib, forall_and_distrib, forall_eq, update_same]
+... ↔ r a b (g a) ∧ ∀ x ≠ a, r x (f x) (g x) :
+  and_congr iff.rfl $ forall_congr $ λ x, forall_congr $ λ hx, by rw [update_noteq hx]
+
+lemma update_eq_iff {a : α} {b : β a} {f g : Π a, β a} :
+  update f a b = g ↔ b = g a ∧ ∀ x ≠ a, f x = g x :=
+funext_iff.trans $ rel_update_iff (λ a x y, x = y)
+
+lemma eq_update_iff {a : α} {b : β a} {f g : Π a, β a} :
+  g = update f a b ↔ g a = b ∧ ∀ x ≠ a, g x = f x :=
+eq_comm.trans $ update_eq_iff.trans $ by simp only [eq_comm]
+
 @[simp] lemma update_eq_self (a : α) (f : Πa, β a) : update f a (f a) = f :=
-begin
-  refine funext (λi, _),
-  by_cases h : i = a,
-  { rw h, simp },
-  { simp [h] }
-end
+update_eq_iff.2 ⟨rfl, λ _ _, rfl⟩
 
 lemma update_comp {β : Sort v} (f : α → β) {g : α' → α} (hg : injective g) (a : α') (v : β) :
   (update f (g a) v) ∘ g = update (f ∘ g) a v :=
-begin
-  refine funext (λi, _),
-  by_cases h : i = a,
-  { rw h, simp },
-  { simp [h, hg.ne] }
-end
+eq_update_iff.2 ⟨update_same _ _ _, λ x hx, update_noteq (hg.ne hx) _ _⟩
 
 lemma apply_update {ι : Sort*} [decidable_eq ι] {α β : ι → Sort*}
   (f : Π i, α i → β i) (g : Π i, α i) (i : ι) (v : α i) (j : ι) :
@@ -346,7 +354,7 @@ theorem update_comm {α} [decidable_eq α] {β : α → Sort*}
   {a b : α} (h : a ≠ b) (v : β a) (w : β b) (f : Πa, β a) :
   update (update f a v) b w = update (update f b w) a v :=
 begin
-  funext c, simp [update],
+  funext c, simp only [update],
   by_cases h₁ : c = b; by_cases h₂ : c = a; try {simp [h₁, h₂]},
   cases h (h₂.symm.trans h₁),
 end

src/order/basic.lean

@@ -324,6 +324,16 @@ lemma pi.le_def {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] {x y
   x ≤ y ↔ ∀ i, x i ≤ y i :=
 iff.rfl
 
+lemma le_update_iff {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] [decidable_eq ι]
+  {x y : Π i, α i} {i : ι} {a : α i} :
+  x ≤ function.update y i a ↔ x i ≤ a ∧ ∀ j ≠ i, x j ≤ y j :=
+function.rel_update_iff (λ i : ι, (≥))
+
+lemma update_le_iff {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] [decidable_eq ι]
+  {x y : Π i, α i} {i : ι} {a : α i} :
+  function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ j ≠ i, x j ≤ y j :=
+function.rel_update_iff (λ i : ι, (≤))
+
 instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀i, partial_order (α i)] :
   partial_order (Πi, α i) :=
 { le_antisymm := λf g h1 h2, funext (λb, le_antisymm (h1 b) (h2 b)),

src/order/bounded_lattice.lean

@@ -346,41 +346,33 @@ instance pi.has_top {ι : Type*} {α : ι → Type*} [Π i, has_top (α i)] : ha
   (⊤ : Π i, α i) i = ⊤ :=
 rfl
 
-@[simps]
 instance pi.semilattice_sup {ι : Type*} {α : ι → Type*} [Π i, semilattice_sup (α i)] :
   semilattice_sup (Π i, α i) :=
 by refine_struct { sup := (⊔), .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.semilattice_inf {ι : Type*} {α : ι → Type*} [Π i, semilattice_inf (α i)] :
   semilattice_inf (Π i, α i) :=
 by refine_struct { inf := (⊓), .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.semilattice_inf_bot {ι : Type*} {α : ι → Type*} [Π i, semilattice_inf_bot (α i)] :
   semilattice_inf_bot (Π i, α i) :=
 by refine_struct { inf := (⊓), bot := ⊥, .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.semilattice_inf_top {ι : Type*} {α : ι → Type*} [Π i, semilattice_inf_top (α i)] :
   semilattice_inf_top (Π i, α i) :=
 by refine_struct { inf := (⊓), top := ⊤, .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.semilattice_sup_bot {ι : Type*} {α : ι → Type*} [Π i, semilattice_sup_bot (α i)] :
   semilattice_sup_bot (Π i, α i) :=
 by refine_struct { sup := (⊔), bot := ⊥, .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.semilattice_sup_top {ι : Type*} {α : ι → Type*} [Π i, semilattice_sup_top (α i)] :
   semilattice_sup_top (Π i, α i) :=
 by refine_struct { sup := (⊔), top := ⊤, .. pi.partial_order }; tactic.pi_instance_derive_field
 
-@[simps]
 instance pi.lattice {ι : Type*} {α : ι → Type*} [Π i, lattice (α i)] : lattice (Π i, α i) :=
 { .. pi.semilattice_sup, .. pi.semilattice_inf }
 
-@[simps]
 instance pi.bounded_lattice {ι : Type*} {α : ι → Type*} [Π i, bounded_lattice (α i)] :
   bounded_lattice (Π i, α i) :=
 { .. pi.semilattice_sup_top, .. pi.semilattice_inf_bot }