mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Basic
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
`a ∈ m`.
 -/
Std.DHashMap.Const.get : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (m : Std.DHashMap α fun x => β) → (a : α) → a ∈ m → β
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOfEquivOfLe_symm_apply_coe_coe : ∀ {G : Type u_7} [inst : Group G] {H K : Subgroup G} (h : H ≤ K) (g : ↥H),
  ↑↑((Subgroup.subgroupOfEquivOfLe h).symm g) = ↑g
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
CategoryTheory.extendFan_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C}
  (c₁ : CategoryTheory.Limits.Fan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt)
  (X : CategoryTheory.Discrete (Fin (n + 1))),
  (CategoryTheory.extendFan c₁ c₂).π.app X =
    Fin.cases c₂.fst (fun i => CategoryTheory.CategoryStruct.comp c₂.snd (c₁.π.app { as := i })) X.as
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roo_eq_zero_iff : ∀ {m n i : ℕ}, (m<...n).toList[i]! = 0 ↔ n ≤ i + (m + 1)
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Submodule.orthogonal_eq_bot_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [K.HasOrthogonalProjection], Kᗮ = ⊥ ↔ K = ⊤
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Iio : ∀ {n : ℕ} (a : Fin n), Finset.map Fin.valEmbedding (Finset.Iio a) = Finset.Iio ↑a
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.charDiff : String → String → Array (Lean.Diff.Action × String)
-- Mathlib.Order.Partition.Basic
Partition.mem_partOf : ∀ {α : Type u_1} {x : α} {u : Set α} {P : Partition u}, x ∈ u → x ∈ P.partOf x
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Construct a completely distributive lattice instance using the minimal amount of work needed.

