bump to nightly-2023-08-09-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/DirectSum/Basic.lean

@@ -394,7 +394,7 @@ indexed by `ι`.
 When `S = submodule _ M`, this is available as a `linear_map`, `direct_sum.coe_linear_map`. -/
 protected def coeAddMonoidHom {M S : Type _} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
     [AddSubmonoidClass S M] (A : ι → S) : (⨁ i, A i) →+ M :=
-  toAddMonoid fun i => AddSubmonoidClass.Subtype (A i)
+  toAddMonoid fun i => AddSubmonoidClass.subtype (A i)
 #align direct_sum.coe_add_monoid_hom DirectSum.coeAddMonoidHom
 -/
 

Mathbin/Algebra/DirectSum/Internal.lean

@@ -174,7 +174,7 @@ variable [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
 #print DirectSum.coeRingHom /-
 /-- The canonical ring isomorphism between `⨁ i, A i` and `R`-/
 def coeRingHom [AddMonoid ι] [SetLike.GradedMonoid A] : (⨁ i, A i) →+* R :=
-  DirectSum.toSemiring (fun i => AddSubmonoidClass.Subtype (A i)) rfl fun _ _ _ _ => rfl
+  DirectSum.toSemiring (fun i => AddSubmonoidClass.subtype (A i)) rfl fun _ _ _ _ => rfl
 #align direct_sum.coe_ring_hom DirectSum.coeRingHom
 -/
 

Mathbin/Algebra/Module/Submodule/Basic.lean

@@ -219,7 +219,7 @@ Case conversion may be inaccurate. Consider using '#align smul_mem_class.to_modu
 -- Prefer subclasses of `module` over `smul_mem_class`.
 /-- A submodule of a `module` is a `module`.  -/
 instance (priority := 75) toModule : Module R S' :=
-  Subtype.coe_injective.Module R (AddSubmonoidClass.Subtype S') (SetLike.val_smul S')
+  Subtype.coe_injective.Module R (AddSubmonoidClass.subtype S') (SetLike.val_smul S')
 #align smul_mem_class.to_module SMulMemClass.toModule
 -/
 

Mathbin/Data/List/Intervals.lean

@@ -128,7 +128,7 @@ theorem inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = [] :=
   by
   apply eq_nil_iff_forall_not_mem.2
   intro a
-  simp only [and_imp, not_and, not_lt, List.mem_inter, List.Ico.mem]
+  simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
   intro h₁ h₂ h₃
   exfalso
   exact not_lt_of_ge h₃ h₂

Mathbin/Data/List/Lattice.lean

@@ -198,24 +198,24 @@ theorem cons_union (l₁ l₂ : List α) (a : α) : a :: l₁ ∪ l₂ = insert
   rfl
 #align list.cons_union List.cons_unionₓ
 
-#print List.mem_union /-
+#print List.mem_union_iff /-
 @[simp]
-theorem mem_union : a ∈ l₁ ∪ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂ := by
+theorem mem_union_iff : a ∈ l₁ ∪ l₂ ↔ a ∈ l₁ ∨ a ∈ l₂ := by
   induction l₁ <;>
     simp only [nil_union, not_mem_nil, false_or_iff, cons_union, mem_insert_iff, mem_cons_iff,
       or_assoc', *]
-#align list.mem_union List.mem_union
+#align list.mem_union List.mem_union_iff
 -/
 
 #print List.mem_union_left /-
 theorem mem_union_left (h : a ∈ l₁) (l₂ : List α) : a ∈ l₁ ∪ l₂ :=
-  mem_union.2 (Or.inl h)
+  mem_union_iff.2 (Or.inl h)
 #align list.mem_union_left List.mem_union_left
 -/
 
 #print List.mem_union_right /-
 theorem mem_union_right (l₁ : List α) (h : a ∈ l₂) : a ∈ l₁ ∪ l₂ :=
-  mem_union.2 (Or.inr h)
+  mem_union_iff.2 (Or.inr h)
 #align list.mem_union_right List.mem_union_right
 -/
 
@@ -309,11 +309,11 @@ theorem mem_inter_of_mem_of_mem : a ∈ l₁ → a ∈ l₂ → a ∈ l₁ ∩ l
 #align list.mem_inter_of_mem_of_mem List.mem_inter_of_mem_of_mem
 -/
 
-#print List.mem_inter /-
+#print List.mem_inter_iff /-
 @[simp]
-theorem mem_inter : a ∈ l₁ ∩ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂ :=
+theorem mem_inter_iff : a ∈ l₁ ∩ l₂ ↔ a ∈ l₁ ∧ a ∈ l₂ :=
   mem_filter
-#align list.mem_inter List.mem_inter
+#align list.mem_inter List.mem_inter_iff
 -/
 
 #print List.inter_subset_left /-
@@ -329,7 +329,7 @@ theorem inter_subset_right (l₁ l₂ : List α) : l₁ ∩ l₂ ⊆ l₂ := fun
 
 #print List.subset_inter /-
 theorem subset_inter {l l₁ l₂ : List α} (h₁ : l ⊆ l₁) (h₂ : l ⊆ l₂) : l ⊆ l₁ ∩ l₂ := fun a h =>
-  mem_inter.2 ⟨h₁ h, h₂ h⟩
+  mem_inter_iff.2 ⟨h₁ h, h₂ h⟩
 #align list.subset_inter List.subset_inter
 -/