bump to nightly-2023-08-21-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Algebra/Ring/Equiv.lean

@@ -1047,7 +1047,6 @@ theorem symm_trans_self (e : R ≃+* S) : e.symm.trans e = RingEquiv.refl S :=
 #align ring_equiv.symm_trans_self RingEquiv.symm_trans_self
 -/
 
-#print RingEquiv.noZeroDivisors /-
 /-- If two rings are isomorphic, and the second doesn't have zero divisors,
 then so does the first. -/
 protected theorem noZeroDivisors {A : Type _} (B : Type _) [Ring A] [Ring B] [NoZeroDivisors B]
@@ -1058,9 +1057,7 @@ protected theorem noZeroDivisors {A : Type _} (B : Type _) [Ring A] [Ring B] [No
       have : e x * e y = 0 := by rw [← e.map_mul, hxy, e.map_zero]
       simpa using eq_zero_or_eq_zero_of_mul_eq_zero this }
 #align ring_equiv.no_zero_divisors RingEquiv.noZeroDivisors
--/
 
-#print RingEquiv.isDomain /-
 /-- If two rings are isomorphic, and the second is a domain, then so is the first. -/
 protected theorem isDomain {A : Type _} (B : Type _) [Ring A] [Ring B] [IsDomain B] (e : A ≃+* B) :
     IsDomain A :=
