mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS b c d 1 = 1
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.of_eq : ∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop}, PrimrecPred p → (∀ (a : α), p a ↔ q a) → PrimrecPred q
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.sum_section : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x}
  {s : Finset ι},
  (∀ i ∈ s, ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) x₀) →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑ i ∈ s, t i x⟩) x₀
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Pi.borelSpace : ∀ {ι : Type u_6} {X : ι → Type u_7} [Countable ι] [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : (i : ι) → MeasurableSpace (X i)] [∀ (i : ι), SecondCountableTopology (X i)] [∀ (i : ι), BorelSpace (X i)],
  BorelSpace ((i : ι) → X i)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.size_containsThenInsert_eq_size : ∀ {α : Type u} {β : α → Type v} [Ord α] (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.containsThenInsert.size t = t.size
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_eq_emod_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → a.tmod b = a % b
-- Mathlib.Analysis.Normed.Group.Defs
/-- Auxiliary class, endowing a type `α` with a function `enorm : α → ℝ≥0∞` with notation `‖x‖ₑ`.  -/
ENorm : Type u_8 → Type u_8
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.hasSum_eval₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ →
    MvPowerSeries.HasEval a →
      ∀ (f : MvPowerSeries σ R),
        HasSum (fun d => φ ((MvPowerSeries.coeff d) f) * d.prod fun s e => a s ^ e) (MvPowerSeries.eval₂ φ a f)
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.norm_single : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [StarOrderedRing A]
  [inst_8 : DecidableEq ι] (i : ι) (y : E i), ‖(WithCStarModule.equiv A ((j : ι) → E j)).symm (Pi.single i y)‖ = ‖y‖
-- Mathlib.Analysis.Convex.Jensen
/-- Canonical form of the **strict Jensen's inequality**.  -/
StrictConcaveOn.lt_map_sum_iff_of_nonneg' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i) ↔ ∃ j ∈ t, w j ≠ 0 ∧ p j ≠ ∑ i ∈ t, w i • p i)
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.mk : Lean.MVarId → Array Lean.Expr → Lean.Meta.FVarSubst → Lean.Meta.InductionSubgoal
-- Lean.Server.CodeActions.Basic
_private.Lean.Server.CodeActions.Basic.0.Lean.Server.evalCodeActionProviderUnsafe : {M : Type → Type} →
  [Lean.MonadEnv M] →
    [Lean.MonadOptions M] → [Lean.MonadError M] → [Monad M] → Lean.Name → M Lean.Server.CodeActionProvider
-- Lean.Server.Requests
Lean.Server.RequestHandler.mk.injEq : ∀ (fileSource : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (handle : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse))
  (fileSource_1 : Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri)
  (handle_1 : Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)),
  ({ fileSource := fileSource, handle := handle } = { fileSource := fileSource_1, handle := handle_1 }) =
    (fileSource = fileSource_1 ∧ handle = handle_1)
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monToMonad_map_toNatTrans : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Mon (CategoryTheory.Functor C C)}
  (f : X ⟶ Y), ((CategoryTheory.Monad.monToMonad C).map f).toNatTrans = f.hom
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B],
      (∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b) → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Linear equivalence between `S : Submodule R A` and `S`. Though these types are equal,
we define it as a `LinearEquiv` to avoid type equalities.  -/
Subalgebra.toSubmoduleEquiv : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → ↥(Subalgebra.toSubmodule S) ≃ₗ[R] ↥S
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.fst_orthogonalDecomposition_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (x : E),
  (K.orthogonalDecomposition x).fst = K.orthogonalProjectionOnto x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varsToConstants.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (c : γ),
  (FirstOrder.Language.var (Sum.inl c)).varsToConstants = FirstOrder.Language.Constants.term (Sum.inr c)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_add_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ∀ (n : ℕ) [inst_4 : n.AtLeastTwo], ⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n
