mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.throw_ExceptT_lift : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α ε' : Type u} {e : ε} [inst : Std.Do.WP m ps]
  [inst_1 : MonadExceptOf ε m] (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' ps)),
  ⦃(Std.Do.wp (MonadExceptOf.throw e)).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)⦄ MonadExceptOf.throw e ⦃Q⦄
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.isSolvable_def`. -/
isSolvable_def : ∀ (G : Type u_1) [inst : Group G], Group.IsSolvable G ↔ ∃ n, derivedSeries G n = ⊥
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `MulActionSemiHomClass F φ X Y` states that
`F` is a type of morphisms which are `φ`-equivariant.

You should extend this class when you extend `MulActionHom`.  -/
MulActionSemiHomClass : (F : Type u_8) →
  {M : outParam (Type u_9)} →
    {N : outParam (Type u_10)} →
      outParam (M → N) →
        (X : outParam (Type u_11)) → (Y : outParam (Type u_12)) → [SMul M X] → [SMul N Y] → [FunLike F X Y] → Prop
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.lt_def : ∀ {M : Type u_1} [inst : AddGroup M] [inst_1 : Lattice M] {a b : ArchimedeanOrder M},
  a < b ↔ ∀ (n : ℕ), n • |ArchimedeanOrder.val b| < |ArchimedeanOrder.val a|
-- Mathlib.Topology.Category.LightProfinite.Basic
instEssentiallySmallLightProfinite : CategoryTheory.EssentiallySmall.{u, u, u + 1} LightProfinite
-- Mathlib.Algebra.Category.MonCat.Limits
/-- If `J` is `u`-small, `AddCommMonCat.{u}` has limits of shape `J`.  -/
AddCommMonCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J AddCommMonCat
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from `Expr` to a variable representing it.  -/
Lean.Meta.Grind.Arith.CommRing.Ring.varMap : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var
-- Mathlib.FieldTheory.Galois.Profinite
/-- The (finite) Galois group `Gal(L / k)` associated to a
`L : FiniteGaloisIntermediateField k K` `L`.  -/
FiniteGaloisIntermediateField.finGaloisGroup : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → FiniteGaloisIntermediateField k K → FiniteGrp.{u_2}
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.leadingCoeff_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : MulZeroOneClass R],
  HahnSeries.leadingCoeff 1 = 1
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_zero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K L : HomologicalComplex C c) (e : c.Embedding c'),
  HomologicalComplex.extendMap 0 e = 0
-- Mathlib.Order.Category.Lat
Lat.coe_id : ∀ {X : Lat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Lean.Structure
Lean.instInhabitedStructureParentInfo.default : Lean.StructureParentInfo
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (FreeAddMonoid α)
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.rfl : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {A : Set X}, CovByVAdd M 1 A A
-- Mathlib.Data.List.Sort
/-- The list obtained from a strictly monotone tuple is sorted.  -/
List.SortedLT.strictMono : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedLT → StrictMono f
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_abs_zsmul : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E) (n : ℤ), ‖|n| • a‖₊ = ‖n • a‖₊
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.preimage_coe_Ioc_bot : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithBot.some ⁻¹' Set.Ioc ⊥ ↑a = Set.Iic a
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.throwApplyError : {α : Type} → Lean.MVarId → Lean.Expr → Option Lean.Expr → Lean.Expr → Option Lean.MessageData → Lean.MetaM α
-- Lean.Expr
/-- Given `a b : Int`, returns `a = b`  -/
Lean.mkIntEq : Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.sign_eq_tdiv_abs : ∀ (a : ℤ), a.sign = a.tdiv ↑a.natAbs
-- Init.Notation
Lean.instCoeSyntaxNodeKindSyntaxNodeKinds : Coe Lean.SyntaxNodeKind Lean.SyntaxNodeKinds
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.coe_flip_mul : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R], ⇑AddMonoidHom.mul.flip = AddMonoidHom.mulRight
-- Mathlib.Data.ENat.BigOperators
/-- Seeing `ℕ∞` as `ℕ` does not change their sum, unless one of the `ℕ∞` is
infinity  -/
ENat.toNat_sum : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, (∀ a ∈ s, f a ≠ ⊤) → (∑ a ∈ s, f a).toNat = ∑ a ∈ s, (f a).toNat
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.coe_ofContinuousOpen : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  ↑(PartialHomeomorph.ofContinuousOpen e hc ho hs) = ↑e
-- Mathlib.Algebra.Order.Module.Defs
IsStrictOrderedModule.toPosSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero α}
  {inst_4 : Zero β} [self : IsStrictOrderedModule α β], PosSMulStrictMono α β
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret a linear isometry equiv as an affine isometry equiv.  -/
LinearIsometryEquiv.toAffineIsometryEquiv : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : SeminormedAddCommGroup V₂] → [inst_4 : NormedSpace 𝕜 V₂] → (V ≃ₗᵢ[𝕜] V₂) → V ≃ᵃⁱ[𝕜] V₂
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_pow : ∀ {x : ENNReal} {n : ℕ}, (x ^ n).log = ↑n * x.log
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.boundary : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f : ↑(GenLoop N X x)),
  ∀ y ∈ Cube.boundary N, f y = x
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of `SimpleGraph.not_mem_edgeSet_of_isDiag`. -/
Sym2.IsDiag.not_mem_edgeSet : ∀ {V : Type u} (G : SimpleGraph V) {e : Sym2 V}, e.IsDiag → e ∉ G.edgeSet
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.comp_sub : ∀ {𝕜 : 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] {f : E → F} {s : Set E},
  AnalyticOnNhd 𝕜 f s → ∀ (y : E), AnalyticOnNhd 𝕜 (fun z => f (z - y)) (s + {y})
-- Lean.Expr
/-- A total order for expressions. We say it is quick because it first compares the hashcodes.  -/
Lean.Expr.quickLt : Lean.Expr → Lean.Expr → Bool
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_1 : FirstOrder.Field.FieldAxiom.addAssoc.toSentence =
  (((FirstOrder.Language.var ∘ Sum.inr) 0 + (FirstOrder.Language.var ∘ Sum.inr) 1 +
              (FirstOrder.Language.var ∘ Sum.inr) 2).bdEqual
          ((FirstOrder.Language.var ∘ Sum.inr) 0 +
            ((FirstOrder.Language.var ∘ Sum.inr) 1 + (FirstOrder.Language.var ∘ Sum.inr) 2))).all.all.all
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.

More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
`L` if it exists, and `0` otherwise.

(Note that even if the unconditional sum exists, it might not be unique if the topology is not
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum
over the support. Otherwise, we choose arbitrarily an `a` satisfying `HasSum f a`. Similar remarks
apply to more general summation filters.)
 -/
tsum_def : ∀ {α : Type u_4} {β : Type u_5} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α)
  (L : SummationFilter β),
  tsum f L =
    if h : Summable f L then
      if L.HasSupport ∧ (Function.support f ∩ L.support).Finite then finsum (L.support.indicator f)
      else if HasSum f 0 L then 0 else Exists.choose h
    else 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.contDiffWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → ContDiffWithinAt 𝕜 n f s x
-- Mathlib.GroupTheory.Abelianization.Defs
/-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map
from the abelianization of a `G` to `A` that factors through `f`.  -/
Abelianization.lift : {G : Type u} → [inst : Group G] → {A : Type v} → [inst_1 : CommGroup A] → (G →* A) ≃ (Abelianization G →* A)
-- Lean.Expr
/-- Expression metadata. Used with the `Expr.mdata` constructor.  -/
Lean.MData : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.π_desc'_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W)
  (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.π
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.IsColimit.desc hs k h) h_1) =
    CategoryTheory.CategoryStruct.comp k h_1
-- Init.Prelude
/-- The underlying `Syntax` value.  -/
Lean.TSyntax.raw : {ks : Lean.SyntaxNodeKinds} → Lean.TSyntax ks → Lean.Syntax
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.val_pos : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π → 0 < v π
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.intermediateFieldEquivSubgroup_apply : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  [inst_3 : FiniteDimensional F E] [inst_4 : IsGalois F E] (a : IntermediateField F E),
  IsGalois.intermediateFieldEquivSubgroup a = OrderDual.toDual a.fixingSubgroup
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_ofSet : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β), e.trans (PartialEquiv.ofSet s) = e.restr (↑e ⁻¹' s)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {k a : α} {h' : k ∈ m.erase a}, (m.erase a).get k h' = m.get k ⋯
-- Lean.Meta.SynthInstance
Lean.Meta.synthInstance? : Lean.Expr → optParam (Option ℕ) none → Lean.MetaM (Option Lean.Expr)
-- Lean.Meta.Basic
/-- Determines whether two expressions are definitionally equal to each other.

To control how metavariables are assigned and unified, metavariables and their context have a "depth".
Given a metavariable `?m` and a `MetavarContext` `mctx`, `?m` is not assigned if `?m.depth != mctx.depth`.
The combinator `withNewMCtxDepth x` will bump the depth while executing `x`.
So, `withNewMCtxDepth (isDefEq a b)` is `isDefEq` without any mvar assignment happening
whereas `isDefEq a b` will assign any metavariables of the current depth in `a` and `b` to unify them.

For matching (where only mvars in `b` should be assigned), we create the term inside the `withNewMCtxDepth`.
For an example, see [Lean.Meta.Simp.tryTheoremWithExtraArgs?](https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L100-L106)
 -/
Lean.Meta.isDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.functorCategoryAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type w} →
      [inst_1 : CategoryTheory.Category.{z, w} D] →
        [CategoryTheory.Abelian D] → CategoryTheory.Abelian (CategoryTheory.Functor C D)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zero : ∀ (n : ℕ) [inst : NeZero n], DirichletCharacter.LFunctionTrivChar₁ n 1 ≠ 0
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.go.match_3.eq_4 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (id₁ : ℕ) (rhs : Lean.Expr)
  (rhsTerms : Lean.Meta.Grind.SolverTerms) (id₂ : ℕ) (lhs : Lean.Expr) (lhsTerms : Lean.Meta.Grind.SolverTerms)
  (h_1 : Unit → motive Lean.Meta.Grind.SolverTerms.nil Lean.Meta.Grind.SolverTerms.nil)
  (h_2 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive Lean.Meta.Grind.SolverTerms.nil (Lean.Meta.Grind.SolverTerms.next solverId e rest))
  (h_3 :
    (solverId : ℕ) →
      (e : Lean.Expr) →
        (rest : Lean.Meta.Grind.SolverTerms) →
          motive (Lean.Meta.Grind.SolverTerms.next solverId e rest) Lean.Meta.Grind.SolverTerms.nil)
  (h_4 :
    (id₁ : ℕ) →
      (rhs : Lean.Expr) →
        (rhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (lhs : Lean.Expr) →
              (lhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms with
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.nil => h_1 ()
    | Lean.Meta.Grind.SolverTerms.nil, Lean.Meta.Grind.SolverTerms.next solverId e rest => h_2 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next solverId e rest, Lean.Meta.Grind.SolverTerms.nil => h_3 solverId e rest
    | Lean.Meta.Grind.SolverTerms.next id₁ rhs rhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ lhs lhsTerms =>
      h_4 id₁ rhs rhsTerms id₂ lhs lhsTerms) =
    h_4 id₁ rhs rhsTerms id₂ lhs lhsTerms
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.toOuterRegular : ∀ {α : Type u_1} {inst : MeasurableSpace α} {inst_1 : TopologicalSpace α} {μ : MeasureTheory.Measure α}
  [self : μ.WeaklyRegular], μ.OuterRegular
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.G.mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)),
  (∃ k f g,
      (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd = (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd) →
    AddGrpCat.FilteredColimits.G.mk F x = AddGrpCat.FilteredColimits.G.mk F y
-- Mathlib.Computability.RE
Partrec.cond : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Bool} {f g : α →. σ},
  Computable c → Partrec f → Partrec g → Partrec fun a => bif c a then f a else g a
-- Mathlib.Topology.Separation.Hausdorff
T2Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (Pairwise fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) → T2Space X
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.addCommMonoid.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommMonoid α],
  Finset.addCommMonoid = Function.Injective.addCommMonoid SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- Noncomputably defines a `StrongNormalizationMonoid` structure on a `UniqueFactorizationMonoid`.
 -/
UniqueFactorizationMonoid.strongNormalizationMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → StrongNormalizationMonoid α
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ) (g : α →*o β),
  f.comp g = { toMonoidHom := f.comp ↑g, monotone' := ⋯ }
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_neg : ∀ {A : Type u_1} {G : Type u_2} [inst : Semiring A] [inst_1 : Monoid G] {V : Type u_6} {W : Type u_7}
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommGroup W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ), ⇑(-f) = -⇑f
-- Mathlib.Algebra.Free
/-- Lifts a function `α → β` to an additive magma homomorphism `FreeAddMagma α → β` given
an additive magma `β`.  -/
FreeAddMagma.liftAux : {α : Type u} → {β : Type v} → [Add β] → (α → β) → FreeAddMagma α → β
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.graphRel.adj.sizeOf_spec : sizeOf FirstOrder.Language.graphRel.adj = 1
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_one : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] [inst_2 : DecidableEq n],
  Matrix.toMvPolynomial 1 = MvPolynomial.X
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, Std.DHashMap.Raw.Const.get? (m.erase k) k = none
-- Mathlib.Order.Bounds.Image
Antitone.image_upperBounds_subset_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → ∀ {s : Set α}, f '' upperBounds s ⊆ lowerBounds (f '' s)
-- Mathlib.Logic.Equiv.Prod
optionProdEquiv_symm_inr : ∀ {α : Type u_9} {β : Type u_10} (p : α × β), optionProdEquiv.symm (Sum.inr p) = Prod.map some id p
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_inclusion_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {hst : t ⊆ s},
  Function.Injective ⇑(SubMulAction.ofFixingSubgroup_of_inclusion M hst)
-- Init.Data.Int.Basic
Int.instMin : Min ℤ
-- Mathlib.Tactic.Ring.Basic
/-- Applies `Nat.cast` to a nat polynomial to produce a polynomial in `α`.

* An atom `e` causes `↑e` to be allocated as a new atom.
* A sum delegates to `ExSum.evalNatCast`.
 -/
Mathlib.Tactic.Ring.ExBase.evalNatCast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          (sβ : Q(CommSemiring «$β»)) →
            {a : Q(ℕ)} →
              Mathlib.Tactic.Ring.ExBase sβ a →
                Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.ExBase sα) q(↑«$a»))
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The monoidal category struct constructed in `DayConvolution.mkMonoidalCategoryStruct` extends
to a `LawfulDayConvolutionMonoidalCategoryStruct`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mkLawfulDayConvolutionMonoidalCategoryStruct : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  [inst_6 :
                      ∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    [inst_7 :
                        ∀ (v : V) (d : C),
                          CategoryTheory.Limits.PreservesColimitsOfShape
                            (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
                            (CategoryTheory.MonoidalCategory.tensorRight v)] →
                      [inst_8 :
                          ∀ (v : V) (d : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape
                              (CategoryTheory.CostructuredArrow
                                (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                d)
                              (CategoryTheory.MonoidalCategory.tensorRight v)] →
                        [inst_9 :
                            ∀ (v : V) (d : C),
                              CategoryTheory.Limits.PreservesColimitsOfShape
                                (CategoryTheory.CostructuredArrow
                                  (CategoryTheory.Functor.fromPUnit
                                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                  d)
                                (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                          CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `PreservesCofilteredLimitsOfSizeShrink.{w, w'} F` tries to obtain
`PreservesCofilteredLimitsOfSize.{w, w'} F` from some other `PreservesCofilteredLimitsOfSize F`.
 -/
CategoryTheory.Limits.preservesCofilteredLimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbolParams : Lean.ToJson Lean.Lsp.DocumentSymbolParams
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instBooleanAlgebra : {α : Type u_1} →
  [inst : TopologicalSpace α] → [CompactSpace α] → [T2Space α] → BooleanAlgebra (TopologicalSpace.CompactOpens α)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasStrictFDerivAt.sub` -/
HasStrictFDerivAt.fun_sub : ∀ {𝕜 : 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 g : E → F}
  {f' g' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt g g' x → HasStrictFDerivAt (fun i => f i - g i) (f' - g') x
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableOn.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableOn 𝕜 c s → ∀ (d : 𝕜'), DifferentiableOn 𝕜 (fun x => c x / d) s
-- Mathlib.MeasureTheory.Constructions.Pi
IsUnifLocDoublingMeasure.doublingConstant.congr_simp : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ μ_1 : MeasureTheory.Measure α)
  (e_μ : μ = μ_1) [inst_2 : IsUnifLocDoublingMeasure μ],
  IsUnifLocDoublingMeasure.doublingConstant μ = IsUnifLocDoublingMeasure.doublingConstant μ_1
-- Mathlib.Combinatorics.Enumerative.Stirling
/-- `Nat.stirlingSecond n k` is the Stirling number of the second kind,
counting the number of ways to partition a set of `n` elements into `k` nonempty subsets.
 -/
Nat.stirlingSecond : ℕ → ℕ → ℕ
-- Std.Data.TreeMap.Iterator
Std.DTreeMap.toList.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp), t.toList = t.inner.toList
-- Std.Time.Format
/-- The leanDateTime24Hour format, which follows the pattern `uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSS` for
representing date, time, and time zone. It uses the default value that can be parsed with the
notation of dates.
 -/
Std.Time.Formats.leanDateTime24Hour : Std.Time.GenericFormat (Std.Time.Awareness.only Std.Time.TimeZone.GMT)
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- Extensions for handling abstraction boundaries for definitions that shouldn't be unfolded.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt : Type