mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.Skyscraper
/-- If `f : 𝓕.stalk p₀ ⟶ c`, then a natural transformation `𝓕 ⟶ skyscraperPresheaf p₀ c` can be
defined by: `𝓕.germ p₀ ≫ f : 𝓕(U) ⟶ c` if `p₀ ∈ U` and the unique morphism to a terminal object
if `p₀ ∉ U`.
 -/
StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasColimits C] →
              {𝓕 : TopCat.Presheaf C X} → {c : C} → (𝓕.stalk p₀ ⟶ c) → (𝓕 ⟶ skyscraperPresheaf p₀ c)
-- Std.Data.Iterators.Producers.Repeat
/-- Internal state of the `repeat` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.RepeatIterator : (α : Type u) → (α → α) → Type u
-- Mathlib.GroupTheory.IsSubnormal
/-- The whole subgroup `G` is subnormal in itself.  -/
Subgroup.IsSubnormal.top : ∀ {G : Type u_1} [inst : Group G], ⊤.IsSubnormal
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instGroup.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Group Y],
  LocallyConstant.instGroup = Function.Injective.group DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.Finset.Max
Finset.min_of_mem : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset α} {a : α}, a ∈ s → ∃ b, s.min = ↑b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.instModuleCarrierPtOppositeRingCat : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] →
      [CategoryTheory.IsCofiltered C] →
        [CategoryTheory.InitiallySmall C] →
          {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
            {cR : CategoryTheory.Limits.Cocone R} →
              (hcR : CategoryTheory.Limits.IsColimit cR) →
                {M : PresheafOfModules R} →
                  {cM : CategoryTheory.Limits.Cocone M.presheaf} →
                    (hcM : CategoryTheory.Limits.IsColimit cM) →
                      Module (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.dualBasis_equivFun : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq ι] (b : Module.Basis ι R M) [inst_4 : Finite ι] (l : Module.Dual R M) (i : ι),
  b.dualBasis.equivFun l i = l (b i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.Data.List.OfFn
/-- A recursor for lists that expands a list into a function mapping to its elements.

This can be used with `induction l using List.ofFnRec`.  -/
List.ofFnRec : {α : Type u} → {C : List α → Sort u_1} → ((n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) → (l : List α) → C l
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
_private.Mathlib.MeasureTheory.Function.LpSpace.Complete.0.MeasureTheory.Lp.lintegral_rpow_tsum_coe_enorm_sub_le_tsum : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
  {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ {p : ℝ},
      1 ≤ p →
        ∀ {B : ℕ → ENNReal},
          (∀ (n : ℕ), ∫⁻ (a : α), (∑ i ∈ Finset.range (n + 1), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ ≤ (∑' (i : ℕ), B i) ^ p) →
            (∫⁻ (a : α), (∑' (i : ℕ), ‖f (i + 1) a - f i a‖ₑ) ^ p ∂μ) ^ (1 / p) ≤ ∑' (i : ℕ), B i
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- A function to 𝕜 is meromorphic in normal form on `U` iff its inverse is.
 -/
meromorphicNFOn_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → 𝕜}, MeromorphicNFOn f⁻¹ U ↔ MeromorphicNFOn f U
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.monMonoidalStruct_tensorObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).X = CategoryTheory.MonoidalCategoryStruct.tensorObj M.X N.X
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.FindSplitImpl.checkVisited : Lean.Expr → OptionT Lean.Meta.FindSplitImpl.FindM Unit
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Fractional linear transformation, also known as the Moebius transformation  -/
UpperHalfPlane.smulAux' : GL (Fin 2) ℝ → ℂ → ℂ
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.add_half_inf_sub_mem_Ioo : ∀ {l u v : ℝ}, v ∈ Set.Ioo l u → v + min (v - l) (u - v) / 2 ∈ Set.Ioo l u
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
RealRMK.integralPositiveLinearMap_rieszMeasure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : T2Space X] [inst_2 : MeasurableSpace X] [inst_3 : BorelSpace X]
  (Λ : CompactlySupportedContinuousMap X ℝ →ₚ[ℝ] ℝ) [inst_4 : LocallyCompactSpace X],
  CompactlySupportedContinuousMap.integralPositiveLinearMap (RealRMK.rieszMeasure Λ) = Λ
-- Lean.Elab.DeclModifiers
/-- `declId` is of the form
```
leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
```
but we also accept a single identifier to users to make macro writing more convenient .
 -/
Lean.Elab.expandDeclIdCore : Lean.Syntax → Lean.Name × Lean.Syntax
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t)[k]? = t[k]?.pbind fun x h' => f (t.getKey k ⋯) x
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The closure of a singleton `{a}` in the upper topology is the left-infinite right-closed interval
$(-∞,a]$.
 -/
Topology.IsUpper.closure_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α] (a : α), closure {a} = Set.Iic a
-- Mathlib.Order.Bounded
Set.bounded_le_inter_not_le : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | ¬b ≤ a}) ↔ Set.Bounded (fun x1 x2 => x1 ≤ x2) s
-- Std.Data.HashSet.Basic
/-- The number of elements present in the set  -/
Std.HashSet.size : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.π_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  s.π.app { as := CategoryTheory.Limits.WalkingPair.right } = s.snd
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- An auxiliary definition for the tensor product of two objects in `AugmentedSimplexCategory`.  -/
AugmentedSimplexCategory.tensorObjOf : SimplexCategory → SimplexCategory → SimplexCategory
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instAssociativeHAdd : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α], Std.Associative fun x1 x2 => x1 + x2
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheorem.origin : Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.Origin
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.lt_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R), I < J ↔ ↑I ⊂ ↑J
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.mk.inj : ∀ {G : Type u_1} {inst : Group G} {A B : Subgroup G} {head : G} {toList : List (ℤˣ × G)}
  {chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList} {head_1 : G}
  {toList_1 : List (ℤˣ × G)}
  {chain_1 : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList_1},
  { head := head, toList := toList, chain := chain } = { head := head_1, toList := toList_1, chain := chain_1 } →
    head = head_1 ∧ toList = toList_1
