feat(order): add some missing pi and Prop instances (#7268)

src/order/boolean_algebra.lean

@@ -661,6 +661,7 @@ boolean_algebra.of_core
   top_le_sup_compl := λ p H, classical.em p,
   .. bounded_distrib_lattice_Prop }
 
-instance pi.boolean_algebra {α : Type u} {β : Type v} [boolean_algebra β] :
-  boolean_algebra (α → β) :=
-by pi_instance
+instance pi.boolean_algebra {ι : Type u} {α : ι → Type v} [∀ i, boolean_algebra (α i)] :
+  boolean_algebra (Π i, α i) :=
+by refine_struct { sdiff := λ x y i, x i \ y i, compl := λ x i, (x i)ᶜ, .. pi.bounded_lattice };
+  tactic.pi_instance_derive_field

src/order/bounded_lattice.lean

@@ -276,7 +276,7 @@ lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c
     calc a ⊓ b ≤ b ⊓ c : by { rw [inf_comm], exact inf_le_inf_left _ this }
       ... = ⊥ : h₂⟩
 
-/- Prop instance -/
+/-- Propositions form a bounded distributive lattice. -/
 instance bounded_distrib_lattice_Prop : bounded_distrib_lattice Prop :=
 { le           := λa b, a → b,
   le_refl      := assume _, id,
@@ -306,8 +306,9 @@ noncomputable instance Prop.linear_order : linear_order Prop :=
   decidable_le := classical.dec_rel _,
   .. (_ : partial_order Prop) }
 
-@[simp]
-lemma le_iff_imp {p q : Prop} : p ≤ q ↔ (p → q) := iff.rfl
+@[simp] lemma le_Prop_eq : ((≤) : Prop → Prop → Prop) = (→) := rfl
+@[simp] lemma sup_Prop_eq : (⊔) = (∨) := rfl
+@[simp] lemma inf_Prop_eq : (⊓) = (∧) := rfl
 
 section logic
 variable [preorder α]

src/order/complete_boolean_algebra.lean

@@ -52,6 +52,16 @@ theorem infi_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i 
 theorem sup_infi_eq (a : α) (f : ι → α) : a ⊔ (⨅ i, f i) = ⨅ i, a ⊔ f i :=
 @inf_supr_eq (order_dual α) _ _ _ _
 
+instance pi.complete_distrib_lattice {ι : Type*} {π : ι → Type*}
+  [∀ i, complete_distrib_lattice (π i)] : complete_distrib_lattice (Π i, π i) :=
+{ infi_sup_le_sup_Inf := λ a s i,
+    by simp only [← sup_infi_eq, complete_lattice.Inf, Inf_apply, ←infi_subtype'', infi_apply,
+      sup_apply],
+  inf_Sup_le_supr_inf := λ a s i,
+    by simp only [complete_lattice.Sup, Sup_apply, supr_apply, inf_apply, inf_supr_eq,
+      ← supr_subtype''],
+  .. pi.complete_lattice }
+
 theorem Inf_sup_Inf : Inf s ⊔ Inf t = (⨅p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) :=
 begin
   apply le_antisymm,
@@ -96,6 +106,17 @@ instance complete_distrib_lattice.bounded_distrib_lattice [d : complete_distrib_
 /-- A complete boolean algebra is a completely distributive boolean algebra. -/
 class complete_boolean_algebra α extends boolean_algebra α, complete_distrib_lattice α
 
+instance pi.complete_boolean_algebra {ι : Type*} {π : ι → Type*}
+  [∀ i, complete_boolean_algebra (π i)] : complete_boolean_algebra (Π i, π i) :=
+{ .. pi.boolean_algebra, .. pi.complete_distrib_lattice }
+
+instance : complete_boolean_algebra Prop :=
+{ infi_sup_le_sup_Inf := λ p s, iff.mp $
+    by simp only [forall_or_distrib_left, complete_lattice.Inf, infi_Prop_eq, sup_Prop_eq],
+  inf_Sup_le_supr_inf := λ p s, iff.mp $
+    by simp only [complete_lattice.Sup, exists_and_distrib_left, inf_Prop_eq, supr_Prop_eq],
+  .. boolean_algebra_Prop, .. complete_lattice_Prop }
+
 section complete_boolean_algebra
 variables [complete_boolean_algebra α] {a b : α} {s : set α} {f : ι → α}
 

src/order/complete_lattice.lean

@@ -741,7 +741,7 @@ lemma supr_sup [h : nonempty ι] {f : ι → α} {a : α} : (⨆ x, f x) ⊔ a =
 lemma sup_supr [nonempty ι] {f : ι → α} {a : α} : a ⊔ (⨆ x, f x) = (⨆ x, a ⊔ f x) :=
 @inf_infi (order_dual α) _ _ _ _ _
 
-/- supr and infi under Prop -/
+/-! ### `supr` and `infi` under `Prop` -/
 
 @[simp] theorem infi_false {s : false → α} : infi s = ⊤ :=
 le_antisymm le_top (le_infi $ assume i, false.elim i)
@@ -930,6 +930,10 @@ lemma supr_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
   (⨆ i (h : p i), f i h) = (⨆ x : subtype p, f x x.property) :=
 (@supr_subtype _ _ _ p (λ x, f x.val x.property)).symm
 
+lemma supr_subtype'' {ι} (s : set ι) (f : ι → α) :
+  (⨆ i : s, f i) = ⨆ (t : ι) (H : t ∈ s), f t :=
+supr_subtype
+
 lemma Sup_eq_supr' {s : set α} : Sup s = ⨆ x : s, (x : α) :=
 by rw [Sup_eq_supr, supr_subtype']; refl
 
@@ -1042,14 +1046,14 @@ instance complete_lattice_Prop : complete_lattice Prop :=
   le_Inf := assume s a h p b hb, h b hb p,
   .. bounded_distrib_lattice_Prop }
 
-lemma Inf_Prop_eq {s : set Prop} : Inf s = (∀p ∈ s, p) := rfl
+@[simp] lemma Inf_Prop_eq {s : set Prop} : Inf s = (∀p ∈ s, p) := rfl
 
-lemma Sup_Prop_eq {s : set Prop} : Sup s = (∃p ∈ s, p) := rfl
+@[simp] lemma Sup_Prop_eq {s : set Prop} : Sup s = (∃p ∈ s, p) := rfl
 
-lemma infi_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨅i, p i) = (∀i, p i) :=
+@[simp] lemma infi_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨅i, p i) = (∀i, p i) :=
 le_antisymm (assume h i, h _ ⟨i, rfl⟩ ) (assume h p ⟨i, eq⟩, eq ▸ h i)
 
