bump to nightly-2023-09-08-06

mathlib commit leanprover-community/mathlib@442a83d

Mathbin/Analysis/NormedSpace/LpSpace.lean

@@ -971,11 +971,11 @@ instance infty_isScalarTower {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)]
 #align lp.infty_is_scalar_tower lp.infty_isScalarTower
 -/
 
-#print lp.infty_sMulCommClass /-
-instance infty_sMulCommClass {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)] [∀ i, BoundedSMul 𝕜 (B i)]
+#print lp.infty_smulCommClass /-
+instance infty_smulCommClass {𝕜} [NormedRing 𝕜] [∀ i, Module 𝕜 (B i)] [∀ i, BoundedSMul 𝕜 (B i)]
     [∀ i, SMulCommClass 𝕜 (B i) (B i)] : SMulCommClass 𝕜 (lp B ∞) (lp B ∞) :=
   ⟨fun r f g => lp.ext <| smul_comm r (⇑f) ⇑g⟩
-#align lp.infty_smul_comm_class lp.infty_sMulCommClass
+#align lp.infty_smul_comm_class lp.infty_smulCommClass
 -/
 
 section StarRing

Mathbin/Analysis/SpecialFunctions/Stirling.lean

@@ -71,7 +71,6 @@ theorem stirlingSeq_one : stirlingSeq 1 = exp 1 / sqrt 2 := by
 #align stirling.stirling_seq_one Stirling.stirlingSeq_one
 -/
 
-#print Stirling.log_stirlingSeq_formula /-
 /-- We have the expression
 `log (stirling_seq (n + 1)) = log(n + 1)! - 1 / 2 * log(2 * n) - n * log ((n + 1) / e)`.
 -/
@@ -82,8 +81,7 @@ theorem log_stirlingSeq_formula (n : ℕ) :
   rw [stirling_seq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub] <;>
       try apply ne_of_gt <;>
     positivity
-#align stirling.log_stirling_seq_formula Stirling.log_stirlingSeq_formula
--/
+#align stirling.log_stirling_seq_formula Stirling.log_stirlingSeq_formulaₓ
 
 #print Stirling.log_stirlingSeq_diff_hasSum /-
 -- TODO: Make `positivity` handle `≠ 0` goals

Mathbin/Data/List/Basic.lean

@@ -1430,15 +1430,15 @@ theorem head!_eq_head? [Inhabited α] (l : List α) : headI l = (head? l).iget :
 #align list.head_eq_head' List.head!_eq_head?
 -/
 
-#print List.surjective_head /-
-theorem surjective_head [Inhabited α] : Surjective (@headI α _) := fun x => ⟨[x], rfl⟩
-#align list.surjective_head List.surjective_head
+#print List.surjective_head! /-
+theorem surjective_head! [Inhabited α] : Surjective (@headI α _) := fun x => ⟨[x], rfl⟩
+#align list.surjective_head List.surjective_head!
 -/
 
-#print List.surjective_head' /-
-theorem surjective_head' : Surjective (@head? α) :=
+#print List.surjective_head? /-
+theorem surjective_head? : Surjective (@head? α) :=
   Option.forall.2 ⟨⟨[], rfl⟩, fun x => ⟨[x], rfl⟩⟩
-#align list.surjective_head' List.surjective_head'
+#align list.surjective_head' List.surjective_head?
 -/
 
 #print List.surjective_tail /-

Mathbin/Data/Set/Intervals/ProjIcc.lean

@@ -312,11 +312,11 @@ theorem IicExtend_apply (f : Iic b → β) (x : α) : IicExtend f x = f ⟨min b
 #align set.Iic_extend_apply Set.IicExtend_apply
 -/
 
-#print Set.iccExtend_apply /-
-theorem iccExtend_apply (h : a ≤ b) (f : Icc a b → β) (x : α) :
+#print Set.IccExtend_apply /-
+theorem IccExtend_apply (h : a ≤ b) (f : Icc a b → β) (x : α) :
     IccExtend h f x = f ⟨max a (min b x), le_max_left _ _, max_le h (min_le_left _ _)⟩ :=
   rfl
-#align set.Icc_extend_apply Set.iccExtend_apply
+#align set.Icc_extend_apply Set.IccExtend_apply
 -/
 
 #print Set.range_IciExtend /-

Mathbin/FieldTheory/Normal.lean