@@ -1069,7 +1066,6 @@ protected theorem isDomain {A : Type _} (B : Type _) [Ring A] [Ring B] [IsDomain
   haveI := e.no_zero_divisors B
   exact NoZeroDivisors.to_isDomain _
 #align ring_equiv.is_domain RingEquiv.isDomain
--/
 
 end RingEquiv
 

Mathbin/Analysis/NormedSpace/OperatorNorm.lean

@@ -1362,7 +1362,6 @@ section Unital
 
 variable (𝕜) (𝕜' : Type _) [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜']
 
-#print ContinuousLinearMap.mulₗᵢ /-
 /-- Multiplication in a normed algebra as a linear isometry to the space of
 continuous linear maps. -/
 def mulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' where
@@ -1372,22 +1371,17 @@ def mulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' where
       (by
         convert ratio_le_op_norm _ (1 : 𝕜'); simp [norm_one]
         infer_instance)
-#align continuous_linear_map.mulₗᵢ ContinuousLinearMap.mulₗᵢ
--/
+#align continuous_linear_map.mulₗᵢ ContinuousLinearMap.mulₗᵢₓ
 
-#print ContinuousLinearMap.coe_mulₗᵢ /-
 @[simp]
 theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 𝕜') = mul 𝕜 𝕜' :=
   rfl
-#align continuous_linear_map.coe_mulₗᵢ ContinuousLinearMap.coe_mulₗᵢ
--/
+#align continuous_linear_map.coe_mulₗᵢ ContinuousLinearMap.coe_mulₗᵢₓ
 
-#print ContinuousLinearMap.op_norm_mul_apply /-
 @[simp]
 theorem op_norm_mul_apply (x : 𝕜') : ‖mul 𝕜 𝕜' x‖ = ‖x‖ :=
   (mulₗᵢ 𝕜 𝕜').norm_map x
-#align continuous_linear_map.op_norm_mul_apply ContinuousLinearMap.op_norm_mul_apply
--/
+#align continuous_linear_map.op_norm_mul_apply ContinuousLinearMap.op_norm_mul_applyₓ
 
 end Unital
 
@@ -2203,13 +2197,11 @@ section
 
 variable [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜']
 
-#print ContinuousLinearMap.op_norm_mul /-
 @[simp]
 theorem op_norm_mul [NormOneClass 𝕜'] : ‖mul 𝕜 𝕜'‖ = 1 :=
   haveI := NormOneClass.nontrivial 𝕜'
   (mulₗᵢ 𝕜 𝕜').norm_toContinuousLinearMap
-#align continuous_linear_map.op_norm_mul ContinuousLinearMap.op_norm_mul
--/
+#align continuous_linear_map.op_norm_mul ContinuousLinearMap.op_norm_mulₓ
 
 end
 

Mathbin/Data/Pi/Lex.lean

@@ -255,15 +255,13 @@ instance Lex.orderedCommGroup [LinearOrder ι] [∀ a, OrderedCommGroup (β a)]
 #align pi.lex.ordered_add_comm_group Pi.Lex.orderedAddCommGroup
 -/
 
-#print Pi.lex_desc /-
 /-- If we swap two strictly decreasing values in a function, then the result is lexicographically
 smaller than the original function. -/
 theorem lex_desc {α} [Preorder ι] [DecidableEq ι] [Preorder α] {f : ι → α} {i j : ι} (h₁ : i < j)
     (h₂ : f j < f i) : toLex (f ∘ Equiv.swap i j) < toLex f :=
   ⟨i, fun k hik => congr_arg f (Equiv.swap_apply_of_ne_of_ne hik.Ne (hik.trans h₁).Ne), by
     simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂⟩
-#align pi.lex_desc Pi.lex_desc
--/
+#align pi.lex_desc Pi.lex_descₓ
 
 end Pi
 

Mathbin/Data/Sum/Basic.lean

@@ -80,22 +80,22 @@ theorem inr_injective : Function.Injective (inr : β → Sum α β) := fun x y =
 
 section get
 
-#print Sum.getLeft /-
+#print Sum.getLeft? /-
 /-- Check if a sum is `inl` and if so, retrieve its contents. -/
 @[simp]
-def getLeft : Sum α β → Option α
+def getLeft? : Sum α β → Option α
   | inl a => some a
   | inr _ => none
-#align sum.get_left Sum.getLeft
+#align sum.get_left Sum.getLeft?
 -/
 
-#print Sum.getRight /-
+#print Sum.getRight? /-
 /-- Check if a sum is `inr` and if so, retrieve its contents. -/
 @[simp]
-def getRight : Sum α β → Option β
+def getRight? : Sum α β → Option β
   | inr b => some b
   | inl _ => none
-#align sum.get_right Sum.getRight
+#align sum.get_right Sum.getRight?
 -/
 
 #print Sum.isLeft /-
@@ -118,34 +118,34 @@ def isRight : Sum α β → Bool
 
 variable {x y : Sum α β}
 
-#print Sum.getLeft_eq_none_iff /-
+#print Sum.getLeft?_eq_none_iff /-
 @[simp]
-theorem getLeft_eq_none_iff : x.getLeft = none ↔ x.isRight := by
+theorem getLeft?_eq_none_iff : x.getLeft? = none ↔ x.isRight := by
   cases x <;>
     simp only [get_left, is_right, Bool.coe_sort_true, Bool.coe_sort_false, eq_self_iff_true]
-#align sum.get_left_eq_none_iff Sum.getLeft_eq_none_iff
+#align sum.get_left_eq_none_iff Sum.getLeft?_eq_none_iff
 -/
 
-#print Sum.getRight_eq_none_iff /-
+#print Sum.getRight?_eq_none_iff /-
 @[simp]
-theorem getRight_eq_none_iff : x.getRight = none ↔ x.isLeft := by
+theorem getRight?_eq_none_iff : x.getRight? = none ↔ x.isLeft := by
   cases x <;>
     simp only [get_right, is_left, Bool.coe_sort_true, Bool.coe_sort_false, eq_self_iff_true]
-#align sum.get_right_eq_none_iff Sum.getRight_eq_none_iff
+#align sum.get_right_eq_none_iff Sum.getRight?_eq_none_iff
 -/
 
-#print Sum.getLeft_eq_some_iff /-
+#print Sum.getLeft?_eq_some_iff /-
 @[simp]
-theorem getLeft_eq_some_iff {a} : x.getLeft = some a ↔ x = inl a := by
+theorem getLeft?_eq_some_iff {a} : x.getLeft? = some a ↔ x = inl a := by
   cases x <;> simp only [get_left]
-#align sum.get_left_eq_some_iff Sum.getLeft_eq_some_iff
+#align sum.get_left_eq_some_iff Sum.getLeft?_eq_some_iff
 -/
 
-#print Sum.getRight_eq_some_iff /-
+#print Sum.getRight?_eq_some_iff /-
 @[simp]
-theorem getRight_eq_some_iff {b} : x.getRight = some b ↔ x = inr b := by
+theorem getRight?_eq_some_iff {b} : x.getRight? = some b ↔ x = inr b := by
   cases x <;> simp only [get_right]
-#align sum.get_right_eq_some_iff Sum.getRight_eq_some_iff
+#align sum.get_right_eq_some_iff Sum.getRight?_eq_some_iff
 -/
 
 #print Sum.not_isLeft /-
@@ -346,18 +346,18 @@ theorem isRight_map (f : α → β) (g : γ → δ) (x : Sum α γ) : isRight (x
 #align sum.is_right_map Sum.isRight_map
 -/
 
-#print Sum.getLeft_map /-
+#print Sum.getLeft?_map /-
 @[simp]
-theorem getLeft_map (f : α → β) (g : γ → δ) (x : Sum α γ) : (x.map f g).getLeft = x.getLeft.map f :=
-  by cases x <;> rfl
-#align sum.get_left_map Sum.getLeft_map
+theorem getLeft?_map (f : α → β) (g : γ → δ) (x : Sum α γ) :
+    (x.map f g).getLeft? = x.getLeft?.map f := by cases x <;> rfl
+#align sum.get_left_map Sum.getLeft?_map
 -/
 
-#print Sum.getRight_map /-
+#print Sum.getRight?_map /-
 @[simp]
-theorem getRight_map (f : α → β) (g : γ → δ) (x : Sum α γ) :
-    (x.map f g).getRight = x.getRight.map g := by cases x <;> rfl
-#align sum.get_right_map Sum.getRight_map
+theorem getRight?_map (f : α → β) (g : γ → δ) (x : Sum α γ) :
+    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
+#align sum.get_right_map Sum.getRight?_map
 -/
 
 open Function (update update_eq_iff update_comp_eq_of_injective update_comp_eq_of_forall_ne)
@@ -500,16 +500,16 @@ theorem isRight_swap (x : Sum α β) : x.symm.isRight = x.isLeft := by cases x <
 #align sum.is_right_swap Sum.isRight_swap
 -/
 
-#print Sum.getLeft_swap /-
+#print Sum.getLeft?_swap /-
 @[simp]
-theorem getLeft_swap (x : Sum α β) : x.symm.getLeft = x.getRight := by cases x <;> rfl
-#align sum.get_left_swap Sum.getLeft_swap
+theorem getLeft?_swap (x : Sum α β) : x.symm.getLeft? = x.getRight? := by cases x <;> rfl
+#align sum.get_left_swap Sum.getLeft?_swap
 -/
 
-#print Sum.getRight_swap /-
+#print Sum.getRight?_swap /-
 @[simp]
-theorem getRight_swap (x : Sum α β) : x.symm.getRight = x.getLeft := by cases x <;> rfl
-#align sum.get_right_swap Sum.getRight_swap
+theorem getRight?_swap (x : Sum α β) : x.symm.getRight? = x.getLeft? := by cases x <;> rfl
+#align sum.get_right_swap Sum.getRight?_swap
 -/
 
 section LiftRel

Mathbin/LinearAlgebra/Finrank.lean

@@ -91,15 +91,15 @@ theorem finrank_lt_of_rank_lt {n : ℕ} (h : Module.rank K V < ↑n) : finrank K
 #align finite_dimensional.finrank_lt_of_rank_lt FiniteDimensional.finrank_lt_of_rank_lt
 -/
 
-#print FiniteDimensional.rank_lt_of_finrank_lt /-
-theorem rank_lt_of_finrank_lt {n : ℕ} (h : n < finrank K V) : ↑n < Module.rank K V :=
+#print FiniteDimensional.lt_rank_of_lt_finrank /-
+theorem lt_rank_of_lt_finrank {n : ℕ} (h : n < finrank K V) : ↑n < Module.rank K V :=
   by
   rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, to_nat_cast]
   · exact nat_lt_aleph_0 n
   · contrapose! h
     rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
     exact n.zero_le
-#align finite_dimensional.rank_lt_of_finrank_lt FiniteDimensional.rank_lt_of_finrank_lt
+#align finite_dimensional.rank_lt_of_finrank_lt FiniteDimensional.lt_rank_of_lt_finrank
 -/
 
 #print FiniteDimensional.finrank_le_finrank_of_rank_le_rank /-
@@ -117,7 +117,7 @@ variable [Nontrivial K] [NoZeroSMulDivisors K V]
 #print FiniteDimensional.nontrivial_of_finrank_pos /-
 /-- A finite dimensional space is nontrivial if it has positive `finrank`. -/
 theorem nontrivial_of_finrank_pos (h : 0 < finrank K V) : Nontrivial V :=
-  rank_pos_iff_nontrivial.mp (rank_lt_of_finrank_lt h)
+  rank_pos_iff_nontrivial.mp (lt_rank_of_lt_finrank h)
 #align finite_dimensional.nontrivial_of_finrank_pos FiniteDimensional.nontrivial_of_finrank_pos
 -/
 

Mathbin/ModelTheory/Encoding.lean

@@ -264,7 +264,7 @@ def listDecode :
       simp only [List.sizeof, ← add_assoc]
       exact le_max_of_le_right le_add_self⟩
   | Sum.inr (Sum.inl ⟨n, R⟩)::Sum.inr (Sum.inr k)::l =>
-    ⟨if h : ∀ i : Fin n, ((l.map Sum.getLeft).get? i).join.isSome then
+    ⟨if h : ∀ i : Fin n, ((l.map Sum.getLeft?).get? i).join.isSome then
         if h' : ∀ i, (Option.get (h i)).1 = k then
           ⟨k, BoundedFormula.rel R fun i => Eq.mp (by rw [h' i]) (Option.get (h i)).2⟩
         else default
@@ -314,7 +314,7 @@ theorem listDecode_encode_list (l : List (Σ n, L.BoundedFormula α n)) :
     · rw [list_encode, cons_append, cons_append, singleton_append, cons_append, list_decode]
       · have h :
           ∀ i : Fin φ_l,
-            ((List.map Sum.getLeft
+            ((List.map Sum.getLeft?
                       (List.map
                           (fun i : Fin φ_l =>
                             Sum.inl
@@ -331,7 +331,7 @@ theorem listDecode_encode_list (l : List (Σ n, L.BoundedFormula α n)) :
           refine' ⟨lt_of_lt_of_le i.2 le_self_add, _⟩
           rw [nth_le_append, nth_le_map]
           ·
-            simp only [Sum.getLeft, nth_le_fin_range, Fin.eta, Function.comp_apply,
+            simp only [Sum.getLeft?, nth_le_fin_range, Fin.eta, Function.comp_apply,
               eq_self_iff_true, heq_iff_eq, and_self_iff]
           · exact lt_of_lt_of_le i.is_lt (ge_of_eq (length_fin_range _))
           · rw [length_map, length_fin_range]

Mathbin/NumberTheory/NumberField/CanonicalEmbedding.lean

@@ -45,28 +45,24 @@ scoped[CanonicalEmbedding]
   notation "E" =>
     ({ w : InfinitePlace K // IsReal w } → ℝ) × ({ w : InfinitePlace K // IsComplex w } → ℂ)
 
-#print NumberField.canonicalEmbedding.space_rank /-
 theorem space_rank [NumberField K] : finrank ℝ E = finrank ℚ K :=
   by
   haveI : Module.Free ℝ ℂ := inferInstance
   rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const,
     Finset.card_univ, ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm, ←
     card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
     Nat.add_sub_of_le (Fintype.card_subtype_le _)]
-#align number_field.canonical_embedding.space_rank NumberField.canonicalEmbedding.space_rank
--/
+#align number_field.canonical_embedding.space_rank NumberField.CanonicalEmbedding.space_rank
 
-#print NumberField.canonicalEmbedding.nontrivial_space /-
-theorem nontrivial_space [NumberField K] : Nontrivial E :=
+theorem non_trivial_space [NumberField K] : Nontrivial E :=
   by
   obtain ⟨w⟩ := infinite_place.nonempty K
   obtain hw | hw := w.is_real_or_is_complex
   · haveI : Nonempty { w : infinite_place K // is_real w } := ⟨⟨w, hw⟩⟩
     exact nontrivial_prod_left
   · haveI : Nonempty { w : infinite_place K // is_complex w } := ⟨⟨w, hw⟩⟩
     exact nontrivial_prod_right
-#align number_field.canonical_embedding.non_trivial_space NumberField.canonicalEmbedding.nontrivial_space
--/
+#align number_field.canonical_embedding.non_trivial_space NumberField.CanonicalEmbedding.non_trivial_space
 
 #print NumberField.canonicalEmbedding /-
 /-- The canonical embedding of a number field `K` of signature `(r₁, r₂)` into `ℝ^r₁ × ℂ^r₂`. -/
@@ -78,29 +74,25 @@ def NumberField.canonicalEmbedding : K →+* E :=
 #print NumberField.canonicalEmbedding_injective /-
 theorem NumberField.canonicalEmbedding_injective [NumberField K] :
     Injective (NumberField.canonicalEmbedding K) :=
-  @RingHom.injective _ _ _ _ (nontrivial_space K) _
+  @RingHom.injective _ _ _ _ (non_trivial_space K) _
 #align number_field.canonical_embedding_injective NumberField.canonicalEmbedding_injective
 -/
 
 open NumberField
 
 variable {K}
 
-#print NumberField.canonicalEmbedding.apply_at_real_infinitePlace /-
 @[simp]
 theorem apply_at_real_infinitePlace (w : { w : InfinitePlace K // IsReal w }) (x : K) :
     (NumberField.canonicalEmbedding K x).1 w = w.Prop.Embedding x := by
   simp only [canonical_embedding, RingHom.prod_apply, Pi.ringHom_apply]
 #align number_field.canonical_embedding.apply_at_real_infinite_place NumberField.canonicalEmbedding.apply_at_real_infinitePlace
--/
 
-#print NumberField.canonicalEmbedding.apply_at_complex_infinitePlace /-
 @[simp]
 theorem apply_at_complex_infinitePlace (w : { w : InfinitePlace K // IsComplex w }) (x : K) :
     (NumberField.canonicalEmbedding K x).2 w = Embedding w.val x := by
   simp only [canonical_embedding, RingHom.prod_apply, Pi.ringHom_apply]
 #align number_field.canonical_embedding.apply_at_complex_infinite_place NumberField.canonicalEmbedding.apply_at_complex_infinitePlace
--/
 
 #print NumberField.canonicalEmbedding.nnnorm_eq /-
 theorem nnnorm_eq [NumberField K] (x : K) :
@@ -157,7 +149,6 @@ def integerLattice : Subring E :=
 #align number_field.canonical_embedding.integer_lattice NumberField.canonicalEmbedding.integerLattice
 -/
 
-#print NumberField.canonicalEmbedding.equivIntegerLattice /-
 /-- The linear equiv between `𝓞 K` and the integer lattice. -/
 def equivIntegerLattice [NumberField K] : 𝓞 K ≃ₗ[ℤ] integerLattice K :=
   LinearEquiv.ofBijective
@@ -171,7 +162,6 @@ def equivIntegerLattice [NumberField K] : 𝓞 K ≃ₗ[ℤ] integerLattice K :=
       rw [LinearMap.coe_mk, Subtype.mk_eq_mk] at h 
       exact IsFractionRing.injective (𝓞 K) K (canonical_embedding_injective K h))
 #align number_field.canonical_embedding.equiv_integer_lattice NumberField.canonicalEmbedding.equivIntegerLattice
--/
 
 #print NumberField.canonicalEmbedding.integerLattice.inter_ball_finite /-
 theorem integerLattice.inter_ball_finite [NumberField K] (r : ℝ) :

Mathbin/Tactic/FreshNames.lean

@@ -139,7 +139,7 @@ unsafe def rename_fresh (renames : name_map (Sum Name (List Name))) (reserved :
       match renames.find h.local_uniq_name with
       | none => Sum.inl h.local_pp_name
       | some new_names => new_names
-  let reserved := reserved.insert_list <| renames.filterMap Sum.getLeft
+  let reserved := reserved.insert_list <| renames.filterMap Sum.getLeft?
   let new_hyps ← intro_lst_fresh_reserved renames reserved
   pure <| reverted new_hyps
 #align tactic.rename_fresh tactic.rename_fresh