bump to nightly-2024-02-15-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/Order/Pi.lean

@@ -157,7 +157,7 @@ theorem const_le_one : const β a ≤ 1 ↔ a ≤ 1 :=
 theorem const_lt_one : const β a < 1 ↔ a < 1 :=
   @const_lt_const _ _ _ _ _ 1
 #align function.const_lt_one Function.const_lt_one
-#align function.const_neg Function.const_neg
+#align function.const_neg Function.const_neg'
 -/
 
 end Function

Mathbin/Analysis/Calculus/MeanValue.lean

@@ -1053,20 +1053,20 @@ theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : Differentiable
 #align image_sub_le_mul_sub_of_deriv_le image_sub_le_mul_sub_of_deriv_le
 -/
 
-#print Convex.strictMonoOn_of_deriv_pos /-
+#print strictMonoOn_of_deriv_pos /-
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
 `f` is a strictly monotone function on `D`.
 Note that we don't require differentiability explicitly as it already implied by the derivative
 being strictly positive. -/
-theorem Convex.strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
-    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D :=
+theorem strictMonoOn_of_deriv_pos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
+    (hf' : ∀ x ∈ interior D, 0 < deriv f x) : StrictMonoOn f D :=
   by
   rintro x hx y hy
   simpa only [MulZeroClass.zero_mul, sub_pos] using
     hD.mul_sub_lt_image_sub_of_lt_deriv hf _ hf' x hx y hy
   exact fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').DifferentiableWithinAt
-#align convex.strict_mono_on_of_deriv_pos Convex.strictMonoOn_of_deriv_pos
+#align convex.strict_mono_on_of_deriv_pos strictMonoOn_of_deriv_pos
 -/
 
 #print strictMono_of_deriv_pos /-
@@ -1083,16 +1083,16 @@ theorem strictMono_of_deriv_pos {f : ℝ → ℝ} (hf' : ∀ x, 0 < deriv f x) :
 #align strict_mono_of_deriv_pos strictMono_of_deriv_pos
 -/
 
-#print Convex.monotoneOn_of_deriv_nonneg /-
+#print monotoneOn_of_deriv_nonneg /-
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonnegative, then
 `f` is a monotone function on `D`. -/
-theorem Convex.monotoneOn_of_deriv_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
-    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D))
-    (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) : MonotoneOn f D := fun x hx y hy hxy => by
+theorem monotoneOn_of_deriv_nonneg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
+    (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
+    MonotoneOn f D := fun x hx y hy hxy => by
   simpa only [MulZeroClass.zero_mul, sub_nonneg] using
     hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x hx y hy hxy
-#align convex.monotone_on_of_deriv_nonneg Convex.monotoneOn_of_deriv_nonneg
+#align convex.monotone_on_of_deriv_nonneg monotoneOn_of_deriv_nonneg
 -/
 
 #print monotone_of_deriv_nonneg /-
@@ -1106,18 +1106,17 @@ theorem monotone_of_deriv_nonneg {f : ℝ → ℝ} (hf : Differentiable ℝ f) (
 #align monotone_of_deriv_nonneg monotone_of_deriv_nonneg
 -/
 
-#print Convex.strictAntiOn_of_deriv_neg /-
+#print strictAntiOn_of_deriv_neg /-
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is negative, then
 `f` is a strictly antitone function on `D`. -/
-theorem Convex.strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
-    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, deriv f x < 0) : StrictAntiOn f D :=
-  fun x hx y => by
+theorem strictAntiOn_of_deriv_neg {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
+    (hf' : ∀ x ∈ interior D, deriv f x < 0) : StrictAntiOn f D := fun x hx y => by
   simpa only [MulZeroClass.zero_mul, sub_lt_zero] using
     hD.image_sub_lt_mul_sub_of_deriv_lt hf
       (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).Ne).DifferentiableWithinAt) hf' x
       hx y
-#align convex.strict_anti_on_of_deriv_neg Convex.strictAntiOn_of_deriv_neg
+#align convex.strict_anti_on_of_deriv_neg strictAntiOn_of_deriv_neg
 -/
 
 #print strictAnti_of_deriv_neg /-
@@ -1134,16 +1133,16 @@ theorem strictAnti_of_deriv_neg {f : ℝ → ℝ} (hf' : ∀ x, deriv f x < 0) :
 #align strict_anti_of_deriv_neg strictAnti_of_deriv_neg
 -/
 
-#print Convex.antitoneOn_of_deriv_nonpos /-
+#print antitoneOn_of_deriv_nonpos /-
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
 `f` is an antitone function on `D`. -/
-theorem Convex.antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
-    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D))
-    (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) : AntitoneOn f D := fun x hx y hy hxy => by
+theorem antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
+    (hf' : DifferentiableOn ℝ f (interior D)) (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
+    AntitoneOn f D := fun x hx y hy hxy => by
   simpa only [MulZeroClass.zero_mul, sub_nonpos] using
     hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy
-#align convex.antitone_on_of_deriv_nonpos Convex.antitoneOn_of_deriv_nonpos
+#align convex.antitone_on_of_deriv_nonpos antitoneOn_of_deriv_nonpos
 -/
 
 #print antitone_of_deriv_nonpos /-

Mathbin/Analysis/InnerProductSpace/TwoDim.lean

@@ -554,7 +554,7 @@ theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) :
       by
       rw [← (o.basis_right_angle_rotation x hx).sum_repr y]
       simp only [Fin.sum_univ_succ, coe_basis_right_angle_rotation, Matrix.cons_val_zero,
-        Fin.succ_zero_eq_one, Fintype.univ_of_isEmpty, Finset.sum_empty, o.area_form_apply_self,
+        Fin.succ_zero_eq_one, Fintype.univ_ofIsEmpty, Finset.sum_empty, o.area_form_apply_self,
         map_smul, map_add, map_zero, inner_smul_left, inner_smul_right, inner_add_left,
         inner_add_right, inner_zero_right, LinearMap.add_apply, Matrix.cons_val_one,
         Matrix.head_cons, Algebra.id.smul_eq_mul, o.area_form_right_angle_rotation_right,

Mathbin/Analysis/MeanInequalities.lean

@@ -200,7 +200,7 @@ for two `nnreal` numbers. -/
 theorem geom_mean_le_arith_mean2_weighted (w₁ w₂ p₁ p₂ : ℝ≥0) :
     w₁ + w₂ = 1 → p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ := by
   simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
-    Fintype.univ_of_isEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using
+    Fintype.univ_ofIsEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using
     geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]
 #align nnreal.geom_mean_le_arith_mean2_weighted NNReal.geom_mean_le_arith_mean2_weighted
 -/
