bump to nightly-2023-09-30-06

mathlib commit leanprover-community/mathlib@ce64cd3

Mathbin/CategoryTheory/Adjunction/Basic.lean

@@ -619,21 +619,15 @@ def toAdjunction (e : C ≌ D) : e.Functor ⊣ e.inverse :=
 #align category_theory.equivalence.to_adjunction CategoryTheory.Equivalence.toAdjunction
 -/
 
-#print CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit /-
 @[simp]
-theorem asEquivalence_toAdjunction_unit {e : C ≌ D} :
-    e.Functor.asEquivalence.toAdjunction.Unit = e.Unit :=
+theorem toAdjunction_unit {e : C ≌ D} : e.Functor.asEquivalence.toAdjunction.Unit = e.Unit :=
   rfl
-#align category_theory.equivalence.as_equivalence_to_adjunction_unit CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit
--/
+#align category_theory.equivalence.as_equivalence_to_adjunction_unit CategoryTheory.Equivalence.toAdjunction_unitₓ
 
-#print CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit /-
 @[simp]
-theorem asEquivalence_toAdjunction_counit {e : C ≌ D} :
-    e.Functor.asEquivalence.toAdjunction.counit = e.counit :=
+theorem toAdjunction_counit {e : C ≌ D} : e.Functor.asEquivalence.toAdjunction.counit = e.counit :=
   rfl
-#align category_theory.equivalence.as_equivalence_to_adjunction_counit CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit
--/
+#align category_theory.equivalence.as_equivalence_to_adjunction_counit CategoryTheory.Equivalence.toAdjunction_counitₓ
 
 end Equivalence
 

Mathbin/Data/Fintype/Powerset.lean

@@ -47,11 +47,11 @@ theorem Finset.powerset_eq_univ [Fintype α] {s : Finset α} : s.powerset = univ
 #align finset.powerset_eq_univ Finset.powerset_eq_univ
 -/
 
-#print Finset.mem_powerset_len_univ_iff /-
-theorem Finset.mem_powerset_len_univ_iff [Fintype α] {s : Finset α} {k : ℕ} :
+#print Finset.mem_powersetLen_univ /-
+theorem Finset.mem_powersetLen_univ [Fintype α] {s : Finset α} {k : ℕ} :
     s ∈ powersetLen k (univ : Finset α) ↔ card s = k :=
   mem_powersetLen.trans <| and_iff_right <| subset_univ _
-#align finset.mem_powerset_len_univ_iff Finset.mem_powerset_len_univ_iff
+#align finset.mem_powerset_len_univ_iff Finset.mem_powersetLen_univ
 -/
 
 #print Finset.univ_filter_card_eq /-

Mathbin/Data/Set/Intervals/Basic.lean

@@ -2368,29 +2368,35 @@ section Lattice
 
 variable [Lattice β] {f : α → β}
 
+#print MonotoneOn.image_Icc_subset /-
 theorem MonotoneOn.image_Icc_subset (hf : MonotoneOn f (Icc a b)) :
     f '' Icc a b ⊆ Icc (f a) (f b) :=
   image_subset_iff.2 fun c hc =>
     ⟨hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1,
       hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2⟩
 #align monotone_on.image_Icc_subset MonotoneOn.image_Icc_subset
+-/
 
+#print AntitoneOn.image_Icc_subset /-
 theorem AntitoneOn.image_Icc_subset (hf : AntitoneOn f (Icc a b)) :
     f '' Icc a b ⊆ Icc (f b) (f a) :=
   image_subset_iff.2 fun c hc =>
     ⟨hf hc (right_mem_Icc.2 <| hc.1.trans hc.2) hc.2,
       hf (left_mem_Icc.2 <| hc.1.trans hc.2) hc hc.1⟩
 #align antitone_on.image_Icc_subset AntitoneOn.image_Icc_subset
+-/
 
 #print Monotone.image_Icc_subset /-
 theorem Monotone.image_Icc_subset (hf : Monotone f) : f '' Icc a b ⊆ Icc (f a) (f b) :=
   (hf.MonotoneOn _).image_Icc_subset
 #align monotone.image_Icc_subset Monotone.image_Icc_subset
 -/
 
+#print Antitone.image_Icc_subset /-
 theorem Antitone.image_Icc_subset (hf : Antitone f) : f '' Icc a b ⊆ Icc (f b) (f a) :=
   (hf.AntitoneOn _).image_Icc_subset
 #align antitone.image_Icc_subset Antitone.image_Icc_subset
+-/
 
 end Lattice
 

Mathbin/Data/Set/Intervals/UnorderedInterval.lean

@@ -254,25 +254,33 @@ section Lattice
 
 variable [Lattice β] {f : α → β} {s : Set α} {a b : α}
 
+#print MonotoneOn.image_uIcc_subset /-
 theorem MonotoneOn.image_uIcc_subset (hf : MonotoneOn f (uIcc a b)) :
     f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   hf.image_Icc_subset.trans <| by
     rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
 #align monotone_on.image_uIcc_subset MonotoneOn.image_uIcc_subset
+-/
 
+#print AntitoneOn.image_uIcc_subset /-
 theorem AntitoneOn.image_uIcc_subset (hf : AntitoneOn f (uIcc a b)) :
     f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   hf.image_Icc_subset.trans <| by
     rw [hf.map_sup left_mem_uIcc right_mem_uIcc, hf.map_inf left_mem_uIcc right_mem_uIcc, uIcc]
 #align antitone_on.image_uIcc_subset AntitoneOn.image_uIcc_subset
+-/
 
+#print Monotone.image_uIcc_subset /-
 theorem Monotone.image_uIcc_subset (hf : Monotone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   (hf.MonotoneOn _).image_uIcc_subset
 #align monotone.image_uIcc_subset Monotone.image_uIcc_subset
+-/
 
+#print Antitone.image_uIcc_subset /-
 theorem Antitone.image_uIcc_subset (hf : Antitone f) : f '' uIcc a b ⊆ uIcc (f a) (f b) :=
   (hf.AntitoneOn _).image_uIcc_subset
 #align antitone.image_uIcc_subset Antitone.image_uIcc_subset
+-/
 
 end Lattice
 

Mathbin/GroupTheory/Coset.lean

@@ -358,7 +358,7 @@ of a subgroup.-/
 @[to_additive
       "The equivalence relation corresponding to the partition of a group by left cosets\nof a subgroup."]
 def leftRel : Setoid α :=
-  MulAction.orbitRel s.opposite α
+  MulAction.orbitRel s.opEquiv α
 #align quotient_group.left_rel QuotientGroup.leftRel
 #align quotient_add_group.left_rel QuotientAddGroup.leftRel
 -/
@@ -369,8 +369,8 @@ variable {s}
 @[to_additive]
 theorem leftRel_apply {x y : α} : @Setoid.r _ (leftRel s) x y ↔ x⁻¹ * y ∈ s :=
   calc
-    (∃ a : s.opposite, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
-      s.oppositeEquiv.symm.exists_congr_left
+    (∃ a : s.opEquiv, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
+      s.equivOp.symm.exists_congr_left
     _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹ := by simp only [inv_mul_eq_iff_eq_mul, eq_mul_inv_iff_mul_eq]
     _ ↔ x⁻¹ * y ∈ s := by simp [SetLike.exists]
 #align quotient_group.left_rel_apply QuotientGroup.leftRel_apply

Mathbin/GroupTheory/GroupAction/Quotient.lean

@@ -70,7 +70,7 @@ instance left_quotientAction : QuotientAction α H :=
 
 #print MulAction.right_quotientAction /-
 @[to_additive]
-instance right_quotientAction : QuotientAction H.normalizer.opposite H :=
+instance right_quotientAction : QuotientAction H.normalizer.opEquiv H :=
   ⟨fun b c _ _ => by
     rwa [smul_def, smul_def, smul_eq_mul_unop, smul_eq_mul_unop, mul_inv_rev, ← mul_assoc,
       mem_normalizer_iff'.mp b.prop, mul_assoc, mul_inv_cancel_left]⟩

Mathbin/GroupTheory/Subgroup/MulOpposite.lean

@@ -23,11 +23,11 @@ variable {G : Type _} [Group G]
 
 namespace Subgroup
 
-#print Subgroup.opposite /-
+#print Subgroup.opEquiv /-
 /-- A subgroup `H` of `G` determines a subgroup `H.opposite` of the opposite group `Gᵐᵒᵖ`. -/
 @[to_additive
       "An additive subgroup `H` of `G` determines an additive subgroup `H.opposite` of the\n  opposite additive group `Gᵃᵒᵖ`."]
-def opposite : Subgroup G ≃ Subgroup Gᵐᵒᵖ
+def opEquiv : Subgroup G ≃ Subgroup Gᵐᵒᵖ
     where
   toFun H :=
     { carrier := MulOpposite.unop ⁻¹' (H : Set G)
@@ -41,30 +41,30 @@ def opposite : Subgroup G ≃ Subgroup Gᵐᵒᵖ
       inv_mem' := fun a => H.inv_mem }
   left_inv H := SetLike.coe_injective rfl
   right_inv H := SetLike.coe_injective rfl
-#align subgroup.opposite Subgroup.opposite
-#align add_subgroup.opposite AddSubgroup.opposite
+#align subgroup.opposite Subgroup.opEquiv
+#align add_subgroup.opposite AddSubgroup.opEquiv
 -/
 
-#print Subgroup.oppositeEquiv /-
+#print Subgroup.equivOp /-
 /-- Bijection between a subgroup `H` and its opposite. -/
 @[to_additive "Bijection between an additive subgroup `H` and its opposite.", simps]
-def oppositeEquiv (H : Subgroup G) : H ≃ H.opposite :=
+def equivOp (H : Subgroup G) : H ≃ H.opEquiv :=
   MulOpposite.opEquiv.subtypeEquiv fun _ => Iff.rfl
-#align subgroup.opposite_equiv Subgroup.oppositeEquiv
-#align add_subgroup.opposite_equiv AddSubgroup.oppositeEquiv
+#align subgroup.opposite_equiv Subgroup.equivOp
+#align add_subgroup.opposite_equiv AddSubgroup.equivOp
 -/
 
 @[to_additive]
-instance (H : Subgroup G) [Encodable H] : Encodable H.opposite :=
-  Encodable.ofEquiv H H.oppositeEquiv.symm
+instance (H : Subgroup G) [Encodable H] : Encodable H.opEquiv :=
+  Encodable.ofEquiv H H.equivOp.symm
 
 @[to_additive]
-instance (H : Subgroup G) [Countable H] : Countable H.opposite :=
-  Countable.of_equiv H H.oppositeEquiv
+instance (H : Subgroup G) [Countable H] : Countable H.opEquiv :=
+  Countable.of_equiv H H.equivOp
 
 #print Subgroup.smul_opposite_mul /-
 @[to_additive]
-theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : H.opposite) : h • (g * x) = g * h • x :=
+theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : H.opEquiv) : h • (g * x) = g * h • x :=
   by
   cases h
   simp [(· • ·), mul_assoc]

Mathbin/GroupTheory/Subgroup/Pointwise.lean

@@ -278,7 +278,7 @@ instance sup_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊔
 
 #print Subgroup.smul_opposite_image_mul_preimage /-
 @[to_additive]
-theorem smul_opposite_image_mul_preimage {H : Subgroup G} (g : G) (h : H.opposite) (s : Set G) :
+theorem smul_opposite_image_mul_preimage {H : Subgroup G} (g : G) (h : H.opEquiv) (s : Set G) :
     (fun y => h • y) '' (Mul.mul g ⁻¹' s) = Mul.mul g ⁻¹' ((fun y => h • y) '' s) := by ext x;
   cases h; simp [(· • ·), mul_assoc]
 #align subgroup.smul_opposite_image_mul_preimage Subgroup.smul_opposite_image_mul_preimage

Mathbin/MeasureTheory/Function/AeEqOfIntegral.lean

@@ -627,8 +627,8 @@ end AeEqOfForallSetIntegralEq
 
 section Lintegral
 
-#print MeasureTheory.AeMeasurable.ae_eq_of_forall_set_lintegral_eq /-
-theorem AeMeasurable.ae_eq_of_forall_set_lintegral_eq {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
+#print MeasureTheory.AEMeasurable.ae_eq_of_forall_set_lintegral_eq /-
+theorem AEMeasurable.ae_eq_of_forall_set_lintegral_eq {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
     (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (hgi : ∫⁻ x, g x ∂μ ≠ ∞)
     (hfg : ∀ ⦃s⦄, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) : f =ᵐ[μ] g :=
   by
@@ -650,7 +650,7 @@ theorem AeMeasurable.ae_eq_of_forall_set_lintegral_eq {f g : α → ℝ≥0∞}
   exacts [ae_of_all _ fun x => ENNReal.toReal_nonneg,
     hg.ennreal_to_real.restrict.ae_strongly_measurable, ae_of_all _ fun x => ENNReal.toReal_nonneg,
     hf.ennreal_to_real.restrict.ae_strongly_measurable]
-#align measure_theory.ae_measurable.ae_eq_of_forall_set_lintegral_eq MeasureTheory.AeMeasurable.ae_eq_of_forall_set_lintegral_eq
+#align measure_theory.ae_measurable.ae_eq_of_forall_set_lintegral_eq MeasureTheory.AEMeasurable.ae_eq_of_forall_set_lintegral_eq
 -/
 
 end Lintegral

Mathbin/MeasureTheory/Integral/Periodic.lean

@@ -69,7 +69,7 @@ theorem isAddFundamentalDomain_Ioc {T : ℝ} (hT : 0 < T) (t : ℝ)
 #print isAddFundamentalDomain_Ioc' /-
 theorem isAddFundamentalDomain_Ioc' {T : ℝ} (hT : 0 < T) (t : ℝ)
     (μ : Measure ℝ := by exact MeasureTheory.MeasureSpace.volume) :
-    IsAddFundamentalDomain (AddSubgroup.zmultiples T).opposite (Ioc t (t + T)) μ :=
+    IsAddFundamentalDomain (AddSubgroup.zmultiples T).opEquiv (Ioc t (t + T)) μ :=
   by
   refine' is_add_fundamental_domain.mk' measurable_set_Ioc.null_measurable_set fun x => _
   have : bijective (cod_restrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=

Mathbin/MeasureTheory/Measure/Haar/Quotient.lean

@@ -57,7 +57,7 @@ instance QuotientGroup.measurableSMul [MeasurableSpace (G ⧸ Γ)] [BorelSpace (
 #align quotient_add_group.has_measurable_vadd QuotientAddGroup.measurableVAdd
 -/
 
-variable {𝓕 : Set G} (h𝓕 : IsFundamentalDomain Γ.opposite 𝓕 μ)
+variable {𝓕 : Set G} (h𝓕 : IsFundamentalDomain Γ.opEquiv 𝓕 μ)
 
 variable [Countable Γ] [MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)]
 
@@ -239,8 +239,8 @@ theorem QuotientGroup.integral_eq_integral_automorphize {E : Type _} [NormedAddC
     (hf₂ : AEStronglyMeasurable (automorphize f) μ_𝓕) :
     ∫ x : G, f x ∂μ = ∫ x : G ⧸ Γ, automorphize f x ∂μ_𝓕 :=
   calc
-    ∫ x : G, f x ∂μ = ∑' γ : Γ.opposite, ∫ x in 𝓕, f (γ • x) ∂μ := h𝓕.integral_eq_tsum'' f hf₁
-    _ = ∫ x in 𝓕, ∑' γ : Γ.opposite, f (γ • x) ∂μ :=
+    ∫ x : G, f x ∂μ = ∑' γ : Γ.opEquiv, ∫ x in 𝓕, f (γ • x) ∂μ := h𝓕.integral_eq_tsum'' f hf₁
+    _ = ∫ x in 𝓕, ∑' γ : Γ.opEquiv, f (γ • x) ∂μ :=
       by
       rw [integral_tsum]
       ·
@@ -309,7 +309,7 @@ theorem quotientAddGroup.integral_hMul_eq_integral_automorphize_hMul {K : Type _
     (f_ℒ_1 : Integrable f μ') {g : G' ⧸ Γ' → K} (hg : AEStronglyMeasurable g μ_𝓕)
     (g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) μ_𝓕 ≠ ∞)
     (F_ae_measurable : AEStronglyMeasurable (quotientAddGroup.automorphize f) μ_𝓕)
-    (h𝓕 : IsAddFundamentalDomain Γ'.opposite 𝓕' μ') :
+    (h𝓕 : IsAddFundamentalDomain Γ'.opEquiv 𝓕' μ') :
     ∫ x : G', g (x : G' ⧸ Γ') * f x ∂μ' =
       ∫ x : G' ⧸ Γ', g x * quotientAddGroup.automorphize f x ∂μ_𝓕 :=
   by

Mathbin/Order/Lattice.lean

@@ -1496,18 +1496,22 @@ theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β]
 
 variable [LinearOrder α]
 
+#print MonotoneOn.map_sup /-
 theorem map_sup [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
     f (x ⊔ y) = f x ⊔ f y := by
   cases le_total x y <;> have := hf _ _ h <;>
     first
     | assumption
     | simp only [h, this, sup_of_le_left, sup_of_le_right]
 #align monotone_on.map_sup MonotoneOn.map_sup
+-/
 
+#print MonotoneOn.map_inf /-
 theorem map_inf [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
     f (x ⊓ y) = f x ⊓ f y :=
   hf.dual.map_sup hx hy
 #align monotone_on.map_inf MonotoneOn.map_inf
+-/
 
 end MonotoneOn
 
@@ -1623,18 +1627,22 @@ theorem of_map_sup [SemilatticeSup α] [SemilatticeInf β]
 
 variable [LinearOrder α]
 
+#print AntitoneOn.map_sup /-
 theorem map_sup [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
     f (x ⊔ y) = f x ⊓ f y := by
   cases le_total x y <;> have := hf _ _ h <;>
     first
     | assumption
     | simp only [h, this, sup_of_le_left, sup_of_le_right, inf_of_le_left, inf_of_le_right]
 #align antitone_on.map_sup AntitoneOn.map_sup
+-/
 
+#print AntitoneOn.map_inf /-
 theorem map_inf [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) :
     f (x ⊓ y) = f x ⊔ f y :=
   hf.dual.map_sup hx hy
 #align antitone_on.map_inf AntitoneOn.map_inf
+-/
 
 end AntitoneOn
 

Mathbin/RingTheory/MvPolynomial/Symmetric.lean

@@ -214,7 +214,7 @@ theorem aeval_esymm_eq_multiset_esymm [Algebra R S] (f : σ → S) (n : ℕ) :
 /-- We can define `esymm σ R n` by summing over a subtype instead of over `powerset_len`. -/
 theorem esymm_eq_sum_subtype (n : ℕ) :
     esymm σ R n = ∑ t : { s : Finset σ // s.card = n }, ∏ i in (t : Finset σ), X i :=
-  sum_subtype _ (fun _ => mem_powerset_len_univ_iff) _
+  sum_subtype _ (fun _ => mem_powersetLen_univ) _
 #align mv_polynomial.esymm_eq_sum_subtype MvPolynomial.esymm_eq_sum_subtype
 -/
 

Mathbin/Topology/Algebra/Group/Basic.lean

@@ -1785,7 +1785,7 @@ to show that the quotient group `G ⧸ S` is Hausdorff. -/
 @[to_additive
       "A subgroup `S` of an additive topological group `G` acts on `G` properly\ndiscontinuously on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact\n`K`. (See also `discrete_topology`.)\n\nIf `G` is Hausdorff, this can be combined with `t2_space_of_properly_discontinuous_vadd_of_t2_space`\nto show that the quotient group `G ⧸ S` is Hausdorff."]
 theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite (S : Subgroup G)
-    (hS : Tendsto S.Subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.opposite G :=
+    (hS : Tendsto S.Subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.opEquiv G :=
   {
     finite_disjoint_inter_image := by
       intro K L hK hL

Mathbin/Topology/Instances/AddCircle.lean

@@ -589,7 +589,7 @@ instance compactSpace [Fact (0 < p)] : CompactSpace <| AddCircle p :=
 
 /-- The action on `ℝ` by right multiplication of its the subgroup `zmultiples p` (the multiples of
 `p:ℝ`) is properly discontinuous. -/
-instance : ProperlyDiscontinuousVAdd (zmultiples p).opposite ℝ :=
+instance : ProperlyDiscontinuousVAdd (zmultiples p).opEquiv ℝ :=
   (zmultiples p).properlyDiscontinuousVAdd_opposite_of_tendsto_cofinite
     (AddSubgroup.tendsto_zmultiples_subtype_cofinite p)
 

lake-manifest.json

@@ -4,18 +4,18 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "c11638cd34fc6001aabe11b109172b09a3640d88",
+    "rev": "e3c4ddfaad66a7f128e2c1403938fe7d0978e33b",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "c11638cd34fc6001aabe11b109172b09a3640d88",
+    "inputRev?": "e3c4ddfaad66a7f128e2c1403938fe7d0978e33b",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "51e00c7c095e7381a6dbee5d1679f028af52ee5f",
+    "rev": "5d32dbdedd926bd86da0ada0c75ea0a57fa68c52",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "51e00c7c095e7381a6dbee5d1679f028af52ee5f",
+    "inputRev?": "5d32dbdedd926bd86da0ada0c75ea0a57fa68c52",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
@@ -41,20 +41,20 @@
     "name": "Cli",
     "inputRev?": "nightly",
     "inherited": true}},
-  {"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.16",
-    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
     "rev": "f2df4ab8c0726fce3bafb73a5727336b0c3120ea",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "9f68f14df384f43b74aeb2908b97ae54a0ad9d95",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.17",
     "inherited": true}}],
  "name": "mathlib3port"}