mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear equivalence seen as a `ContinuousAddEquiv`.  -/
ContinuousLinearEquiv.toContinuousAddEquiv : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R₁ M₁] →
            {M : Type u_8} →
              [inst_4 : TopologicalSpace M] →
                [inst_5 : AddCommMonoid M] → [inst_6 : Module R₁ M] → (M₁ ≃L[R₁] M) → M₁ ≃ₜ+ M
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Multiplicative equivalence between additive endomorphisms of an `AddZeroClass` `A`
and multiplicative endomorphisms of `Multiplicative A`.  -/
addMonoidEndToMultiplicative : (A : Type u_4) → [inst : AddZeroClass A] → AddMonoid.End A ≃* Monoid.End (Multiplicative A)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.mem_span_range_iff_exists_finsupp : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} {x : M}, x ∈ Submodule.span R (Set.range v) ↔ ∃ c, (c.sum fun i a => a • v i) = x
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds_append_left : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α},
  i < n → (xs ++ ys).setIfInBounds i x = xs.setIfInBounds i x ++ ys
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_pullback_to_base_isOpenImmersion : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.SheafedSpace.IsOpenImmersion g],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion
    (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousMul.mk : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M],
  (∀ {a : M}, Continuous fun x => a * x) → (∀ {a : M}, Continuous fun x => x * a) → SeparatelyContinuousMul M
-- Mathlib.Data.Finset.Option
Finset.insertNone_nonempty : ∀ {α : Type u_1} {s : Finset α}, (Finset.insertNone s).Nonempty
-- Mathlib.Algebra.Group.Subgroup.Finsupp
Subgroup.mem_closure_iff_of_fintype : ∀ {M : Type u_1} [inst : CommGroup M] {x : M} {s : Set M} [inst_1 : Fintype ↑s],
  x ∈ Subgroup.closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.final_fromFinalModel : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [inst_1 : CategoryTheory.FinallySmall J],
  (CategoryTheory.fromFinalModel J).Final
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_of_finite : ∀ (X : Type u_1) [Finite X] (κ : Cardinal.{u_2}), Cardinal.aleph0 ≤ κ → HasCardinalLT X κ
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise scalar multiplication of
`f` and `g`, which monovary together on `s`, is strictly decreased by a permutation if and only if
`f ∘ σ` and `g` do not monovary together on `s`. Stated by permuting the entries of `f`.  -/
MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {s : Finset ι} {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → (∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_const_div_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α}, a ≠ 0 → (Summable (fun i => a / f i) L ↔ Summable (1 / f) L)
-- Mathlib.Algebra.Group.Units.Hom
isLocalHom_toMonoidHom : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : FunLike F R S]
  [inst_3 : MonoidHomClass F R S] (f : F) [IsLocalHom f], IsLocalHom ↑f
