mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.ExistsUnique
/-- For `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`.  -/
ExistsUnique : {α : Sort u_1} → (α → Prop) → Prop
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_mul : ∀ (a b : BitVec 64), Int64.ofBitVec (a * b) = Int64.ofBitVec a * Int64.ofBitVec b
-- Init.Data.Order.Ord
Std.instReflCmpCompareLex : ∀ {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [Std.ReflCmp cmp₁] [Std.ReflCmp cmp₂],
  Std.ReflCmp (compareLex cmp₁ cmp₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.isEmpty = true ↔
    ∀ (k : α) (h : Std.DTreeMap.Internal.Impl.contains k t = true), f k (t.get k h) = false
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Generators.C_mul_X_sub_one_mem_ker : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  MvPolynomial.C r * MvPolynomial.X () - 1 ∈ (Algebra.Generators.localizationAway S r).ker
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.distinct_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) (Std.DTreeMap.Const.toList t)
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.continuous_equiv_symm : ∀ {ι : Type t} {X : ι → Type u} {inst : (i : ι) → TopologicalSpace (X i)} {Y : Type v} {tY : TopologicalSpace Y}
  [self : Topology.IsGeneratedBy X Y], Continuous ⇑Topology.WithGeneratedByTopology.equiv.symm
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_mem_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.NumberTheory.LegendreSymbol.Basic
legendreSym.eq_1 : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (a : ℤ), legendreSym p a = (quadraticChar (ZMod p)) ↑a
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.associator_hom_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] {E' : Type u₃}
  [inst_5 : CategoryTheory.EnrichedCategory V E'] (F : CategoryTheory.EnrichedFunctor V C D)
  (G : CategoryTheory.EnrichedFunctor V D E) (H : CategoryTheory.EnrichedFunctor V E E')
  (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.associator F G H).hom.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (H.obj (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to V X)))))
-- Mathlib.MeasureTheory.Integral.MeanInequalities
/-- A version of Hölder with multiple arguments, one of which plays a distinguished role.  -/
ENNReal.lintegral_mul_prod_norm_pow_le : ∀ {α : Type u_2} {ι : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} (s : Finset ι)
  {g : α → ENNReal} {f : ι → α → ENNReal},
  AEMeasurable g μ →
    (∀ i ∈ s, AEMeasurable (f i) μ) →
      ∀ (q : ℝ) {p : ι → ℝ},
        q + ∑ i ∈ s, p i = 1 →
          0 ≤ q →
            (∀ i ∈ s, 0 ≤ p i) →
              ∫⁻ (a : α), g a ^ q * ∏ i ∈ s, f i a ^ p i ∂μ ≤
                (∫⁻ (a : α), g a ∂μ) ^ q * ∏ i ∈ s, (∫⁻ (a : α), f i a ∂μ) ^ p i
