feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281)

Generalize lemmas from `(generalized_)boolean_algebra` to `(generalized_)coheyting_algebra`. Dualize (some of) them. Duplicate lemmas have been made aliases. Add supporting lemmas to golf the proofs.



Co-authored-by: Mauricio Collares <mauricio@collares.org>

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -298,15 +298,15 @@ lemma vanishing_ideal_Union {ι : Sort*} (t : ι → set (prime_spectrum R)) :
 
 lemma zero_locus_inf (I J : ideal R) :
   zero_locus ((I ⊓ J : ideal R) : set R) = zero_locus I ∪ zero_locus J :=
-set.ext $ λ x, by simpa using x.2.inf_le
+set.ext $ λ x, x.2.inf_le
 
 lemma union_zero_locus (s s' : set R) :
   zero_locus s ∪ zero_locus s' = zero_locus ((ideal.span s) ⊓ (ideal.span s') : ideal R) :=
 by { rw zero_locus_inf, simp }
 
 lemma zero_locus_mul (I J : ideal R) :
   zero_locus ((I * J : ideal R) : set R) = zero_locus I ∪ zero_locus J :=
-set.ext $ λ x, by simpa using x.2.mul_le
+set.ext $ λ x, x.2.mul_le
 
 lemma zero_locus_singleton_mul (f g : R) :
   zero_locus ({f * g} : set R) = zero_locus {f} ∪ zero_locus {g} :=

src/algebraic_geometry/projective_spectrum/topology.lean

@@ -252,19 +252,19 @@ by convert (gc_ideal 𝒜).u_infi; exact homogeneous_ideal.to_ideal_infi _
 
 lemma zero_locus_inf (I J : ideal A) :
   zero_locus 𝒜 ((I ⊓ J : ideal A) : set A) = zero_locus 𝒜 I ∪ zero_locus 𝒜 J :=
-set.ext $ λ x, by simpa using x.2.1.inf_le
+set.ext $ λ x, x.2.1.inf_le
 
 lemma union_zero_locus (s s' : set A) :
   zero_locus 𝒜 s ∪ zero_locus 𝒜 s' = zero_locus 𝒜 ((ideal.span s) ⊓ (ideal.span s'): ideal A) :=
 by { rw zero_locus_inf, simp }
 
 lemma zero_locus_mul_ideal (I J : ideal A) :
   zero_locus 𝒜 ((I * J : ideal A) : set A) = zero_locus 𝒜 I ∪ zero_locus 𝒜 J :=
-set.ext $ λ x, by simpa using x.2.1.mul_le
+set.ext $ λ x, x.2.1.mul_le
 
 lemma zero_locus_mul_homogeneous_ideal (I J : homogeneous_ideal 𝒜) :
   zero_locus 𝒜 ((I * J : homogeneous_ideal 𝒜) : set A) = zero_locus 𝒜 I ∪ zero_locus 𝒜 J :=
-set.ext $ λ x, by simpa using x.2.1.mul_le
+set.ext $ λ x, x.2.1.mul_le
 
 lemma zero_locus_singleton_mul (f g : A) :
   zero_locus 𝒜 ({f * g} : set A) = zero_locus 𝒜 {f} ∪ zero_locus 𝒜 {g} :=

src/data/finset/basic.lean

@@ -1250,14 +1250,13 @@ sdiff_le_sdiff ‹s ≤ t› ‹v ≤ u›
 @[simp, norm_cast] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : set α) :=
 set.ext $ λ _, mem_sdiff
 
-@[simp] theorem union_sdiff_self_eq_union : s ∪ (t \ s) = s ∪ t := sup_sdiff_self_right
-
-@[simp] theorem sdiff_union_self_eq_union : (s \ t) ∪ t = s ∪ t := sup_sdiff_self_left
+@[simp] lemma union_sdiff_self_eq_union : s ∪ t \ s = s ∪ t := sup_sdiff_self_right _ _
+@[simp] lemma sdiff_union_self_eq_union : s \ t ∪ t = s ∪ t := sup_sdiff_self_left _ _
 
 lemma union_sdiff_left (s t : finset α) : (s ∪ t) \ s = t \ s := sup_sdiff_left_self
 lemma union_sdiff_right (s t : finset α) : (s ∪ t) \ t = s \ t := sup_sdiff_right_self
 