@@ -211,7 +211,7 @@ theorem geom_mean_le_arith_mean3_weighted (w₁ w₂ w₃ p₁ p₂ p₃ : ℝ
       p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) * p₃ ^ (w₃ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ :=
   by
   simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
-    Fintype.univ_of_isEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
+    Fintype.univ_ofIsEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
     mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃] ![p₁, p₂, p₃]
 #align nnreal.geom_mean_le_arith_mean3_weighted NNReal.geom_mean_le_arith_mean3_weighted
 -/
@@ -223,7 +223,7 @@ theorem geom_mean_le_arith_mean4_weighted (w₁ w₂ w₃ w₄ p₁ p₂ p₃ p
         w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄ :=
   by
   simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
-    Fintype.univ_of_isEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
+    Fintype.univ_ofIsEmpty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
     mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃, w₄] ![p₁, p₂, p₃, p₄]
 #align nnreal.geom_mean_le_arith_mean4_weighted NNReal.geom_mean_le_arith_mean4_weighted
 -/

Mathbin/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

@@ -125,7 +125,7 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x :=
     rwa [lt_inv, inv_one]
     · exact zero_lt_one
     simpa only [sq, mul_self_pos] using this.ne'
-  have mono := Convex.strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
+  have mono := strictMonoOn_of_deriv_pos (convex_Ico 0 (π / 2)) tan_minus_id_cts deriv_pos
   have zero_in_U : (0 : ℝ) ∈ U := by rwa [left_mem_Ico]
   have x_in_U : x ∈ U := ⟨h1.le, h2⟩
   simpa only [tan_zero, sub_zero, sub_pos] using mono zero_in_U x_in_U h1

