mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instIsCentralScalar : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {R : Type u_2}
  [inst_3 : Zero R] [inst_4 : SMulWithZero R β] [inst_5 : SMulWithZero Rᵐᵒᵖ β] [inst_6 : ContinuousConstSMul R β]
  [inst_7 : IsCentralScalar R β], IsCentralScalar R (ZeroAtInftyContinuousMap α β)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.sum_induction_nonempty : ∀ {M : Type u_3} [inst : AddCommMonoid M] {s : Multiset M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a + b)) → s ≠ ∅ → (∀ a ∈ s, p a) → p s.sum
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- Turn a non-unital subsemiring containing `1` into a subsemiring.  -/
NonUnitalSubsemiring.toSubsemiring : {R : Type u} → [inst : NonAssocSemiring R] → (S : NonUnitalSubsemiring R) → 1 ∈ S → Subsemiring R
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- If `K` is a nonarchimedean normed field `L/K` is a finite extension, then there exists a
power-multiplicative nonarchimedean `K`-algebra norm on `L` extending the norm on `K`.  -/
exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Field L] [inst_2 : Algebra K L],
  FiniteDimensional K L →
    IsNonarchimedean norm → ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f
-- Lean.Server.References
/-- Selection range of the parent declaration.  -/
Lean.Server.References.ParentDecl.selectionRange : Lean.Server.References.ParentDecl → Lean.Lsp.Range
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_σ_self'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.castSucc →
    ∀ {Z : C} (h : X.obj { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.σ i) h) = h
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.of_hom_of_source : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C}
  {Q : CategoryTheory.MorphismProperty C} [self : P.InheritedFromSource Q] {X Y : C} (f : X ⟶ Y), Q f → P X → P Y
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compYonedaIso_hom_app_app_hom_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : D) (X_1 : Cᵒᵖ)
  (x : Opposite.unop X_1 ⟶ G.obj X),
  (CategoryTheory.ConcreteCategory.hom ((adj.compYonedaIso.hom.app X).app X_1)) x =
    CategoryTheory.CategoryStruct.comp (F.map x) (adj.counit.app X)
-- Batteries.Data.Vector.Lemmas
Vector.isNone_finIdxOf? : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α},
  (v.finIdxOf? a).isNone = !v.contains a
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.hom_ofHom : ∀ {X Y : Type u} (f : X → Y), TypeCat.Hom.hom (TypeCat.ofHom f) = { toFun := f }
-- Mathlib.Data.SetLike.Basic
SetLike.exists_of_lt : ∀ {A : Type u_1} {B : Type u_2} [inst : SetLike A B] [inst_1 : PartialOrder A] [IsConcreteLE A B] {p q : A},
  p < q → ∃ x ∈ q, x ∉ p
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.Subgroup.val_conj_smul : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] (g : ConjAct G) (h : ↥H), ↑(g • h) = g • ↑h
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- Prop registering if an open partial homeomorphism is a local diffeomorphism on its source  -/
OpenPartialHomeomorph.MDifferentiable : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] →
                                      [ChartedSpace H' M'] → OpenPartialHomeomorph M M' → Prop
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The lift of an isomorphism `Φ : (ι S).obj a ≅ (ι S).obj b` lying over `𝟙 S` to an isomorphism
in `Fib S`.  -/
HasFibers.Fib.isoMk : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            {S : 𝒮} →
              {a b : HasFibers.Fib p S} →
                (Φ : (HasFibers.ι S).obj a ≅ (HasFibers.ι S).obj b) →
                  p.IsHomLift (CategoryTheory.CategoryStruct.id S) Φ.hom → (a ≅ b)
-- Aesop.Rule.Name
Aesop.PhaseName.safe.sizeOf_spec : sizeOf Aesop.PhaseName.safe = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
`cocycles₁ A`, which is a simpler type.  -/
groupCohomology.isoCocycles₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → groupCohomology.cocycles A 1 ≅ ModuleCat.of k ↥(groupCohomology.cocycles₁ A)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.separatesPoints_of_measurableSingletonClass : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α], MeasurableSpace.SeparatesPoints α
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonDeleteFile : Lean.ToJson Lean.Lsp.DeleteFile
-- Mathlib.Algebra.Polynomial.Identities
_private.Mathlib.Algebra.Polynomial.Identities.0.Polynomial.poly_binom_aux3 : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R) (x y : R),
  Polynomial.eval (x + y) f =
    ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) +
      f.sum fun e a => a * ↑(Polynomial.polyBinomAux1✝ x y e a) * y ^ 2
