mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α}
  {fallback : Unit}, Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.Const.unitOfList l) k fallback = ()
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.map_intNormAux : ∀ {A : Type u_1} {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : IsIntegrallyClosed A] (x : B),
  (algebraMap A K) ((Algebra.intNormAux A K L B) x) = (Algebra.norm K) ((algebraMap B L) x)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).obj₃ = (t.truncGE b).obj j
-- Mathlib.Data.List.Rotate
List.Nodup.rotate_congr : ∀ {α : Type u} {l : List α}, l.Nodup → l ≠ [] → ∀ (i j : ℕ), l.rotate i = l.rotate j → i % l.length = j % l.length
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_obj_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C),
  (CategoryTheory.sum.inverseAssociator C D E).obj (Sum.inl X) = Sum.inl (Sum.inl X)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_zero : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [inst_1 : Zero β], AEMeasurable (fun x => 0) μ
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instCoeFunForallSetPresieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CoeFun (CategoryTheory.Precoverage C) fun x => (X : C) → Set (CategoryTheory.Presieve X)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.ncard_primesOver_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K], ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1
-- Batteries.Data.List.Basic
List.sectionsTR.eq_1 : ∀ {α : Type u_1} (L : List (List α)),
  L.sectionsTR = bif L.any List.isEmpty then [] else (List.foldr List.sectionsTR.go #[[]] L).toList
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.toFun.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g), lTensor.toFun Q hfg = lTensor.toFun Q ⋯
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- An element a divides the sum b + a if and only if a divides b.  -/
dvd_add_self_right : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, a ∣ b + a ↔ a ∣ b
-- Mathlib.Order.Minimal
Minimal.and_left : ∀ {α : Type u_2} {P Q : α → Prop} {x : α} [inst : LE α], Minimal P x → Q x → Minimal (fun x => Q x ∧ P x) x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, (m.insertMany l).isEmpty = true → m.isEmpty = true
-- Mathlib.Data.Part
Part.zero_mem_zero : ∀ {α : Type u_1} [inst : Zero α], 0 ∈ 0
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.upperMoebius_lambdaSquared : ∀ (weights : ℕ → ℝ), weights 1 = 1 → BoundingSieve.IsUpperMoebius (BoundingSieve.lambdaSquared weights)
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The norm of a finite extension of integrally closed domains `B/A` is the restriction of
the norm on `Frac(B)/Frac(A)` onto `B/A`. See `Algebra.algebraMap_intNorm`.  -/
Algebra.intNorm : (A : Type u_1) →
  (B : Type u_6) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [IsIntegrallyClosed A] →
            [IsDomain A] →
              [IsDomain B] → [IsIntegrallyClosed B] → [Algebra.IsIntegral A B] → [Module.IsTorsionFree A B] → B →* A
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.hexagon_forward_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv
      (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).inv Z) h))
-- Batteries.Recycling.RBTree.Basic
RBTree.RBMap.instForMValuesOfMonad : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {m : Type u_1 → Type u_2} → [Monad m] → ForM m (RBTree.RBMap.Values α β cmp) β
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.g_h₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {Z : C}
  (h : S₂.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S₁.g (CategoryTheory.CategoryStruct.comp self.h₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Aesop.Index.Basic
Aesop.IndexingMode.format : Aesop.IndexingMode → Std.Format
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedCompBipointedToPointedFst_inv_app_toFun : ∀ (X : Pointed) (a : ((CategoryTheory.Functor.id Pointed).obj X).X),
  (pointedToBipointedCompBipointedToPointedFst.inv.app X).toFun a = a
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If `f` is integrable on intervals `Ioc (a i) b`,
where `a i` tends to -∞, and
`∫ x in a i .. b, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`,
then `f` is integrable on the interval (-∞, b)  -/
MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] {a : ι → ℝ} {f : ℝ → E} (I b : ℝ),
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) →
    Filter.Tendsto a l Filter.atBot →
      Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ) l (nhds I) → MeasureTheory.IntegrableOn f (Set.Iic b) μ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.tensorUnit_whiskerLeft_comp_leftUnitor_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.ε F) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom) h))
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_union_eq_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α), K ⊆ M.coloops → M.closure (X ∪ K) = M.closure X ∪ K
-- Init.Data.List.MinMaxOn
List.foldl.match_1.congr_eq_2 : ∀ {α : Type u_3} {β : Type u_1} (motive : α → List β → Sort u_2) (x : α) (x_1 : List β) (h_1 : (a : α) → motive a [])
  (h_2 : (a : α) → (b : β) → (l : List β) → motive a (b :: l)) (a : α) (b : β) (l : List β),
  x = a →
    x_1 = b :: l →
      (match x, x_1 with
        | a, [] => h_1 a
        | a, b :: l => h_2 a b l) ≍
        h_2 a b l
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A `R`-algebra homomorphism from `A[M]` is uniquely defined by its
values on the functions `single m 1` and `single 1 a`.

