[Merged by Bors] - feat(order): add some missing pi and Prop instances

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,
@@ -309,6 +309,9 @@ noncomputable instance Prop.linear_order : linear_order Prop :=
 @[simp]
 lemma le_iff_imp {p q : Prop} : p ≤ q ↔ (p → q) := iff.rfl
 
+@[simp] lemma sup_Prop_eq (p q : Prop) : p ⊔ q = (p ∨ q) := rfl
+@[simp] lemma inf_Prop_eq (p q : Prop) : p ⊓ q = (p ∧ q) := 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,
@@ -94,6 +104,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

@@ -737,7 +737,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)
@@ -926,6 +926,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
 
@@ -1026,14 +1030,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) :=
@@ -1057,7 +1061,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]
@@ -1066,8 +1070,8 @@ lemma Sup_apply {α : Type*} {β : α → Type*} [Π i, has_Sup (β i)] {s : set
   (Sup s) a = (⨆f:s, (f : Πa, β a) a) :=
 rfl
 
-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