mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Ker
/-- The kernel of a linear map `f : M → M₂` is defined to be `comap f ⊥`. This is equivalent to the
set of `x : M` such that `f x = 0`. The kernel is a submodule of `M`.  -/
LinearMap.ker : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] → [inst_5 : Module R₂ M₂] → {τ₁₂ : R →+* R₂} → (M →ₛₗ[τ₁₂] M₂) → Submodule R M
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_toSubsemiring : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (m : M)
  (S : Subring R), (m • S).toSubsemiring = m • S.toSubsemiring
-- Mathlib.Data.Set.Lattice
Set.iInter_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (s : ι → ι' → Set α), ⋂ i, ⋂ i', s i i' = ⋂ i', ⋂ i, s i i'
-- Lean.Elab.Command
/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state.  -/
Lean.Elab.Command.wrapAsync : {α β : Type} →
  (α → Lean.Elab.Command.CommandElabM β) →
    Option IO.CancelToken → Lean.Elab.Command.CommandElabM (α → EIO Lean.Exception β)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSubtractionMonoid : {α : Type u_1} → [SubtractionMonoid α] → SubtractionMonoid αᵒᵈ
-- Std.Async.Signal
/-- User-defined signal 2.
 -/
Std.Async.Signal.sigusr2 : Std.Async.Signal
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- Structure containing the two adjunctions of an adjoint triple `F ⊣ G ⊣ H`.  -/
CategoryTheory.Adjunction.Triple : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor D C → CategoryTheory.Functor C D → Type (max (max (max u_1 u_2) v_1) v_2)
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- The coercion from `Set.Icc 0 1` as a `MonoidWithZeroHom`.  -/
Set.Icc.coeMonoidWithZeroHom : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [inst_2 : IsOrderedRing R] → ↑(Set.Icc 0 1) →*₀ R
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.map_inf : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N N₂ : LieSubmodule R L M},
  Function.Injective ⇑f → LieSubmodule.map f (N ⊓ N₂) = LieSubmodule.map f N ⊓ LieSubmodule.map f N₂
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {n : Type u_4} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (M : Matrix n n R) (f : R →+* S), (M.map ⇑f).charpoly = Polynomial.map f M.charpoly
-- Mathlib.Logic.Relation
/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
`a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image
of some `a' : α` under `f`, and `a'` and `a` are related by `rα`.  -/
Relation.Fibration : {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → (β → β → Prop) → (α → β) → Prop
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.hasProjectiveDimensionLE_iff_forall_maximalSpectrum : ∀ {R : Type u} [inst : CommRing R] (n : ℕ) [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M],
  CategoryTheory.HasProjectiveDimensionLE M n ↔
    ∀ (m : MaximalSpectrum R), CategoryTheory.HasProjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
-- Init.Data.List.Find
List.idxOf_le_length : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, List.idxOf a l ≤ l.length
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.lt : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.unop_hom_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ),
  (β_ X Y).hom.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).hom
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCocone_pt : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q), c.toCocone.pt = c.pt
-- Mathlib.Topology.MetricSpace.Isometry
MetricSpace.isometry_induced : ∀ {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) [m : MetricSpace β], Isometry f
-- Mathlib.Order.SetNotation
iSup.eq_1 : ∀ {α : Type u} {ι : Sort v} [inst : SupSet α] (s : ι → α), iSup s = sSup (Set.range s)
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.add : {m : Type → Type} →
  {α β σ : Type} →
    [Monad m] →
      [Lean.MonadResolveName m] →
        [Lean.MonadEnv m] →
          Lean.ScopedEnvExtension α β σ → β → optParam Lean.AttributeKind Lean.AttributeKind.global → m Unit
-- Std.Http.Server.Connection
/-- The set of I/O sources to wait on during a single poll iteration.
Each `Option` field is `none` when that source is not currently active.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources : Type → Type → Type
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux : (s : String) → s.Pos → Lean.Name → String → ℕ → Lean.Name
-- Mathlib.Topology.Constructions.SumProd
Continuous.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Continuous f → Continuous g → Continuous (Sum.elim f g)
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Lattice.BicartSq.le₁₃ : ∀ {T : Type u} {x₁ x₂ x₃ x₄ : T} [inst : Lattice T], Lattice.BicartSq x₁ x₂ x₃ x₄ → x₁ ≤ x₃
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_of_indiscreteTopology : ∀ {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Add N] [IndiscreteTopology N], ContinuousAdd N
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instConcreteCategoryContIntertwiningMapVρ : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → CategoryTheory.ConcreteCategory (TopRep k G) fun A B => ContIntertwiningMap A.ρ B.ρ
-- Mathlib.Order.CompleteLattice.Chain
chainClosure_maxChain : ∀ {α : Type u_1} {r : α → α → Prop}, ChainClosure r (maxChain r)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
SzemerediRegularity.increment_isEquipartition : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ), (SzemerediRegularity.increment hP G ε).IsEquipartition
-- Init.Data.SInt.Lemmas
ISize.toInt64_ofNat : ∀ {n : ℕ}, n ≤ 2147483647 → (OfNat.ofNat n).toInt64 = OfNat.ofNat n
-- Mathlib.Data.Set.Basic
Set.mem_union : ∀ {α : Type u} (x : α) (a b : Set α), x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.linearEquiv_symm_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {S : Type u_3}
  [inst_2 : Ring S] [inst_3 : Module R S] (v : Valuation S Γ₀) (x : S),
  (WithVal.linearEquiv R v).symm x = WithVal.toVal v x
-- Mathlib.Algebra.Group.Commute.Units
/-- If the sum of two commuting elements is an additive unit, then the right summand
is an additive unit.  -/
AddUnits.rightOfAdd : {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (a b : M) → a + b = ↑u → AddCommute a b → AddUnits M
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_right_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₂.size ≤ (m₁ ∪ m₂).size
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁_self : ∀ (q : Turing.PartrecToTM2.Λ'), q ∈ Turing.PartrecToTM2.trStmts₁ q
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coe_algebraMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : CommSemiring R]
  [inst_2 : Semiring Y] [inst_3 : Algebra R Y] (r : R),
  ⇑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R (X → Y)) r
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given a morphism property `P` in a category `C`, a morphism `f : F ⟶ G` of presheaves in the
category `Cᵒᵖ ⥤ Type v` satisfies the morphism property `P.presheaf` iff:
* The morphism is representable.
* For any morphism `g : F.obj a ⟶ G`, the property `P` holds for any represented pullback of
  `f` by `g`.

This is implemented as a special case of the more general notion of `P.relative`, to the case when
the functor `F` is `yoneda`.  -/
CategoryTheory.MorphismProperty.presheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty (CategoryTheory.Functor Cᵒᵖ (Type v₁))
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.isOpen_baseSet : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (self : VectorBundleCore R B F ι) (i : ι),
  IsOpen (self.baseSet i)
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.symm_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f : HomotopyEquiv C D), f.symm.inv = f.hom
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_dvd_iff_modMonomial_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} {x : MvPolynomial σ R},
  MvPolynomial.X i ∣ x ↔ (x.modMonomial fun₀ | i => 1) = 0
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E), T.IsPositive = ((↑T).IsSymmetric ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x)
-- Mathlib.Logic.Small.Basic
small_Pi : ∀ {α : Type u_2} (β : α → Type u_1) [Small.{w, u_2} α] [∀ (a : α), Small.{w, u_1} (β a)],
  Small.{w, max u_1 u_2} ((a : α) → β a)
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- For propositions and terms of types, we store a rewrite theorem that unfolds it.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfolds : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries → Lean.NameMap Lean.Meta.SimpTheorem
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofFin : ∀ (n : Fin USize.size), (USize.ofFin n).toBitVec = { toFin := n }
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars.congr_simp : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] (c c_1 : ℕ → 𝕜),
  c = c_1 → ∀ (n : ℕ), FormalMultilinearSeries.ofScalars E c n = FormalMultilinearSeries.ofScalars E c_1 n
-- Mathlib.Data.FP.Basic
FP.Float : [C : FP.FloatCfg] → Type
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.uliftFunctor_obj : ∀ (X : AddGrpCat), AddGrpCat.uliftFunctor.obj X = AddGrpCat.of (ULift.{u, v} ↑X)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_eq_some_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {a : α} {h : m.contains a = true},
      Std.DHashMap.Internal.Raw₀.Const.get? m a = some (Std.DHashMap.Internal.Raw₀.Const.get m a h)
-- Lean.Expr
Lean.ExprStructEq.val : Lean.ExprStructEq → Lean.Expr
-- Std.Time.Internal.Bounded
/-- Convert a `Nat` to a `Bounded.LE` by wrapping it.
 -/
Std.Time.Internal.Bounded.LE.ofNatWrapping : {lo hi : ℤ} → ℤ → lo ≤ hi → Std.Time.Internal.Bounded.LE lo hi
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.instCoeQuotientSubgroup.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α}, QuotientGroup.instCoeQuotientSubgroup = { coe := QuotientGroup.mk }
-- Mathlib.RingTheory.PicardGroup
/-- When a flat `R`-module `M` is embedded as a submodule of a faithful `R`-algebra `A`,
we have `I ⊗[R] M ≃ₗ[R] I * M` for any `R`-submodule `I` of `A`.  -/
Module.Flat.tensorSubmoduleAlgebraEquivMul : {R : Type u} →
  {M : Type v} →
    {A : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                (e : TensorProduct R A M ≃ₗ[A] A) →
                  [Module.Flat R M] →
                    [FaithfulSMul R A] →
                      (I : Submodule R A) →
                        TensorProduct R ↥I ↥(Module.Flat.submoduleAlgebra e) ≃ₗ[R] ↥(I * Module.Flat.submoduleAlgebra e)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Cat.instBraidedCategory : CategoryTheory.BraidedCategory CategoryTheory.Cat
-- Mathlib.Data.PFun
PFun.fix.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β ⊕ α) (a : α),
  f.fix a =
    Part.assert (Acc (fun x y => Sum.inr x ∈ f y) a) fun h =>
      WellFounded.fixF
        (fun a IH =>
          Part.assert (f a).Dom fun hf =>
            match e : (f a).get hf with
            | Sum.inl b => Part.some b
            | Sum.inr a' => IH a' ⋯)
        a h
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- As for products, any functor between categories with biproducts gives rise to a morphism
`F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f)`.  -/
CategoryTheory.Functor.biproductComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} →
              (F : CategoryTheory.Functor C D) →
                (f : J → C) →
                  [inst_4 : CategoryTheory.Limits.HasBiproduct f] →
                    [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] → F.obj (⨁ f) ⟶ ⨁ F.obj ∘ f
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.homogeneousHull_mono : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜],
  Monotone (Ideal.homogeneousHull 𝒜)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey! k = default
-- Mathlib.CategoryTheory.Category.PartialFun
/-- Turns a type into a `PartialFun`.  -/
PartialFun.of : Type u_1 → PartialFun
-- Batteries.Lean.EStateM
EStateM.run_tryCatch : ∀ {σ ε α δ : Type u_1} [h : EStateM.Backtrackable δ σ] (body : EStateM ε σ α) (handler : ε → EStateM ε σ α) (s : σ),
  (tryCatch body handler).run s =
    match body.run s with
    | EStateM.Result.ok x s => EStateM.Result.ok x s
    | EStateM.Result.error e s' => (handler e).run (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s))
-- Mathlib.Control.EquivFunctor.Instances
EquivFunctorPerm : EquivFunctor Equiv.Perm
-- Mathlib.Order.Defs.PartialOrder
instTransLELT : {α : Type u_1} → [inst : Preorder α] → Trans LE.le LT.lt LT.lt
-- Mathlib.Algebra.Group.TransferInstance
Equiv.zero_def : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Zero β], 0 = e.symm 0
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
/-- A nonempty set is scaled by zero to the singleton set containing 0.  -/
Set.zero_smul_set : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] {s : Set β},
  s.Nonempty → 0 • s = 0
-- Mathlib.Order.LiminfLimsup
Filter.limsSup_eq_iInf_sSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {f : Filter α}, f.limsSup = ⨅ s ∈ f, sSup s
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.isGaussian_map_equiv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  [BorelSpace E] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] (L : E ≃L[ℝ] F),
  ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ)
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_of_core : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_of_core_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≠ Int.Internal.Linear.Poly.denote' ctx p₂ →
      Int.Internal.Linear.Poly.denote' ctx p₃ ≠ 0
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemKind.comma : Lean.Json.CompressWorkItemKind✝
-- Init.WFComputable
/-- A computable version of `Acc.ndrec`.  -/
Acc.ndrecC : {α : Sort u_1} →
  {r : α → α → Prop} →
    {C : α → Sort v} →
      ((x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) → {a : α} → Acc r a → C a
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.instLiesOverMaximalIdeal : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [IsLocalHom (algebraMap R S)],
  (IsLocalRing.maximalIdeal S).LiesOver (IsLocalRing.maximalIdeal R)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of.inj : ∀ {carrier : Type u} {str : TopologicalSpace carrier} {carrier_1 : Type u} {str_1 : TopologicalSpace carrier_1},
  TopCat.of carrier = TopCat.of carrier_1 → carrier = carrier_1 ∧ str ≍ str_1
-- Init.Data.UInt.Basic
instNegUInt8 : Neg UInt8
-- Init.Prelude
/-- Converts a `String` into a `Substring` that denotes the entire string.

This is a version of `String.toRawSubstring` that doesn't have an `@[inline]` annotation.
 -/
String.toRawSubstring' : String → Substring.Raw
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.Const.modifyKey : {α : Type u} → {β : Type v} → [BEq α] → α → (β → β) → List ((_ : α) × β) → List ((_ : α) × β)
-- Init.Data.Fin.Fold
Fin.foldl.loop.eq_1 : ∀ {α : Sort u_1} (n : ℕ) (f : α → Fin n → α) (x : α) (i : ℕ),
  Fin.foldl.loop n f x i = if h : i < n then Fin.foldl.loop n f (f x ⟨i, h⟩) (i + 1) else x
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_closure_iff_exists_list : ∀ {R : Type u_1} [inst : Semiring R] {s : Set R} {x : R},
  x ∈ Subsemiring.closure s ↔ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.clm_postcomp : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₂ →L[𝕜] F₃} {s : Set M}
  {x : M}, MDiffAt[s] f x → (MDiffAt[s] fun y => ContinuousLinearMap.postcomp F₁ (f y)) x
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.isoApp_inv : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y), (CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on connected sets.  -/
IsPreconnected.intermediate_value : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s → ∀ {a b : X}, a ∈ s → b ∈ s → ∀ {f : X → α}, ContinuousOn f s → Set.Icc (f a) (f b) ⊆ f '' s
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquivClass.toMonoidWithZeroHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : MulZeroOneClass α]
  [inst_2 : MulZeroOneClass β] [MulEquivClass F α β], MonoidWithZeroHomClass F α β
-- Mathlib.Analysis.Real.Sqrt
/-- Square root of a nonnegative real number.  -/
NNReal.sqrt : NNReal ≃o NNReal
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
/-- The following square commutes:
```
Proj ℬ         ⟶ Proj 𝒜₁
    ^                   ^
    |                   |
Spec A₂[f(s)⁻¹]₀ ⟶ Spec A₁[s⁻¹]₀
```
 -/
AlgebraicGeometry.Proj.awayι_comp_map : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {i : ℕ} (hi : 0 < i)
  (s : A) (hs : s ∈ 𝒜 i),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι ℬ (f s) ⋯ hi) (AlgebraicGeometry.Proj.map f hf) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.map f s)))
      (AlgebraicGeometry.Proj.awayι 𝒜 s hs hi)
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.taylorLinearEquiv_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] (r : R) (n : ℕ) (x : ↥(Polynomial.degreeLT R n)),
  ↑((Polynomial.taylorLinearEquiv r n) x) = ↑(↑((↑(Polynomial.taylorEquiv r)).submoduleMap (Polynomial.degreeLT R n)) x)
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.List.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Mathlib.Analysis.Convex.Segment
image_openSegment : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] (f : E →ᵃ[𝕜] F)
  (a b : E), ⇑f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Ico i j) = Finset.Ico (Fin.castAdd m i) (Fin.castAdd m j)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        k ∉ m₁ → Std.DHashMap.Raw.Const.getD (m₁ ∪ m₂) k fallback = Std.DHashMap.Raw.Const.getD m₂ k fallback