bump to nightly-2023-08-02-09

mathlib commit leanprover-community/mathlib@63721b2

Mathbin/Algebra/Order/Hom/Ring.lean

@@ -301,26 +301,26 @@ theorem id_apply (a : α) : OrderRingHom.id α a = a :=
 #align order_ring_hom.id_apply OrderRingHom.id_apply
 -/
 
-#print OrderRingHom.coe_RingHom_id /-
+#print OrderRingHom.coe_ringHom_id /-
 @[simp]
-theorem coe_RingHom_id : (OrderRingHom.id α : α →+* α) = RingHom.id α :=
+theorem coe_ringHom_id : (OrderRingHom.id α : α →+* α) = RingHom.id α :=
   rfl
-#align order_ring_hom.coe_ring_hom_id OrderRingHom.coe_RingHom_id
+#align order_ring_hom.coe_ring_hom_id OrderRingHom.coe_ringHom_id
 -/
 
-#print OrderRingHom.coe_OrderAddMonoidHom_id /-
+#print OrderRingHom.coe_orderAddMonoidHom_id /-
 @[simp]
-theorem coe_OrderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
+theorem coe_orderAddMonoidHom_id : (OrderRingHom.id α : α →+o α) = OrderAddMonoidHom.id α :=
   rfl
-#align order_ring_hom.coe_order_add_monoid_hom_id OrderRingHom.coe_OrderAddMonoidHom_id
+#align order_ring_hom.coe_order_add_monoid_hom_id OrderRingHom.coe_orderAddMonoidHom_id
 -/
 
-#print OrderRingHom.coe_OrderMonoidWithZeroHom_id /-
+#print OrderRingHom.coe_orderMonoidWithZeroHom_id /-
 @[simp]
-theorem coe_OrderMonoidWithZeroHom_id :
+theorem coe_orderMonoidWithZeroHom_id :
     (OrderRingHom.id α : α →*₀o α) = OrderMonoidWithZeroHom.id α :=
   rfl
-#align order_ring_hom.coe_order_monoid_with_zero_hom_id OrderRingHom.coe_OrderMonoidWithZeroHom_id
+#align order_ring_hom.coe_order_monoid_with_zero_hom_id OrderRingHom.coe_orderMonoidWithZeroHom_id
 -/
 
 #print OrderRingHom.comp /-

Mathbin/Algebra/Order/LatticeGroup.lean

@@ -662,15 +662,15 @@ theorem mabs_mul_le [CovariantClass α α (· * ·) (· ≤ ·)] (a b : α) : |a
 #align lattice_ordered_comm_group.abs_add_le LatticeOrderedCommGroup.abs_add_le
 -/
 
-#print LatticeOrderedCommGroup.abs_inv_comm /-
+#print LatticeOrderedCommGroup.abs_div_comm /-
 -- |a - b| = |b - a|
 @[to_additive]
-theorem abs_inv_comm (a b : α) : |a / b| = |b / a| :=
+theorem abs_div_comm (a b : α) : |a / b| = |b / a| :=
   by
   unfold Abs.abs
   rw [inv_div a b, ← inv_inv (a / b), inv_div, sup_comm]
-#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_inv_comm
-#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_neg_comm
+#align lattice_ordered_comm_group.abs_inv_comm LatticeOrderedCommGroup.abs_div_comm
+#align lattice_ordered_comm_group.abs_neg_comm LatticeOrderedCommGroup.abs_sub_comm
 -/
 
 #print LatticeOrderedCommGroup.abs_abs_div_abs_le /-

Mathbin/Algebra/Ring/BooleanRing.lean

@@ -682,7 +682,7 @@ protected def BoundedLatticeHom.asBoolRing (f : BoundedLatticeHom α β) :
   toFun := toBoolRing ∘ f ∘ ofBoolRing
   map_zero' := f.map_bot'
   map_one' := f.map_top'