-lemma union_sdiff_symm : s ∪ (t \ s) = t ∪ (s \ t) := sup_sdiff_symm
+lemma union_sdiff_symm : s ∪ (t \ s) = t ∪ (s \ t) := by simp [union_comm]
 
 lemma sdiff_union_inter (s t : finset α) : (s \ t) ∪ (s ∩ t) = s := sup_sdiff_inf _ _
 

src/data/set/basic.lean

@@ -945,7 +945,7 @@ ext $ λ x, and_iff_not_or_not
 @[simp] theorem compl_union_self (s : set α) : sᶜ ∪ s = univ := by rw [union_comm, union_compl_self]
 
 lemma compl_subset_comm : sᶜ ⊆ t ↔ tᶜ ⊆ s := @compl_le_iff_compl_le _ s _ _
-lemma subset_compl_comm : s ⊆ tᶜ ↔ t ⊆ sᶜ := @le_compl_iff_le_compl _ t _ _
+lemma subset_compl_comm : s ⊆ tᶜ ↔ t ⊆ sᶜ := @le_compl_iff_le_compl _ _ _ t
 
 @[simp] lemma compl_subset_compl : sᶜ ⊆ tᶜ ↔ t ⊆ s := @compl_le_compl_iff_le (set α) _ _ _
 
@@ -1140,11 +1140,8 @@ ext $ λ x, and_congr_right $ λ hx, or_iff_right $ ne_of_mem_of_not_mem hx h
 lemma insert_inter_of_not_mem (h : a ∉ t) : insert a s ∩ t = s ∩ t :=
 ext $ λ x, and_congr_left $ λ hx, or_iff_right $ ne_of_mem_of_not_mem hx h
 
-@[simp] theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
-sup_sdiff_self_right
-
-@[simp] theorem diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t :=
-sup_sdiff_self_left
+@[simp] lemma union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t := sup_sdiff_self _ _
+@[simp] lemma diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t := sdiff_sup_self _ _
 
 @[simp] theorem diff_inter_self {a b : set α} : (b \ a) ∩ a = ∅ :=
 inf_sdiff_self_left
@@ -2137,10 +2134,10 @@ by rw [← image_univ, preimage_inl_image_inr]
 by rw [← image_univ, preimage_inr_image_inl]
 
 @[simp] lemma compl_range_inl : (range (sum.inl : α → α ⊕ β))ᶜ = range (sum.inr : β → α ⊕ β) :=
-is_compl_range_inl_range_inr.compl_eq
+is_compl.compl_eq is_compl_range_inl_range_inr
 
 @[simp] lemma compl_range_inr : (range (sum.inr : β → α ⊕ β))ᶜ = range (sum.inl : α → α ⊕ β) :=
-is_compl_range_inl_range_inr.symm.compl_eq
+is_compl.compl_eq is_compl_range_inl_range_inr.symm
 
 @[simp] theorem range_quot_mk (r : α → α → Prop) : range (quot.mk r) = univ :=
 (surjective_quot_mk r).range_eq

src/model_theory/definability.lean

@@ -180,9 +180,6 @@ begin
     simp }
 end
 
