bump to nightly-2023-04-10-18

mathlib commit leanprover-community/mathlib@e05ead7

Mathbin/Algebra/Category/Module/Projective.lean

@@ -37,7 +37,7 @@ theorem IsProjective.iff_projective {R : Type u} [Ring R] {P : Type max u v} [Ad
     exact
       ⟨fun E X f e epi =>
         Module.projective_lifting_property _ _ ((ModuleCat.epi_iff_surjective _).mp epi)⟩
-  · refine' Module.projectiveOfLiftingProperty _
+  · refine' Module.Projective.of_lifting_property _
     intro E X mE mX sE sX f g s
     haveI : epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
     letI : projective (ModuleCat.of R P) := h
@@ -52,7 +52,7 @@ variable {R : Type u} [Ring R] {M : ModuleCat.{max u v} R}
 /-- Modules that have a basis are projective. -/
 theorem projective_of_free {ι : Type _} (b : Basis ι R M) : Projective M :=
   Projective.of_iso (ModuleCat.ofSelfIso _)
-    (IsProjective.iff_projective.mp (Module.projectiveOfBasis b))
+    (IsProjective.iff_projective.mp (Module.Projective.of_basis b))
 #align Module.projective_of_free ModuleCat.projective_of_free
 
 /-- The category of modules has enough projectives, since every module is a quotient of a free

Mathbin/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean

@@ -62,7 +62,7 @@ def SimpleContinuedFraction.of : SimpleContinuedFraction K :=
 
 theorem SimpleContinuedFraction.of_isContinuedFraction :
     (SimpleContinuedFraction.of v).IsContinuedFraction := fun _ denom nth_part_denom_eq =>
-  lt_of_lt_of_le zero_lt_one (of_one_le_nth_part_denom nth_part_denom_eq)
+  lt_of_lt_of_le zero_lt_one (of_one_le_get?_part_denom nth_part_denom_eq)
 #align simple_continued_fraction.of_is_continued_fraction SimpleContinuedFraction.of_isContinuedFraction
 
 /-- Creates the continued fraction of a value. -/

Mathbin/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -146,7 +146,7 @@ fraction `generalized_continued_fraction.of`.
 
 
 /-- Shows that the integer parts of the continued fraction are at least one. -/
-theorem of_one_le_nth_part_denom {b : K}
+theorem of_one_le_get?_part_denom {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) : 1 ≤ b :=
   by
   obtain ⟨gp_n, nth_s_eq, ⟨-⟩⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b;
@@ -156,7 +156,7 @@ theorem of_one_le_nth_part_denom {b : K}
   exact int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some nth_s_eq
   rw [← ifp_n_b_eq_gp_n_b]
   exact_mod_cast int_fract_pair.one_le_succ_nth_stream_b succ_nth_stream_eq
-#align generalized_continued_fraction.of_one_le_nth_part_denom GeneralizedContinuedFraction.of_one_le_nth_part_denom
+#align generalized_continued_fraction.of_one_le_nth_part_denom GeneralizedContinuedFraction.of_one_le_get?_part_denom
 
 /--
 Shows that the partial numerators `aᵢ` of the continued fraction are equal to one and the partial
@@ -299,25 +299,25 @@ theorem zero_le_of_denom : 0 ≤ (of v).denominators n :=
   exact zero_le_of_continuants_aux_b
 #align generalized_continued_fraction.zero_le_of_denom GeneralizedContinuedFraction.zero_le_of_denom
 
-theorem le_of_succ_succ_nth_continuantsAux_b {b : K}
+theorem le_of_succ_succ_get?_continuantsAux_b {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) :
     b * ((of v).continuantsAux <| n + 1).b ≤ ((of v).continuantsAux <| n + 2).b :=
   by
   obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b
   exact exists_s_b_of_part_denom nth_part_denom_eq
   simp [of_part_num_eq_one (part_num_eq_s_a nth_s_eq), zero_le_of_continuants_aux_b,
     GeneralizedContinuedFraction.continuantsAux_recurrence nth_s_eq rfl rfl]
-#align generalized_continued_fraction.le_of_succ_succ_nth_continuants_aux_b GeneralizedContinuedFraction.le_of_succ_succ_nth_continuantsAux_b
+#align generalized_continued_fraction.le_of_succ_succ_nth_continuants_aux_b GeneralizedContinuedFraction.le_of_succ_succ_get?_continuantsAux_b
 
 /-- Shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is the `n`th partial denominator and `Bₙ₊₁` and `Bₙ` are
 the `n + 1`th and `n`th denominator of the continued fraction. -/
-theorem le_of_succ_nth_denom {b : K}
+theorem le_of_succ_get?_denom {b : K}
     (nth_part_denom_eq : (of v).partialDenominators.get? n = some b) :
     b * (of v).denominators n ≤ (of v).denominators (n + 1) :=
   by
   rw [denom_eq_conts_b, nth_cont_eq_succ_nth_cont_aux]
   exact le_of_succ_succ_nth_continuants_aux_b nth_part_denom_eq
-#align generalized_continued_fraction.le_of_succ_nth_denom GeneralizedContinuedFraction.le_of_succ_nth_denom
+#align generalized_continued_fraction.le_of_succ_nth_denom GeneralizedContinuedFraction.le_of_succ_get?_denom
 
 /-- Shows that the sequence of denominators is monotone, that is `Bₙ ≤ Bₙ₊₁`. -/
 theorem of_denom_mono : (of v).denominators n ≤ (of v).denominators (n + 1) :=

Mathbin/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

@@ -225,15 +225,15 @@ theorem coe_of_h_rat_eq : (↑((of q).h : ℚ) : K) = (of v).h :=
   simp
 #align generalized_continued_fraction.coe_of_h_rat_eq GeneralizedContinuedFraction.coe_of_h_rat_eq
 
-theorem coe_of_s_nth_rat_eq :
+theorem coe_of_s_get?_rat_eq :
     (((of q).s.get? n).map (Pair.map coe) : Option <| Pair K) = (of v).s.get? n :=
   by
   simp only [of, int_fract_pair.seq1, seq.map_nth, seq.nth_tail]
   simp only [seq.nth]
   rw [← int_fract_pair.coe_stream_rat_eq v_eq_q]
   rcases succ_nth_stream_eq : int_fract_pair.stream q (n + 1) with (_ | ⟨_, _⟩) <;>
     simp [Stream'.map, Stream'.nth, succ_nth_stream_eq]
-#align generalized_continued_fraction.coe_of_s_nth_rat_eq GeneralizedContinuedFraction.coe_of_s_nth_rat_eq
+#align generalized_continued_fraction.coe_of_s_nth_rat_eq GeneralizedContinuedFraction.coe_of_s_get?_rat_eq
 
 theorem coe_of_s_rat_eq : ((of q).s.map (Pair.map coe) : Seq <| Pair K) = (of v).s :=
   by

Mathbin/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -197,10 +197,10 @@ sequence implies the termination of another sequence.
 
 variable {n : ℕ}
 
-theorem IntFractPair.nth_seq1_eq_succ_nth_stream :
+theorem IntFractPair.get?_seq1_eq_succ_get?_stream :
     (IntFractPair.seq1 v).snd.get? n = (IntFractPair.stream v) (n + 1) :=
   rfl
-#align generalized_continued_fraction.int_fract_pair.nth_seq1_eq_succ_nth_stream GeneralizedContinuedFraction.IntFractPair.nth_seq1_eq_succ_nth_stream
+#align generalized_continued_fraction.int_fract_pair.nth_seq1_eq_succ_nth_stream GeneralizedContinuedFraction.IntFractPair.get?_seq1_eq_succ_get?_stream
 
 section Termination
 
@@ -233,7 +233,7 @@ Now let's show how the values of the sequences correspond to one another.
 -/
 
 
-theorem IntFractPair.exists_succ_nth_stream_of_gcf_of_nth_eq_some {gp_n : Pair K}
+theorem IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some {gp_n : Pair K}
     (s_nth_eq : (of v).s.get? n = some gp_n) :
     ∃ ifp : IntFractPair K, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
   by
@@ -246,32 +246,32 @@ theorem IntFractPair.exists_succ_nth_stream_of_gcf_of_nth_eq_some {gp_n : Pair K
   injection gp_n_eq with _ ifp_b_eq_gp_n_b
   exists ifp
   exact ⟨stream_succ_nth_eq, ifp_b_eq_gp_n_b⟩
-#align generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some GeneralizedContinuedFraction.IntFractPair.exists_succ_nth_stream_of_gcf_of_nth_eq_some
+#align generalized_continued_fraction.int_fract_pair.exists_succ_nth_stream_of_gcf_of_nth_eq_some GeneralizedContinuedFraction.IntFractPair.exists_succ_get?_stream_of_gcf_of_get?_eq_some
 
 /-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
 integer parts of the stream of integer and fractional parts.
 -/
-theorem nth_of_eq_some_of_succ_nth_intFractPair_stream {ifp_succ_n : IntFractPair K}
+theorem get?_of_eq_some_of_succ_get?_intFractPair_stream {ifp_succ_n : IntFractPair K}
     (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) :
     (of v).s.get? n = some ⟨1, ifp_succ_n.b⟩ :=
   by
   unfold of int_fract_pair.seq1
   rw [seq.map_tail, seq.nth_tail, seq.map_nth]
   simp [seq.nth, stream_succ_nth_eq]
-#align generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream GeneralizedContinuedFraction.nth_of_eq_some_of_succ_nth_intFractPair_stream
+#align generalized_continued_fraction.nth_of_eq_some_of_succ_nth_int_fract_pair_stream GeneralizedContinuedFraction.get?_of_eq_some_of_succ_get?_intFractPair_stream
 
 /-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
 fractional parts of the stream of integer and fractional parts.
 -/
-theorem nth_of_eq_some_of_nth_intFractPair_stream_fr_ne_zero {ifp_n : IntFractPair K}
+theorem get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero {ifp_n : IntFractPair K}
     (stream_nth_eq : IntFractPair.stream v n = some ifp_n) (nth_fr_ne_zero : ifp_n.fr ≠ 0) :
     (of v).s.get? n = some ⟨1, (IntFractPair.of ifp_n.fr⁻¹).b⟩ :=
   have : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹) :=
     by
     cases ifp_n
     simp [int_fract_pair.stream, stream_nth_eq, nth_fr_ne_zero]
-  nth_of_eq_some_of_succ_nth_intFractPair_stream this
-#align generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero GeneralizedContinuedFraction.nth_of_eq_some_of_nth_intFractPair_stream_fr_ne_zero
+  get?_of_eq_some_of_succ_get?_intFractPair_stream this
+#align generalized_continued_fraction.nth_of_eq_some_of_nth_int_fract_pair_stream_fr_ne_zero GeneralizedContinuedFraction.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero
 
 open Int IntFractPair
 
@@ -337,7 +337,7 @@ an element `v` of `K` as the coefficient sequence of that of the inverse of the
 fractional part of `v`.
 -/
 theorem of_s_tail : (of v).s.tail = (of (fract v)⁻¹).s :=
-  Seq.ext fun n => Seq.nth_tail (of v).s n ▸ of_s_succ v n
+  Seq.ext fun n => Seq.get?_tail (of v).s n ▸ of_s_succ v n
 #align generalized_continued_fraction.of_s_tail GeneralizedContinuedFraction.of_s_tail
 
 variable (K) (n)

Mathbin/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -117,14 +117,14 @@ theorem squashSeq_eq_self_of_terminated (terminated_at_succ_n : s.TerminatedAt (
 
 /-- If the sequence has not terminated before position `n + 1`, the value at `n + 1` gets
 squashed into position `n`. -/
-theorem squashSeq_nth_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s.get? n = some gp_n)
+theorem squashSeq_get?_of_not_terminated {gp_n gp_succ_n : Pair K} (s_nth_eq : s.get? n = some gp_n)
     (s_succ_nth_eq : s.get? (n + 1) = some gp_succ_n) :
     (squashSeq s n).get? n = some ⟨gp_n.a, gp_n.b + gp_succ_n.a / gp_succ_n.b⟩ := by
   simp [*, squash_seq]
-#align generalized_continued_fraction.squash_seq_nth_of_not_terminated GeneralizedContinuedFraction.squashSeq_nth_of_not_terminated
+#align generalized_continued_fraction.squash_seq_nth_of_not_terminated GeneralizedContinuedFraction.squashSeq_get?_of_not_terminated
 
 /-- The values before the squashed position stay the same. -/
-theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m :=
+theorem squashSeq_get?_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m :=
   by
   cases s_succ_nth_eq : s.nth (n + 1)
   case none => rw [squash_seq_eq_self_of_terminated s_succ_nth_eq]
@@ -133,7 +133,7 @@ theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m
     obtain ⟨gp_m, s_mth_eq⟩ : ∃ gp_m, s.nth m = some gp_m;
     exact s.ge_stable (le_of_lt m_lt_n) s_nth_eq
     simp [*, squash_seq, m_lt_n.ne]
-#align generalized_continued_fraction.squash_seq_nth_of_lt GeneralizedContinuedFraction.squashSeq_nth_of_lt
+#align generalized_continued_fraction.squash_seq_nth_of_lt GeneralizedContinuedFraction.squashSeq_get?_of_lt
 
 /-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the
 sequence at position `n`. -/
@@ -225,10 +225,10 @@ theorem squashGcf_eq_self_of_terminated (terminated_at_n : TerminatedAt g n) : s
 #align generalized_continued_fraction.squash_gcf_eq_self_of_terminated GeneralizedContinuedFraction.squashGcf_eq_self_of_terminated
 
 /-- The values before the squashed position stay the same. -/
-theorem squashGcf_nth_of_lt {m : ℕ} (m_lt_n : m < n) :
+theorem squashGcf_get?_of_lt {m : ℕ} (m_lt_n : m < n) :
     (squashGcf g (n + 1)).s.get? m = g.s.get? m := by
   simp only [squash_gcf, squash_seq_nth_of_lt m_lt_n]
-#align generalized_continued_fraction.squash_gcf_nth_of_lt GeneralizedContinuedFraction.squashGcf_nth_of_lt
+#align generalized_continued_fraction.squash_gcf_nth_of_lt GeneralizedContinuedFraction.squashGcf_get?_of_lt
 
 /-- `convergents'` returns the same value for a gcf and the corresponding squashed gcf at the
 squashed position. -/
@@ -272,7 +272,7 @@ end WithDivisionRing
 
 /-- The convergents coincide in the expected way at the squashed position if the partial denominator
 at the squashed position is not zero. -/
-theorem succ_nth_convergent_eq_squashGcf_nth_convergent [Field K]
+theorem succ_get?_convergent_eq_squashGcf_get?_convergent [Field K]
     (nth_part_denom_ne_zero : ∀ {b : K}, g.partialDenominators.get? n = some b → b ≠ 0) :
     g.convergents (n + 1) = (squashGcf g n).convergents n :=
   by
@@ -348,7 +348,7 @@ theorem succ_nth_convergent_eq_squashGcf_nth_convergent [Field K]
         simpa only [eq1, eq2, eq3, eq4, mul_div_cancel _ b_ne_zero]
       field_simp
       congr 1 <;> ring
-#align generalized_continued_fraction.succ_nth_convergent_eq_squash_gcf_nth_convergent GeneralizedContinuedFraction.succ_nth_convergent_eq_squashGcf_nth_convergent
+#align generalized_continued_fraction.succ_nth_convergent_eq_squash_gcf_nth_convergent GeneralizedContinuedFraction.succ_get?_convergent_eq_squashGcf_get?_convergent
 
 end Squash
 

Mathbin/Algebra/Module/Pid.lean

@@ -292,7 +292,7 @@ theorem equiv_free_prod_directSum [h' : Module.Finite R N] :
   haveI := Module.Finite.of_surjective _ (torsion R N).mkQ_surjective
   obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ := equiv_direct_sum_of_is_torsion (@torsion_is_torsion R N _ _ _)
   obtain ⟨n, ⟨g⟩⟩ := @Module.basisOfFiniteTypeTorsionFree' R _ _ _ (N ⧸ torsion R N) _ _ _ _
-  haveI : Module.Projective R (N ⧸ torsion R N) := Module.projectiveOfBasis ⟨g⟩
+  haveI : Module.Projective R (N ⧸ torsion R N) := Module.Projective.of_basis ⟨g⟩
   obtain ⟨f, hf⟩ := Module.projective_lifting_property _ LinearMap.id (torsion R N).mkQ_surjective
   refine'
     ⟨n, I, fI, p, hp, e,