-  map_add' := map_symm_diff' f
+  map_add' := map_symmDiff' f
   map_mul' := f.map_inf'
 #align bounded_lattice_hom.as_boolring BoundedLatticeHom.asBoolRing
 -/

Mathbin/Data/Finset/Image.lean

@@ -684,7 +684,7 @@ theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Inj
 #print Finset.image_symmDiff /-
 theorem image_symmDiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
     (s ∆ t).image f = s.image f ∆ t.image f :=
-  coe_injective <| by push_cast ; exact Set.image_symm_diff hf _ _
+  coe_injective <| by push_cast ; exact Set.image_symmDiff hf _ _
 #align finset.image_symm_diff Finset.image_symmDiff
 -/
 

Mathbin/Data/Finset/Pointwise.lean

@@ -2633,10 +2633,10 @@ theorem smul_finset_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t
 #align finset.smul_finset_sdiff₀ Finset.smul_finset_sdiff₀
 -/
 
-#print Finset.smul_finset_symm_diff₀ /-
-theorem smul_finset_symm_diff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
+#print Finset.smul_finset_symmDiff₀ /-
+theorem smul_finset_symmDiff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
   image_symmDiff _ _ <| MulAction.injective₀ ha
-#align finset.smul_finset_symm_diff₀ Finset.smul_finset_symm_diff₀
+#align finset.smul_finset_symm_diff₀ Finset.smul_finset_symmDiff₀
 -/
 
 #print Finset.smul_univ₀ /-

Mathbin/Data/LazyList/Basic.lean

@@ -25,10 +25,10 @@ universe u
 
 namespace Thunk
 
-#print Thunk.pure /-
+#print Thunk.mk /-
 /-- Creates a thunk with a (non-lazy) constant value. -/
-def pure {α} (x : α) : Thunk α := fun _ => x
-#align thunk.mk Thunk.pure
+def mk {α} (x : α) : Thunk α := fun _ => x
+#align thunk.mk Thunk.mk
 -/
 
 instance {α : Type u} [DecidableEq α] : DecidableEq (Thunk α)
@@ -74,7 +74,7 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (LazyList α)
 protected def traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (f : α → m β) :
     LazyList α → m (LazyList β)
   | LazyList.nil => pure LazyList.nil
-  | LazyList.cons x xs => LazyList.cons <$> f x <*> Thunk.pure <$> traverse (xs ())
+  | LazyList.cons x xs => LazyList.cons <$> f x <*> Thunk.mk <$> traverse (xs ())
 #align lazy_list.traverse LazyList.traverse
 -/
 

Mathbin/Data/Set/Image.lean

@@ -548,11 +548,11 @@ theorem subset_image_diff (f : α → β) (s t : Set α) : f '' s \ f '' t ⊆ f
 #align set.subset_image_diff Set.subset_image_diff
 -/
 