-- Mathlib.Data.ENat.Lattice
/-- **Alias** of `ENat.natCast_sSup`. -/
ENat.coe_sSup : ∀ {s : Set ℕ}, BddAbove s → ↑(sSup s) = ⨆ a ∈ s, ↑a
-- Aesop.Util.UnorderedArraySet
_private.Aesop.Util.UnorderedArraySet.0.Aesop.UnorderedArraySet.mk.inj : ∀ {α : Type u_1} {inst : BEq α} {rep rep_1 : Array α}, { rep := rep } = { rep := rep_1 } → rep = rep_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter_eq_filter! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {h : t.Balanced}
  {f : (a : α) → β a → Bool}, (Std.DTreeMap.Internal.Impl.filter f t h).impl = Std.DTreeMap.Internal.Impl.filter! f t
-- Mathlib.Combinatorics.Quiver.Path
/-- Bounded paths of length zero between two vertices form a subsingleton.  -/
Quiver.Path.instSubsingletonBddPaths : ∀ {V : Type u_1} [inst : Quiver V] (v w : V), Subsingleton (Quiver.Path.BoundedPaths v w 0)
-- Init.Data.List.Find
List.findFinIdx?_eq_bind_find?_finIdxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool},
  List.findFinIdx? p xs = (List.find? p xs).bind fun a => List.finIdxOf? a xs
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.id_apply : ∀ (M : SemiNormedGrp) (r : M.carrier), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) r = r
-- Mathlib.Data.List.Sym
List.sym2_eq_sym_two : ∀ {α : Type u_1} {xs : List α}, List.map (⇑(Sym2.equivSym α)) xs.sym2 = List.sym 2 xs
-- Mathlib.Logic.Equiv.Basic
Equiv.Perm.extendDomain_apply_subtype : ∀ {α' : Type u_9} {β' : Type u_10} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  {b : β'} (h : p b), (e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.pure : {α ι : Type} → α → Std.Internal.Parsec ι α
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.involutiveInv.eq_1 : ∀ {M₂ : Type u_2} {M₁ : Type u_3} [inst : Inv M₁] [inst_1 : InvolutiveInv M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹), Function.Injective.involutiveInv f hf inv = { toInv := inst, inv_inv := ⋯ }
-- Init.Data.SInt.Lemmas
Int8.toInt32_neg_of_ne : ∀ {x : Int8}, x ≠ -128 → (-x).toInt32 = -x.toInt32
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.instIsStableUnderCoproductsLlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{w, v, u} T.llp
-- Mathlib.RingTheory.Ideal.Prod
Ideal.mem_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (I : Ideal R) (J : Ideal S) {x : R × S},
  x ∈ I.prod J ↔ x.1 ∈ I ∧ x.2 ∈ J
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_mulLeft : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  ⇑(MeasurableEquiv.mulLeft g) = fun x => g * x
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α},
  μ.toOuterMeasure = MeasureTheory.inducedOuterMeasure (fun s x => μ s) ⋯ ⋯
-- ProofWidgets.Component.PenroseDiagram
/-- Add an object `nm` of Penrose type `tp`,
labelled by `h`, to the substance program.  -/
ProofWidgets.Penrose.DiagramBuilderM.addEmbed : String → String → ProofWidgets.Html → ProofWidgets.Penrose.DiagramBuilderM Unit
-- Batteries.Data.String.Lemmas
/-- A string position is valid if it is equal to the UTF-8 length of an initial substring of `s`.
 -/