-- Lean.Compiler.NameMangling
Lean.Name.mangle : Lean.Name → optParam String "l_" → String
-- Mathlib.Order.Notation
_private.Mathlib.Order.Notation.0.Mathlib.Meta.linearOrderToMax : (u : Lean.Level) →
  have a := Mathlib.Meta.linearOrderExpr✝ u;
  Q((a : Type u) → «$a» a → Max a)
-- Aesop.Forward.State
/-- Map from variables to the matches and hypotheses of slots whose types
contain the variables.  -/
Aesop.VariableMap : Type
-- Mathlib.RingTheory.PicardGroup
Module.Flat.tensorSubmoduleAlgebraEquivMul.congr_simp : ∀ {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) [inst_5 : Module.Flat R M]
  [inst_6 : FaithfulSMul R A] (I : Submodule R A),
  Module.Flat.tensorSubmoduleAlgebraEquivMul e I = Module.Flat.tensorSubmoduleAlgebraEquivMul e I
-- Mathlib.RingTheory.Congruence.Defs
RingCon.comap_nonUnitalRingHomId : ∀ {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (J : RingCon R), J.comap (NonUnitalRingHom.id R) = J
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₂₃_eq_pullHom_of_chosenPullback₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })}
  (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (obj' i₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₂ i₃) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
      h
-- Lean.Elab.Do.Basic
/-- Throw an error if a declaration of the given name would shadow a `mut` variable.  -/
Lean.Elab.Do.checkMutVarsForShadowing : Array Lean.Ident → Lean.Elab.Do.DoElabM Unit
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.exists_forall_abs_repr_le_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {L : Submodule ℤ E}
  [DiscreteTopology ↥L] {ι : Type u_2} (b : Module.Basis ι ℤ ↥L),
  ∃ ε, 0 < ε ∧ ∀ (x : ↥L) (i : ι), ε * ↑|(b.repr x) i| ≤ ‖x‖
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- Any category with finite products and equalizers has all finite limits.  -/
CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasFiniteLimits C
-- Init.Data.RArray
Lean.RArray.branch : {α : Type u} → ℕ → Lean.RArray α → Lean.RArray α → Lean.RArray α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.trans : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β},
  m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₂ → (m₁ ∪ m₂).get? k = m₁.get? k
-- Mathlib.Tactic.Simps.Basic
/-- Get the projections used by `simps` associated to a given structure `str`.

The returned information is also stored in the environment extension `Simps.structureExt`, which
is given to `str`. If `str` already has this attribute, the information is read from this
extension instead. See the documentation for this extension for the data this tactic returns.

The returned universe levels are the universe levels of the structure. For the projections there
are three cases
* If the declaration `{StructureName}.Simps.{projectionName}` has been declared, then the value
  of this declaration is used (after checking that it is definitionally equal to the actual
  projection). If you rename the projection name, the declaration should have the *new* projection
  name.
* You can also declare a custom projection that is a composite of multiple projections.
* Otherwise, for every class with the `notation_class` attribute, and the structure has an
  instance of that notation class, then the projection of that notation class is used for the
  projection that is definitionally equal to it (if there is such a projection).
  This means in practice that coercions to function types and sorts will be used instead of
  a projection, if this coercion is definitionally equal to a projection. Furthermore, for
  notation classes like `Mul` and `Zero` those projections are used instead of the
  corresponding projection.
  Projections for coercions and notation classes are not automatically generated if they are
  composites of multiple projections (for example when you use `extend` without the
  `oldStructureCmd` (does this exist?)).
* Otherwise, the projection of the structure is chosen.
  For example: ``getRawProjections env `Prod`` gives the default projections.
  ```
  ([u, v], [(`fst, `(Prod.fst.{u v}), [0], true, false),
     (`snd, `(@Prod.snd.{u v}), [1], true, false)])
  ```

Optionally, this command accepts three optional arguments:
* If `traceIfExists` the command will always generate a trace message when the structure already
  has an entry in `structureExt`.
* The `rules` argument specifies whether projections should be added, renamed, used as prefix, and
  not used by default.
* if `trc` is true, this tactic will trace information just as if
  `set_option trace.simps.verbose true` was set.
 -/
Simps.getRawProjections : Lean.Syntax →
  Lean.Name →
    optParam Bool false →
      optParam (Array Simps.ProjectionRule) #[] →
        optParam Bool false → Lean.CoreM (List Lean.Name × Array Simps.ProjectionData)
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `get?_filter` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.get?_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Bool} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filter f t) k = Option.filter (f k) (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.Tactic.NormNum.NatLog
Mathlib.Meta.NormNum.nat_log_zero : ∀ (n : ℕ), Nat.log 0 n = 0
-- Lean.Expr
/-- Lift loose bound variables `>= s` in `e` by `d`.  -/
Lean.Expr.liftLooseBVars : Lean.Expr → ℕ → ℕ → Lean.Expr
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type u_2)
  [inst_2 : MulAction R X], OreLocalization S X = Quotient (OreLocalization.oreEqv S X)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShift.leftUnitor : ∀ {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] {F₁ : CategoryTheory.Functor C D} (A : Type u_5)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A], CategoryTheory.NatTrans.CommShift F₁.leftUnitor.hom A
-- Mathlib.Algebra.Order.Group.PosPart
instPosPart.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α], instPosPart = { posPart := fun a => a ⊔ 0 }
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If `b ≤ a`, then integrating `f` against `partialTraj κ a b` does nothing.  -/
ProbabilityTheory.Kernel.lmarginalPartialTraj_le : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))),
  b ≤ a → ∀ {f : ((n : ℕ) → X n) → ENNReal}, Measurable f → ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f = f
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_inv_dvd : ∀ {K : Type u} [inst : Field K] {x : RatFunc K}, x ≠ 0 → x⁻¹.denom ∣ x.num
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instInhabitedContMDiffAddMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : AddMonoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], instInhabitedContMDiffAddMonoidMorphism = { default := 0 }
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.graph_map_snd_eq_range : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F),
  Submodule.map (LinearMap.snd R E F) f.graph = f.toFun.range
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.termε : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_rangeSRestrict : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  RingHom.ker f.rangeSRestrict = RingHom.ker f
-- Lean.Server.Rpc.RequestHandling
Lean.Server.wrapRpcProcedure : Lean.Name →
  (paramType respType : Type) →
    [Lean.Server.RpcEncodable paramType] →
      [Lean.Server.RpcEncodable respType] →
        (paramType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) → Lean.Server.RpcProcedure
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.hasShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (t : CategoryTheory.TwistShiftData C A) → CategoryTheory.HasShift t.Category A
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_dirac_of_mem : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {s : Set α} {x : α} {m : M},
  MeasurableSet s → x ∈ s → (MeasureTheory.VectorMeasure.dirac x m).restrict s = MeasureTheory.VectorMeasure.dirac x m
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.adj_toSubgraph_mapLe : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V} {w x : V} {p : G.Walk u v} (h : G ≤ G'),
  (SimpleGraph.Walk.mapLe h p).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x
-- Init.Data.Vector.Basic
Vector.mk.injEq : ∀ {α : Type u} {n : ℕ} (toArray : Array α) (size_toArray : toArray.size = n) (toArray_1 : Array α)
  (size_toArray_1 : toArray_1.size = n),
  (Vector.mk toArray size_toArray = Vector.mk toArray_1 size_toArray_1) = (toArray = toArray_1)
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_sub_left : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddGroup N]
  (f g₁ g₂ : α →₀ N), (f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.continuous_of_continuous_uncurry : ∀ {B : Type u_3} {C : Type u_4} [inst : AddMonoid B] [inst_1 : AddMonoid C] [inst_2 : TopologicalSpace B]
  [inst_3 : TopologicalSpace C] {A : Type u_7} [inst_4 : TopologicalSpace A] (f : A → B →ₜ+ C),
  Continuous (Function.uncurry fun x y => (f x) y) → Continuous f
-- Mathlib.Algebra.Group.End
Equiv.Perm.instPowNat : {α : Type u_4} → Pow (Equiv.Perm α) ℕ
-- Mathlib.MeasureTheory.Function.Holder
/-- The map between `MeasureTheory.Lp` spaces satisfying `ENNReal.HolderTriple`
induced by a continuous bilinear map on the underlying spaces.  -/
ContinuousLinearMap.holder : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        {G : Type u_5} →
          {m : MeasurableSpace α} →
            {μ : MeasureTheory.Measure α} →
              {p q : ENNReal} →
                (r : ENNReal) →
                  [hpqr : p.HolderTriple q r] →
                    [inst : NontriviallyNormedField 𝕜] →
                      [inst_1 : NormedAddCommGroup E] →
                        [inst_2 : NormedAddCommGroup F] →
                          [inst_3 : NormedAddCommGroup G] →
                            [inst_4 : NormedSpace 𝕜 E] →
                              [inst_5 : NormedSpace 𝕜 F] →
                                [inst_6 : NormedSpace 𝕜 G] →
                                  (E →L[𝕜] F →L[𝕜] G) →
                                    ↥(MeasureTheory.Lp E p μ) → ↥(MeasureTheory.Lp F q μ) → ↥(MeasureTheory.Lp G r μ)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A linear surjection between modules with the module topology is an open quotient map.  -/
IsModuleTopology.isOpenQuotientMap_of_surjective : ∀ {R : Type u_1} [τR : TopologicalSpace R] [inst : Ring R] {A : Type u_3} [inst_1 : AddCommGroup A]
  [inst_2 : Module R A] [inst_3 : TopologicalSpace A] [IsModuleTopology R A] {B : Type u_4} [inst_5 : AddCommGroup B]
  [inst_6 : Module R B] [inst_7 : TopologicalSpace B] [IsModuleTopology R B] {φ : A →ₗ[R] B},
  Function.Surjective ⇑φ → IsOpenQuotientMap ⇑φ
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.h_apply_infinity : ∀ {A B : GrpCat} (f : A ⟶ B),
  ∀ x ∈ (GrpCat.Hom.hom f).range,
    ((GrpCat.SurjectiveOfEpiAuxs.h f) x) GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
      GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
-- Init.Control.Except
/-- Handles exceptions produced in the `ExceptT ε` transformer.
 -/
ExceptT.tryCatch : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → ExceptT ε m α → (ε → ExceptT ε m α) → ExceptT ε m α
-- Mathlib.Data.Finset.NAry
Set.toFinset_image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β)
  [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t] [inst_3 : Fintype ↑(Set.image2 f s t)],
  (Set.image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_single : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_3} [inst_1 : Fintype ι] (F' : ι → Type u_5)
  [inst_2 : (i : ι) → NormedAddCommGroup (F' i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (F' i)] [inst_4 : DecidableEq ι]
  (k : WithTop ℕ∞) (i : ι), ContDiff 𝕜 k (Pi.single i)
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.PolarizationIn_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [inst_11 : P.IsValuedIn S] [inst_12 : Fintype ι]
  (x : ↥(P.rootSpan S)), (P.PolarizationIn S) x = ∑ i, (P.coroot'In S i) x • P.coroot i
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsFinite
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- These are the invariants satisfied by the KMP search iterator. They are sufficient to ensure that
the code does not panic and returns the correct result.
 -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants : String.Slice → String.Slice → String.Pos.Raw → String.Pos.Raw → Prop