-#print Set.subset_image_symm_diff /-
-theorem subset_image_symm_diff : (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
+#print Set.subset_image_symmDiff /-
+theorem subset_image_symmDiff : (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
   (union_subset_union (subset_image_diff _ _ _) <| subset_image_diff _ _ _).trans
     (image_union _ _ _).Superset
-#align set.subset_image_symm_diff Set.subset_image_symm_diff
+#align set.subset_image_symm_diff Set.subset_image_symmDiff
 -/
 
 #print Set.image_diff /-
@@ -563,10 +563,10 @@ theorem image_diff {f : α → β} (hf : Injective f) (s t : Set α) : f '' (s \
 #align set.image_diff Set.image_diff
 -/
 
-#print Set.image_symm_diff /-
-theorem image_symm_diff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
+#print Set.image_symmDiff /-
+theorem image_symmDiff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
   simp_rw [Set.symmDiff_def, image_union, image_diff hf]
-#align set.image_symm_diff Set.image_symm_diff
+#align set.image_symm_diff Set.image_symmDiff
 -/
 
 #print Set.Nonempty.image /-

Mathbin/Data/Set/Ncard.lean

@@ -757,8 +757,8 @@ theorem ncard_union_eq (h : Disjoint s t)
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/
-#print Set.ncard_diff_add_ncard_eq_ncard /-
-theorem ncard_diff_add_ncard_eq_ncard (h : s ⊆ t)
+#print Set.ncard_diff_add_ncard_of_subset /-
+theorem ncard_diff_add_ncard_of_subset (h : s ⊆ t)
     (ht : t.Finite := by
       run_tac
         to_finite_tac) :
@@ -768,7 +768,7 @@ theorem ncard_diff_add_ncard_eq_ncard (h : s ⊆ t)
     ncard_eq_to_finset_card _ (ht.diff s), finite.to_finset_diff]
   refine' Finset.card_sdiff_add_card_eq_card _
   rwa [finite.to_finset_subset_to_finset]
-#align set.ncard_diff_add_ncard_eq_ncard Set.ncard_diff_add_ncard_eq_ncard
+#align set.ncard_diff_add_ncard_eq_ncard Set.ncard_diff_add_ncard_of_subset
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic to_finite_tac -/

Mathbin/Data/Set/Pointwise/Smul.lean

@@ -1222,12 +1222,12 @@ theorem smul_set_sdiff : a • (s \ t) = a • s \ a • t :=
 #align set.vadd_set_sdiff Set.vadd_set_sdiff
 -/
 
-#print Set.smul_set_symm_diff /-
+#print Set.smul_set_symmDiff /-
 @[to_additive]
-theorem smul_set_symm_diff : a • s ∆ t = (a • s) ∆ (a • t) :=
-  image_symm_diff (MulAction.injective a) _ _
-#align set.smul_set_symm_diff Set.smul_set_symm_diff
-#align set.vadd_set_symm_diff Set.vadd_set_symm_diff
+theorem smul_set_symmDiff : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff (MulAction.injective a) _ _
+#align set.smul_set_symm_diff Set.smul_set_symmDiff
+#align set.vadd_set_symm_diff Set.vadd_set_symmDiff
 -/
 
 #print Set.smul_set_univ /-
@@ -1373,10 +1373,10 @@ theorem smul_set_sdiff₀ (ha : a ≠ 0) : a • (s \ t) = a • s \ a • t :=
 #align set.smul_set_sdiff₀ Set.smul_set_sdiff₀
 -/
 
-#print Set.smul_set_symm_diff₀ /-
-theorem smul_set_symm_diff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
-  image_symm_diff (MulAction.injective₀ ha) _ _
-#align set.smul_set_symm_diff₀ Set.smul_set_symm_diff₀
+#print Set.smul_set_symmDiff₀ /-
+theorem smul_set_symmDiff₀ (ha : a ≠ 0) : a • s ∆ t = (a • s) ∆ (a • t) :=
+  image_symmDiff (MulAction.injective₀ ha) _ _
+#align set.smul_set_symm_diff₀ Set.smul_set_symmDiff₀
 -/
 
 #print Set.smul_set_univ₀ /-

Mathbin/FieldTheory/SplittingField/Construction.lean

@@ -314,7 +314,7 @@ instance inhabited : Inhabited (SplittingField f) :=
 -/
 
 instance {S : Type _} [DistribSMul S K] [IsScalarTower S K K] : SMul S (SplittingField f) :=
-  Submodule.Quotient.hasSmul' _
+  Submodule.Quotient.instSMul' _
 
 #print Polynomial.SplittingField.algebra /-
 instance algebra : Algebra K (SplittingField f) :=

Mathbin/LinearAlgebra/Quotient.lean

@@ -147,19 +147,19 @@ section SMul
 
 variable {S : Type _} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)
 
-#print Submodule.Quotient.hasSmul' /-
-instance hasSmul' : SMul S (M ⧸ P) :=
+#print Submodule.Quotient.instSMul' /-
+instance instSMul' : SMul S (M ⧸ P) :=
   ⟨fun a =>
     Quotient.map' ((· • ·) a) fun x y h =>
       leftRel_apply.mpr <| by simpa [smul_sub] using P.smul_mem (a • 1 : R) (left_rel_apply.mp h)⟩
-#align submodule.quotient.has_smul' Submodule.Quotient.hasSmul'
+#align submodule.quotient.has_smul' Submodule.Quotient.instSMul'
 -/
 
-#print Submodule.Quotient.hasSmul /-
+#print Submodule.Quotient.instSMul /-
 /-- Shortcut to help the elaborator in the common case. -/
-instance hasSmul : SMul R (M ⧸ P) :=
-  Quotient.hasSmul' P
-#align submodule.quotient.has_smul Submodule.Quotient.hasSmul
+instance instSMul : SMul R (M ⧸ P) :=
+  Quotient.instSMul' P
+#align submodule.quotient.has_smul Submodule.Quotient.instSMul
 -/
 
 #print Submodule.Quotient.mk_smul /-
@@ -222,18 +222,18 @@ instance smulZeroClass (P : Submodule R M) : SMulZeroClass R (M ⧸ P) :=
 #align submodule.quotient.smul_zero_class Submodule.Quotient.smulZeroClass
 -/
 
-#print Submodule.Quotient.distribSmul' /-
-instance distribSmul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
+#print Submodule.Quotient.distribSMul' /-
+instance distribSMul' [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) :
     DistribSMul S (M ⧸ P) :=
   Function.Surjective.distribSMul ⟨mk, rfl, fun _ _ => rfl⟩ (surjective_quot_mk _)
     P.Quotient.mk_smul
-#align submodule.quotient.distrib_smul' Submodule.Quotient.distribSmul'
+#align submodule.quotient.distrib_smul' Submodule.Quotient.distribSMul'
 -/
 
-#print Submodule.Quotient.distribSmul /-
-instance distribSmul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
-  Quotient.distribSmul' P
-#align submodule.quotient.distrib_smul Submodule.Quotient.distribSmul
+#print Submodule.Quotient.distribSMul /-
+instance distribSMul (P : Submodule R M) : DistribSMul R (M ⧸ P) :=
+  Quotient.distribSMul' P
+#align submodule.quotient.distrib_smul Submodule.Quotient.distribSMul
 -/
 
 #print Submodule.Quotient.distribMulAction' /-

Mathbin/Order/Hom/Lattice.lean

@@ -325,11 +325,11 @@ theorem map_sdiff' (a b : α) : f (a \ b) = f a \ f b := by
 #align map_sdiff' map_sdiff'
 -/
 
-#print map_symm_diff' /-
+#print map_symmDiff' /-
 /-- Special case of `map_symm_diff` for boolean algebras. -/
-theorem map_symm_diff' (a b : α) : f (a ∆ b) = f a ∆ f b := by
+theorem map_symmDiff' (a b : α) : f (a ∆ b) = f a ∆ f b := by
   rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']
-#align map_symm_diff' map_symm_diff'
+#align map_symm_diff' map_symmDiff'
 -/
 
 end BooleanAlgebra

Mathbin/Order/LiminfLimsup.lean

@@ -1554,40 +1554,40 @@ section Order
 
 open Filter
 
-#print Monotone.isBoundedUnder_le_comp /-
-theorem Monotone.isBoundedUnder_le_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
+#print Monotone.isBoundedUnder_le_comp_iff /-
+theorem Monotone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atTop atTop) :
     IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
   by
   refine' ⟨_, fun h => h.IsBoundedUnder hg⟩
   rintro ⟨c, hc⟩; rw [eventually_map] at hc 
   obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_at_top.1 (hg'.eventually_gt_at_top c)
   exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩
-#align monotone.is_bounded_under_le_comp Monotone.isBoundedUnder_le_comp
+#align monotone.is_bounded_under_le_comp Monotone.isBoundedUnder_le_comp_iff
 -/
 
-#print Monotone.isBoundedUnder_ge_comp /-
-theorem Monotone.isBoundedUnder_ge_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
+#print Monotone.isBoundedUnder_ge_comp_iff /-
+theorem Monotone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Monotone g) (hg' : Tendsto g atBot atBot) :
     IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
   hg.dual.isBoundedUnder_le_comp hg'
-#align monotone.is_bounded_under_ge_comp Monotone.isBoundedUnder_ge_comp
+#align monotone.is_bounded_under_ge_comp Monotone.isBoundedUnder_ge_comp_iff
 -/
 
-#print Antitone.isBoundedUnder_le_comp /-
-theorem Antitone.isBoundedUnder_le_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
+#print Antitone.isBoundedUnder_le_comp_iff /-
+theorem Antitone.isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atBot atTop) :
     IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
   hg.dual_right.isBoundedUnder_ge_comp hg'