-lemma fin.coe_cast_add_zero {m : ℕ} : (fin.cast_add 0 : fin m → fin (m + 0)) = id :=
-funext (λ _, fin.ext rfl)
-
 /-- This lemma is only intended as a helper for `definable.image_comp. -/
 lemma definable.image_comp_sum_inl_fin (m : ℕ) {s : set ((α ⊕ fin m) → M)}
   (h : A.definable L s) :
@@ -192,7 +189,7 @@ begin
   refine ⟨(bounded_formula.relabel id φ).exs, _⟩,
   ext x,
   simp only [set.mem_image, mem_set_of_eq, bounded_formula.realize_exs,
-    bounded_formula.realize_relabel, function.comp.right_id, fin.coe_cast_add_zero],
+    bounded_formula.realize_relabel, function.comp.right_id, fin.cast_add_zero, fin.cast_refl],
   split,
   { rintro ⟨y, hy, rfl⟩,
     exact ⟨y ∘ sum.inr,
@@ -203,10 +200,11 @@ end
 
 /-- Shows that definability is closed under finite projections. -/
 lemma definable.image_comp_embedding {s : set (β → M)} (h : A.definable L s)
-  (f : α ↪ β) [fintype β] :
+  (f : α ↪ β) [finite β] :
   A.definable L ((λ g : β → M, g ∘ f) '' s) :=
 begin
   classical,
+  casesI nonempty_fintype β,
   refine (congr rfl (ext (λ x, _))).mp (((h.image_comp_equiv
     (equiv.set.sum_compl (range f))).image_comp_equiv (equiv.sum_congr
     (equiv.of_injective f f.injective) (fintype.equiv_fin _).symm)).image_comp_sum_inl_fin _),
@@ -217,10 +215,12 @@ end
 
 /-- Shows that definability is closed under finite projections. -/
 lemma definable.image_comp {s : set (β → M)} (h : A.definable L s)
-  (f : α → β) [fintype α] [fintype β] :
+  (f : α → β) [finite α] [finite β] :
   A.definable L ((λ g : β → M, g ∘ f) '' s) :=
 begin
   classical,
+  casesI nonempty_fintype α,
+  casesI nonempty_fintype β,
   have h := (((h.image_comp_equiv (equiv.set.sum_compl (range f))).image_comp_equiv
     (equiv.sum_congr (_root_.equiv.refl _)
     (fintype.equiv_fin _).symm)).image_comp_sum_inl_fin _).preimage_comp (range_splitting f),
@@ -270,90 +270,42 @@ variables (L : first_order.language.{u v}) {M : Type w} [L.Structure M] (A : set
 def definable_set := { s : set (α → M) // A.definable L s}
 
 namespace definable_set
-variables {L} {A} {α}
-
-instance : has_top (L.definable_set A α) := ⟨⟨⊤, definable_univ⟩⟩
-
-instance : has_bot (L.definable_set A α) := ⟨⟨⊥, definable_empty⟩⟩
-
-instance : inhabited (L.definable_set A α) := ⟨⊥⟩
+variables {L A α} {s t : L.definable_set A α} {x : α → M}
 
 instance : set_like (L.definable_set A α) (α → M) :=
 { coe := subtype.val,
   coe_injective' := subtype.val_injective }
 
-@[simp]
-lemma mem_top {x : α → M} : x ∈ (⊤ : L.definable_set A α) := mem_univ x
-
-@[simp]
-lemma coe_top : ((⊤ : L.definable_set A α) : set (α → M)) = ⊤ := rfl
-
-@[simp]
-lemma not_mem_bot {x : α → M} : ¬ x ∈ (⊥ : L.definable_set A α) := not_mem_empty x
+instance : has_top (L.definable_set A α) := ⟨⟨⊤, definable_univ⟩⟩
+instance : has_bot (L.definable_set A α) := ⟨⟨⊥, definable_empty⟩⟩
+instance : has_sup (L.definable_set A α) := ⟨λ s t, ⟨s ∪ t, s.2.union t.2⟩⟩
+instance : has_inf (L.definable_set A α) := ⟨λ s t, ⟨s ∩ t, s.2.inter t.2⟩⟩
+instance : has_compl (L.definable_set A α) := ⟨λ s, ⟨sᶜ, s.2.compl⟩⟩
+instance : has_sdiff (L.definable_set A α) := ⟨λ s t, ⟨s \ t, s.2.sdiff t.2⟩⟩
 
-@[simp]
-lemma coe_bot : ((⊥ : L.definable_set A α) : set (α → M)) = ⊥ := rfl
+instance : inhabited (L.definable_set A α) := ⟨⊥⟩
 
-instance : lattice (L.definable_set A α) :=
-subtype.lattice (λ _ _, definable.union) (λ _ _, definable.inter)
+lemma le_iff : s ≤ t ↔ (s : set (α → M)) ≤ (t : set (α → M)) := iff.rfl
 
-lemma le_iff {s t : L.definable_set A α} : s ≤ t ↔ (s : set (α → M)) ≤ (t : set (α → M)) := iff.rfl
+@[simp] lemma mem_top : x ∈ (⊤ : L.definable_set A α) := mem_univ x
+@[simp] lemma not_mem_bot {x : α → M} : ¬ x ∈ (⊥ : L.definable_set A α) := not_mem_empty x
+@[simp] lemma mem_sup : x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t := iff.rfl
+@[simp] lemma mem_inf : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t := iff.rfl
+@[simp] lemma mem_compl : x ∈ sᶜ ↔ ¬ x ∈ s := iff.rfl
+@[simp] lemma mem_sdiff : x ∈ s \ t ↔ x ∈ s ∧ ¬ x ∈ t := iff.rfl
 
-@[simp]
-lemma coe_sup {s t : L.definable_set A α} : ((s ⊔ t : L.definable_set A α) : set (α → M)) = s ∪ t :=
+@[simp, norm_cast] lemma coe_top : ((⊤ : L.definable_set A α) : set (α → M)) = univ := rfl
+@[simp, norm_cast] lemma coe_bot : ((⊥ : L.definable_set A α) : set (α → M)) = ∅ := rfl
+@[simp, norm_cast] lemma coe_sup (s t : L.definable_set A α) : (↑(s ⊔ t) : set (α → M)) = s ∪ t :=
 rfl
-
-@[simp]
-lemma mem_sup {s t : L.definable_set A α} {x : α → M} : x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t := iff.rfl
-
-@[simp]
-lemma coe_inf {s t : L.definable_set A α} : ((s ⊓ t : L.definable_set A α) : set (α → M)) = s ∩ t :=
+@[simp, norm_cast] lemma coe_inf (s t : L.definable_set A α) : (↑(s ⊓ t) : set (α → M)) = s ∩ t :=
+rfl
+@[simp, norm_cast] lemma coe_compl (s : L.definable_set A α) : (↑(sᶜ) : set (α → M)) = sᶜ := rfl
+@[simp, norm_cast] lemma coe_sdiff (s t : L.definable_set A α) : (↑(s \ t) : set (α → M)) = s \ t :=
 rfl
-
-@[simp]
-lemma mem_inf {s t : L.definable_set A α} {x : α → M} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t := iff.rfl
-
-instance : bounded_order (L.definable_set A α) :=
-{ bot_le := λ s x hx, false.elim hx,
-  le_top := λ s x hx, mem_univ x,
-  .. definable_set.has_top,
-  .. definable_set.has_bot }
-
-instance : distrib_lattice (L.definable_set A α) :=
-{ le_sup_inf := begin
-    intros s t u x,
-    simp only [and_imp, mem_inter_eq, set_like.mem_coe, coe_sup, coe_inf, mem_union_eq,
-      subtype.val_eq_coe],
-    tauto,
-  end,
-  .. definable_set.lattice }
-
-/-- The complement of a definable set is also definable. -/
-@[reducible] instance : has_compl (L.definable_set A α) :=
-⟨λ ⟨s, hs⟩, ⟨sᶜ, hs.compl⟩⟩
-
-@[simp]
-lemma mem_compl {s : L.definable_set A α} {x : α → M} : x ∈ sᶜ ↔ ¬ x ∈ s :=
-begin
-  cases s with s hs,
-  refl,
-end
-
-@[simp]
-lemma coe_compl {s : L.definable_set A α} : ((sᶜ : L.definable_set A α) : set (α → M)) = sᶜ :=
-begin
-  ext,
-  simp,
-end
 
 instance : boolean_algebra (L.definable_set A α) :=
-{ sdiff := λ s t, s ⊓ tᶜ,
-  sdiff_eq := λ s t, rfl,
-  inf_compl_le_bot := λ ⟨s, hs⟩, by simp [le_iff],
-  top_le_sup_compl := λ ⟨s, hs⟩, by simp [le_iff],
-  .. definable_set.has_compl,
-  .. definable_set.bounded_order,
-  .. definable_set.distrib_lattice }
+subtype.coe_injective.boolean_algebra _ coe_sup coe_inf coe_top coe_bot coe_compl coe_sdiff
 
 end definable_set
 end language