Mathbin/Data/Fintype/Basic.lean

@@ -757,14 +757,14 @@ instance (priority := 100) ofIsEmpty [IsEmpty α] : Fintype α :=
 #align fintype.of_is_empty Fintype.ofIsEmpty
 -/
 
-#print Fintype.univ_of_isEmpty /-
+#print Fintype.univ_ofIsEmpty /-
 -- no-lint since while `finset.univ_eq_empty` can prove this, it isn't applicable for `dsimp`.
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
 arbitrary `fintype` instances, use `finset.univ_eq_empty`. -/
 @[simp, nolint simp_nf]
-theorem univ_of_isEmpty [IsEmpty α] : @univ α _ = ∅ :=
+theorem univ_ofIsEmpty [IsEmpty α] : @univ α _ = ∅ :=
   rfl
-#align fintype.univ_of_is_empty Fintype.univ_of_isEmpty
+#align fintype.univ_of_is_empty Fintype.univ_ofIsEmpty
 -/
 
 end Fintype

Mathbin/Data/Fintype/Card.lean

@@ -255,13 +255,13 @@ theorem card_unique [Unique α] [h : Fintype α] : Fintype.card α = 1 :=
 #align fintype.card_unique Fintype.card_unique
 -/
 
-#print Fintype.card_of_isEmpty /-
+#print Fintype.card_ofIsEmpty /-
 /-- Note: this lemma is specifically about `fintype.of_is_empty`. For a statement about
 arbitrary `fintype` instances, use `fintype.card_eq_zero_iff`. -/
 @[simp]
-theorem card_of_isEmpty [IsEmpty α] : Fintype.card α = 0 :=
+theorem card_ofIsEmpty [IsEmpty α] : Fintype.card α = 0 :=
   rfl
-#align fintype.card_of_is_empty Fintype.card_of_isEmpty
+#align fintype.card_of_is_empty Fintype.card_ofIsEmpty
 -/
 
 end Fintype

Mathbin/Data/Pi/Algebra.lean

@@ -69,12 +69,12 @@ theorem one_def [∀ i, One <| f i] : (1 : ∀ i, f i) = fun i => 1 :=
 #align pi.zero_def Pi.zero_def
 -/
 
-#print Pi.const_one /-
+#print Function.const_one /-
 @[simp, to_additive]
 theorem const_one [One β] : const α (1 : β) = 1 :=
   rfl
-#align pi.const_one Pi.const_one
-#align pi.const_zero Pi.const_zero
+#align pi.const_one Function.const_one
+#align pi.const_zero Function.const_zero
 -/
 
 #print Pi.one_comp /-
@@ -117,12 +117,12 @@ theorem mul_def [∀ i, Mul <| f i] : x * y = fun i => x i * y i :=
 #align pi.add_def Pi.add_def
 -/
 
-#print Pi.const_mul /-
+#print Function.const_mul /-
 @[simp, to_additive]
 theorem const_mul [Mul β] (a b : β) : const α a * const α b = const α (a * b) :=
   rfl
-#align pi.const_mul Pi.const_mul
-#align pi.const_add Pi.const_add
+#align pi.const_mul Function.const_mul
+#align pi.const_add Function.const_add
 -/
 
 #print Pi.mul_comp /-
@@ -157,12 +157,12 @@ theorem smul_def [∀ i, SMul α <| f i] (s : α) (x : ∀ i, f i) : s • x = f
 #align pi.vadd_def Pi.vadd_def
 -/
 
-#print Pi.smul_const /-
+#print Function.smul_const /-
 @[simp, to_additive]
 theorem smul_const [SMul α β] (a : α) (b : β) : a • const I b = const I (a • b) :=
   rfl
-#align pi.smul_const Pi.smul_const
-#align pi.vadd_const Pi.vadd_const
+#align pi.smul_const Function.smul_const
+#align pi.vadd_const Function.vadd_const
 -/
 
 #print Pi.smul_comp /-
@@ -195,13 +195,13 @@ theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i
 #align pi.smul_def Pi.smul_def
 -/
 