String.Pos.Raw.Valid.mk : ∀ (cs cs' : List Char) {p : String.Pos.Raw},
  p.byteIdx = String.utf8Len cs → String.Pos.Raw.Valid (String.ofList (cs ++ cs')) p
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- A continuous linear map `u : E →L[𝕜] F` is a **Fredholm operator** if it is strict,
its range is closed and has finite codimension, and its kernel is (topologically) complemented and
has finite dimension.

See also `isFredholm_tfae` for other equivalent characterizations.
We will also prove later (not in Mathlib yet) that for maps between Banach (or even Fréchet)
spaces over `ℝ` or `ℂ`, all the conditions follow from the kernel and cokernel having finite
dimension.  -/
ContinuousLinearMap.IsFredholm : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] → [inst_5 : TopologicalSpace E] → [inst_6 : TopologicalSpace F] → (E →L[𝕜] F) → Prop
-- Mathlib.Analysis.Complex.ValueDistribution.Cartan
_private.Mathlib.Analysis.Complex.ValueDistribution.Cartan.0.ValueDistribution.eventuallyEq_log_trailingCoeff_of_meromorphicOrderAt_eq_zero : ∀ {f : ℂ → ℂ},
  MeromorphicAt f 0 →
    meromorphicOrderAt f 0 = 0 →
      (fun x => Real.log ‖meromorphicTrailingCoeffAt f 0 - x‖) =ᶠ[Filter.codiscreteWithin (Metric.sphere 0 |1|)]
        fun a => Real.log ‖meromorphicTrailingCoeffAt (fun x => f x - a) 0‖
-- Mathlib.CategoryTheory.Limits.Fubini
/-- If `coneOfConeUncurry Q c` is a limit cone then `c` is in fact a limit cone.
 -/
CategoryTheory.Limits.IsLimit.ofConeOfConeUncurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCones F} →
                (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) →
                  {c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)} →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfConeUncurry Q c) →
                      CategoryTheory.Limits.IsLimit c
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.ofι_pt : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [inst_1 : Nonempty J]
  {P : C} (ι : P ⟶ X)
  (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)),
  (CategoryTheory.Limits.Trident.ofι ι w).pt = P
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_of_sigmaFinite : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)],
  ProbabilityTheory.condVar m X μ =
    if MeasureTheory.Integrable (fun ω => (X ω - μ[X | m] ω) ^ 2) μ then
      if MeasureTheory.StronglyMeasurable fun ω => (X ω - μ[X | m] ω) ^ 2 then fun ω => (X ω - μ[X | m] ω) ^ 2
      else MeasureTheory.AEStronglyMeasurable.mk ↑↑(MeasureTheory.condExpL1 hm μ fun ω => (X ω - μ[X | m] ω) ^ 2) ⋯
    else 0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α}
  [self : s.HaveLebesgueDecomposition μ], s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldrM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (init : δ), Std.DTreeMap.Internal.Impl.foldrM f init Std.DTreeMap.Internal.Impl.leaf = pure init
-- Mathlib.Order.Interval.Finset.Defs
/-- Note we define `Ici (toDual a)` as `Iic a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Iic a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Ici (toDual (toDual a)) :) = (Ici a :) := rfl
```
 -/
OrderDual.instLocallyFiniteOrderTop : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderBot α] → LocallyFiniteOrderTop αᵒᵈ
-- Init.Data.Sum.Basic
Sum.getLeft.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (ab ab_1 : α ⊕ β) (e_ab : ab = ab_1) (a : ab.isLeft = true),
  ab.getLeft a = ab_1.getLeft ⋯
-- Mathlib.Topology.MetricSpace.Contracting
ContractingWith.edist_efixedPoint_lt_top : ∀ {α : Type u_1} [inst : EMetricSpace α] {K : NNReal} {f : α → α} [inst_1 : CompleteSpace α] (hf : ContractingWith K f)
  {x : α} (hx : edist x (f x) ≠ ⊤), edist x (ContractingWith.efixedPoint f hf x hx) < ⊤
-- Mathlib.CategoryTheory.Grothendieck
/-- The forgetful functor from `Grothendieck F` to the source category.  -/
CategoryTheory.Grothendieck.forget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) → CategoryTheory.Functor (CategoryTheory.Grothendieck F) C
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_coeff_cert.eq_1 : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly) (k : ℕ), Lean.Grind.Linarith.eq_coeff_cert p₁ p₂ k = (k != 0 && p₁ == p₂.mul ↑k)
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.inst : ∀ {R : Type u} [inst : CommRing R], Algebra.Etale R R
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.of_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] (X : C), P X → P.colimitsClosure J X
-- Mathlib.Data.ENat.Pow
ENat.one_epow : ∀ {y : ℕ∞}, 1 ^ y = 1
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- If two global sections agree after restriction to each member of an open cover, then
they agree globally.  -/
AlgebraicGeometry.Scheme.OpenCover.ext_elem : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover),
  (∀ (i : 𝒰.I₀),
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) f =
        (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (𝒰.f i) U)) g) →
    f = g
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Week.Aligned.Ordinal n
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- Group-like elements in a bialgebra are stable under multiplication.  -/
IsGroupLikeElem.mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] {a b : A},
  IsGroupLikeElem R a → IsGroupLikeElem R b → IsGroupLikeElem R (a * b)