-- Mathlib.Algebra.Order.Group.Cone
instPartialOrderGroupCone.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G], instPartialOrderGroupCone G = PartialOrder.ofSetLike (GroupCone G) G
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
IsSimplyConnected.simplyConnectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsSimplyConnected s → SimplyConnectedSpace ↑s
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.NormalizedMooreComplex.obj.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.SimplicialObject C),
  AlgebraicTopology.NormalizedMooreComplex.obj X =
    ChainComplex.of
      (fun n => CategoryTheory.Subobject.underlying.obj (AlgebraicTopology.NormalizedMooreComplex.objX X n))
      (AlgebraicTopology.NormalizedMooreComplex.objD X) ⋯
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- The co-Yoneda embedding `Cᵒᵖ ⥤ C ⥤ Type w` for a locally `w`-small category `C`.  -/
CategoryTheory.shrinkCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type w))
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_apply' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] {s : Set ↑(Metric.sphere 0 1)},
  MeasurableSet s → μ.toSphere s = ↑(Module.finrank ℝ E) * μ (Set.Ioo 0 1 • Subtype.val '' s)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a))
  (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryLT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getEntryLT?.go k (some ⟨ky, y⟩) r
      | x => Std.DTreeMap.Internal.Impl.getEntryLT?.go k best l
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorSemiring.ceil` is the lower adjoint of the coercion `↑ : ℕ → α`.  -/
FloorSemiring.gc_ceil : ∀ {α : Type u_4} {inst : Semiring α} {inst_1 : PartialOrder α} [self : FloorSemiring α],
  GaloisConnection FloorSemiring.ceil Nat.cast
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_toENat : ∀ (o : Ordinal.{u_1}), Cardinal.toENat (Cardinal.aleph o) = ⊤
-- Mathlib.Algebra.Notation.Support
Function.support_curry : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : Zero M] (f : ι × κ → M),
  Function.support (Function.curry f) = Prod.fst '' Function.support f
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Typecheck a `LinearMap` as a morphism in `ModuleCat`.  -/
ModuleCat.ofHom : {R : Type u} →
  [inst : Ring R] →
    {X Y : Type v} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommGroup Y] → [inst_4 : Module R Y] → (X →ₗ[R] Y) → (ModuleCat.of R X ⟶ ModuleCat.of R Y)
-- Mathlib.Logic.Equiv.Option
Equiv.removeNone_optionCongr : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.optionCongr.removeNone = e
-- Mathlib.Order.Closure
LowerAdjoint.ext_iff : ∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} {l₁ l₂ : LowerAdjoint u},
  l₁ = l₂ ↔ l₁.toFun = l₂.toFun
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorRight_apply_tmul_apply : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (v : V) (f : α →₀ W) (i : α),
  ((σ.finsuppTensorRight ρ α) (v ⊗ₜ[k] f)) i = v ⊗ₜ[k] f i
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFinitaryMap : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).Finitary
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelMonoid α],
  Colex.instAddLeftCancelMonoid = { toAddMonoid := Colex.instAddMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compLeft_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₃ ⟶ S₁), (h.compLeft ψ).h₁ = CategoryTheory.CategoryStruct.comp ψ.τ₂ h.h₁
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_bot_iff_card : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊥ ↔ Nat.card ↥H = 1
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted subtraction with `weightedVSubVSubWeights` gives the result of subtracting the
specified points.  -/
Finset.weightedVSub_weightedVSubVSubWeights : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] (p : ι → P) {i j : ι},
  i ∈ s → j ∈ s → (s.weightedVSub p) (Finset.weightedVSubVSubWeights k i j) = p i -ᵥ p j
-- Init.Coe
/-- Helper definition used by the elaborator. It is not meant to be used directly by users.

This is used for coercing the result type under a monad.
 -/
Lean.Internal.coeM : {m : Type u → Type v} → {α β : Type u} → [(a : α) → CoeT α a β] → [Monad m] → m α → m β
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.mapDomainLinearEquiv.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N),
  MonoidAlgebra.mapDomainLinearEquiv R S e =
    MonoidAlgebra.coeffLinearEquiv R ≪≫ₗ (Finsupp.domLCongr e ≪≫ₗ (MonoidAlgebra.coeffLinearEquiv R).symm)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.IndepFun.hasLaw_fun_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {M : Type u_3} [inst : Monoid M]
  {mM : MeasurableSpace M} [MeasurableMul₂ M] {μ ν : MeasureTheory.Measure M} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] {X Y : Ω → M},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasLaw (fun ω => X ω * Y ω) (μ.mconv ν) P
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- Given two additive groups that are generated by elements `g` and `g'` of the same order,
we obtain an isomorphism sending `g` to `g'`.  -/
addEquivOfAddOrderOfEq : {G : Type u_2} →
  {G' : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddGroup G'] →
        {g : G} →
          (∀ (x : G), x ∈ AddSubgroup.zmultiples g) →
            {g' : G'} → (∀ (x : G'), x ∈ AddSubgroup.zmultiples g') → addOrderOf g = addOrderOf g' → G ≃+ G'
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.triple_eq_triple_of_mem : ∀ {α : Type u_1} {s t u : Finset α} [inst : DecidableEq α],
  Disjoint s t →
    Disjoint s u →
      Disjoint t u →
        ∀ {x₁ x₂ y₁ y₂ z₁ z₂ : α},
          {x₁, y₁, z₁} = {x₂, y₂, z₂} →
            x₁ ∈ s → x₂ ∈ s → y₁ ∈ t → y₂ ∈ t → z₁ ∈ u → z₂ ∈ u → (x₁, y₁, z₁) = (x₂, y₂, z₂)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} [inst_1 : SizeOf C] (a : C)
  (str : F.obj a ⟶ a), sizeOf { a := a, str := str } = 1 + sizeOf a + sizeOf str
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Throw an error if the monoidal category instance is not found.  -/
Mathlib.Tactic.Monoidal.synthMonoidalError : {α : Type} → Lean.MetaM α
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.measurePreserving_symm : MeasureTheory.MeasurePreserving unitInterval.symm MeasureTheory.volume MeasureTheory.volume
-- Batteries.Tactic.SqueezeScope
/-- We implement `squeeze_scope` using a global variable that tracks all `squeeze_scope` invocations
in flight. It is a map `a => (x => (stx, simps))` where `a` is a unique identifier for
the `squeeze_scope` invocation which is shared with all contained simps, and `x` is a unique
identifier for a particular piece of simp syntax (which can be called multiple times).
Within that, `stx` is the simp syntax itself, and `simps` is the aggregated list of simps used
so far.
 -/
Batteries.Tactic.squeezeScopes : IO.Ref (Lean.NameMap (Lean.NameMap (Lean.Syntax × List Lean.Meta.Simp.UsedSimps)))
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.id_coweightMap_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) (x : N),
  (↑(RootPairing.Equiv.id P)).coweightMap x = x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.some.congr_simp : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x x_1 : R) (e_x : x = x_1) (y y_1 : R)
  (e_y : y = y_1) (h : W'.Nonsingular x y),
  WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x_1 y_1 ⋯
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.ofSubmodule'_apply : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M₂] [inst_5 : TopologicalSpace M₂]
  {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M ≃SL[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : ↥(Submodule.comap (↑↑f) U)),
  ↑((f.ofSubmodule' U) x) = f ↑x
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instInjectiveXIntI : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K : CochainComplex C ℤ} (n : ℤ),
  CategoryTheory.Injective ((CochainComplex.cm5b.I K).X n)
-- Mathlib.Combinatorics.Derangements.Finite
numDerangements_one : numDerangements 1 = 0
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.leadCoeff.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (x : Int.Internal.Linear.Poly)
  (h_1 :
    (a : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a v p))
  (h_2 : (x : Int.Internal.Linear.Poly) → motive x),
  (∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
      x = Int.Internal.Linear.Poly.add a v p → False) →
    (match x with
      | Int.Internal.Linear.Poly.add a v p => h_1 a v p
      | x => h_2 x) =
      h_2 x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportFailure.mk : Lean.Name → Lean.Name → Lean.Exception → Lean.Meta.LazyDiscrTree.ImportFailure
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedCommRing.toCommRing : {α : Type u_5} → [self : SeminormedCommRing α] → CommRing α
-- Mathlib.Algebra.CubicDiscriminant
Cubic.discr.eq_1 : ∀ {R : Type u_5} [inst : Ring R] (P : Cubic R),
  P.discr =
    P.b ^ 2 * P.c ^ 2 - 4 * P.a * P.c ^ 3 - 4 * P.b ^ 3 * P.d - 27 * P.a ^ 2 * P.d ^ 2 + 18 * P.a * P.b * P.c * P.d
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiff.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {n : WithTop ℕ∞},
  ContDiff ℂ n f → ContDiff ℂ n fun x => Complex.sinh (f x)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mrange_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (MonoidHom.inl M N) = ⊤.prod ⊥
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.inf_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R), (I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.reorder c_1) =
    (c = c_1)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelπ.eq_1 : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y),
  SemiNormedGrp.explicitCokernelπ f =
    (SemiNormedGrp.cokernelCocone f).ι.app CategoryTheory.Limits.WalkingParallelPair.one
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.PatternModel.mk : {ρ : Type} → {pat : ρ} → (String → Prop) → String.Slice.Pattern.Model.PatternModel pat
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.genLTOne_unique : ∀ (G : Type u_1) [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G] [inst_3 : Nontrivial G]
  [inst_4 : IsCyclic G] {g : G}, g < 1 → Subgroup.zpowers g = ⊤ → g = LinearOrderedCommGroup.genLTOne G
-- Mathlib.Algebra.Group.End
AddAut.coe_zero : ∀ (M : Type u_2) [inst : Add M], ⇑0 = id
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.index.inj : ∀ {imode imode_1 : Aesop.IndexingMode},
  Aesop.Frontend.BuilderOption.index imode = Aesop.Frontend.BuilderOption.index imode_1 → imode = imode_1
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.MvPolynomialC.numBound.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_zero_iff_isBigO_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u 0 ↔ u =O[l] 0
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryLED : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Sigma β → (a : α) × β a
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_apply_eq : ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : α}, e.symm x = y ↔ x = e y
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.norm_mkContinuous₂_aux : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) (C : ℝ) (h : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖) (x : E),
  ‖(f x).mkContinuous (C * ‖x‖) ⋯‖ ≤ max C 0 * ‖x‖
