bump to nightly-2023-06-01-04

mathlib commit leanprover-community/mathlib@cca4078

Mathbin/Algebra/Algebra/Basic.lean

@@ -458,53 +458,37 @@ section
 
 variable {r : R} {a : A}
 
-/- warning: algebra.bit0_smul_one clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit0_smul_one [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit0 r • (1 : A) = bit0 (r • (1 : A)) := by simp [bit0, add_smul]
-#align algebra.bit0_smul_one [anonymous]
+theorem bit0_smul_one : bit0 r • (1 : A) = bit0 (r • (1 : A)) := by simp [bit0, add_smul]
+#align algebra.bit0_smul_one Algebra.bit0_smul_one
 
-/- warning: algebra.bit0_smul_one' clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit0_smul_one' [anonymous]ₓ'. -/
-theorem [anonymous] : bit0 r • (1 : A) = r • 2 := by simp [bit0, add_smul, smul_add]
-#align algebra.bit0_smul_one' [anonymous]
+theorem bit0_smul_one' : bit0 r • (1 : A) = r • 2 := by simp [bit0, add_smul, smul_add]
+#align algebra.bit0_smul_one' Algebra.bit0_smul_one'
 
-/- warning: algebra.bit0_smul_bit0 clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit0_smul_bit0 [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit0 r • bit0 a = r • bit0 (bit0 a) := by simp [bit0, add_smul, smul_add]
-#align algebra.bit0_smul_bit0 [anonymous]
+theorem bit0_smul_bit0 : bit0 r • bit0 a = r • bit0 (bit0 a) := by simp [bit0, add_smul, smul_add]
+#align algebra.bit0_smul_bit0 Algebra.bit0_smul_bit0
 
-/- warning: algebra.bit0_smul_bit1 clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit0_smul_bit1 [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit0 r • bit1 a = r • bit0 (bit1 a) := by simp [bit0, add_smul, smul_add]
-#align algebra.bit0_smul_bit1 [anonymous]
+theorem bit0_smul_bit1 : bit0 r • bit1 a = r • bit0 (bit1 a) := by simp [bit0, add_smul, smul_add]
+#align algebra.bit0_smul_bit1 Algebra.bit0_smul_bit1
 
-/- warning: algebra.bit1_smul_one clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit1_smul_one [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit1 r • (1 : A) = bit1 (r • (1 : A)) := by simp [bit1, add_smul]
-#align algebra.bit1_smul_one [anonymous]
+theorem bit1_smul_one : bit1 r • (1 : A) = bit1 (r • (1 : A)) := by simp [bit1, add_smul]
+#align algebra.bit1_smul_one Algebra.bit1_smul_one
 
-/- warning: algebra.bit1_smul_one' clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit1_smul_one' [anonymous]ₓ'. -/
-theorem [anonymous] : bit1 r • (1 : A) = r • 2 + 1 := by simp [bit1, bit0, add_smul, smul_add]
-#align algebra.bit1_smul_one' [anonymous]
+theorem bit1_smul_one' : bit1 r • (1 : A) = r • 2 + 1 := by simp [bit1, bit0, add_smul, smul_add]
+#align algebra.bit1_smul_one' Algebra.bit1_smul_one'
 
-/- warning: algebra.bit1_smul_bit0 clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit1_smul_bit0 [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit1 r • bit0 a = r • bit0 (bit0 a) + bit0 a := by
+theorem bit1_smul_bit0 : bit1 r • bit0 a = r • bit0 (bit0 a) + bit0 a := by
   simp [bit1, add_smul, smul_add]
-#align algebra.bit1_smul_bit0 [anonymous]
+#align algebra.bit1_smul_bit0 Algebra.bit1_smul_bit0
 
-/- warning: algebra.bit1_smul_bit1 clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align algebra.bit1_smul_bit1 [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] : bit1 r • bit1 a = r • bit0 (bit1 a) + bit1 a := by
+theorem bit1_smul_bit1 : bit1 r • bit1 a = r • bit0 (bit1 a) + bit1 a := by
   simp only [bit0, bit1, add_smul, smul_add, one_smul]; abel
-#align algebra.bit1_smul_bit1 [anonymous]
+#align algebra.bit1_smul_bit1 Algebra.bit1_smul_bit1
 
 end
 

Mathbin/Algebra/Algebra/Bilinear.lean

@@ -169,12 +169,10 @@ def Algebra.lmul : A →ₐ[R] End R A :=
 
 variable {R A}
 
-#print Algebra.coe_lmul_eq_mul /-
 @[simp]
 theorem Algebra.coe_lmul_eq_mul : ⇑(Algebra.lmul R A) = mul R A :=
   rfl
 #align algebra.coe_lmul_eq_mul Algebra.coe_lmul_eq_mul
--/
 
 @[simp]
 theorem mulLeft_eq_zero_iff (a : A) : mulLeft R a = 0 ↔ a = 0 :=

Mathbin/Algebra/Algebra/Equiv.lean

@@ -165,12 +165,10 @@ theorem mk_coe (e : A₁ ≃ₐ[R] A₂) (e' h₁ h₂ h₃ h₄ h₅) :
   ext fun _ => rfl
 #align alg_equiv.mk_coe AlgEquiv.mk_coe
 
-/- warning: alg_equiv.to_fun_eq_coe clashes with [anonymous] -> [anonymous]
-Case conversion may be inaccurate. Consider using '#align alg_equiv.to_fun_eq_coe [anonymous]ₓ'. -/
 @[simp]
-theorem [anonymous] (e : A₁ ≃ₐ[R] A₂) : e.toFun = e :=
+theorem toFun_eq_coe (e : A₁ ≃ₐ[R] A₂) : e.toFun = e :=
   rfl
-#align alg_equiv.to_fun_eq_coe [anonymous]
+#align alg_equiv.to_fun_eq_coe AlgEquiv.toFun_eq_coe
 
 #print AlgEquiv.toEquiv_eq_coe /-
 @[simp]
@@ -255,12 +253,10 @@ theorem toAlgHom_eq_coe : e.toAlgHom = e :=
   rfl
 #align alg_equiv.to_alg_hom_eq_coe AlgEquiv.toAlgHom_eq_coe
 
-#print AlgEquiv.coe_algHom /-
 @[simp, norm_cast]
 theorem coe_algHom : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e :=
   rfl
 #align alg_equiv.coe_alg_hom AlgEquiv.coe_algHom
--/
 
 theorem coe_algHom_injective : Function.Injective (coe : (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂) :=
   fun e₁ e₂ h => ext <| AlgHom.congr_fun h
@@ -522,27 +518,21 @@ theorem ofAlgHom_symm (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁
 #align alg_equiv.of_alg_hom_symm AlgEquiv.ofAlgHom_symm
 -/
 
-#print AlgEquiv.ofBijective /-
 /-- Promotes a bijective algebra homomorphism to an algebra equivalence. -/
 noncomputable def ofBijective (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) : A₁ ≃ₐ[R] A₂ :=
   { RingEquiv.ofBijective (f : A₁ →+* A₂) hf, f with }
 #align alg_equiv.of_bijective AlgEquiv.ofBijective
--/
 
-#print AlgEquiv.coe_ofBijective /-
 @[simp]
 theorem coe_ofBijective {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} :
     (AlgEquiv.ofBijective f hf : A₁ → A₂) = f :=
   rfl
 #align alg_equiv.coe_of_bijective AlgEquiv.coe_ofBijective
--/
 
-#print AlgEquiv.ofBijective_apply /-
 theorem ofBijective_apply {f : A₁ →ₐ[R] A₂} {hf : Function.Bijective f} (a : A₁) :
     (AlgEquiv.ofBijective f hf) a = f a :=
   rfl
 #align alg_equiv.of_bijective_apply AlgEquiv.ofBijective_apply
--/
 
 #print AlgEquiv.toLinearEquiv /-
 /-- Forgetting the multiplicative structures, an equivalence of algebras is a linear equivalence. -/

Mathbin/Algebra/Algebra/Hom.lean

@@ -160,17 +160,13 @@ theorem coe_toAddMonoidHom (f : A →ₐ[R] B) : ⇑(f : A →+ B) = f :=
 
 variable (φ : A →ₐ[R] B)
 
-#print AlgHom.coe_fn_injective /-
 theorem coe_fn_injective : @Function.Injective (A →ₐ[R] B) (A → B) coeFn :=
   FunLike.coe_injective
 #align alg_hom.coe_fn_injective AlgHom.coe_fn_injective
--/
 
-#print AlgHom.coe_fn_inj /-
 theorem coe_fn_inj {φ₁ φ₂ : A →ₐ[R] B} : (φ₁ : A → B) = φ₂ ↔ φ₁ = φ₂ :=
   FunLike.coe_fn_eq
 #align alg_hom.coe_fn_inj AlgHom.coe_fn_inj
--/
 
 theorem coe_ringHom_injective : Function.Injective (coe : (A →ₐ[R] B) → A →+* B) := fun φ₁ φ₂ H =>
   coe_fn_injective <| show ((φ₁ : A →+* B) : A → B) = ((φ₂ : A →+* B) : A → B) from congr_arg _ H
@@ -184,85 +180,61 @@ theorem coe_addMonoidHom_injective : Function.Injective (coe : (A →ₐ[R] B) 
   RingHom.coe_addMonoidHom_injective.comp coe_ringHom_injective
 #align alg_hom.coe_add_monoid_hom_injective AlgHom.coe_addMonoidHom_injective
 
-#print AlgHom.congr_fun /-
 protected theorem congr_fun {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) : φ₁ x = φ₂ x :=
   FunLike.congr_fun H x
 #align alg_hom.congr_fun AlgHom.congr_fun
--/
 
-#print AlgHom.congr_arg /-
 protected theorem congr_arg (φ : A →ₐ[R] B) {x y : A} (h : x = y) : φ x = φ y :=
   FunLike.congr_arg φ h
 #align alg_hom.congr_arg AlgHom.congr_arg
--/
 
-#print AlgHom.ext /-
 @[ext]
 theorem ext {φ₁ φ₂ : A →ₐ[R] B} (H : ∀ x, φ₁ x = φ₂ x) : φ₁ = φ₂ :=
   FunLike.ext _ _ H
 #align alg_hom.ext AlgHom.ext
--/
 
-#print AlgHom.ext_iff /-
 theorem ext_iff {φ₁ φ₂ : A →ₐ[R] B} : φ₁ = φ₂ ↔ ∀ x, φ₁ x = φ₂ x :=
   FunLike.ext_iff
 #align alg_hom.ext_iff AlgHom.ext_iff
--/
 
-#print AlgHom.mk_coe /-
 @[simp]
 theorem mk_coe {f : A →ₐ[R] B} (h₁ h₂ h₃ h₄ h₅) : (⟨f, h₁, h₂, h₃, h₄, h₅⟩ : A →ₐ[R] B) = f :=
   ext fun _ => rfl
 #align alg_hom.mk_coe AlgHom.mk_coe
--/
 
-#print AlgHom.commutes /-
 @[simp]
 theorem commutes (r : R) : φ (algebraMap R A r) = algebraMap R B r :=
   φ.commutes' r
 #align alg_hom.commutes AlgHom.commutes
--/
 
 theorem comp_algebraMap : (φ : A →+* B).comp (algebraMap R A) = algebraMap R B :=
   RingHom.ext <| φ.commutes
 #align alg_hom.comp_algebra_map AlgHom.comp_algebraMap
 
-#print AlgHom.map_add /-
 protected theorem map_add (r s : A) : φ (r + s) = φ r + φ s :=
   map_add _ _ _
 #align alg_hom.map_add AlgHom.map_add
--/
 
-#print AlgHom.map_zero /-
 protected theorem map_zero : φ 0 = 0 :=
   map_zero _
 #align alg_hom.map_zero AlgHom.map_zero
--/
 
-#print AlgHom.map_mul /-
 protected theorem map_mul (x y) : φ (x * y) = φ x * φ y :=
   map_mul _ _ _
 #align alg_hom.map_mul AlgHom.map_mul
--/
 
-#print AlgHom.map_one /-
 protected theorem map_one : φ 1 = 1 :=
   map_one _
 #align alg_hom.map_one AlgHom.map_one
--/
 
-#print AlgHom.map_pow /-
 protected theorem map_pow (x : A) (n : ℕ) : φ (x ^ n) = φ x ^ n :=
   map_pow _ _ _
 #align alg_hom.map_pow AlgHom.map_pow
--/
 
-#print AlgHom.map_smul /-
 @[simp]
 protected theorem map_smul (r : R) (x : A) : φ (r • x) = r • φ x :=
   map_smul _ _ _
 #align alg_hom.map_smul AlgHom.map_smul
--/
 
 protected theorem map_sum {ι : Type _} (f : ι → A) (s : Finset ι) :
     φ (∑ x in s, f x) = ∑ x in s, φ (f x) :=
@@ -274,17 +246,13 @@ protected theorem map_finsupp_sum {α : Type _} [Zero α] {ι : Type _} (f : ι
   map_finsupp_sum _ _ _
 #align alg_hom.map_finsupp_sum AlgHom.map_finsupp_sum
 
-#print AlgHom.map_bit0 /-
 protected theorem map_bit0 (x) : φ (bit0 x) = bit0 (φ x) :=
   map_bit0 _ _
 #align alg_hom.map_bit0 AlgHom.map_bit0
--/
 
-#print AlgHom.map_bit1 /-
 protected theorem map_bit1 (x) : φ (bit1 x) = bit1 (φ x) :=
   map_bit1 _ _
 #align alg_hom.map_bit1 AlgHom.map_bit1
--/
 
 /-- If a `ring_hom` is `R`-linear, then it is an `alg_hom`. -/
 def mk' (f : A →+* B) (h : ∀ (c : R) (x), f (c • x) = c • f x) : A →ₐ[R] B :=
@@ -309,12 +277,10 @@ protected def id : A →ₐ[R] A :=
 #align alg_hom.id AlgHom.id
 -/
 
-#print AlgHom.coe_id /-
 @[simp]
 theorem coe_id : ⇑(AlgHom.id R A) = id :=
   rfl
 #align alg_hom.coe_id AlgHom.coe_id
--/
 
 @[simp]
 theorem id_toRingHom : (AlgHom.id R A : A →+* A) = RingHom.id _ :=
@@ -323,11 +289,9 @@ theorem id_toRingHom : (AlgHom.id R A : A →+* A) = RingHom.id _ :=
 
 end
 
-#print AlgHom.id_apply /-
 theorem id_apply (p : A) : AlgHom.id R A p = p :=
   rfl
 #align alg_hom.id_apply AlgHom.id_apply
--/
 
 #print AlgHom.comp /-
 /-- Composition of algebra homeomorphisms. -/
@@ -337,18 +301,14 @@ def comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : A →ₐ[R] C :=
 #align alg_hom.comp AlgHom.comp
 -/
 
-#print AlgHom.coe_comp /-
 @[simp]
 theorem coe_comp (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) : ⇑(φ₁.comp φ₂) = φ₁ ∘ φ₂ :=
   rfl
 #align alg_hom.coe_comp AlgHom.coe_comp
--/
 
-#print AlgHom.comp_apply /-
 theorem comp_apply (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) : φ₁.comp φ₂ p = φ₁ (φ₂ p) :=
   rfl
 #align alg_hom.comp_apply AlgHom.comp_apply
--/
 
 theorem comp_toRingHom (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
     (φ₁.comp φ₂ : A →+* C) = (φ₁ : B →+* C).comp ↑φ₂ :=
@@ -443,11 +403,9 @@ theorem map_smul_of_tower {R'} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul
   φ.toLinearMap.map_smul_of_tower r x
 #align alg_hom.map_smul_of_tower AlgHom.map_smul_of_tower
 
-#print AlgHom.map_list_prod /-
 theorem map_list_prod (s : List A) : φ s.Prod = (s.map φ).Prod :=
   φ.toRingHom.map_list_prod s
 #align alg_hom.map_list_prod AlgHom.map_list_prod
--/
 
 #print AlgHom.End /-
 @[simps (config := { attrs := [] }) mul one]
@@ -460,19 +418,15 @@ instance End : Monoid (A →ₐ[R] A) where
 #align alg_hom.End AlgHom.End
 -/
 
-#print AlgHom.one_apply /-
 @[simp]
 theorem one_apply (x : A) : (1 : A →ₐ[R] A) x = x :=
   rfl
 #align alg_hom.one_apply AlgHom.one_apply
--/
 
-#print AlgHom.mul_apply /-
 @[simp]
 theorem mul_apply (φ ψ : A →ₐ[R] A) (x : A) : (φ * ψ) x = φ (ψ x) :=
   rfl
 #align alg_hom.mul_apply AlgHom.mul_apply
--/
 
 theorem algebraMap_eq_apply (f : A →ₐ[R] B) {y : R} {x : A} (h : algebraMap R A y = x) :
     algebraMap R B y = f x :=
@@ -487,11 +441,9 @@ variable [CommSemiring R] [CommSemiring A] [CommSemiring B]
 
 variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
 
-#print AlgHom.map_multiset_prod /-
 protected theorem map_multiset_prod (s : Multiset A) : φ s.Prod = (s.map φ).Prod :=
   map_multiset_prod _ _
 #align alg_hom.map_multiset_prod AlgHom.map_multiset_prod
--/
 
 protected theorem map_prod {ι : Type _} (f : ι → A) (s : Finset ι) :
     φ (∏ x in s, f x) = ∏ x in s, φ (f x) :=
@@ -511,17 +463,13 @@ variable [CommSemiring R] [Ring A] [Ring B]
 
 variable [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B)
 
-#print AlgHom.map_neg /-
 protected theorem map_neg (x) : φ (-x) = -φ x :=
   map_neg _ _
 #align alg_hom.map_neg AlgHom.map_neg
--/
 
-#print AlgHom.map_sub /-
 protected theorem map_sub (x y) : φ (x - y) = φ x - φ y :=
   map_sub _ _ _
 #align alg_hom.map_sub AlgHom.map_sub
--/
 
 end Ring
 
@@ -600,11 +548,9 @@ def ofId : R →ₐ[R] A :=
 
 variable {R}
 
-#print Algebra.ofId_apply /-
 theorem ofId_apply (r) : ofId R A r = algebraMap R A r :=
   rfl
 #align algebra.of_id_apply Algebra.ofId_apply
--/
 
 end Algebra