-- Mathlib.Data.Set.Basic
Set.inter_eq_right : ∀ {α : Type u} {s t : Set α}, s ∩ t = t ↔ t ⊆ s
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents'_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : Y ⟶ X),
        CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) =
          CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv)
      CategoryTheory.NatIso.ofComponents'._auto_1)
  (X : C), (CategoryTheory.NatIso.ofComponents' app naturality).inv.app X = (app X).inv
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instLieRingModuleSubtypeMem : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → (N : LieSubmodule R L M) → LieRingModule L ↥N
-- Mathlib.Algebra.Group.Defs
/-- Any `AddCancelMonoid G` satisfies `IsCancelAdd G`.  -/
AddCancelMonoid.toIsCancelAdd : ∀ (M : Type u) [inst : AddCancelMonoid M], IsCancelAdd M
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β) (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- An additive action is isometric if each map `x ↦ c +ᵥ x` is an isometry.  -/
IsIsometricVAdd : (M : Type u) → (X : Type w) → [PseudoEMetricSpace X] → [VAdd M X] → Prop
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient by a decidable additive congruence relation has decidable equality.  -/
AddCon.instDecidableEqQuotientOfDecidableCoeForallProp : {M : Type u_1} → [inst : Add M] → (c : AddCon M) → [(a b : M) → Decidable (c a b)] → DecidableEq c.Quotient
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- The natural map `Φ.X₀ ⟶ (Φ.iterationFunctor J).obj j`.  -/
CategoryTheory.SmallObject.SuccStruct.ιIterationFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Φ : CategoryTheory.SmallObject.SuccStruct C) →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [inst_2 : OrderBot J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : WellFoundedLT J] →
                [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] →
                  (CategoryTheory.Functor.const J).obj Φ.X₀ ⟶ Φ.iterationFunctor J
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.prop_X₁_of_shortExact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderSubobjects] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C},
  S.ShortExact → P S.X₂ → P S.X₁
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H2π_comp_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.H2π A) (groupHomology.map f φ 2) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ) (groupHomology.H2π B)
-- Mathlib.Analysis.Complex.Order
Complex.le_def : ∀ {z w : ℂ}, z ≤ w ↔ z.re ≤ w.re ∧ z.im = w.im
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.zero.eq_1 : ∀ {α : Type u} [inst : Zero α], WithTop.zero = { zero := ↑0 }
-- Lean.Elab.Tactic.Basic
/-- Elaborate `x` with `stx` on the macro stack  -/
Lean.Elab.Tactic.withMacroExpansion : {α : Type} → Lean.Syntax → Lean.Syntax → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKey!_eq_minKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : Std.Internal.List.containsKey (Std.Internal.List.minKey! l) l = true},
      Std.Internal.List.getKey (Std.Internal.List.minKey! l) l he = Std.Internal.List.minKey l ⋯
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.instAssociative : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [inst_1 : c.TensorSigns], c.Associative c c c c c
-- Mathlib.Algebra.Star.Unitary
Unitary.commute_self_star : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (u : ↥(unitary R)), Commute u (star u)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
/-- The product of two finite measures `μ` and `ν` is the only finite measure `ξ` such that
for all real bounded continuous functions `f` and `g` we have
`∫ z, f z.1 * g z.2 ∂ξ = ∫ x, f x ∂μ * ∫ y, g y ∂ν`.  -/
Measure.eq_prod_of_integral_mul_boundedContinuousFunction : ∀ {Z : Type u_3} {T : Type u_4} {mZ : MeasurableSpace Z} [inst : TopologicalSpace Z] [BorelSpace Z]
  [HasOuterApproxClosed Z] {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T]
  [HasOuterApproxClosed T] {μ : MeasureTheory.Measure Z} {ν : MeasureTheory.Measure T}
  {ξ : MeasureTheory.Measure (Z × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : BoundedContinuousFunction Z ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : Z × T), f p.1 * g p.2 ∂ξ = (∫ (z : Z), f z ∂μ) * ∫ (t : T), g t ∂ν) →
    ξ = μ.prod ν
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
  ProbabilityTheory.IdentDistrib f g μ ν → ProbabilityTheory.IdentDistrib g f ν μ
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.factorThruKernelSubobject.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] {W : C} (h h_1 : W ⟶ X) (e_h : h = h_1)
  (w : CategoryTheory.CategoryStruct.comp h f = 0),
  CategoryTheory.Limits.factorThruKernelSubobject f h w = CategoryTheory.Limits.factorThruKernelSubobject f h_1 ⋯