-- Mathlib.Util.CountHeartbeats
/-- The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to `#count_heartbeats in xxx`, except that it applies
to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations:
it looks inside `set_option ... in`, but not, for instance, inside `mutual` blocks.

There is a convenience notation `#count_heartbeats` that simply sets the linter option to true.
 -/
Mathlib.Linter.CountHeartbeats.countHeartbeats : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetPlusMinusOneOfHasDetOne : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ : Subgroup (GL n R)) [Γ.HasDetOne], Γ.HasDetPlusMinusOne
-- Lean.Expr
_private.Lean.Expr.0.Lean.intNatCastFn : Lean.Expr
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.gradedZeroRingHom_apply_coe : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_4 : AddSubmonoidClass σ A]
  [inst_5 : AddSubmonoidClass τ B] [inst_6 : AddMonoid ι] [inst_7 : SetLike.GradedMonoid 𝒜]
  [inst_8 : SetLike.GradedMonoid ℬ] (f : 𝒜 →+*ᵍ ℬ) (a : ↥(𝒜 0)), ↑(f.gradedZeroRingHom a) = f ↑a
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Subfunctor.eq_sheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} (G : CategoryTheory.Subfunctor F),
  CategoryTheory.Presieve.IsSheaf J F →
    CategoryTheory.Presieve.IsSheaf J G.toFunctor → G = CategoryTheory.Subfunctor.sheafify J G
