bump

FltRegular/CaseII/AuxLemmas.lean

@@ -139,7 +139,7 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime'
   rw [← Ne.def, ← isUnit_iff_ne_zero] at Izero
   show Submodule.IsPrincipal (Izero.unit' : FractionalIdeal A⁰ K)
   rw [← ClassGroup.mk_eq_one_iff, ← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
-  refine ⟨?_, orderOf_dvd_card_univ⟩
+  refine ⟨?_, orderOf_dvd_card⟩
   rw [orderOf_dvd_iff_pow_eq_one, ← map_pow, ClassGroup.mk_eq_one_iff]
   simp only [Units.val_pow_eq_pow_val, IsUnit.val_unit', hI]
 

FltRegular/NumberTheory/AuxLemmas.lean

@@ -53,23 +53,15 @@ lemma AlgEquiv.toAlgHom_toRingHom {R A₁ A₂} [CommSemiring R] [Semiring A₁]
     [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = e :=
   rfl
 
--- Mathlib/Algebra/Algebra/Hom.lean
-lemma AlgEquiv.toRingEquiv_toRingHom {R A₁ A₂} [CommSemiring R] [Semiring A₁] [Semiring A₂]
-    [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e :=
-  rfl
-
 -- Mathlib/RingTheory/Localization/Away/Basic.lean
 -- Sounds like a bad place but this should go before `IsLocalization.atUnits`.
 lemma IsLocalization.at_units {R : Type*} [CommSemiring R] (S : Submonoid R)
     (hS : ∀ s : S, IsUnit (s : R)) : IsLocalization S R where
   map_units' := hS
   surj' := fun s ↦ ⟨⟨s, 1⟩, by simp⟩
-  eq_iff_exists' := fun {x y} ↦ by
-    constructor
-    · rintro (rfl : x = y)
-      exact ⟨1, rfl⟩
-    · rintro ⟨c, hc⟩
-      exact (hS c).mul_left_cancel hc
+  exists_of_eq := fun {x y} ↦ by
+    rintro (rfl : x = y)
+    exact ⟨1, rfl⟩
 
 -- Mathlib/RingTheory/Localization/FractionRing.lean
 instance {R : Type*} [Field R] : IsFractionRing R R :=
@@ -561,7 +553,7 @@ theorem IsIntegralClosure.isLocalization' (ha : Algebra.IsAlgebraic K L) [NoZero
   haveI : IsDomain C :=
     (IsIntegralClosure.equiv A C L (integralClosure A L)).toMulEquiv.isDomain (integralClosure A L)
   haveI : NoZeroSMulDivisors A C := IsIntegralClosure.noZeroSMulDivisors A L
-  refine' ⟨_, fun z => _, fun {x y} => ⟨fun h => ⟨1, _⟩, _⟩⟩
+  refine' ⟨_, fun z => _, fun {x y} => fun h => ⟨1, _⟩⟩
   · rintro ⟨_, x, hx, rfl⟩
     rw [isUnit_iff_ne_zero, map_ne_zero_iff _ (IsIntegralClosure.algebraMap_injective C A L),
       Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
@@ -574,10 +566,6 @@ theorem IsIntegralClosure.isLocalization' (ha : Algebra.IsAlgebraic K L) [NoZero
     rw [Subtype.coe_mk, ← IsScalarTower.algebraMap_apply, hx, mul_comm, Submonoid.smul_def,
       smul_def]
   · simp only [IsIntegralClosure.algebraMap_injective C A L h]
-  · rintro ⟨⟨_, m, hm, rfl⟩, h⟩
-    refine' congr_arg (algebraMap C L) ((mul_right_inj' _).mp h)
-    rw [Subtype.coe_mk, map_ne_zero_iff _ (NoZeroSMulDivisors.algebraMap_injective A C)]
-    exact mem_nonZeroDivisors_iff_ne_zero.mp hm
 end
 
 -- Mathlib/RingTheory/Algebraic.lean
@@ -652,13 +640,14 @@ lemma isAlgebraic_of_isFractionRing {R S} (K L) [CommRing R] [CommRing S] [Field
   intro x
   obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective S⁰ x
   rw [isAlgebraic_iff_isIntegral, IsLocalization.mk'_eq_mul_mk'_one]
-  apply isIntegral_mul
+  apply RingHom.is_integral_mul
   · apply isIntegral_of_isScalarTower (R := R)
-    apply map_isIntegral (IsScalarTower.toAlgHom R S L)
+    apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
     exact h x
-  · rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
+  · show IsIntegral _ _
+    rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
     apply isIntegral_of_isScalarTower (R := R)
-    apply map_isIntegral (IsScalarTower.toAlgHom R S L)
+    apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
     exact h s
 
 -- Mathlib/RingTheory/IntegralClosure.lean
@@ -669,7 +658,7 @@ lemma isIntegralClosure_of_isIntegrallyClosed (R S K) [CommRing R] [CommRing S]
   refine ⟨IsLocalization.injective _ le_rfl, fun {x} ↦
     ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (isIntegral_of_isScalarTower (A := S) hx), ?_⟩⟩
   rintro ⟨y, rfl⟩
-  exact map_isIntegral (IsScalarTower.toAlgHom R S K) (hRS y)
+  exact IsIntegral.map (IsScalarTower.toAlgHom R S K) (hRS y)
 
 -- Mathlib/RingTheory/IntegralClosure.lean
 -- or Mathlib/RingTheory/LocalProperties.lean
@@ -707,11 +696,14 @@ lemma IsIntegral_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRing S] [Co
   obtain ⟨x, ⟨_, t, ht, rfl⟩, rfl⟩ := IsLocalization.mk'_surjective
     (Algebra.algebraMapSubmonoid S M) x
   rw [IsLocalization.mk'_eq_mul_mk'_one]
-  apply isIntegral_mul
-  · exact isIntegral_of_isScalarTower (map_isIntegral (IsScalarTower.toAlgHom R S Sₚ) (hRS x))
-  · convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
+  apply RingHom.is_integral_mul
+  · exact isIntegral_of_isScalarTower (IsIntegral.map (IsScalarTower.toAlgHom R S Sₚ) (hRS x))
+  · show IsIntegral _ _
+    convert isIntegral_algebraMap (x := IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
     rw [this, IsLocalization.map_mk', _root_.map_one]
 
+
+
 -- Mathlib/RingTheory/Polynomial/ScaleRoots.lean (this section is not needed anymore)
 section scaleRoots
 

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -174,8 +174,7 @@ theorem prim_coe (ζ : R) (hζ : IsPrimitiveRoot ζ p) : IsPrimitiveRoot (ζ : C
 
 theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη : η ∈ nthRootsFinset p R)
     (hne1 : η ≠ 1) : 1 - η ∣ (p : R) := by
-  have h00 : 1 - η ∣ (p : R) ↔ η - 1 ∣ (p : R) :=
-    by
+  have h00 : 1 - η ∣ (p : R) ↔ η - 1 ∣ (p : R) :=  by
     have hh : -(η - 1) = 1 - η := by ring
     simp_rw [← hh]
     apply neg_dvd
@@ -192,7 +191,8 @@ theorem zeta_sub_one_dvb_p [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η : R} (hη :
   ext
   rw [RingOfIntegers.coe_algebraMap_norm]
   norm_cast at h2
-  simp [h2]
+  rw [h2]
+  simp
 
 theorem one_sub_zeta_prime [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R)
     (hne1 : η ≠ 1) : Prime (1 - η) := by

FltRegular/NumberTheory/Cyclotomic/CyclotomicUnits.lean

@@ -70,7 +70,7 @@ theorem associated_one_sub_pow_primitive_root_of_coprime {n j k : ℕ} {ζ : A}
   replace hn := Nat.one_lt_of_ne n hn' hn
   obtain ⟨m, hm⟩ := Nat.exists_mul_emod_eq_one_of_coprime hj hn
   use ∑ i in range m, (ζ ^ j) ^ i
-  have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, pow_eq_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
+  have : ζ = (ζ ^ j) ^ m := by rw [← pow_mul, ←pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]
   nth_rw 1 [this]
   rw [← geom_sum_mul_neg, mul_comm]
 

FltRegular/NumberTheory/Cyclotomic/GaloisActionOnCyclo.lean

@@ -71,7 +71,6 @@ theorem embedding_conj (x : K) (φ : K →+* ℂ) : conj (φ x) = φ (galConj K
   suffices φ (galConj K p ζ) = conj (φ ζ)
     by
     rw [← Function.funext_iff]
-    dsimp only
     congr
     rw [FunLike.coe_fn_eq]
     apply (hζ.powerBasis ℚ).rat_hom_ext
@@ -90,7 +89,7 @@ variable (p)
 
 --generalize this
 theorem gal_map_mem {x : K} (hx : x ∈ RR) (σ : K →ₐ[ℚ] K) : σ x ∈ RR :=
-  map_isIntegral (σ.restrictScalars ℤ) hx
+  map_isIntegral_int (σ.restrictScalars ℤ) hx
 
 theorem gal_map_mem_subtype (σ : K →ₐ[ℚ] K) (x : RR) : σ x ∈ RR := by simp [gal_map_mem]
 

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -77,8 +77,7 @@ theorem zeta_runity_pow_even (hpo : Odd (p : ℕ)) (n : ℕ) :
 
 variable [NumberField K]
 
-theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p :=
-  by
+theorem IsPrimitiveRoot.unit'_coe : IsPrimitiveRoot (hζ.unit' : R) p := by
   have z1 := hζ
   have : (algebraMap R K) (hζ.unit' : R) = ζ := rfl
   rw [← this] at z1
@@ -415,7 +414,7 @@ theorem unit_inv_conj_is_root_of_unity (h : p ≠ 2) (hp : (p : ℕ).Prime) (u :
       Units.val_pow_eq_pow_val] at hz
     norm_cast at hz
     simpa [hz] using unit_inv_conj_not_neg_zeta_runity hζ h u n hp
-  · apply isIntegral_mul
+  · apply RingHom.is_integral_mul
     exact NumberField.RingOfIntegers.isIntegral_coe _
     exact NumberField.RingOfIntegers.isIntegral_coe _
   · exact unit_lemma_val_one p u

FltRegular/NumberTheory/Different.lean

@@ -115,7 +115,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule
   apply IsIntegral.sum
   intro i _
   rw [smul_mul_assoc, b.equivFun.map_smul, discr_def, mul_comm, ← H, Algebra.smul_def]
-  refine isIntegral_mul ?_ (hb _)
+  refine RingHom.is_integral_mul _ ?_ (hb _)
   apply IsIntegral.algebraMap
   rw [cramer_apply]
   apply IsIntegral.det
@@ -128,7 +128,7 @@ lemma isIntegral_discr_mul_of_mem_traceFormDualSubmodule
     have ⟨y, hy⟩ := (IsIntegralClosure.isIntegral_iff (A := B)).mp (hb j)
     rw [mul_comm, ← hy, ← Algebra.smul_def]
     exact I.smul_mem _ (ha)
-  · exact isIntegral_trace (isIntegral_mul (hb j) (hb k))
+  · exact isIntegral_trace (RingHom.is_integral_mul _ (hb j) (hb k))
 
 variable (A K)
 
@@ -427,7 +427,7 @@ lemma conductor_mul_differentIdeal [NoZeroSMulDivisors A B]
     mem_coeIdeal_conductor]
   have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0
   · rwa [ne_eq, inv_eq_zero]
-  have : IsIntegral A (algebraMap B L x) := map_isIntegral (IsScalarTower.toAlgHom A B L) hAx
+  have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx
   simp_rw [← Subalgebra.mem_toSubmodule, ← Submodule.mul_mem_smul_iff (y := y * _) hne₂]
   rw [← traceFormDualSubmodule_span_adjoin A K L _ hx this]
   simp only [mem_traceFormDualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule,

FltRegular/NumberTheory/GaloisPrime.lean

@@ -114,7 +114,7 @@ noncomputable
 def galRestrictHom : (L →ₐ[K] L) →* (S →ₐ[R] S) where
   toFun := fun f ↦ (IsIntegralClosure.equiv R (integralClosure R L) L S).toAlgHom.comp
       (((f.restrictScalars R).comp (IsScalarTower.toAlgHom R S L)).codRestrict
-        (integralClosure R L) (fun x ↦ map_isIntegral _ (IsIntegralClosure.isIntegral R L x)))
+        (integralClosure R L) (fun x ↦ IsIntegral.map _ (IsIntegralClosure.isIntegral R L x)))
   map_one' := by
     ext x
     apply (IsIntegralClosure.equiv R (integralClosure R L) L S).symm.injective

FltRegular/NumberTheory/IdealNorm.lean

@@ -40,7 +40,7 @@ def Algebra.intNormAux (R S K L) [CommRing R] [CommRing S] [Field K] [Field L]
     [IsFractionRing R K] [FiniteDimensional K L] [IsSeparable K L] :
     S →* R where
   toFun := fun s ↦ IsIntegralClosure.mk' (R := R) R (Algebra.norm K (algebraMap S L s))
-    (isIntegral_norm K <| map_isIntegral (IsScalarTower.toAlgHom R S L)
+    (isIntegral_norm K <| IsIntegral.map (IsScalarTower.toAlgHom R S L)
       (IsIntegralClosure.isIntegral R L s))
   map_one' := by simp
   map_mul' := fun x y ↦ by simpa using IsIntegralClosure.mk'_mul _ _ _ _ _
@@ -288,7 +288,7 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R
     isIntegralClosure_of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (A := Sₘ))
   cases h : subsingleton_or_nontrivial R
   · haveI := IsLocalization.unique R Rₘ M
-    simp
+    simp only [eq_iff_true_of_subsingleton]
   rw [map_spanIntNorm]
   refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
   · rintro a' ha'

FltRegular/NumberTheory/KummerExtension.lean

@@ -452,7 +452,7 @@ lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) :
   -- However `{ σⁱ }` are linear independent (via Dedekind's linear independence of characters).
   have := Fintype.linearIndependent_iff.mp
     ((linearIndependent_algEquiv_toLinearMap K L).comp _
-      (Subtype.val_injective.comp (finEquivPowers σ).injective))
+      (Subtype.val_injective.comp ((finEquivPowers σ (isOfFinOrder_of_finite σ)).injective)))
     ((minpoly K σ.toLinearMap).coeff ∘ (↑)) this ⟨_, H⟩
   simpa using this
 
@@ -500,15 +500,15 @@ lemma irreducible_X_pow_sub_C_of_root_adjoin_eq_top
     {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a) (hα : K⟮α⟯ = ⊤) :
     Irreducible (X ^ (finrank K L) - C a) := by
   have : minpoly K α = X ^ (finrank K L) - C a
-  · apply eq_of_monic_of_associated (minpoly.monic (isIntegral_of_finite K α))
+  · apply eq_of_monic_of_associated (minpoly.monic (IsIntegral.of_finite K α))
       (monic_X_pow_sub_C _ finrank_pos.ne.symm)
     refine Polynomial.associated_of_dvd_of_natDegree_eq ?_ ?_
       (X_pow_sub_C_ne_zero finrank_pos _)
     · refine minpoly.dvd _ _ ?_
       simp only [aeval_def, eval₂_sub, eval₂_X_pow, ha, eval₂_C, sub_self]
-    · rw [← IntermediateField.adjoin.finrank (isIntegral_of_finite K α), hα, natDegree_X_pow_sub_C]
+    · rw [← IntermediateField.adjoin.finrank (IsIntegral.of_finite K α), hα, natDegree_X_pow_sub_C]
       exact finrank_top K L
-  exact this ▸ minpoly.irreducible (isIntegral_of_finite K α)
+  exact this ▸ minpoly.irreducible (IsIntegral.of_finite K α)
 
 lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top
     {a : K} {α : L} (ha : α ^ (finrank K L) = algebraMap K L a) (hα : K⟮α⟯ = ⊤) :
@@ -520,7 +520,7 @@ lemma isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top
     rw [mem_primitiveRoots finrank_pos] at hζ
     exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha
   · rw [eq_top_iff, ← IntermediateField.top_toSubalgebra, ← hα,
-      IntermediateField.adjoin_simple_toSubalgebra_of_integral (isIntegral_of_finite K α)]
+      IntermediateField.adjoin_simple_toSubalgebra_of_integral (IsIntegral.of_finite K α)]
     apply Algebra.adjoin_mono
     rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero finrank_pos a),
       aeval_def, eval₂_sub, eval₂_X_pow, eval₂_C, ha, sub_self]

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -7,8 +7,6 @@ import Mathlib.Data.Polynomial.Taylor
 
 open scoped NumberField BigOperators
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220
-
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
 variable (hp : p ≠ 2)
 
@@ -256,7 +254,7 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
     AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one,
     SubmonoidClass.coe_pow] at hv
   have hα : IsIntegral (𝓞 K) α
-  · apply isIntegral_of_pow p.pos; rw [e]; exact isIntegral_algebraMap
+  · apply IsIntegral.of_pow p.pos; rw [e]; exact isIntegral_algebraMap
   have : IsUnit (⟨α, isIntegral_trans (IsIntegralClosure.isIntegral_algebra ℤ K) _ hα⟩ : 𝓞 L)
   · rw [← isUnit_pow_iff p.pos.ne.symm]
     convert (algebraMap (𝓞 K) (𝓞 L)).isUnit_map u.isUnit

FltRegular/NumberTheory/KummersLemma/KummersLemma.lean

@@ -5,8 +5,6 @@ import FltRegular.NumberTheory.IdealNorm
 
 open scoped NumberField
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue #2220
-
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K]
 variable (hp : p ≠ 2) [Fintype (ClassGroup (𝓞 K))] (hreg : (p : ℕ).Coprime <| Fintype.card <| ClassGroup (𝓞 K))
 
@@ -157,7 +155,7 @@ theorem eq_pow_prime_of_unit_of_congruent (u : (𝓞 K)ˣ)
   simp only [not_forall, not_not] at this
   obtain ⟨v, hv⟩ := this
   have hv' : IsIntegral ℤ v
-  · apply isIntegral_of_pow p.pos; rw [hv]; exact (u ^ (p - 1 : ℕ) : 𝓞 K).prop
+  · apply IsIntegral.of_pow p.pos; rw [hv]; exact (u ^ (p - 1 : ℕ) : 𝓞 K).prop
   have : IsUnit (⟨v, hv'⟩ : 𝓞 K)
   · rw [← isUnit_pow_iff p.pos.ne.symm]; convert (u ^ (p - 1 : ℕ) : (𝓞 K)ˣ).isUnit; ext; exact hv
   have hv'' : this.unit ^ (p : ℕ) = u ^ (p - 1 : ℕ)

FltRegular/NumberTheory/RegularPrimes.lean

@@ -81,7 +81,9 @@ def cyclotomicFieldTwoEquiv [IsCyclotomicExtension {2} K L] : L ≃ₐ[K] K := b
     exact
       (IsSplittingField.algEquiv L (cyclotomic 2 K)).trans
         (IsSplittingField.algEquiv K <| cyclotomic 2 K).symm
-  exact ⟨by simpa using @splits_X_sub_C _ _ _ _ (RingHom.id K) (-1), by simp⟩
+  exact ⟨by simpa using @splits_X_sub_C _ _ _ _ (RingHom.id K) (-1),
+    by simp [eq_iff_true_of_subsingleton]⟩
+
 
 instance IsPrincipalIdealRing_of_IsCyclotomicExtension_two
   (L : Type _) [Field L] [CharZero L] [IsCyclotomicExtension {2} ℚ L] :
@@ -126,5 +128,5 @@ theorem IsPrincipal_of_IsPrincipal_pow_of_Coprime
   swap; · exact Izero
   swap; · exact pow_ne_zero p Izero
   rw [← orderOf_eq_one_iff, ← Nat.dvd_one, ← H, Nat.dvd_gcd_iff]
-  refine ⟨?_, orderOf_dvd_card_univ⟩
+  refine ⟨?_, orderOf_dvd_card⟩
   rwa [orderOf_dvd_iff_pow_eq_one, ← map_pow, SubmonoidClass.mk_pow]

FltRegular/ReadyForMathlib/Homogenization.lean

@@ -410,7 +410,6 @@ theorem exists_coeff_ne_zero_totalDegree {p : MvPolynomial ι R} (hp : p ≠ 0)
   constructor
   · rw [← totalDegree_eq p] at hb₂
     rw [hb₂]
-    dsimp
 
     -- TODO break this out as a lemma
     exact (Finsupp.card_toMultiset _).symm

lake-manifest.json

@@ -4,39 +4,31 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "5f066e77432aee5c14c229c3aaa178ff639be1a2",
+    "rev": "48237d43209009b253cafc0920ca4e0772c2aeac",
     "opts": {},
     "name": "mathlib",
     "inputRev?": null,
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/doc-gen4",
     "subDir?": null,
-    "rev": "e859e2f777521f82050b8f28e0205491a4ead0f5",
+    "rev": "96147eaa0c066a95210fe5518c987e77be034b9f",
     "opts": {},
     "name": "«doc-gen4»",
     "inputRev?": "main",
     "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
+    "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
+    "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
@@ -52,10 +44,18 @@
   {"git":
    {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "rev": "c3b9f0d4ebedc43635d3f7e764e277b1010844b7",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.21",
+    "inputRev?": "v0.0.22",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "c14f6a65b2c08caa38e1ab5db83451460d6cde3e",
+    "opts": {},
+    "name": "std",
+    "inputRev?": "main",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/xubaiw/CMark.lean",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc1
+leanprover/lean4:v4.3.0-rc1