This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}`, `aᶜ := a ⇨ ⊥`, `a \ b := sInf {c | a ≤ b ⊔ c}` and
`￢a := ⊤ \ a`.  -/
CompletelyDistribLattice.ofMinimalAxioms : {α : Type u} → [inst : CompleteLattice α] → CompletelyDistribLattice.MinimalAxioms α → CompletelyDistribLattice α
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax'_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)],
  (CategoryTheory.Pseudofunctor.mkOfOplax' F).toPrelaxFunctor = F.toPrelaxFunctor
-- Mathlib.Analysis.Matrix.PosDef
/-- A positive definite matrix `M` induces a norm `‖x‖ = sqrt (re xᴴMx)`.  -/
Matrix.toNormedAddCommGroup : {n : Type u_2} →
  {𝕜 : Type u_3} → [Fintype n] → [inst : RCLike 𝕜] → (M : Matrix n n 𝕜) → M.PosDef → NormedAddCommGroup (n → 𝕜)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.zsmul : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] → [inst_1 : SeminormedAddCommGroup V₂] → SMul ℤ (NormedAddGroupHom V₁ V₂)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_add_union_subset_union : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t₁ t₂ : Set α}, s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.branch a q₁ q₂) =
    insert (Turing.TM2.Stmt.branch a q₁ q₂) (Turing.TM2.stmts₁ q₁ ∪ Turing.TM2.stmts₁ q₂)
-- Init.Omega.Logic
Lean.Omega.Decidable.and_or_not_and_not_of_iff : ∀ {p q : Prop} [Decidable q], (p ↔ q) → p ∧ q ∨ ¬p ∧ ¬q
-- Mathlib.Algebra.GroupWithZero.Defs
SemigroupWithZero.toSemigroup : {S₀ : Type u} → [self : SemigroupWithZero S₀] → Semigroup S₀
-- Lean.Environment
/-- Opaque environment extension state.  -/
Lean.EnvExtensionStateSpec : (α : Type) × Inhabited α
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimitGroup : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J GrpCat) → Group ↑(GrpCat.FilteredColimits.G F)
-- Batteries.Data.Fin.Lemmas
Fin.sum_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Add α] (x : Fin 0 → α), Fin.sum x = 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_add_succ_right_eq_push' : ∀ {m n : ℕ}, (m<...=m + (n + 1)).toArray = (m<...=m + n).toArray.push (m + n + 1)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.irreducible_of_mem_factorSet : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : Associates α} {s : Associates.FactorSet α}, p ∈ s → Irreducible p
-- Init.Data.SInt.Lemmas
Int16.toInt_bmod : ∀ (x : Int16), x.toInt.bmod 65536 = x.toInt
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- The entire category viewed as a subcategory is an exponential ideal.  -/
CategoryTheory.instExponentialIdealId : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.MonoidalClosed C], CategoryTheory.ExponentialIdeal (CategoryTheory.Functor.id C)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_mul_cancel : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R}, PowerSeries.X * φ = PowerSeries.X * ψ → φ = ψ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N)
  (e_x : x = x_1) {d : ℕ} (hd : x.dim = d) (i i_1 : Fin (d + 2)),
  i = i_1 → SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i = SSet.prodStdSimplex.pairingCore.IsType₂.φ x_1 ⋯ i_1
-- Init.Data.Option.Lemmas
Option.ne_none_iff_exists : ∀ {α : Type u_1} {o : Option α}, o ≠ none ↔ ∃ x, some x = o
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, Monotone CategoryTheory.Sieve.arrows
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Partial denominator  -/
GenContFract.Pair.b : {α : Type u_1} → GenContFract.Pair α → α
-- Mathlib.Data.ZMod.IntUnitsPower
uzpow_coe_nat : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s : ℤˣ) (n : ℕ) [inst_2 : n.AtLeastTwo],
  s ^ OfNat.ofNat n = s ^ OfNat.ofNat n
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.map_map : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I)
  {j : J} {X Y : C (g j)} (f : X ⟶ Y),
  (CategoryTheory.Sigma.map C g).map (CategoryTheory.Sigma.SigmaHom.mk f) = CategoryTheory.Sigma.SigmaHom.mk f
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftComp.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃)
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (hl' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l'.app X.left) X.hom))
  (hll' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₃ R P Q W),
      P (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp l l').app X.left) X.hom)),
  CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll' =
    CategoryTheory.MorphismProperty.Comma.mapLeftComp R l l' hl hl' hll'
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.jacobiSymNat.one_left : ∀ (b : ℕ), Mathlib.Meta.NormNum.jacobiSymNat 1 b = 1
-- Mathlib.Analysis.Calculus.Implicit
/-- Implicit function theorem. If `f : E → F` and `g : E → G` are two maps strictly differentiable
at `a`, their derivatives `f'`, `g'` are surjective, and the kernels of these derivatives are
complementary subspaces of `E`, then `implicitFunction` is the unique (germ of a) map
`φ : F → G → E` such that `f (φ y z) = y` and `g (φ y z) = z`.  -/
ImplicitFunctionData.implicitFunction : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : CompleteSpace E] →
            {F : Type u_3} →
              [inst_4 : NormedAddCommGroup F] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : CompleteSpace F] →
                    {G : Type u_4} →
                      [inst_7 : NormedAddCommGroup G] →
                        [inst_8 : NormedSpace 𝕜 G] →
                          [inst_9 : CompleteSpace G] → ImplicitFunctionData 𝕜 E F G → F → G → E
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_liftExtend : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ), e.homRestrict (e.liftExtend φ hφ) = φ
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.map_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A]
  [inst_5 : Bialgebra R B] [inst_6 : Algebra R A] [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A]
  [inst_9 : Semiring C] [inst_10 : Semiring D] [inst_11 : Bialgebra S C] [inst_12 : Bialgebra R D]
  [inst_13 : Algebra R C] [inst_14 : IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D) (x : A) (y : B),
  (Bialgebra.TensorProduct.map f g) (x ⊗ₜ[R] y) = f x ⊗ₜ[R] g y
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.prod_alternatingWord_eq_mul_pow : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (m : ℕ),
  cs.wordProd (CoxeterSystem.alternatingWord i i' m) =
    (if Even m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2)
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toSemigrpIso_hom : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y] (e : X ≃* Y), e.toSemigrpIso.hom = Semigrp.ofHom e.toMulHom
-- Mathlib.Tactic.Sat.FromLRAT
/-- `f.proof c` asserts that `c` is derivable from `f`.  -/
Sat.Fmla.proof : Sat.Fmla → Sat.Clause → Prop
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mk : Lean.Syntax →
  Lean.Elab.ContextInfo →
    Lean.MetavarContext →
      Lean.MetavarContext → List Lean.MVarId → List Lean.MVarId → Mathlib.Linter.Flexible.TacticData✝
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.coe_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Order.Hom.WithTopBot
WithTop.subtypeOrderIso.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : DecidablePred fun x => x = ⊤],
  WithTop.subtypeOrderIso =
    { toFun := fun a => WithTop.untopD ⊤ (WithTop.map Subtype.val a),
      invFun := fun a => if h : a = ⊤ then ⊤ else ↑⟨a, h⟩, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Std.Async.Basic
/-- Converts a `BaseAsync` to a `BaseIO Task`.
 -/
Std.Async.BaseAsync.toBaseIO : {α : Type} → Std.Async.BaseAsync α → BaseIO (Task α)
-- Init.Data.Vector.InsertIdx
Vector.getElem?_insertIdx_self : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i : ℕ} (w : i ≤ n), (xs.insertIdx i x w)[i]? = some x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.phase : Aesop.PhaseName → Aesop.Frontend.Feature
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.mk.inj : ∀ {originSelectionRange? : Option Lean.Lsp.Range} {targetUri : Lean.Lsp.DocumentUri}
  {targetRange targetSelectionRange : Lean.Lsp.Range} {originSelectionRange?_1 : Option Lean.Lsp.Range}
  {targetUri_1 : Lean.Lsp.DocumentUri} {targetRange_1 targetSelectionRange_1 : Lean.Lsp.Range},
  { originSelectionRange? := originSelectionRange?, targetUri := targetUri, targetRange := targetRange,
        targetSelectionRange := targetSelectionRange } =
      { originSelectionRange? := originSelectionRange?_1, targetUri := targetUri_1, targetRange := targetRange_1,
        targetSelectionRange := targetSelectionRange_1 } →
    originSelectionRange? = originSelectionRange?_1 ∧
      targetUri = targetUri_1 ∧ targetRange = targetRange_1 ∧ targetSelectionRange = targetSelectionRange_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_of_X_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F}
  {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ ≠ x₂),
  WeierstrassCurve.Affine.Point.some x₁ y₁ h₁ + WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =
    WeierstrassCurve.Affine.Point.some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯
-- Mathlib.CategoryTheory.Localization.Bifunctor
/-- The natural isomorphism `F₁' ≅ F₂'` of bifunctors induced by a
natural isomorphism `e : F₁ ≅ F₂` when `Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'`
and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold.  -/
CategoryTheory.Localization.lift₂NatIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            [L₁.IsLocalization W₁] →
                              [L₂.IsLocalization W₂] →
                                [W₁.ContainsIdentities] →
                                  [W₂.ContainsIdentities] →
                                    (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                                      (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                        [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁'] →
                                          [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] →
                                            (F₁ ≅ F₂) → (F₁' ≅ F₂')
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.combine.go.match_1.splitter : (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) →
  (p₁ p₂ : Lean.Grind.CommRing.Poly) →
    ((k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂)) →
      ((k₁ k₂ : ℤ) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            (p₂ : Lean.Grind.CommRing.Poly) →
              motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)) →
        ((k₁ : ℤ) →
            (m₁ : Lean.Grind.CommRing.Mon) →
              (p₁ : Lean.Grind.CommRing.Poly) →
                (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂)) →
          ((k₁ : ℤ) →
              (m₁ : Lean.Grind.CommRing.Mon) →
                (p₁ : Lean.Grind.CommRing.Poly) →
                  (k₂ : ℤ) →
                    (m₂ : Lean.Grind.CommRing.Mon) →
                      (p₂ : Lean.Grind.CommRing.Poly) →
                        motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)) →
            motive p₁ p₂
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_apply_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  {i : Set α}, MeasurableSet i → μ.toSignedMeasure i = μ.real i
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.const : ∀ {n : ℕ} (m : ℕ), Nat.Primrec' fun x => m
-- Init.Data.String.TakeDrop
String.dropRightWhile : String → (Char → Bool) → String
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.Option.instDecidableEq.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (val : α) → motive (some val)),
  (match none with
    | none => h_1 ()
    | some val => h_2 val) =
    h_1 ()
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.w_map_wMk : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : α.Arrow β) (a : P.A) (f' : (P.drop.B a).Arrow α)
  (f : P.last.B a → P.W α), MvFunctor.map g (P.wMk a f' f) = P.wMk a (TypeVec.comp g f') fun i => MvFunctor.map g (f i)
-- Std.Do.PostCond
Std.Do.PostCond.entails.rfl : ∀ {α : Type u_1} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond α ps}, Q.entails Q
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An additive submagma of a right cancellative additive magma inherits right cancellation.  -/
AddMemClass.isRightCancelAdd : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] [IsRightCancelAdd M]
  (S : A), IsRightCancelAdd ↥S
