refactor(order/bounds): use dot notation, reorder, prove more propert…

…ies (leanprover-community#2028)

* refactor(order/bounds): use dot notation, prove more properties

Also make parts of `complete_lattice` and
`conditionally_complete_lattice` use these lemmas.

* Comments

* Add a module docstring

* Fixes from review, +4 lemmas about images

* Fix a typo in the previous commit

* Update src/order/bounds.lean

* Update src/order/bounds.lean

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/set/finite.lean

@@ -450,19 +450,14 @@ variables [semilattice_sup α] [nonempty α] {s : set α}
 
 /--A finite set is bounded above.-/
 lemma bdd_above_finite (hs : finite s) : bdd_above s :=
-finite.induction_on hs bdd_above_empty $ λ a s _ _, bdd_above_insert.2
+finite.induction_on hs bdd_above_empty $ λ a s _ _ h, h.insert a
 
 /--A finite union of sets which are all bounded above is still bounded above.-/
 lemma bdd_above_finite_union {I : set β} {S : β → set α} (H : finite I) :
-(bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) :=
-⟨λ (bdd : bdd_above (⋃i∈I, S i)) i (hi : i ∈ I),
-  bdd_above_subset (subset_bUnion_of_mem hi) bdd,
-show (∀i ∈ I, bdd_above (S i)) → (bdd_above (⋃i∈I, S i)), from
+  (bdd_above (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_above (S i)) :=
 finite.induction_on H
-  (λ _, by rw bUnion_empty; exact bdd_above_empty)
-  (λ x s hn hf IH h, by simp only [
-      set.mem_insert_iff, or_imp_distrib, forall_and_distrib, forall_eq] at h;
-    rw [set.bUnion_insert, bdd_above_union]; exact ⟨h.1, IH h.2⟩)⟩
+  (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
+  (λ a s ha _ hs, by simp only [bUnion_insert, ball_insert_iff, bdd_above_union, hs])
 
 end
 
@@ -472,19 +467,12 @@ variables [semilattice_inf α] [nonempty α] {s : set α}
 
 /--A finite set is bounded below.-/
 lemma bdd_below_finite (hs : finite s) : bdd_below s :=
-finite.induction_on hs bdd_below_empty $ λ a s _ _, bdd_below_insert.2
+finite.induction_on hs bdd_below_empty $ λ a s _ _ h, h.insert a
 
 /--A finite union of sets which are all bounded below is still bounded below.-/
 lemma bdd_below_finite_union {I : set β} {S : β → set α} (H : finite I) :
-(bdd_below (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_below (S i)) :=
-⟨λ (bdd : bdd_below (⋃i∈I, S i)) i (hi : i ∈ I),
-  bdd_below_subset (subset_bUnion_of_mem hi) bdd,
-show (∀i ∈ I, bdd_below (S i)) → (bdd_below (⋃i∈I, S i)), from
-finite.induction_on H
-  (λ _, by rw bUnion_empty; exact bdd_below_empty)
-  (λ x s hn hf IH h, by simp only [
-      set.mem_insert_iff, or_imp_distrib, forall_and_distrib, forall_eq] at h;
-    rw [set.bUnion_insert, bdd_below_union]; exact ⟨h.1, IH h.2⟩)⟩
+  (bdd_below (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_below (S i)) :=
+@bdd_above_finite_union (order_dual α) _ _ _ _ _ H
 
 end
 

src/data/set/lattice.lean

@@ -382,10 +382,10 @@ theorem sInter_union (S T : set (set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂
 @[simp] theorem sInter_insert (s : set α) (T : set (set α)) : ⋂₀ (insert s T) = s ∩ ⋂₀ T := Inf_insert
 
 theorem sUnion_pair (s t : set α) : ⋃₀ {s, t} = s ∪ t :=
-(sUnion_insert _ _).trans $ by rw [union_comm, sUnion_singleton]
+Sup_pair
 
 theorem sInter_pair (s t : set α) : ⋂₀ {s, t} = s ∩ t :=
-(sInter_insert _ _).trans $ by rw [inter_comm, sInter_singleton]
+Inf_pair
 
 @[simp] theorem sUnion_image (f : α → set β) (s : set α) : ⋃₀ (f '' s) = ⋃ x ∈ s, f x := Sup_image
 

src/order/basic.lean

@@ -137,6 +137,7 @@ end monotone
 def order_dual (α : Type*) := α
 
 namespace order_dual
+instance (α : Type*) [h : nonempty α] : nonempty (order_dual α) := h
 instance (α : Type*) [has_le α] : has_le (order_dual α) := ⟨λx y:α, y ≤ x⟩
 instance (α : Type*) [has_lt α] : has_lt (order_dual α) := ⟨λx y:α, y < x⟩