-- Init.Data.Prod
/-- For two functions `f` and `g`, the composition of `Prod.map f g` with `Prod.swap`
is equal to the composition of `Prod.swap` with `Prod.map g f`.
 -/
Prod.map_comp_swap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ),
  Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, (Std.ExtTreeMap.unitOfList l cmp).contains k = l.contains k
-- Mathlib.Algebra.Module.Submodule.Ker
Submodule.inclusion.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p'), Submodule.inclusion h = LinearMap.codRestrict p' p.subtype ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.semivariation_union_le : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s t : Set X}, μ.semivariation (s ∪ t) ≤ μ.semivariation s + μ.semivariation t
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `SummableLocallyUniformly f` means that `∑' i, f i b` converges locally
uniformly to something.  -/
SummableLocallyUniformly : {α : Type u_1} →
  {β : Type u_2} → {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → [UniformSpace α] → [TopologicalSpace β] → Prop
-- Mathlib.Data.PNat.Defs
PNat.coe_toPNat' : ∀ (n : ℕ+), (↑n).toPNat' = n
-- Mathlib.Tactic.PNatToNat
/-- For each `x : PNat` in the context, add the hypothesis `0 < (↑x : ℕ)`.  -/
Mathlib.Tactic.PNatToNat.tacticPnat_positivity : Lean.ParserDescr
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `Mul` across an `Equiv`  -/
Equiv.mul : {α : Type u_2} → {β : Type u_3} → α ≃ β → [Mul β] → Mul α
-- Lean.Parser.Tactic.Doc
/-- Stores a collection of *tactic alternatives*, to track which new syntax rules represent new forms of
existing tactics.
 -/
Lean.Parser.Tactic.Doc.tacticAlternativeExt : Lean.PersistentEnvExtension (Lean.Name × Lean.Name) (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.range : {α : Type u} → {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RicSliceData α β → Std.Ric α
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_bot : ∀ {α : Type u_1} {β : Type u_2} {g : β → α}, MeasurableSpace.comap g ⊥ = ⊥
-- Mathlib.Order.Disjoint
ComplementedLattice.instOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] [ComplementedLattice α], ComplementedLattice αᵒᵈ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.toList_toArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → m.toArray.toList = m.toList
-- Mathlib.Data.Nat.Log
Nat.log_of_lt : ∀ {b n : ℕ}, n < b → Nat.log b n = 0
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α) (i : n), A.cramer b i = (A.updateCol i b).det
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformAddGroup.cauchy_iff_tendsto_swapped : ∀ {G : Type u_4} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter G),
  Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => p.2 - p.1) (𝓕 ×ˢ 𝓕) (nhds 0)
-- Mathlib.Data.Part
Part.sdiff_get_eq : ∀ {α : Type u_1} [inst : SDiff α] (a b : Part α) (hab : (a \ b).Dom), (a \ b).get hab = a.get ⋯ \ b.get ⋯
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A purely inseparable extension has finite separable degree one.  -/
IsPurelyInseparable.finSepDegree_eq_one : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  Field.finSepDegree F E = 1
-- Init.Data.Float.Float
/-- Checks whether a floating point number is `NaN` (“not a number”) value.

`NaN` values result from operations that might otherwise be errors, such as dividing zero by zero.

This function has a logical model in terms of `Float.Model`. It is compiled to the C operator `isnan`.
 -/