-- Lean.Elab.Tactic.Ext
/-- Creates the type of the extensionality theorem for the given structure,
returning `∀ {x y : Struct}, x.1 = y.1 → x.2 = y.2 → x = y`, for example.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.mkExtType : Lean.Name → Bool → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Algebra.Algebra
/-- See Note [custom simps projection].  -/
ContinuousAlgHom.Simps.coe : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A →A[R] B) → A →ₐ[R] B
-- Lean.Elab.App
/-- The eliminator.  -/
Lean.Elab.Term.ElabElimInfo.elimExpr : Lean.Elab.Term.ElabElimInfo → Lean.Expr
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp.injEq : ∀ (e : Lean.Expr) (isoLift? : Option Mathlib.Tactic.BicategoryLike.IsoLift)
  (f₁ g₁ f₂ g₂ : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂) (e_1 : Lean.Expr)
  (isoLift?_1 : Option Mathlib.Tactic.BicategoryLike.IsoLift) (f₁_1 g₁_1 f₂_1 g₂_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂),
  (Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e isoLift? f₁ g₁ f₂ g₂ η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂.horizontalComp e_1 isoLift?_1 f₁_1 g₁_1 f₂_1 g₂_1 η_1 θ_1) =
    (e = e_1 ∧ isoLift? = isoLift?_1 ∧ f₁ = f₁_1 ∧ g₁ = g₁_1 ∧ f₂ = f₂_1 ∧ g₂ = g₂_1 ∧ η = η_1 ∧ θ = θ_1)
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.toPartialMap_domain : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y), f.toPartialMap.domain = f.source
-- Init.Coe
instCoeOutOfCoeSort : {α : Sort u_1} → {β : Sort u_2} → [CoeSort α β] → CoeOut α β
-- Mathlib.Algebra.Ring.Defs
Semiring.mk : {α : Type u} →
  [toAddCommMonoid : AddCommMonoid α] →
    [toMonoid : Monoid α] →
      (∀ (a : α), 0 * a = 0) →
        (∀ (a : α), a * 0 = 0) →
          (∀ (a b c : α), a * (b + c) = a * b + a * c) →
            (∀ (a b c : α), (a + b) * c = a * c + b * c) →
              [toNatCast : NatCast α] →
                autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
                  autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam → Semiring α
-- Mathlib.Topology.Order.NhdsSet
Ioo_mem_nhdsSet_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a ≤ b → c < d → Set.Ioo a d ∈ nhdsSet (Set.Ioc b c)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α},
  (Std.ExtHashMap.filterMap f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => (f x_2 m[x_2]).isSome