@@ -603,11 +603,9 @@ instance is_finiteDimensional [FiniteDimensional F K] : FiniteDimensional F (nor
 #align normal_closure.is_finite_dimensional normalClosure.is_finiteDimensional
 -/
 
-#print normalClosure.isScalarTower /-
 instance isScalarTower : IsScalarTower F (normalClosure F K L) L :=
   IsScalarTower.subalgebra' F L L _
 #align normal_closure.is_scalar_tower normalClosure.isScalarTower
--/
 
 end normalClosure
 

Mathbin/GroupTheory/FreeProduct.lean

@@ -373,14 +373,12 @@ private def mk_aux {l} (ls : List (Σ i, M i)) (h1 : ∀ l' ∈ l::ls, Sigma.snd
   ⟨ls, fun l' hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-#print Monoid.CoprodI.Word.cons_eq_rcons /-
 theorem Monoid.CoprodI.Word.cons_eq_rcons {i} {m : M i} {ls h1 h2} :
     Monoid.CoprodI.Word.mk (⟨i, m⟩::ls) h1 h2 =
       Monoid.CoprodI.Word.rcons
         ⟨m, mkAux ls h1 h2, Monoid.CoprodI.Word.fstIdx_ne_iff.mpr h2.rel_head?⟩ :=
   by rw [rcons, dif_neg]; rfl; exact h1 ⟨i, m⟩ (ls.mem_cons_self _)
 #align free_product.word.cons_eq_rcons Monoid.CoprodI.Word.cons_eq_rcons
--/
 
 #print Monoid.CoprodI.Word.prod_rcons /-
 @[simp]

Mathbin/GroupTheory/SpecificGroups/Alternating.lean

@@ -207,7 +207,7 @@ theorem IsThreeCycle.alternating_normalClosure (h5 : 5 ≤ Fintype.card α) {f :
     (by
       have hi : Function.Injective (alternatingGroup α).Subtype := Subtype.coe_injective
       refine' eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _))
-      rw [← MonoidHom.range_eq_map, subtype_range, normalClosure, MonoidHom.map_closure]
+      rw [← MonoidHom.range_eq_map, subtype_range, normal_closure, MonoidHom.map_closure]
       refine' (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _)
       intro g h
       obtain ⟨c, rfl⟩ := isConj_iff.1 (is_conj_iff_cycle_type_eq.2 (hf.trans h.symm))
@@ -276,7 +276,7 @@ theorem normalClosure_finRotate_five :
       rw [Set.singleton_subset_iff, SetLike.mem_coe]
       have h :
         (⟨finRotate 5, fin_rotate_bit1_mem_alternating_group⟩ : alternatingGroup (Fin 5)) ∈
-          normalClosure _ :=
+          normal_closure _ :=
         SetLike.mem_coe.1 (subset_normal_closure (Set.mem_singleton _))
       exact
         mul_mem
@@ -306,7 +306,7 @@ theorem normalClosure_swap_mul_swap_five :
   rw [eq_top_iff, ← normal_closure_fin_rotate_five]
   refine' normal_closure_le_normal _
   rw [Set.singleton_subset_iff, SetLike.mem_coe, ← h5]
-  have h : g2 ∈ normalClosure {g2} :=
+  have h : g2 ∈ normal_closure {g2} :=
     SetLike.mem_coe.1 (subset_normal_closure (Set.mem_singleton _))
   exact mul_mem (subgroup.normal_closure_normal.conj_mem _ h g1) (inv_mem h)
 #align alternating_group.normal_closure_swap_mul_swap_five alternatingGroup.normalClosure_swap_mul_swap_five

Mathbin/GroupTheory/Subgroup/Basic.lean

@@ -2979,7 +2979,7 @@ instance normalClosure_normal : (normalClosure s).Normal :=
     by
     refine' Subgroup.closure_induction h (fun x hx => _) _ (fun x y ihx ihy => _) fun x ihx => _
     · exact conjugates_of_set_subset_normal_closure (conj_mem_conjugates_of_set hx)
-    · simpa using (normalClosure s).one_mem
+    · simpa using (normal_closure s).one_mem
     · rw [← conj_mul]
       exact mul_mem ihx ihy
     · rw [← conj_inv]

Mathbin/LinearAlgebra/Alternating.lean

@@ -875,12 +875,14 @@ theorem domDomCongr_add (σ : ι ≃ ι') (f g : AlternatingMap R M N ι) :
 #align alternating_map.dom_dom_congr_add AlternatingMap.domDomCongr_add
 -/
 
+#print AlternatingMap.domDomCongr_smul /-
 @[simp]
 theorem domDomCongr_smul {S : Type _} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N]
     (σ : ι ≃ ι') (c : S) (f : AlternatingMap R M N ι) :
     (c • f).domDomCongr σ = c • f.domDomCongr σ :=
   rfl
 #align alternating_map.dom_dom_congr_smul AlternatingMap.domDomCongr_smul
+-/
 
 #print AlternatingMap.domDomCongrEquiv /-
 /-- `alternating_map.dom_dom_congr` as an equivalence.
@@ -901,6 +903,7 @@ section DomDomLcongr
 
 variable (S : Type _) [Semiring S] [Module S N] [SMulCommClass R S N]
 
+#print AlternatingMap.domDomLcongr /-
 /-- `alternating_map.dom_dom_congr` as a linear equivalence. -/
 @[simps apply symm_apply]
 def domDomLcongr (σ : ι ≃ ι') : AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι'
@@ -912,20 +915,25 @@ def domDomLcongr (σ : ι ≃ ι') : AlternatingMap R M N ι ≃ₗ[S] Alternati
   map_add' := domDomCongr_add σ
   map_smul' := domDomCongr_smul σ
 #align alternating_map.dom_dom_lcongr AlternatingMap.domDomLcongr
+-/
 
+#print AlternatingMap.domDomLcongr_refl /-
 @[simp]
 theorem domDomLcongr_refl :
     (domDomLcongr S (Equiv.refl ι) : AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι) =
       LinearEquiv.refl _ _ :=
   LinearEquiv.ext domDomCongr_refl
 #align alternating_map.dom_dom_lcongr_refl AlternatingMap.domDomLcongr_refl
+-/
 
+#print AlternatingMap.domDomLcongr_toAddEquiv /-
 @[simp]
 theorem domDomLcongr_toAddEquiv (σ : ι ≃ ι') :
     (domDomLcongr S σ : AlternatingMap R M N ι ≃ₗ[S] AlternatingMap R M N ι').toAddEquiv =
       domDomCongrEquiv σ :=
   rfl
 #align alternating_map.dom_dom_lcongr_to_add_equiv AlternatingMap.domDomLcongr_toAddEquiv
+-/
 
 end DomDomLcongr
 

Mathbin/LinearAlgebra/Determinant.lean

@@ -741,10 +741,12 @@ theorem Basis.det_reindex {ι' : Type _} [Fintype ι'] [DecidableEq ι'] (b : Ba
 #align basis.det_reindex Basis.det_reindex
 -/
 
+#print Basis.det_reindex' /-
 theorem Basis.det_reindex' {ι' : Type _} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)
     (e : ι ≃ ι') : (b.reindex e).det = b.det.domDomCongr e :=
   AlternatingMap.ext fun _ => Basis.det_reindex _ _ _
 #align basis.det_reindex' Basis.det_reindex'
+-/
 
 #print Basis.det_reindex_symm /-
 theorem Basis.det_reindex_symm {ι' : Type _} [Fintype ι'] [DecidableEq ι'] (b : Basis ι R M)

Mathbin/LinearAlgebra/Orientation.lean

@@ -105,28 +105,36 @@ section Reindex
 
 variable (R M) {ι ι'}
 
+#print Orientation.reindex /-
 /-- An equivalence between indices implies an equivalence between orientations. -/
 def Orientation.reindex (e : ι ≃ ι') : Orientation R M ι ≃ Orientation R M ι' :=
   Module.Ray.map <| AlternatingMap.domDomLcongr R e
 #align orientation.reindex Orientation.reindex
+-/
 
+#print Orientation.reindex_apply /-
 @[simp]
 theorem Orientation.reindex_apply (e : ι ≃ ι') (v : AlternatingMap R M R ι) (hv : v ≠ 0) :
     Orientation.reindex R M e (rayOfNeZero _ v hv) =
       rayOfNeZero _ (v.domDomCongr e) (mt (v.domDomCongr_eq_zero_iff e).mp hv) :=
   rfl
 #align orientation.reindex_apply Orientation.reindex_apply
+-/
 
+#print Orientation.reindex_refl /-
 @[simp]
 theorem Orientation.reindex_refl : (Orientation.reindex R M <| Equiv.refl ι) = Equiv.refl _ := by
   rw [Orientation.reindex, AlternatingMap.domDomLcongr_refl, Module.Ray.map_refl]
 #align orientation.reindex_refl Orientation.reindex_refl
+-/
 
+#print Orientation.reindex_symm /-
 @[simp]
 theorem Orientation.reindex_symm (e : ι ≃ ι') :
     (Orientation.reindex R M e).symm = Orientation.reindex R M e.symm :=
   rfl
 #align orientation.reindex_symm Orientation.reindex_symm
+-/
 
 end Reindex
 
@@ -177,11 +185,13 @@ protected theorem Orientation.map_neg {ι : Type _} (f : M ≃ₗ[R] N) (x : Ori
 #align orientation.map_neg Orientation.map_neg
 -/
 
+#print Orientation.reindex_neg /-
 @[simp]
 protected theorem Orientation.reindex_neg {ι ι' : Type _} (e : ι ≃ ι') (x : Orientation R M ι) :
     Orientation.reindex R M e (-x) = -Orientation.reindex R M e x :=
   Module.Ray.map_neg _ x
 #align orientation.reindex_neg Orientation.reindex_neg
+-/
 
 namespace Basis
 
@@ -219,10 +229,12 @@ theorem orientation_map [Nontrivial R] (e : Basis ι R M) (f : M ≃ₗ[R] N) :
 #align basis.orientation_map Basis.orientation_map
 -/
 
+#print Basis.orientation_reindex /-
 theorem orientation_reindex [Nontrivial R] (e : Basis ι R M) (eι : ι ≃ ι') :
     (e.reindex eι).Orientation = Orientation.reindex R M eι e.Orientation := by
   simp_rw [Basis.orientation, Orientation.reindex_apply, Basis.det_reindex']
 #align basis.orientation_reindex Basis.orientation_reindex
+-/
 
 #print Basis.orientation_unitsSMul /-
 /-- The orientation given by a basis derived using `units_smul`, in terms of the product of those

Mathbin/LinearAlgebra/QuadraticForm/Dual.lean

@@ -32,6 +32,7 @@ section Semiring
 
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
+#print BilinForm.dualProd /-
 /-- The symmetric bilinear form on `module.dual R M × M` defined as
 `B (f, x) (g, y) = f y + g x`. -/
 @[simps]
@@ -42,16 +43,20 @@ def dualProd : BilinForm R (Module.Dual R M × M) :=
       ((LinearMap.applyₗ.comp (LinearMap.snd R (Module.Dual R M) M)).compl₂
           (LinearMap.fst R (Module.Dual R M) M)).flip
 #align bilin_form.dual_prod BilinForm.dualProd
+-/
 
+#print BilinForm.isSymm_dualProd /-
 theorem isSymm_dualProd : (dualProd R M).IsSymm := fun x y => add_comm _ _
 #align bilin_form.is_symm_dual_prod BilinForm.isSymm_dualProd
+-/
 
 end Semiring
 
 section Ring
 
 variable [CommRing R] [AddCommGroup M] [Module R M]
 
+#print BilinForm.nondenerate_dualProd /-
 theorem nondenerate_dualProd :
     (dualProd R M).Nondegenerate ↔ Function.Injective (Module.Dual.eval R M) := by
   classical
@@ -75,6 +80,7 @@ theorem nondenerate_dualProd :
   refine' prod.map_injective.trans _
   exact and_iff_right Function.injective_id
 #align bilin_form.nondenerate_dual_prod BilinForm.nondenerate_dualProd
+-/
 
 end Ring
 
@@ -86,6 +92,7 @@ section Semiring
 
 variable [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N]
 
+#print QuadraticForm.dualProd /-
 /-- The quadratic form on `module.dual R M × M` defined as `Q (f, x) = f x`. -/
 @[simps]
 def dualProd : QuadraticForm R (Module.Dual R M × M)
@@ -100,23 +107,29 @@ def dualProd : QuadraticForm R (Module.Dual R M × M)
         map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
         add_assoc]⟩
 #align quadratic_form.dual_prod QuadraticForm.dualProd
+-/
 
+#print BilinForm.dualProd.toQuadraticForm /-
 @[simp]
 theorem BilinForm.dualProd.toQuadraticForm :
     (BilinForm.dualProd R M).toQuadraticForm = 2 • dualProd R M :=
   ext fun a => (two_nsmul _).symm
 #align bilin_form.dual_prod.to_quadratic_form BilinForm.dualProd.toQuadraticForm
+-/
 
 variable {R M N}
 
+#print QuadraticForm.dualProdIsometry /-
 /-- Any module isomorphism induces a quadratic isomorphism between the corresponding `dual_prod.` -/
 @[simps]
 def dualProdIsometry (f : M ≃ₗ[R] N) : (dualProd R M).IsometryEquiv (dualProd R N)
     where
   toLinearEquiv := f.dualMap.symm.Prod f
   map_app' x := FunLike.congr_arg x.fst <| f.symm_apply_apply _
 #align quadratic_form.dual_prod_isometry QuadraticForm.dualProdIsometry
+-/
 
+#print QuadraticForm.dualProdProdIsometry /-
 /-- `quadratic_form.dual_prod` commutes (isometrically) with `quadratic_form.prod`. -/
 @[simps]
 def dualProdProdIsometry : (dualProd R (M × N)).IsometryEquiv ((dualProd R M).Prod (dualProd R N))
@@ -127,6 +140,7 @@ def dualProdProdIsometry : (dualProd R (M × N)).IsometryEquiv ((dualProd R M).P
   map_app' m :=
     (m.fst.map_add _ _).symm.trans <| FunLike.congr_arg m.fst <| Prod.ext (add_zero _) (zero_add _)
 #align quadratic_form.dual_prod_prod_isometry QuadraticForm.dualProdProdIsometry
+-/
 
 end Semiring
 
@@ -136,6 +150,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M]
 
 variable {R M}
 
+#print QuadraticForm.toDualProd /-
 /-- The isometry sending `(Q.prod $ -Q)` to `(quadratic_form.dual_prod R M)`.
 
 This is `σ` from Proposition 4.8, page 84 of
@@ -147,7 +162,9 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : M × M →ₗ[R] M
     (Q.Associated.toLin.comp (LinearMap.fst _ _ _) + Q.Associated.toLin.comp (LinearMap.snd _ _ _))
     (LinearMap.fst _ _ _ - LinearMap.snd _ _ _)
 #align quadratic_form.to_dual_prod QuadraticForm.toDualProd
+-/
 
+#print QuadraticForm.toDualProd_isometry /-
 theorem toDualProd_isometry [Invertible (2 : R)] (Q : QuadraticForm R M) (x : M × M) :
     QuadraticForm.dualProd R M (toDualProd Q x) = (Q.Prod <| -Q) x :=
   by
@@ -156,6 +173,7 @@ theorem toDualProd_isometry [Invertible (2 : R)] (Q : QuadraticForm R M) (x : M
   simp [polar_comm _ x.1 x.2, ← sub_add, mul_sub, sub_mul, smul_sub, Submonoid.smul_def, ←
     sub_eq_add_neg (Q x.1) (Q x.2)]
 #align quadratic_form.to_dual_prod_isometry QuadraticForm.toDualProd_isometry
+-/
 
 -- TODO: show that `to_dual_prod` is an equivalence
 end Ring

Mathbin/Logic/Equiv/Array.lean

@@ -54,17 +54,13 @@ instance : LawfulTraversable (Array' n) :=
 
 end Array'
 
-#print Array.encodable /-
 /-- If `α` is encodable, then so is `array n α`. -/
-instance Array.encodable {α} [Encodable α] {n} : Encodable (Array' n α) :=
+instance Array'.encodable {α} [Encodable α] {n} : Encodable (Array' n α) :=
   Encodable.ofEquiv _ (Equiv.arrayEquivFin _ _)
-#align array.encodable Array.encodable
--/
+#align array.encodable Array'.encodable
 
-#print Array.countable /-
 /-- If `α` is countable, then so is `array n α`. -/
-instance Array.countable {α} [Countable α] {n} : Countable (Array' n α) :=
+instance Array'.countable {α} [Countable α] {n} : Countable (Array' n α) :=
   Countable.of_equiv _ (Equiv.vectorEquivArray _ _)
-#align array.countable Array.countable
--/
+#align array.countable Array'.countable