-#print Pi.const_pow /-
+#print Function.const_pow /-
 -- `to_additive` generates bad output if we take `has_pow α β`.
 @[simp, to_additive smul_const, to_additive_reorder 5]
 theorem const_pow [Pow β α] (b : β) (a : α) : const I b ^ a = const I (b ^ a) :=
   rfl
-#align pi.const_pow Pi.const_pow
-#align pi.smul_const Pi.smul_const
+#align pi.const_pow Function.const_pow
+#align pi.smul_const Function.smul_const
 -/
 
 #print Pi.pow_comp /-
@@ -250,12 +250,12 @@ theorem inv_def [∀ i, Inv <| f i] : x⁻¹ = fun i => (x i)⁻¹ :=
 #align pi.neg_def Pi.neg_def
 -/
 
-#print Pi.const_inv /-
+#print Function.const_inv /-
 @[to_additive]
 theorem const_inv [Inv β] (a : β) : (const α a)⁻¹ = const α a⁻¹ :=
   rfl
-#align pi.const_inv Pi.const_inv
-#align pi.const_neg Pi.const_neg
+#align pi.const_inv Function.const_inv
+#align pi.const_neg Function.const_neg
 -/
 
 #print Pi.inv_comp /-
@@ -298,12 +298,12 @@ theorem div_comp [Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x
 #align pi.sub_comp Pi.sub_comp
 -/
 
-#print Pi.const_div /-
+#print Function.const_div /-
 @[simp, to_additive]
 theorem const_div [Div β] (a b : β) : const α a / const α b = const α (a / b) :=
   rfl
-#align pi.const_div Pi.const_div
-#align pi.const_sub Pi.const_sub
+#align pi.const_div Function.const_div
+#align pi.const_sub Function.const_sub
 -/
 
 section

Mathbin/FieldTheory/IntermediateField.lean

@@ -474,24 +474,20 @@ theorem coe_smul {R} [Semiring R] [SMul R K] [Module R L] [IsScalarTower R K L]
 #align intermediate_field.coe_smul IntermediateField.coe_smul
 -/
 
-#print IntermediateField.algebra' /-
 instance algebra' {K'} [CommSemiring K'] [SMul K' K] [Algebra K' L] [IsScalarTower K' K L] :
     Algebra K' S :=
   S.toSubalgebra.algebra'
 #align intermediate_field.algebra' IntermediateField.algebra'
--/
 
 #print IntermediateField.algebra /-
 instance algebra : Algebra K S :=
   S.toSubalgebra.Algebra
 #align intermediate_field.algebra IntermediateField.algebra
 -/
 
-#print IntermediateField.toAlgebra /-
 instance toAlgebra {R : Type _} [Semiring R] [Algebra L R] : Algebra S R :=
   S.toSubalgebra.toAlgebra
 #align intermediate_field.to_algebra IntermediateField.toAlgebra
--/
 
 #print IntermediateField.isScalarTower_bot /-
 instance isScalarTower_bot {R : Type _} [Semiring R] [Algebra L R] : IsScalarTower S L R :=

Mathbin/LinearAlgebra/Orientation.lean

@@ -493,7 +493,7 @@ theorem map_eq_iff_det_pos (x : Orientation R M ι) (f : M ≃ₗ[R] M)
   cases isEmpty_or_nonempty ι
   · have H : finrank R M = 0 := by
       refine' h.symm.trans _
-      convert Fintype.card_of_isEmpty
+      convert Fintype.card_ofIsEmpty
       infer_instance
     simp [LinearMap.det_eq_one_of_finrank_eq_zero H]
   have H : 0 < finrank R M := by
@@ -514,7 +514,7 @@ theorem map_eq_neg_iff_det_neg (x : Orientation R M ι) (f : M ≃ₗ[R] M)
   cases isEmpty_or_nonempty ι
   · have H : finrank R M = 0 := by
       refine' h.symm.trans _
-      convert Fintype.card_of_isEmpty
+      convert Fintype.card_ofIsEmpty
       infer_instance
     simp [LinearMap.det_eq_one_of_finrank_eq_zero H, Module.Ray.ne_neg_self x]
   have H : 0 < finrank R M := by

Mathbin/MeasureTheory/Integral/SetToL1.lean