Float.isNaN : Float → Bool
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) ⁻¹' Set.Iio b = Set.Iio (b * a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey? =
        some (t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k')
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G G_1 : C} (e_G : G = G_1) [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ A₀_1 : CategoryTheory.Subobject X),
  A₀ = A₀_1 →
    ∀ (J : Type w) [inst_3 : LinearOrder J] [inst_4 : OrderBot J] [inst_5 : SuccOrder J] [inst_6 : WellFoundedLT J],
      CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor hG A₀ J =
        CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor ⋯ A₀_1 J
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet.toJson : Lean.Lsp.CodeActionLiteralSupportValueSet → Lean.Json
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
/-- The length of a walk is the number of edges/darts along it.  -/
SimpleGraph.Walk.length : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → ℕ
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.differentiableOn_inv_log : DifferentiableOn ℝ (fun x => (Real.log x)⁻¹) (Set.Ioi 1)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts : ∀ {G : Type u_3} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsAddHaarMeasure], MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ ∩ m₂).get! k = default
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.AbelianStruct.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f : X ⟶ Y} [inst_2 : SizeOf C] (kernelFork : CategoryTheory.Limits.KernelFork f)
  (isLimitKernelFork : CategoryTheory.Limits.IsLimit kernelFork)
  (cokernelCofork : CategoryTheory.Limits.CokernelCofork f)
  (isColimitCokernelCofork : CategoryTheory.Limits.IsColimit cokernelCofork) (image : C) (imageπ : X ⟶ image)
  (ι_imageπ :
    autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kernelFork) imageπ = 0)
      CategoryTheory.Abelian.AbelianStruct.ι_imageπ._autoParam)
  (imageIsCokernel : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ imageπ ι_imageπ))
  (imageι : image ⟶ Y)
  (imageι_π :
    autoParam (CategoryTheory.CategoryStruct.comp imageι (CategoryTheory.Limits.Cofork.π cokernelCofork) = 0)
      CategoryTheory.Abelian.AbelianStruct.imageι_π._autoParam)
  (imageIsKernel : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι imageι imageι_π))
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp imageπ imageι = f)
      CategoryTheory.Abelian.AbelianStruct.fac._autoParam),
  sizeOf
      { kernelFork := kernelFork, isLimitKernelFork := isLimitKernelFork, cokernelCofork := cokernelCofork,
        isColimitCokernelCofork := isColimitCokernelCofork, image := image, imageπ := imageπ, ι_imageπ := ι_imageπ,
        imageIsCokernel := imageIsCokernel, imageι := imageι, imageι_π := imageι_π, imageIsKernel := imageIsKernel,
        fac := fac } =
    1 + sizeOf kernelFork + sizeOf isLimitKernelFork + sizeOf cokernelCofork + sizeOf isColimitCokernelCofork +
                    sizeOf image +
                  sizeOf imageπ +
                sizeOf ι_imageπ +
              sizeOf imageIsCokernel +
            sizeOf imageι +
          sizeOf imageι_π +
        sizeOf imageIsKernel +
      sizeOf fac
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coeNat_prime : ∀ (v : PrimeMultiset), ∀ p ∈ v.toNatMultiset, Nat.Prime p
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isTheta_completion_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (fun x => ↑(g x)) =Θ[l] f ↔ g =Θ[l] f
-- Init.Data.Vector.Lemmas
Vector.back_eq_getElem : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] {xs : Vector α n}, xs.back = xs[n - 1]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.Limits.Cofork.ext.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (i i_1 : s.pt ≅ t.pt) (e_i : i = i_1)
  (w : CategoryTheory.CategoryStruct.comp s.π i.hom = t.π),
  CategoryTheory.Limits.Cofork.ext i w = CategoryTheory.Limits.Cofork.ext i_1 ⋯
-- Mathlib.Algebra.Order.Star.Basic
MulOpposite.instStarOrderedRing : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : StarRing R] [inst_2 : PartialOrder R] [StarOrderedRing R],
  StarOrderedRing Rᵐᵒᵖ
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_eraseIdx_of_le : ∀ {α : Type u} {a : α} {n i j : ℕ} {xs : Vector α n} (w₁ : i < n) (w₂ : j ≤ n - 1) (h : j ≤ i),
  (xs.eraseIdx i w₁).insertIdx j a w₂ = Vector.cast ⋯ ((xs.insertIdx j a ⋯).eraseIdx (i + 1) ⋯)
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.lift_natCast`. -/
ENat.lift_coe : ∀ (n : ℕ), (↑n).lift ⋯ = n
-- Lean.Elab.Util
Lean.Elab.expandOptNamedPrio : Lean.Syntax → Lean.MacroM ℕ
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instTypeNameRealizeConstResult : TypeName Lean.Environment.RealizeConstResult✝
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mk : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] →
              {𝒜 : ι → σ} →
                [inst_4 : DecidableEq ι] →
                  [inst_5 : GradedRing 𝒜] →
                    (toSubsemiring : Subsemiring A) →
                      DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring → HomogeneousSubsemiring 𝒜