bump

FltRegular/CaseII/InductionStep.lean

@@ -40,6 +40,8 @@ lemma zeta_sub_one_dvd : π ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by
   apply dvd_pow_self
   simp
 
+set_option synthInstance.maxHeartbeats 160000 in
+set_option maxHeartbeats 400000 in
 lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI : Fact (Nat.Prime p) := hpri
   letI := IsCyclotomicExtension.numberField {p} ℚ K
@@ -522,6 +524,8 @@ lemma exists_solution'_aux {ε₁ ε₂ : (𝓞 K)ˣ} (hx : ¬ π ∣ x)
   rw [neg_mul, (Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow,
     sub_neg_eq_add, mul_sub, mul_one, mul_comm x b, add_sub_sub_cancel, add_comm]
 
+set_option synthInstance.maxHeartbeats 160000 in
+set_option maxHeartbeats 400000 in
 lemma exists_solution' :
     ∃ (x' y' z' : 𝓞 K) (ε₃ : (𝓞 K)ˣ),
       ¬ π ∣ y' ∧ ¬ π ∣ z' ∧ x' ^ (p : ℕ) + y' ^ (p : ℕ) = ε₃ * (π ^ m * z') ^ (p : ℕ) := by

FltRegular/NumberTheory/AuxLemmas.lean

@@ -11,7 +11,7 @@ This file contains lemmas that should go somewhere in a file in mathlib.
 open BigOperators UniqueFactorizationMonoid
 
 -- Mathlib/RingTheory/Ideal/Operations.lean
-lemma Ideal.comap_coe {R S F : Type*} [Semiring R] [Semiring S] [RingHomClass F R S]
+lemma Ideal.comap_coe {R S F : Type*} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S]
   (f : F) (I : Ideal S) : I.comap (f : R →+* S) = I.comap f := rfl
 
 -- Mathlib/RingTheory/IntegralClosure.lean

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -226,6 +226,7 @@ theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} (
 instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup
 
 set_option maxHeartbeats 300000 in
+set_option synthInstance.maxHeartbeats 80000 in
 lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ} {η₁ η₂ : R}
     (hη₁ : η₁ ∈ nthRootsFinset p R)
     (hη₂ : η₂ ∈ nthRootsFinset p R) (hdiff : η₁ ≠ η₂) (hp : IsCoprime x y)
@@ -296,7 +297,7 @@ lemma fltIdeals_coprime2_lemma [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {x y : ℤ}
         rw [span_singleton_le_span_singleton]
         apply zeta_sub_one_dvb_p ph hη₁ hwlog
       have H2 : IsPrime (P.comap (Int.castRingHom R)) := by
-        apply @IsPrime.comap _ _ _ _ _ _ _ _ hPrime
+        exact IsPrime.comap _
       have H4 : Ideal.span ({(p : ℤ)} : Set ℤ) ≠ ⊥ := by simp
       apply ((@Ring.DimensionLeOne.prime_le_prime_iff_eq _ _ _ _ _ H5 H2 H4).1 H1).symm
     have hxyinP : (x + y : R) ∈ P := by

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -91,7 +91,7 @@ lemma isCoprime_of_not_zeta_sub_one_dvd (hx : ¬ (hζ.unit' : 𝓞 K) - 1 ∣ x)
     Ideal.mem_span_singleton]
   · simpa only [ge_iff_le, tsub_pos_iff_lt] using hpri.out.one_lt
 
-set_option synthInstance.maxHeartbeats 40000 in
+set_option synthInstance.maxHeartbeats 80000 in
 lemma exists_zeta_sub_one_dvd_sub_Int (a : 𝓞 K) : ∃ b : ℤ, (hζ.unit' - 1: 𝓞 K) ∣ a - b := by
   letI : AddGroup (𝓞 K ⧸ Ideal.span (singleton (hζ.unit' - 1: 𝓞 K))) := inferInstance
   letI : Fact (Nat.Prime p) := hpri
@@ -162,7 +162,7 @@ lemma IsPrimitiveRoot.sub_one_dvd_sub {A : Type*} [CommRing A] [IsDomain A]
   · rw [h, sub_self]; exact dvd_zero _
   · exact (hζ.associated_sub_one hp hη₁ hη₂ h).dvd
 
-set_option synthInstance.maxHeartbeats 40000 in
+set_option synthInstance.maxHeartbeats 80000 in
 lemma quotient_zero_sub_one_comp_aut (σ : 𝓞 K →+* 𝓞 K) :
     (Ideal.Quotient.mk (Ideal.span {(hζ.unit' : 𝓞 K) - 1})).comp σ = Ideal.Quotient.mk _ := by
   have : Fact (Nat.Prime p) := hpri

FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean

@@ -321,16 +321,17 @@ lemma IsUnit.eq_mul_left_iff {S : Type*} [CommRing S] {x : S} (hx : IsUnit x) (y
   nth_rw 1 [← one_mul x]
   rw [eq_comm, hx.mul_left_injective.eq_iff]
 
-lemma map_two {S T F: Type*} [NonAssocSemiring S] [NonAssocSemiring T]
+lemma map_two {S T F: Type*} [NonAssocSemiring S] [NonAssocSemiring T] [FunLike F S T]
   [RingHomClass F S T] (f : F) : f 2 = 2 := by
   rw [← one_add_one_eq_two, map_add, map_one]
   exact one_add_one_eq_two
 
 lemma neg_one_eq_one_iff_two_eq_zero {M : Type*} [AddGroupWithOne M] : (-1 : M) = 1 ↔ (2 : M) = 0 := by
   rw [neg_eq_iff_add_eq_zero, one_add_one_eq_two]
 
-lemma Units.coe_map_inv' {M N F : Type*} [Monoid M] [Monoid N] [MonoidHomClass F M N]
-  (f : F) (m : Mˣ) : ↑((Units.map (f : M →* N) m)⁻¹) = f ↑(m⁻¹ : Mˣ) :=
+lemma Units.coe_map_inv' {M N F : Type*} [Monoid M] [Monoid N] [FunLike F M N]
+    [MonoidHomClass F M N] (f : F) (m : Mˣ) :
+    ↑((Units.map (f : M →* N) m)⁻¹) = f ↑(m⁻¹ : Mˣ) :=
   m.coe_map_inv (f : M →* N)
 
 lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) :
@@ -366,6 +367,7 @@ lemma unit_inv_conj_not_neg_zeta_runity_aux (u : Rˣ) (hp : (p : ℕ).Prime) :
     rw [this a]
   exact (aux hζ hζ hu).trans (aux hζ hζ.inv hu').symm
 
+set_option synthInstance.maxHeartbeats 40000 in
 theorem unit_inv_conj_not_neg_zeta_runity (h : p ≠ 2) (u : Rˣ) (n : ℕ) (hp : (p : ℕ).Prime) :
     u * (unitGalConj K p u)⁻¹ ≠ -hζ.unit' ^ n := by
   by_contra H

FltRegular/NumberTheory/CyclotomicRing.lean

@@ -73,6 +73,7 @@ lemma one_sub_zeta_mem_nonZeroDivisors :
 lemma not_isUnit_one_sub_zeta :
     ¬ IsUnit (1 - zeta p) := (prime_one_sub_zeta p).irreducible.1
 
+set_option synthInstance.maxHeartbeats 40000 in
 lemma one_sub_zeta_dvd_int_iff (n : ℤ) : 1 - zeta p ∣ n ↔ ↑p ∣ n := by
   letI p' : ℕ+ := ⟨p, hpri.out.pos⟩
   letI : Fact (PNat.Prime p') := hpri
@@ -90,6 +91,7 @@ lemma isCoprime_one_sub_zeta (n : ℤ) (hn : ¬ (p : ℤ) ∣ n) : IsCoprime (1
     (algebraMap ℤ <| CyclotomicIntegers p)).of_isCoprime_of_dvd_left
   exact one_sub_zeta_dvd p
 
+set_option synthInstance.maxHeartbeats 80000 in
 lemma exists_dvd_int (n : CyclotomicIntegers p) (hn : n ≠ 0) : ∃ m : ℤ, m ≠ 0 ∧ n ∣ m := by
   refine ⟨Algebra.norm ℤ ((equiv p) n), by simpa, ?_⟩
   rw [← map_dvd_iff (equiv p), map_intCast]

FltRegular/NumberTheory/Different.lean

@@ -74,7 +74,7 @@ lemma pow_sub_one_dvd_differentIdeal_aux
     obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)
     have : Algebra.trace K L (algebraMap B L z) ∈ (p : FractionalIdeal A⁰ K)
     · rw [← Algebra.algebraMap_intTrace (A := A)]
-      exact Submodule.mem_map_of_mem (this z hz)
+      exact ⟨intTrace A B z, this z hz, rfl⟩
     rwa [mul_comm, ← smul_eq_mul, ← LinearMap.map_smul, Algebra.smul_def, mul_comm,
       ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B L, ← hz']
   intros x hx

FltRegular/NumberTheory/Hilbert90.lean

@@ -7,7 +7,7 @@ import Mathlib.Tactic.Widget.Conv
 import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90
 
 open scoped NumberField nonZeroDivisors
-open FiniteDimensional Finset BigOperators Submodule
+open FiniteDimensional Finset BigOperators Submodule groupCohomology
 
 variable {K L : Type*} [Field K] [Field L] [NumberField K] [Algebra K L]
 variable [IsGalois K L] [FiniteDimensional K L]
@@ -84,7 +84,7 @@ lemma cocycle_spec (hone : orderOf σ ≠ 1) : (cocycle hσ hη) σ = (ηu hη)
   simp only [cocycle, SetLike.coe_sort_coe, horder, this, range_one, prod_singleton, pow_zero]
   rfl
 
-lemma is_cocycle : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β) =
+lemma is_cocycle_aux : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β) =
     α ((cocycle hσ hη) β) * (cocycle hσ hη) α := by
   intro α β
   have hσmon : ∀ x, x ∈ Submonoid.powers σ := by
@@ -106,6 +106,10 @@ lemma is_cocycle : ∀ (α β : (L ≃ₐ[K] L)), (cocycle hσ hη) (α * β) =
   rw [← prod_range_add (fun (n : ℕ) ↦ (σ ^ n) (ηu hη)) (a % orderOf σ) (b % orderOf σ)]
   simpa using bar hσ hη (by simp)
 
+lemma is_cocycle : IsMulOneCocycle (cocycle hσ hη) := by
+  intro α β
+  simp [← Units.eq_iff, is_cocycle_aux hσ hη α β]
+
 lemma Hilbert90 : ∃ ε : L, η = ε / σ ε := by
   by_cases hone : orderOf σ = 1
   · suffices finrank K L = 1 by
@@ -118,14 +122,18 @@ lemma Hilbert90 : ∃ ε : L, η = ε / σ ε := by
     refine ⟨σ, fun τ ↦ ?_⟩
     simp only [orderOf_eq_one_iff.1 hone, Subgroup.zpowers_one_eq_bot, Subgroup.mem_bot] at hσ
     rw [orderOf_eq_one_iff.1 hone, hσ τ]
-  obtain ⟨ε, hε⟩ := hilbert90 _ (is_cocycle hσ hη)
-  use ε
+  obtain ⟨ε, hε⟩ := isMulOneCoboundary_of_isMulOneCocycle_of_aut_to_units _ (is_cocycle hσ hη)
+  use ε⁻¹
+  simp only [map_inv₀, div_inv_eq_mul]
   specialize hε σ
-  rw [cocycle_spec hσ hη hone] at hε
-  nth_rewrite 1 [← hε]
-  simp
+  nth_rewrite 2 [← inv_inv ε] at hε
+  rw [div_inv_eq_mul, cocycle_spec hσ hη hone, mul_inv_eq_iff_eq_mul, mul_comm, ← Units.eq_iff] at hε
+  simp only [AlgEquiv.smul_units_def, Units.coe_map, MonoidHom.coe_coe, Units.val_mul] at hε
+  symm
+  rw [inv_mul_eq_iff_eq_mul₀ ε.ne_zero, hε]
   rfl
 
+
 variable {A B} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Algebra A K]
 variable [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K] [IsDomain A]
 variable [IsIntegralClosure B A L] [IsDomain B]
@@ -153,8 +161,9 @@ lemma Hilbert90_integral (σ : L ≃ₐ[K] L) (hσ : ∀ x, x ∈ Subgroup.zpowe
   · rw [eq_div_iff_mul_eq] at hε
     replace hε := congr_arg (t • ·) hε
     simp only at hε
-    rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t, ← AlgHom.coe_coe,
-      ← AlgHom.map_smul_of_tower, this] at hε
+    rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t] at hε
+    change (algebraMap B L) η * t • σ.toAlgHom _ = _ at hε
+    rw [← AlgHom.map_smul_of_tower, this] at hε
     apply IsIntegralClosure.algebraMap_injective B A L
     rw [map_mul, ← hε]
     congr 1

FltRegular/NumberTheory/Hilbert92.lean

@@ -251,6 +251,8 @@ lemma coe_galRestrictHom_apply (σ : K →ₐ[k] K) (x) :
     (galRestrictHom (𝓞 k) k K (𝓞 K) σ x : K) = σ x :=
   algebraMap_galRestrictHom_apply (𝓞 k) k K (𝓞 K) σ x
 
+set_option synthInstance.maxHeartbeats 160000 in
+set_option maxHeartbeats 400000 in
 noncomputable
 def relativeUnitsMap (σ : K →ₐ[k] K) : RelativeUnits k K →* RelativeUnits k K := by
   apply QuotientGroup.lift _
@@ -299,6 +301,8 @@ lemma pow_finEquivZPowers_symm_apply {M} [Group M] (x : M) (hx) (a) :
     x ^ ((finEquivZPowers x hx).symm a : ℕ) = a :=
   congr_arg Subtype.val ((finEquivZPowers x hx).apply_symm_apply a)
 
+set_option synthInstance.maxHeartbeats 160000 in
+set_option maxHeartbeats 400000 in
 open Polynomial in
 lemma isTors' : Module.IsTorsionBySet ℤ[X]
     (Module.AEval' (addMonoidEndRingEquivInt _
@@ -474,6 +478,7 @@ lemma unitlifts_spec (S : systemOfUnits p G (NumberField.Units.rank k + 1)) (i)
   simp only [toMul_ofMul, Quotient.out_eq', ofMul_toMul]
   exact Quotient.out_eq' _
 
+set_option synthInstance.maxHeartbeats 80000 in
 lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : (mkG u) = (1 - zeta p : A) • (mkG v) := by
   rw [sub_smul, one_smul, relativeUnitsModule_zeta_smul, ← unit_to_U_div]
   congr
@@ -587,7 +592,7 @@ lemma lh_pow_free' {M} [CommGroup M] [Module.Finite ℤ (Additive M)] (ζ : M)
       (Fin.succAbove i₁.castSucc) ι₂ 0, i₁.castSucc, ?_, ?_, fun H ↦ (hζ' H).elim⟩
   · rw [sub_mul, eq_sub_iff_add_eq.mpr h₁, eq_sub_iff_add_eq.mpr h₂]
     simp only [zsmul_eq_mul, Pi.coe_int, Int.cast_id, Pi.sub_apply, Pi.mul_apply,
-      Fin.exists_succ_eq_iff, ne_eq, not_not, not_exists, sub_sub_sub_cancel_left]
+      Fin.succAbove_of_le_castSucc, ne_eq, not_not, not_exists, sub_sub_sub_cancel_left]
     simp only [sub_smul, mul_smul, ← e₁, ← e₂, sum_sub_distrib]
     rw [Fin.sum_univ_castSucc, Fin.sum_univ_succAbove _ i₁.castSucc]
     simp [(Fin.castSucc_injective r).extend_apply, Fin.succAbove_right_injective.extend_apply,
@@ -715,6 +720,7 @@ lemma norm_eq_prod_pow_gen
 
 attribute [-instance] instCoeOut
 
+set_option synthInstance.maxHeartbeats 160000 in
 lemma Hilbert92ish_aux0 (h : ℕ) (ζ : (𝓞 k)ˣ) (hζ : IsPrimitiveRoot (ζ : k) (p ^ h))
   (H : ∀ ε : (𝓞 K)ˣ, algebraMap k K ζ ^ ((p : ℕ) ^ (h - 1)) ≠ ε / (σ ε : K)) :
     ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by
@@ -736,6 +742,7 @@ lemma Hilbert92ish_aux0 (h : ℕ) (ζ : (𝓞 k)ˣ) (hζ : IsPrimitiveRoot (ζ :
       SubmonoidClass.coe_pow]
     rfl
 
+set_option synthInstance.maxHeartbeats 160000 in
 lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : (𝓞 k)ˣ)
     (a : ℤ) (ι : Fin n → ℤ) (η : Fin n → Additive (𝓞 k)ˣ)
     (ha : ∑ i : Fin n, ι i • η i = (a * ↑↑p) • Additive.ofMul ζ)
@@ -788,8 +795,6 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
 
 
 attribute [-instance] instDecidableEq Fintype.decidableForallFintype
-attribute [local instance 2000] MulHomClass.toDFunLike Classical.propDecidable
-
 lemma unit_to_U_pow (x) (n : ℕ) : mkG (x ^ n) = n • (mkG x) := by
   induction n with
   | zero => simp [unit_to_U_one]
@@ -807,6 +812,7 @@ lemma unit_to_U_map (x : (𝓞 k)ˣ) : mkG (Units.map (algebraMap (𝓞 k) (𝓞
   rw [ofMul_eq_zero, QuotientGroup.eq_one_iff]
   exact ⟨_, rfl⟩
 
+set_option synthInstance.maxHeartbeats 160000 in
 lemma unit_to_U_neg (x) : mkG (-x) = mkG x := by
   rw [← one_mul x, ← neg_mul, unit_to_U_mul, one_mul, add_left_eq_self]
   convert unit_to_U_map p hp hKL σ hσ (-1)
@@ -827,6 +833,8 @@ lemma Algebra.norm_of_finrank_eq_two (hKL : finrank k K = 2) (x : K) :
   rfl
 
 -- TODO : remove `p ≠ 2`. The offending case is when `K = k[i]`.
+set_option synthInstance.maxHeartbeats 160000 in
+set_option maxHeartbeats 400000 in
 lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
     ∃ η : (𝓞 K)ˣ, Algebra.norm k (η : K) = 1 ∧ ∀ ε : (𝓞 K)ˣ, (η : K) ≠ ε / (σ ε : K) := by
   classical

FltRegular/NumberTheory/IdealNorm.lean

@@ -145,9 +145,6 @@ theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R
     (Algebra.algebraMapSubmonoid S M) Sₘ L
   haveI : IsIntegralClosure Sₘ Rₘ L :=
     IsIntegralClosure.of_isIntegrallyClosed _ _ _ (Algebra.IsIntegral.of_finite (R := Rₘ) (B := Sₘ))
-  cases h : subsingleton_or_nontrivial R
-  · haveI := IsLocalization.unique R Rₘ M
-    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/QuotientTrace.lean

@@ -45,7 +45,9 @@ theorem quotient_span_eq_top_iff_span_eq_top_of_localRing (s : Set S) :
       rw [← this, ← Submodule.comap_map_eq, Submodule.mem_comap, ← H, hs]
       trivial
   · intro hs
-    rwa [hs, Submodule.map_top, LinearMap.range_eq_top.mpr Ideal.Quotient.mk_surjective,
+    rw [hs, Submodule.map_top] at H
+    change _ = LinearMap.range (Ideal.Quotient.mkₐ _ _) at H
+    rwa [LinearMap.range_eq_top.mpr (Ideal.Quotient.mkₐ_surjective _ _),
       Submodule.restrictScalars_eq_top_iff] at H
 
 theorem finrank_quotient_map_of_localRing :

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "f1cae6351cf7010d504e6652f05e8aa2da0dd4cb",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "190ec9abbc4cd43b1b6a1401722c0b54418a98b0",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "1f200b89e635064ba6f614ae82c7aced0b28d929",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.28",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "9618fa9d33d128679a5e376a9ffd3c9440b088f4",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "7f6325178f4a6a093fcecb905a0077b3a9e9db76",
+   "rev": "9ff7dbc133122ef393ea8b98883281947d3f3c78",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,