See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of `MonoidHom`s because `of` doesn't additivise.  -/
MonoidAlgebra.algHom_ext : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M]
  ⦃φ₁ φ₂ : MonoidAlgebra A M →ₐ[R] B⦄,
  (∀ (m : M), φ₁ (MonoidAlgebra.single m 1) = φ₂ (MonoidAlgebra.single m 1)) →
    φ₁.comp MonoidAlgebra.singleOneAlgHom = φ₂.comp MonoidAlgebra.singleOneAlgHom → φ₁ = φ₂
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModuleFunctor_map_exact : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R)
  (T : CategoryTheory.ShortComplex (ModuleCat R)), T.Exact → (T.map (ModuleCat.localizedModuleFunctor S)).Exact
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.eId.eq_1 : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (X : C), CategoryTheory.eId V X = CategoryTheory.EnrichedCategory.id X
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mk.congr_simp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (carrier carrier_1 : Set M)
  (e_carrier : carrier = carrier_1)
  (fun_mem : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f carrier),
  { carrier := carrier, fun_mem := fun_mem } = { carrier := carrier_1, fun_mem := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ : CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonIso 1).hom (SSet.stdSimplex.face {1}).ι =
  SSet.stdSimplex.δ 0
-- Lean.ResolveName
Lean.getAliasState : Lean.Environment → Lean.AliasState
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalarsComp'_inv_app_hom_apply : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  (f : R →+* S) (g : S →+* T) (gf : R →+* T) (hfg : gf = g.comp f) (X : AlgCat T)
  (a : ↑((AlgCat.restrictScalars g).obj X)), (AlgCat.Hom.hom ((AlgCat.restrictScalarsComp' f g gf hfg).inv.app X)) a = a
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁ ++ s == s₂`  -/
Lean.Grind.AC.SubseqResult.prefix : Lean.Grind.AC.Seq → Lean.Grind.AC.SubseqResult
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lequivCongrLeft_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : Type u_1} (h : ι ≃ κ) (f : DirectSum ι fun i => M i) (k : κ),
  ((DirectSum.lequivCongrLeft R h) f) k = f (h.symm k)
-- Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Pi.algebraMap.eq_1 : ∀ (ι : Type u_1) (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Pi.algebraMap ι R A = { toFun := fun v => ⇑(algebraMap R A) ∘ v, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM_lpMeas : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  [inst_3 : CompleteSpace F'] (f : ↥(MeasureTheory.lpMeas F' ℝ m 1 μ)), (MeasureTheory.condExpL1CLM F' hm μ) ↑f = ↑f
-- Std.Internal.Do.Triple.SpecLemmas
/-- Specification for `forIn` over a `Lean.Loop`. The cursor is `β ⊕ β`: `.inl b` means
"still iterating with `b`", `.inr b` means "finished with result `b`".
 -/
Std.Internal.Do.Spec.forIn_loop : ∀ {β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [Lean.Order.MonadTail m]
  [inst_2 : Std.Internal.Do.Assertion Pred] [inst_3 : Std.Internal.Do.Assertion EPred]
  [inst_4 : Std.Internal.Do.WPMonad m Pred EPred] {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)}
  (measure : Std.Internal.Do.RepeatVariant β) (inv : Std.Internal.Do.RepeatInvariant β β Pred) (einv : EPred),
  (∀ (b : β),
      ⦃ inv (Sum.inl b) ⦄ f () b ⦃ fun r =>
        match r with
        | ForInStep.yield b' =>
          Lean.Order.meet (Lean.Order.CompleteLattice.ofProp (measure b' < measure b)) (inv (Sum.inl b'))
        | ForInStep.done b' => inv (Sum.inr b');
        einv ⦄) →
    ⦃ inv (Sum.inl init) ⦄ forIn l init f ⦃ fun b => inv (Sum.inr b); einv ⦄
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.rccIterator : {α : Type u_1} → {β : α → Type u_2} → [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → α → α → Std.Iter ((a : α) × β a)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.cone_pt : ∀ (P : ProfiniteAddGrp.{u}), P.cone.pt = P
-- Mathlib.Computability.EpsilonNFA
NFA.toεNFA_correct : ∀ {α : Type u} {σ : Type v} (M : NFA α σ), M.toεNFA.accepts = M.accepts
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given an initial object of `J` and that the morphisms in the
diagram are isomorphisms, show the cone `coconeOfDiagramInitial` is a colimit.  -/
CategoryTheory.Limits.colimitOfDiagramInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          (hX : CategoryTheory.Limits.IsInitial X) →
            (F : CategoryTheory.Functor J C) →
              [inst_2 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfDiagramInitial hX F)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km fallback : α},
  t.maxKey? = some km → t.getKeyD km fallback = km
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- `if ... then ... else` characterization of a set of vectors being orthonormal.  (Inner product
equals Kronecker delta.)  -/
orthonormal_subtype_iff_ite : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : DecidableEq E] {s : Set E},
  Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, inner 𝕜 v w = if v = w then 1 else 0
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_vcomp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {g : E → F} {f : 𝕜 → E} {x : 𝕜}
  {n : WithTop ℕ∞} {i : ℕ},
  ContDiffAt 𝕜 n g (f x) →
    ContDiffAt 𝕜 n f x →
      ↑i ≤ n →
        iteratedDeriv i (g ∘ f) x = ∑ c, (iteratedFDeriv 𝕜 c.length g (f x)) fun j => iteratedDeriv (c.partSize j) f x
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
isQuasiregular_iff_isUnit' : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {x : A}, IsQuasiregular x ↔ IsUnit (1 + ↑x)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mul_nonsing_inv_cancel_right : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) (B : Matrix m n α), IsUnit A.det → B * A * A⁻¹ = B
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertMany_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {l : List (α × β)}, (↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- For a functor `F : J ⥤ C`, if `J` has an initial object and all the morphisms in the diagram
are isomorphisms, then the image of the initial object is isomorphic to the colimit of `F`.  -/
CategoryTheory.Limits.colimitOfInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasInitial J] →
            [inst_3 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] →
              CategoryTheory.Limits.colimit F ≅ F.obj (⊥_ J)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- The common part of the proofs of `le_nhds_of_cauchy_adhp` and
`SequentiallyComplete.le_nhds_of_seq_tendsto_nhds`: if for any entourage `s`
one can choose a set `t ∈ f` of diameter `s` such that it contains a point `y`
with `(x, y) ∈ s`, then `f` converges to `x`.  -/
le_nhds_of_cauchy_adhp_aux : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α},
  (∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) → f ≤ nhds x
-- Mathlib.Algebra.Order.Group.Synonym
toColex_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : α}, toColex a = 0 ↔ a = 0
-- Mathlib.Combinatorics.Graph.Delete
Graph.restrict_edgeSet_inter : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (F : Set β), G.restrict (G.edgeSet ∩ F) = G.restrict F
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The real part of the inner product, in terms of the norm.  -/
re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y) = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4
-- Std.Time.Format.Modifier
Std.Time.DayPeriod.midnight.sizeOf_spec : sizeOf Std.Time.DayPeriod.midnight = 1
-- Mathlib.NumberTheory.Zsqrtd.ToReal
/-- The image of `Zsqrtd` in `ℝ`, using `Real.sqrt` which takes the positive root of `d`.

If the negative root is desired, use `toReal h (star a)`.  -/
Zsqrtd.toReal : {d : ℤ} → 0 ≤ d → ℤ√d →+* ℝ
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instIsCancelSMulSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul M' α]
  [IsCancelSMul M' α], IsCancelSMul (↥s) α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldr_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.DTreeMap.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run a tactic (given as a string) at each proof step, with optional timing.

`label` is the human-readable name shown in output (e.g., "grind").
`tacticStr` is the tactic syntax as a string (e.g., "grind +suggestions").
Tactic sequences like "simp; grind" are also supported.

Reports elapsed time in milliseconds for each successful replacement
when `linter.tacticAnalysis.tryAtEachStep.showTiming` is true.
To limit tactic runtime, use `set_option maxHeartbeats N` in the build command.

When `linter.tacticAnalysis.tryAtEachStep.selfReplacements` is false, cases where
the suggested tactic matches the existing proof are suppressed.
 -/
Mathlib.TacticAnalysis.tryAtEachStepFromStrings : String → String → Mathlib.TacticAnalysis.Config
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.sum_map_count_dedup_eq_length : ∀ {α : Type u_2} [inst : DecidableEq α] (l : List α), (List.map (fun x => List.count x l) l.dedup).sum = l.length
-- Mathlib.Order.SupClosed
image_latticeClosure : ∀ {α : Type u_3} {β : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] (s : Set α) (f : α → β),
  (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
    (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → f '' latticeClosure s = latticeClosure (f '' s)
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instOfNatQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    {n : ℕ} → [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → OfNat (Lean.Grind.Ring.OfSemiring.Q α) n
-- Mathlib.Order.Filter.Map
Filter.eventually_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {p : α → Prop},
  (∀ᶠ (a : α) in Filter.comap f l, p a) ↔ ∀ᶠ (b : β) in l, ∀ (a : α), f a = b → p a
-- Init.ShareCommon
ShareCommonT.monadShareCommon : {m : Type u_1 → Type u_2} → {σ : ShareCommon.StateFactory} → [Monad m] → MonadShareCommon (ShareCommonT σ m)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_erase_eq_of_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).min? = t.min?
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Functor.sectionsFunctor_obj : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w)),
  (CategoryTheory.Functor.sectionsFunctor J).obj F = ↑F.sections
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.copy.eq_1 : ∀ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) (s : Set M) (hs : s = ↑S),
  S.copy s hs = { carrier := s, add_mem' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_hom_assoc : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.OplaxRightLinear C] (d : D) {Z : D'}
  (h : F.obj d ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).hom h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom) h
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.continuous_of_continuous_eval : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : ContinuousAdd 𝕜] [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace α] {g : α → WeakDual 𝕜 E},
  (∀ (y : E), Continuous fun a => (g a) y) → Continuous g
-- Mathlib.Control.Random
/-- Generate a random `Nat`.  -/
Rand.next : {g : Type} → {m : Type → Type u_1} → [RandomGen g] → [Monad m] → RandGT g m ℕ