-lemma supr_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨆i, p i) = (∃i, p i) :=
+@[simp] lemma supr_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨆i, p i) = (∃i, p i) :=
 le_antisymm (λ ⟨q, ⟨i, (eq : p i = q)⟩, hq⟩, ⟨i, eq.symm ▸ hq⟩) (λ ⟨i, hi⟩, ⟨p i, ⟨i, rfl⟩, hi⟩)
 
 instance pi.has_Sup {α : Type*} {β : α → Type*} [Π i, has_Sup (β i)] : has_Sup (Π i, β i) :=
@@ -1073,7 +1077,7 @@ lemma Inf_apply {α : Type*} {β : α → Type*} [Π i, has_Inf (β i)]
   (Inf s) a = (⨅ f : s, (f : Πa, β a) a) :=
 rfl
 
-lemma infi_apply {α : Type*} {β : α → Type*} {ι : Sort*} [Π i, has_Inf (β i)]
+@[simp] lemma infi_apply {α : Type*} {β : α → Type*} {ι : Sort*} [Π i, has_Inf (β i)]
   {f : ι → Πa, β a} {a : α} :
   (⨅i, f i) a = (⨅i, f i a) :=
 by rw [infi, Inf_apply, infi, infi, ← image_eq_range (λ f : Π i, β i, f a) (range f), ← range_comp]
@@ -1090,8 +1094,8 @@ lemma binary_relation_Sup_iff {α β : Type*} (s : set (α → β → Prop)) {a
   Sup s a b ↔ ∃ (r : α → β → Prop), r ∈ s ∧ r a b :=
 by { change (∃ _, _) ↔ _, simp [-eq_iff_iff] }
 
-lemma supr_apply {α : Type*} {β : α → Type*} {ι : Sort*} [Π i, has_Sup (β i)] {f : ι → Πa, β a}
-  {a : α} :
+@[simp] lemma supr_apply {α : Type*} {β : α → Type*} {ι : Sort*} [Π i, has_Sup (β i)]
+  {f : ι → Πa, β a} {a : α} :
   (⨆i, f i) a = (⨆i, f i a) :=
 @infi_apply α (λ i, order_dual (β i)) _ _ f a
 

src/topology/omega_complete_partial_order.lean

@@ -100,12 +100,12 @@ lemma not_below_is_open : is_open (not_below y) :=
 begin
   have h : monotone (not_below y),
   { intros x y' h,
-    simp only [not_below, set_of, le_iff_imp],
+    simp only [not_below, set_of, le_Prop_eq],
     intros h₀ h₁, apply h₀ (le_trans h h₁) },
   existsi h, rintros c,
   apply eq_of_forall_ge_iff, intro z,
   rw ωSup_le_iff,
-  simp only [ωSup_le_iff, not_below, set.mem_set_of_eq, le_iff_imp, preorder_hom.coe_fun_mk,
+  simp only [ωSup_le_iff, not_below, set.mem_set_of_eq, le_Prop_eq, preorder_hom.coe_fun_mk,
              chain.map_to_fun, function.comp_app, exists_imp_distrib, not_forall],
 end
 
@@ -132,7 +132,7 @@ begin
   have h : monotone f,
   { intros x y h,
     cases (hf {x | ¬ x ≤ f y} (not_below_is_open _)) with hf hf', clear hf',
-    specialize hf h, simp only [set.preimage, set_of, (∈), set.mem, le_iff_imp] at hf,
+    specialize hf h, simp only [set.preimage, set_of, (∈), set.mem, le_Prop_eq] at hf,
     by_contradiction H, apply hf H (le_refl (f y)) },
   existsi h, intro c,
   apply eq_of_forall_ge_iff, intro z,