-#align antitone.is_bounded_under_le_comp Antitone.isBoundedUnder_le_comp
+#align antitone.is_bounded_under_le_comp Antitone.isBoundedUnder_le_comp_iff
 -/
 
-#print Antitone.isBoundedUnder_ge_comp /-
-theorem Antitone.isBoundedUnder_ge_comp [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
+#print Antitone.isBoundedUnder_ge_comp_iff /-
+theorem Antitone.isBoundedUnder_ge_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMinOrder γ]
     {g : β → γ} {f : α → β} {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atTop atBot) :
     IsBoundedUnder (· ≥ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≤ ·) l f :=
   hg.dual_right.isBoundedUnder_le_comp hg'
-#align antitone.is_bounded_under_ge_comp Antitone.isBoundedUnder_ge_comp
+#align antitone.is_bounded_under_ge_comp Antitone.isBoundedUnder_ge_comp_iff
 -/
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic is_bounded_default -/

Mathbin/RingTheory/AdjoinRoot.lean

@@ -119,10 +119,10 @@ def of : R →+* AdjoinRoot f :=
 -/
 
 instance [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
-  Submodule.Quotient.hasSmul' _
+  Submodule.Quotient.instSMul' _
 
 instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
-  Submodule.Quotient.distribSmul' _
+  Submodule.Quotient.distribSMul' _
 
 #print AdjoinRoot.smul_mk /-
 @[simp]

Mathbin/Topology/Algebra/Order/MonotoneConvergence.lean

@@ -245,18 +245,18 @@ instance {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] [∀ i, Top
     [∀ i, InfConvergenceClass (α i)] : InfConvergenceClass (∀ i, α i) :=
   show InfConvergenceClass (∀ i, (α i)ᵒᵈ)ᵒᵈ from OrderDual.infConvergenceClass
 
-#print Pi.Sup_convergence_class' /-
-instance Pi.Sup_convergence_class' {ι : Type _} [Preorder α] [TopologicalSpace α]
+#print Pi.supConvergenceClass' /-
+instance Pi.supConvergenceClass' {ι : Type _} [Preorder α] [TopologicalSpace α]
     [SupConvergenceClass α] : SupConvergenceClass (ι → α) :=
   Pi.supConvergenceClass
-#align pi.Sup_convergence_class' Pi.Sup_convergence_class'
+#align pi.Sup_convergence_class' Pi.supConvergenceClass'
 -/
 
-#print Pi.Inf_convergence_class' /-
-instance Pi.Inf_convergence_class' {ι : Type _} [Preorder α] [TopologicalSpace α]
+#print Pi.infConvergenceClass' /-
+instance Pi.infConvergenceClass' {ι : Type _} [Preorder α] [TopologicalSpace α]
     [InfConvergenceClass α] : InfConvergenceClass (ι → α) :=
   Pi.infConvergenceClass
-#align pi.Inf_convergence_class' Pi.Inf_convergence_class'
+#align pi.Inf_convergence_class' Pi.infConvergenceClass'
 -/
 
 #print tendsto_of_monotone /-