-- Mathlib.Topology.Order.Rolle
/-- A continuous function on an unordered closed interval with `f a = f b`
takes either its maximum or its minimum value at a point in the interior of the interval.  -/
exists_uIoo_isExtrOn_uIcc : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X},
  a ≠ b → ContinuousOn f (Set.uIcc a b) → f a = f b → ∃ c ∈ Set.uIoo a b, IsExtrOn f (Set.uIcc a b) c
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.replaceEntry.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (k : α) (v : β k) (k_1 : α) (v_1 : β k_1) (l : List ((a : α) × β a)),
  Std.Internal.List.replaceEntry k v (⟨k_1, v_1⟩ :: l) =
    bif k_1 == k then ⟨k, v⟩ :: l else ⟨k_1, v_1⟩ :: Std.Internal.List.replaceEntry k v l
-- Mathlib.Algebra.Ring.NonZeroDivisors
/-- In a finite ring, an element is a unit iff it is a non-zero-divisor.  -/
isUnit_iff_mem_nonZeroDivisors_of_finite : ∀ {R : Type u_1} [inst : Ring R] {a : R} [Finite R], IsUnit a ↔ a ∈ nonZeroDivisors R
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.iff_eq : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  (I : Ideal A), Ideal.IsHomogeneous 𝒜 I ↔ (Ideal.homogeneousCore 𝒜 I).toIdeal = I
-- Mathlib.Condensed.Solid
Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit : ∀ (R : Type (u + 1)) [inst : Ring R],
  (Condensed.profiniteSolid R).IsRightKanExtension (Condensed.profiniteSolidCounit R)