-- Lean.Server.Rpc.Basic
Lean.Server.RpcEncodable.mk : {α : Type} →
  (α → StateM Lean.Server.RpcObjectStore Lean.Json) →
    (Lean.Json → ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) α) → Lean.Server.RpcEncodable α
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.instMonoIMonomorphismsRlpMonoMapFactorizationDataRlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono (CategoryTheory.IsGrothendieckAbelian.monoMapFactorizationDataRlp f).i
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {k : α},
  l.Perm l' → Std.Internal.List.containsKey k l = Std.Internal.List.containsKey k l'
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.divRight_symm_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a b : α),
  (RelIso.symm (OrderIso.divRight a)) b = b * a
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_inv_atTop_nhds_zero_nat : ∀ {𝕜 : Type u_4} [inst : DivisionSemiring 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜],
  Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
-- Mathlib.Computability.MyhillNerode
/-- The left quotients of a language are the states of an automaton that accepts the language.  -/
Language.toDFA : {α : Type u} → (L : Language α) → DFA α ↑(Set.range L.leftQuotient)
-- Lean.Parser.Types
Lean.Parser.instInhabitedParserInfo.default : Lean.Parser.ParserInfo
-- Batteries.Data.Stream
Std.List.stream_drop_eq_drop : ∀ {α : Type u_1} {n : ℕ} (l : List α), Std.Stream.drop l n = List.drop n l
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.eq_X_add_C_of_natDegree_le_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.natDegree ≤ 1 → p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.renameEquiv_trans : ∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} (R : Type u_4) [inst : CommSemiring R] (e : σ ≃ τ) (f : τ ≃ α),
  (MvPolynomial.renameEquiv R e).trans (MvPolynomial.renameEquiv R f) = MvPolynomial.renameEquiv R (e.trans f)
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
Polynomial.isOpenMap_comap_C : ∀ {R : Type u_1} [inst : CommRing R], IsOpenMap (PrimeSpectrum.comap Polynomial.C)
-- Init.Data.Array.Extract
Array.takeWhile_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Bool} {as : Array α},
  Array.takeWhile p (Array.map f as) = Array.map f (Array.takeWhile (p ∘ f) as)
-- Lean.Elab.Command
Lean.Elab.Command.addModuleLinter : Lean.Elab.Command.ModuleLinter → IO Unit
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.self_le_maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, (cmp k (t.insert k v).maxKey!).isLE = true
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernelRelations_R : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁), (pres₂.cokernelRelations data).R = (pres₂.R ⊕ ι)
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toHImp : {α : Type u} → [self : BooleanAlgebra α] → HImp α
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.map_continuous : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {A : DiscreteQuotient X} {B : DiscreteQuotient Y} (cond : DiscreteQuotient.LEComap f A B),
  Continuous (DiscreteQuotient.map f cond)
-- Mathlib.Algebra.Group.Action.Defs
instIsCancelVAdd : ∀ (G : Type u_9) [inst : AddCancelMonoid G], IsCancelVAdd G G
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.instInhabitedGHSpace : Inhabited GromovHausdorff.GHSpace
-- Lean.Syntax
/-- `for _ in stx.topDown` iterates through each node and leaf in `stx` top-down, left-to-right.
If `firstChoiceOnly` is `true`, only visit the first argument of each choice node.
 -/
Lean.Syntax.topDown : Lean.Syntax → optParam Bool false → Lean.Syntax.TopDown
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.uncurry_curryRight : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂),
  f.curryRight.uncurryRight = f
-- Init.Data.List.Erase
List.eraseIdx_eq_self : ∀ {α : Type u_1} {l : List α} {k : ℕ}, l.eraseIdx k = l ↔ l.length ≤ k
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.r : (α : Type u) → [Lean.Grind.NatModule α] → α × α → α × α → Prop
-- Mathlib.Topology.Inseparable
SeparationQuotient.surjective_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Function.Surjective SeparationQuotient.mk
-- Mathlib.Algebra.Group.Defs
neg_add_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), -a + (a + b) = b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofZeroDvd c_1 →
    c = c_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastClz : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec fun {len} => Std.Tactic.BVDecide.BVExpr.bitblast.blastClz