@@ -756,11 +756,11 @@ theorem setToSimpleFunc_indicator (T : Set α → F →L[ℝ] F') (hT_empty : T
   swap; · rw [Finset.mem_singleton]; exact hx0
   rw [sum_singleton, (T _).map_zero, add_zero]
   congr
-  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Pi.const_zero,
+  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
     piecewise_eq_indicator]
   rw [indicator_preimage, preimage_const_of_mem]
   swap; · exact Set.mem_singleton x
-  rw [← Pi.const_zero, preimage_const_of_not_mem]
+  rw [← Function.const_zero, preimage_const_of_not_mem]
   swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
   simp
 #align measure_theory.simple_func.set_to_simple_func_indicator MeasureTheory.SimpleFunc.setToSimpleFunc_indicator

Mathbin/MeasureTheory/Measure/Haar/Basic.lean

@@ -821,9 +821,9 @@ theorem regular_of_isMulLeftInvariant {μ : Measure G} [SigmaFinite μ] [IsMulLe
 #align measure_theory.measure.regular_of_is_add_left_invariant MeasureTheory.Measure.regular_of_isAddLeftInvariant
 -/
 
-#print MeasureTheory.Measure.isHaarMeasure_eq_smul /-
+#print MeasureTheory.Measure.isMulLeftInvariant_eq_smul /-
 @[to_additive is_add_haar_measure_eq_smul_is_add_haar_measure]
-theorem isHaarMeasure_eq_smul [LocallyCompactSpace G] (μ ν : Measure G) [IsHaarMeasure μ]
+theorem isMulLeftInvariant_eq_smul [LocallyCompactSpace G] (μ ν : Measure G) [IsHaarMeasure μ]
     [IsHaarMeasure ν] : ∃ c : ℝ≥0∞, c ≠ 0 ∧ c ≠ ∞ ∧ μ = c • ν :=
   by
   have K : positive_compacts G := Classical.arbitrary _
@@ -843,8 +843,8 @@ theorem isHaarMeasure_eq_smul [LocallyCompactSpace G] (μ ν : Measure G) [IsHaa
       _ = (μ K / ν K) • ν K • haar_measure K := by
         rw [smul_smul, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel νpos.ne' νne, mul_one]
       _ = (μ K / ν K) • ν := by rw [← haar_measure_unique ν K]
-#align measure_theory.measure.is_haar_measure_eq_smul_is_haar_measure MeasureTheory.Measure.isHaarMeasure_eq_smul
-#align measure_theory.measure.is_add_haar_measure_eq_smul_is_add_haar_measure MeasureTheory.Measure.isAddHaarMeasure_eq_smul
+#align measure_theory.measure.is_haar_measure_eq_smul_is_haar_measure MeasureTheory.Measure.isMulLeftInvariant_eq_smul
+#align measure_theory.measure.is_add_haar_measure_eq_smul_is_add_haar_measure MeasureTheory.Measure.isAddLeftInvariant_eq_smul
 -/
 
 -- see Note [lower instance priority]

Mathbin/ModelTheory/Basic.lean

@@ -112,7 +112,7 @@ instance {n : ℕ} : IsEmpty (Sequence₂ a₀ a₁ a₂ (n + 3)) :=
 theorem lift_mk {i : ℕ} :
     Cardinal.lift (#Sequence₂ a₀ a₁ a₂ i) = (#Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) i) := by
   rcases i with (_ | _ | _ | i) <;>
-    simp only [sequence₂, mk_ulift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]
+    simp only [sequence₂, mk_ulift, mk_fintype, Fintype.card_ofIsEmpty, Nat.cast_zero, lift_zero]
 #align first_order.sequence₂.lift_mk FirstOrder.Sequence₂.lift_mk
 -/
 

Mathbin/RingTheory/Subring/Basic.lean

@@ -1892,7 +1892,7 @@ end Actions
 /-- The subgroup of positive units of a linear ordered semiring. -/
 def Units.posSubgroup (R : Type _) [LinearOrderedSemiring R] : Subgroup Rˣ :=
   {
-    (posSubmonoid R).comap
+    (Submonoid.pos R).comap
       (Units.coeHom R) with
     carrier := {x | (0 : R) < x}
     inv_mem' := fun x => Units.inv_pos.mpr }