-- Init.Data.Vector.Basic
/-- Array size.  -/
Vector.size_toArray : ∀ {α : Type u} {n : ℕ} (self : Vector α n), self.toArray.size = n
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.below.zero : ∀ {motive : (a : ONote) → (a_1 : Ordinal.{0}) → a.NFBelow a_1 → Prop} {b : Ordinal.{0}}, ONote.NFBelow.below ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.mapHomologicalComplexXIso.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.Category.{v', u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F G : CochainComplex C ℤ} (φ : F ⟶ G)
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] (n : ℤ),
  CochainComplex.mappingCone.mapHomologicalComplexXIso φ H n =
    CochainComplex.mappingCone.mapHomologicalComplexXIso' φ H n (n + 1) ⋯
-- Init.Data.Order.Lemmas
Std.instIdempotentOpMaxOfMaxEqOr : ∀ {α : Type u} [inst : Max α] [Std.MaxEqOr α], Std.IdempotentOp max
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.rankInfinite_iff_aleph0_le_cRank : ∀ {α : Type u} {M : Matroid α}, M.RankInfinite ↔ Cardinal.aleph0 ≤ M.cRank
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.of_dvd_add : ∀ {R : Type u_1} [inst : CommRing R] {a b r : Polynomial R} {m n : ℕ},
  n ≤ m →
    a.IsMonicOfDegree m →
      b.IsMonicOfDegree n → r.natDegree < m → b ∣ a + r → ∃ q, q.IsMonicOfDegree (m - n) ∧ a = q * b - r
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_zsmul : ∀ {α : Type u_1} (n : ℤ) (f : α → ℝ), Complex.ofReal ∘ (n • f) = n • Complex.ofReal ∘ f
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.iso_inv_base_hom_base_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat),
  (CategoryTheory.ConcreteCategory.hom e.hom.base) ((CategoryTheory.ConcreteCategory.hom e.inv.base) y) = y
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {f : α → Bool},
  m.WF → (Std.HashSet.Raw.filter f m).WF
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.eq_append_of_dropSuffix?_prop_eq_some : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {res : String.Slice},
  s.dropSuffix? P = some res → ∃ c, s = res.copy ++ String.singleton c ∧ P c
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) '' Set.Ico b c = Set.Ioc (a - c) (a - b)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.Equiv.refl : ∀ {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : LawfulMonad m] (it : Std.BundledIterM m β),
  Std.BundledIterM.Equiv m β it it
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.instIteratorLoopIdSearchStep : {ρ : Type} →
  (pat : ρ) →
    {s : String.Slice} →
      [inst : String.Slice.Pattern.ForwardPattern pat] →
        Std.IteratorLoop (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s) Id Id
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Restriction of a ring homomorphism to its range interpreted as a subsemiring.

This is the bundled version of `Set.rangeFactorization`.  -/
RingHom.rangeSRestrict : {R : Type u} →
  {S : Type v} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (f : R →+* S) → R →+* ↥f.rangeS
-- Lean.Parser.Types
/-- Reports given 'expected' messages at range of top stack element (assumed to be a single token).
Replaces the element with `missing` and resets position to the token position.
`iniPos` can be specified to avoid this position lookup but still must be identical to the token position.  -/
Lean.Parser.ParserState.mkUnexpectedTokenErrors : Lean.Parser.ParserState → List String → optParam String.Pos.Raw 0 → Lean.Parser.ParserState
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.restrictIndex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (f : ι → E.I₀) (i : ι), (E.restrictIndex f).f i = E.f (f i)