-- Mathlib.FieldTheory.IntermediateField.Algebraic
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K]` is finite,
then `F = E` iff `[F : K] = [E : K]`.  -/
IntermediateField.eq_iff_finrank_eq_of_le : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  [FiniteDimensional K ↥E], F ≤ E → (F = E ↔ Module.finrank K ↥F = Module.finrank K ↥E)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_sub_comm : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a b : α), |a - b| = |b - a|
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- See also `Ideal.mem_quotient_iff_mem` in case `I ≤ J`.  -/
Ideal.mem_quotient_iff_mem_sup : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] {x : R},
  (Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J ⊔ I
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.toFun_eq_coe : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion), K.toFun = ⇑K
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_dvd_finrank_top_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → A.relfinrank B ∣ Module.finrank (↥A) E
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.lt_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} (entry : Std.Sat.AIG.Entrypoint α)
  (input : β entry.aig len), entry.ref.gate < (f entry.aig input).aig.decls.size
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.monotone_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N}, Monotone (Subsemigroup.map f)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instHasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Limits.HasTerminal (CategoryTheory.Factorisation f)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_right_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.id b)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.Bicategory.rightUnitor (self.map f)).hom)
-- Mathlib.Data.Fin.Fin2
/-- `0` as a member of `Fin (n + 1)` (`Fin 0` is empty)  -/
Fin2.fz : {n : ℕ} → Fin2 (n + 1)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse_unique : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a) {g : F → E},
  (∀ᶠ (x : E) in nhds a, g (f x) = x) → ∀ᶠ (y : F) in nhds (f a), g y = HasStrictFDerivAt.localInverse f f' a hf y
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- The mates equivalence commutes with vertical composition.  -/
CategoryTheory.mateEquiv_vcomp : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {D : Type u₄} {E : Type u₅} {F : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] [inst_3 : CategoryTheory.Category.{v₄, u₄} D]
  [inst_4 : CategoryTheory.Category.{v₅, u₅} E] [inst_5 : CategoryTheory.Category.{v₆, u₆} F]
  {G₁ : CategoryTheory.Functor A C} {G₂ : CategoryTheory.Functor C E} {H₁ : CategoryTheory.Functor B D}
  {H₂ : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor A B} {R₁ : CategoryTheory.Functor B A}
  {L₂ : CategoryTheory.Functor C D} {R₂ : CategoryTheory.Functor D C} {L₃ : CategoryTheory.Functor E F}
  {R₃ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃)
  (α : CategoryTheory.TwoSquare G₁ L₁ L₂ H₁) (β : CategoryTheory.TwoSquare G₂ L₂ L₃ H₂),
  (CategoryTheory.mateEquiv adj₁ adj₃) (α.hComp β) =
    ((CategoryTheory.mateEquiv adj₁ adj₂) α).vComp ((CategoryTheory.mateEquiv adj₂ adj₃) β)
-- Mathlib.LinearAlgebra.Matrix.Basis
/-- See also `Basis.toMatrix_reindex` which gives the `simp` normal form of this result.  -/
Module.Basis.toMatrix_reindex' : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι'] [inst_4 : Fintype ι] [inst_5 : DecidableEq ι] [inst_6 : DecidableEq ι']
  (b : Module.Basis ι R M) (v : ι' → M) (e : ι ≃ ι'),
  (b.reindex e).toMatrix v = (Matrix.reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))
-- Lean.Meta.Tactic.Grind.AC.DenoteExpr
Lean.Meta.Grind.AC.DiseqCnstr.denoteExpr : {M : Type → Type} → [Monad M] → [Lean.Meta.Grind.AC.MonadGetStruct M] → Lean.Meta.Grind.AC.DiseqCnstr → M Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.trans_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] (e₁ : α ≃ᵐ β) (e₂ : β ≃ᵐ γ), (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.prod_apply : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] {ι : Type u_3} (s : Finset ι)
  [inst_2 : CommMonoid R] [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R] (f : ι → BoundedContinuousFunction α R)
  (a : α), (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.subsemigroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (s : UpperSet (MulArchimedeanClass M)),
  MulArchimedeanClass.subsemigroup s = { carrier := MulArchimedeanClass.mk ⁻¹' ↑s, mul_mem' := ⋯ }
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofIsoSelf_hom : ∀ {R : Type u} [inst : CommRing R] (A : CommHopfAlgCat R), A.ofIsoSelf.hom = CategoryTheory.CategoryStruct.id A
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.right_assoc' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Bimod.TensorBimod.X P Q) CategoryTheory.MonObj.mul)
      (Bimod.TensorBimod.actRight P Q) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (Bimod.TensorBimod.X P Q) T.X T.X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.TensorBimod.actRight P Q) T.X)
        (Bimod.TensorBimod.actRight P Q))
-- Mathlib.Topology.Separation.Basic
isClosedMap_prodMk_right : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space Y] (y : Y),
  IsClosedMap fun x => (x, y)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.toAddMonoidHom_injective : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Function.Injective ContinuousAddMonoidHom.toAddMonoidHom
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (f g : Turing.ToPartrec.Code)
  (h_1 : Unit → motive Turing.ToPartrec.Code.zero') (h_2 : Unit → motive Turing.ToPartrec.Code.succ)
  (h_3 : Unit → motive Turing.ToPartrec.Code.tail) (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs))
  (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g)) (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g))
  (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match f.comp g with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_5 f g
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.coe_centralizer_centralizer : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : IsScalarTower R A A] [inst_5 : SMulCommClass R A A] (s : Set A),
  ↑(NonUnitalStarSubalgebra.centralizer R ↑(NonUnitalStarSubalgebra.centralizer R s)) =
    (s ∪ star s).centralizer.centralizer
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (x : R), x ∈ ⊤
-- Mathlib.Order.PFilter
Order.PFilter.mem_mk : ∀ {P : Type u_1} [inst : Preorder P] (x : P) (I : Order.Ideal Pᵒᵈ), x ∈ { dual := I } ↔ OrderDual.toDual x ∈ I
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is an additive monoid object, then `Hom(X, M)` has an additive monoid structure.  -/
CategoryTheory.Hom.addMonoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → {M X : C} → [CategoryTheory.AddMonObj M] → AddMonoid (X ⟶ M)
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel (without cancellation hook).

Returns an iterator that yields results in original order, wrapped in `Except Exception α`.
 -/
Lean.Meta.MetaM.parIter : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (Std.IterM Lean.MetaM (Except Lean.Exception α))
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `i` is an isomorphism such that `cokernel.π f ≫ i.hom = l`, then `l` is a cokernel of `f`.  -/
CategoryTheory.Limits.cokernel.cokernelIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            {Z : C} →
              (l : Y ⟶ Z) →
                (i : CategoryTheory.Limits.cokernel f ≅ Z) →
                  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) i.hom = l) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ l ⋯)
-- Mathlib.Data.Set.Finite.Basic
Set.card_ne_eq : ∀ {α : Type u} [inst : Fintype α] (a : α) [inst_1 : Fintype ↑{x | x ≠ a}],
  Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1
-- Mathlib.SetTheory.Cardinal.Order
/-- **Alias** of `exists_wellFoundedLT`.

---

The **well-ordering theorem** (or **Zermelo's theorem**): every type can be well-ordered.  -/
exists_wellOrder : ∀ (α : Type u), ∃ x, WellFoundedLT α
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.applySimprocConst : Lean.Expr → Lean.Name → Array Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.filter_equiv_self_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF → ((Std.HashMap.Raw.filter f m).Equiv m ↔ ∀ (a : α) (h : a ∈ m), f (m.getKey a h) m[a] = true)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.instCoeTypeForall_1 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.id_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂),
  ContinuousLinearMap.id R₂ M₂ ∘SL f = f
-- Mathlib.Tactic.MinImports
/-- `#min_imports in cmd` scans the syntax `cmd` and the declaration obtained by elaborating `cmd`
to find a collection of minimal imports that should be sufficient for `cmd` to work.  -/
Mathlib.Command.MinImports.minImpsStx : Lean.ParserDescr
-- Lean.Parser.Do
Lean.Parser.Term.doFinally : Lean.Parser.Parser
-- Lean.Meta.Tactic.Backtrack
Lean.Meta.Tactic.Backtrack.BacktrackConfig.mk.sizeOf_spec : ∀ (maxDepth : ℕ) (proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (suspend : Lean.MVarId → Lean.MetaM Bool) (discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (commitIndependentGoals : Bool),
  sizeOf
      { maxDepth := maxDepth, proc := proc, suspend := suspend, discharge := discharge,
        commitIndependentGoals := commitIndependentGoals } =
    1 + sizeOf maxDepth + sizeOf commitIndependentGoals
-- Mathlib.NumberTheory.NumberField.DirichletDensity
_private.Mathlib.NumberTheory.NumberField.DirichletDensity.0.NumberField.Set.HasDirichletDensity.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (S : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (δ : ℝ),
  NumberField.Set.HasDirichletDensity S δ =
    Filter.Tendsto (fun s => NumberField.Set.primeIdealZetaSum S s / NumberField.Set.primeIdealZetaSum Set.univ s)
      (nhdsWithin 1 (Set.Ioi 1)) (nhds δ)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatMono
/-- [Stacks Tag 06NC](https://stacks.math.columbia.edu/tag/06NC) -/
AlgebraicGeometry.Flat.isIso_of_surjective_of_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.QuasiCompact f]
  [AlgebraicGeometry.Surjective f] [CategoryTheory.Mono f], CategoryTheory.IsIso f
-- Mathlib.Order.Cover
WithBot.coe_covBy_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ↑b ⋖ ↑a ↔ b ⋖ a
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ofHom_hom : ∀ {M N : CommMonCat} (f : M ⟶ N), CommMonCat.ofHom (CommMonCat.Hom.hom f) = f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter_eq_self_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF →
    k ∈ m → (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true → (Std.DHashMap.Raw.Const.alter m k f).size = m.size
-- Init.Meta.Defs
/-- Decodes a character literal.

Returns `(default : Char)` if the syntax is malformed.
 -/
Lean.TSyntax.getChar : Lean.CharLit → Char
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.one_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : MulOneClass P]
  (f : M →* N), MonoidHom.comp 1 f = 1
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.log_two_mul_two_le_sqrt_log_eight : Real.log 2 * 2 ≤ √(Real.log 8)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.instInhabited : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → [Inhabited Ω] → Inhabited (MeasureTheory.ProbabilityMeasure Ω)
-- Mathlib.Logic.Equiv.Defs
Equiv.forall₃_congr' : ∀ {α₁ : Sort u_1} {α₂ : Sort u_2} {β₁ : Sort u_3} {β₂ : Sort u_4} {γ₁ : Sort u_5} {γ₂ : Sort u_6}
  {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (eγ : γ₁ ≃ γ₂),
  (∀ {x : α₂} {y : β₂} {z : γ₂}, p (eα.symm x) (eβ.symm y) (eγ.symm z) ↔ q x y z) →
    ((∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z)
-- Init.Data.Vector.Basic
/-- Note that the universe level is constrained to `Type` here,
to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 -/
Vector.findM? : {n : ℕ} → {α : Type} → {m : Type → Type} → [Monad m] → (α → m Bool) → Vector α n → m (Option α)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.foldM_filter : ∀ {α β δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad m] [LawfulMonad n] [inst_6 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Bool} {g : δ → β → n δ}
  {init : δ} {it : Std.IterM m β},
  Std.IterM.foldM g init (Std.IterM.filter f it) =
    Std.IterM.foldM (fun d b => if f b = true then g d b else pure d) init it
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is one if the characteristic is zero.  -/
expChar_one_of_char_zero : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (q : ℕ) [hp : CharP R 0] [hq : ExpChar R q], q = 1
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiff.div₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : GroupWithZero G] [ContMDiffInv₀ I n G]
  [ContMDiffMul I n G] {E' : Type u_5} [inst_9 : NormedAddCommGroup E'] [inst_10 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_11 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {f g : M → G},
  ContMDiff I' I n f → ContMDiff I' I n g → (∀ (x : M), g x ≠ 0) → ContMDiff I' I n (f / g)
-- Mathlib.GroupTheory.Transfer
MonoidHom.transferCenterPow_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : (Subgroup.center G).FiniteIndex] (g : G),
  ↑((MonoidHom.transferCenterPow G) g) = g ^ (Subgroup.center G).index
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.lid_comm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (x : TensorProduct R M R), (TensorProduct.lid R M) ((TensorProduct.comm R M R) x) = (TensorProduct.rid R M) x
-- Mathlib.SetTheory.Lists
Lists.ofList.eq_1 : ∀ {α : Type u_1} (l : List (Lists α)), Lists.ofList l = Lists.of' (Lists'.ofList l)
-- Mathlib.Order.Disjoint
Codisjoint.sup_left : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b : α} (c : α),
  Codisjoint a b → Codisjoint (a ⊔ c) b
-- Init.Data.Array.QSort.Basic
/-- Sort an array using `compare` to compare elements.
 -/
Array.qsortOrd : {α : Type u_1} → [ord : Ord α] → Array α → Array α
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.coe_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv) (n : ℕ), ↑(f ^ n) = ↑f ^ n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α}
  {h' : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl = true},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getKey a h' = t.getKey a ⋯
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_subConst : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.subConst B) = ↑(A - B).card / ↑A.card
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.lid_symm_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W) (w : W), (Representation.TensorProduct.lid A σ).symm w = 1 ⊗ₜ[A] w
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Set.Ioi x) x
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalFVarId_qq : Lean.Meta.ReduceEval Lean.FVarId
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.Isometry.single_apply : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : AddCommMonoid P] [inst_3 : (i : ι) → Module R (Mᵢ i)]
  [inst_4 : Module R P] [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (Q : (i : ι) → QuadraticMap R (Mᵢ i) P) (i : ι)
  (x : Mᵢ i) (j : ι), (QuadraticMap.Isometry.single Q i) x j = Pi.single i x j