mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.plusCompIso_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.plusMap η) F) (J.plusCompIso F Q).hom =
    CategoryTheory.CategoryStruct.comp (J.plusCompIso F P).hom (J.plusMap (CategoryTheory.Functor.whiskerRight η F))
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- An equalizer cone for a parallel pair `f` and `g`  -/
CategoryTheory.Limits.equalizer.fork : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) → [CategoryTheory.Limits.HasEqualizer f g] → CategoryTheory.Limits.Fork f g
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_add_left : ∀ {R : Type u_1} [inst : CommRing R] (a b c : Polynomial R), (a + b).wronskian c = a.wronskian c + b.wronskian c
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.im_smul_eq_div_normSq : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  (g • z).im =
    z.im /
      Complex.normSq
        (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))
          ↑z)
-- Batteries.Recycling.RBTree.Depth
_private.Batteries.Recycling.RBTree.Depth.0.RBTree.RBNode.depthLB.match_1.splitter : (motive : RBTree.RBColor → ℕ → Sort u_1) →
  (x : RBTree.RBColor) →
    (x_1 : ℕ) → ((n : ℕ) → motive RBTree.RBColor.red n) → ((n : ℕ) → motive RBTree.RBColor.black n) → motive x x_1
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_mul_unit_right_right : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsUnit x → (IsRelPrime y (z * x) ↔ IsRelPrime y z)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.removeNth_update_succAbove : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : Fin (n + 1)) (i : Fin n) (x : α (p.succAbove i))
  (f : (j : Fin (n + 1)) → α j), p.removeNth (Function.update f (p.succAbove i) x) = Function.update (p.removeNth f) i x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.jacobiTheta₂''_conj : ∀ (z τ : ℂ),
  (starRingEnd ℂ) (HurwitzZeta.jacobiTheta₂'' z τ) = HurwitzZeta.jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.traj_map_frestrictLe : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a b : ℕ),
  (ProbabilityTheory.Kernel.traj κ a).map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialTraj κ a b
-- Mathlib.Data.List.SplitBy
List.splitBy_nil : ∀ {α : Type u_1} (r : α → α → Bool), List.splitBy r [] = []
-- Mathlib.Algebra.GroupWithZero.Basic
div_zero : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a / 0 = 0
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.eq_1 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s : AffineSubspace R P) (x y : P), s.SOppSide x y = (s.WOppSide x y ∧ x ∉ s ∧ y ∉ s)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zero_zpow_eq : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R] (n : ℤ),
  0 ^ n = if n = 0 then 1 else 0
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_eq_zero_iff_add_comm : ∀ {G : Type u_1} [inst : AddGroup G] {g₁ g₂ : G}, ⁅g₁, g₂⁆ = 0 ↔ g₁ + g₂ = g₂ + g₁
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) `a`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.a : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} → (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) → D.obj self.i ⟶ X
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.HasTrivialRadical R L], (LieAlgebra.ad R L).ker = ⊥
-- Init.Data.List.MinMaxOn
List.minOn_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α}
  {f : α → β}, List.minOn f (x :: xs) ⋯ = if h : xs = [] then x else minOn f x (List.minOn f xs h)
-- Mathlib.Order.Bounds.Image
BddBelow.image2_bddAbove : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : Add α] [inst_1 : SMul γ β],
  Function.Periodic f c → ∀ (a : γ), Function.Periodic (a • f) c
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.le_iff_bounds : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, I ≤ J ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
-- Mathlib.Data.Finset.Functor
Multiset.traverse.congr_simp : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : CommApplicative F] {α' β' : Type u} (f f_1 : α' → F β'),
  f = f_1 → ∀ (a a_1 : Multiset α'), a = a_1 → Multiset.traverse f a = Multiset.traverse f_1 a_1
-- Aesop.Script.TacticState
Aesop.Script.TacticState.onGoalM : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      {α : Type} →
        Aesop.Script.TacticState →
          Lean.MVarId → (Aesop.Script.TacticState → m (α × Aesop.Script.TacticState)) → m (α × Aesop.Script.TacticState)
-- Mathlib.Logic.Function.Coequalizer
/-- The canonical projection to the coequalizer.  -/
Function.Coequalizer.mk : {α : Type u_1} → {β : Type u_2} → (f g : α → β) → β → Function.Coequalizer f g
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.LFunctionTrivChar₁.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n] (a a_1 : ℂ),
  a = a_1 → DirichletCharacter.LFunctionTrivChar₁ n a = DirichletCharacter.LFunctionTrivChar₁ n_1 a_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roc_eq_some_iff : ∀ {k m n i : ℕ}, (m<...=n).toList[i]? = some k ↔ i < n - m ∧ m + 1 + i = k
-- Init.Data.Option.Lemmas
Option.some_eq_ite_none_right : ∀ {α : Type u_1} {a : α} {p : Prop} {x : Decidable p} {b : Option α}, (some a = if p then b else none) ↔ p ∧ some a = b
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.str : (self : AddSemigrp) → AddSemigroup ↑self
-- Init.Data.String.TakeDrop
String.Internal.nextWhileImpl : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Topology.Order.DenselyOrdered
frontier_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [NoMaxOrder α] {a b : α}, a ≤ b → frontier (Set.Icc a b) = {a, b}
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.toProd_comp_ofProd : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂),
  (CliffordAlgebra.toProd Q₁ Q₂).comp (CliffordAlgebra.ofProd Q₁ Q₂) =
    AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
/-- The fiber of a prime `p` of `R` in an `R`-algebra `S`, defined to be `κ(p) ⊗ S`.

See `PrimeSpectrum.preimageHomeomorphFiber` for the homeomorphism between the spectrum of it
and the actual set-theoretic fiber of `PrimeSpectrum S → PrimeSpectrum R` at `p`.  -/
Ideal.Fiber : {R : Type u_1} →
  [inst : CommRing R] →
    (p : Ideal R) → [p.IsPrime] → (S : Type u_3) → [inst_2 : AddCommGroup S] → [Module R S] → Type (max u_3 u_1)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a multiplication-invariant pseudodistance.  -/
NormedCommGroup.ofMulDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : CommGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)) → NormedCommGroup E
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.mul_slash_SL2 : ∀ (k1 k2 : ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f g : UpperHalfPlane → ℂ),
  SlashAction.map (k1 + k2) A (f * g) = SlashAction.map k1 A f * SlashAction.map k2 A g
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.source_preimage_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.source ⊆ ↑e ⁻¹' e.target
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The single functor `C ⥤ DerivedCategory.Plus C` which sends `X : C` to the
single cochain complex with `X` sitting in degree `n : ℤ`.  -/
DerivedCategory.Plus.singleFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → ℤ → CategoryTheory.Functor C (DerivedCategory.Plus C)
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type E₆.

The corresponding Coxeter-Dynkin diagram is:
```
                o
                |
    o --- o --- o --- o --- o
```
 -/
CoxeterMatrix.E₆ : CoxeterMatrix (Fin 6)
-- Mathlib.RingTheory.FiniteType
/-- An additive monoid `M` is finitely generated if and only if `R[M]` is of
finite type.  -/
AddMonoidAlgebra.finiteType_iff_fg : ∀ {R : Type u_1} {M : Type u_2} [inst : AddMonoid M] [inst_1 : CommRing R] [Nontrivial R],
  Algebra.FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  (Std.DHashMap.filter (fun k x => f k) m).getKey! k = (Option.filter f (m.getKey? k)).get!
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} {f : Option β → Option β} {t : Std.TreeMap.Raw α β cmp},
  t.WF → (t.alter a f).WF
-- Lean.Data.Trie
Lean.Data.Trie.brecOn.eq : ∀ {α : Type} {motive_1 : Lean.Data.Trie α → Sort u} {motive_2 : Array (Lean.Data.Trie α) → Sort u}
  {motive_3 : List (Lean.Data.Trie α) → Sort u} (t : Lean.Data.Trie α)
  (F_1 : (t : Lean.Data.Trie α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Data.Trie α)) → Lean.Data.Trie.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Data.Trie α)) → Lean.Data.Trie.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.Data.Trie.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.Ring.Idempotent
isIdempotentElem_iff_mul_one_sub_self : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a ↔ a * (1 - a) = 0
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank.eq_1 : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] (A : Matrix m n R),
  A.cRank = Module.rank R ↥(Submodule.span R (Set.range A.col))
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_zero_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (i : n),
  Matrix.updateCol 0 i 0 = 0
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Constructs intermediate states of an iterator created with the combinator `IterM.dropWhile`.
When `it.dropWhile P` has stopped dropping elements, its new state cannot be created
directly with `IterM.dropWhile` but only with `Intermediate.dropWhile`.

`Intermediate.dropWhile` is meant to be used only for internally or for verification purposes.
 -/
Std.IterM.Intermediate.dropWhile : {α : Type w} →
  {m : Type w → Type w'} → {β : Type w} → [inst : Monad m] → (P : β → Bool) → Bool → Std.IterM m β → Std.IterM m β
-- Mathlib.Order.Filter.Defs
/-- `IsCoboundedUnder (≺) f u` states that the image of the filter `f` under the map `u` does not
tend to infinity w.r.t. `≺`. This is also called frequently bounded. Will be usually instantiated
with `≤` or `≥`.  -/
Filter.IsCoboundedUnder : {α : Type u_1} → {β : Type u_2} → (α → α → Prop) → Filter β → (β → α) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.ExactAt.isZero_homology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex C c} {i : ι} [inst_2 : K.HasHomology i],
  K.ExactAt i → CategoryTheory.Limits.IsZero (K.homology i)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.isometryEquivBoundedOfCompact_toEquiv : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  (ContinuousMap.isometryEquivBoundedOfCompact α β).toEquiv = ContinuousMap.equivBoundedOfCompact α β
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_uSizeToNat : ∀ (n : USize) (h : n.toNat < UInt8.size), UInt8.ofNatLT n.toNat h = n.toUInt8
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- The last dart of a walk.  -/
SimpleGraph.Walk.lastDart : {V : Type u} → {G : SimpleGraph V} → {v w : V} → (p : G.Walk v w) → ¬p.Nil → G.Dart
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.Mon C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Endowing the space `PiLp p β` with the `L^p` norm. We register this instance
separate from `PiLp.seminormedAddCommGroup` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future norm-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. These are called *quasi-norms*.  -/
PiLp.instNorm : (p : ENNReal) → {ι : Type u_2} → (β : ι → Type u_4) → [Fintype ι] → [(i : ι) → Norm (β i)] → Norm (PiLp p β)
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (f : ContMDiffMap I I' M M' n), ContMDiff I I' n ⇑f
-- Mathlib.NumberTheory.PythagoreanTriples
/-- `(k*x, k*y, k*z)` is a Pythagorean triple if and only if
`(x, y, z)` is also a triple.  -/
PythagoreanTriple.mul_iff : ∀ {x y z : ℤ} (k : ℤ), k ≠ 0 → (PythagoreanTriple (k * x) (k * y) (k * z) ↔ PythagoreanTriple x y z)
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.map_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₗ[R] N) (x : M)
  (y : ↥S), ((LocalizedModule.map S) f) (LocalizedModule.mk x y) = LocalizedModule.mk (f x) y
-- Lean.Meta.Coe
/-- Return `true` if `type` is of the form `m α` where `m` is a `Monad`.
Note that we reduce `type` using transparency `[reducible]`.
 -/
Lean.Meta.isMonadApp : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Logic.Equiv.Fintype
/-- Computably turn an embedding `f : α ↪ β` into an equiv `α ≃ Set.range f`,
if `α` is a `Fintype`. Has poor computational performance, due to exhaustive searching in
constructed inverse. When a better inverse is known, use `Equiv.ofLeftInverse'` or
`Equiv.ofLeftInverse` instead. This is the computable version of `Equiv.ofInjective`.
 -/
Function.Embedding.toEquivRange : {α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → (f : α ↪ β) → α ≃ ↑(Set.range ⇑f)
-- Init.Core
/-- `a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. -/
Ne : {α : Sort u} → α → α → Prop
-- Init.Data.SInt.Bitwise
Int8.toUInt8_and : ∀ (a b : Int8), (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath.eq_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (x b : C) (p : Quiver.Path X b) (e : b ⟶ x),
  CategoryTheory.composePath (p.cons e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath p) e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_alter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k k' : α} {fallback : β} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k' fallback =
        if compare k k' = Ordering.eq then (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
        else Std.DTreeMap.Internal.Impl.Const.getD t k' fallback
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.rotate.obj₂ = T.obj₃
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.mul_kstar_le_self : ∀ {α : Type u_5} [self : KleeneAlgebra α] (a b : α), b * a ≤ b → b * KStar.kstar a ≤ b
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
/-- A cone on `F` with cone point `X` is the same as an element of `lim Hom(X, F·)`.  -/
CategoryTheory.Limits.limitCompCoyonedaIsoCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (X : C) →
            CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) ≅
              (CategoryTheory.Functor.const J).obj X ⟶ F
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.IntFractPair.stream_eq_none_of_fr_eq_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → ifp_n.fr = 0 → GenContFract.IntFractPair.stream v (n + 1) = none
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map_id : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.map (fun exp => exp) (fun coef => coef) ms = ms
-- Aesop.Forward.State
Aesop.ClusterState.mk.inj : ∀ {slots : Array Aesop.Slot} {conclusionDeps : Array Aesop.PremiseIndex} {variableMap : Aesop.VariableMap}
  {completeMatches : Lean.PHashSet Aesop.Match} {haveHypForEachSlot : Bool} {slotQueues : Array (Array Aesop.RawHyp)}
  {slotQueues_size : slotQueues.size = slots.size} {slots_1 : Array Aesop.Slot}
  {conclusionDeps_1 : Array Aesop.PremiseIndex} {variableMap_1 : Aesop.VariableMap}
  {completeMatches_1 : Lean.PHashSet Aesop.Match} {haveHypForEachSlot_1 : Bool}
  {slotQueues_1 : Array (Array Aesop.RawHyp)} {slotQueues_size_1 : slotQueues_1.size = slots_1.size},
  { slots := slots, conclusionDeps := conclusionDeps, variableMap := variableMap, completeMatches := completeMatches,
        haveHypForEachSlot := haveHypForEachSlot, slotQueues := slotQueues, slotQueues_size := slotQueues_size } =
      { slots := slots_1, conclusionDeps := conclusionDeps_1, variableMap := variableMap_1,
        completeMatches := completeMatches_1, haveHypForEachSlot := haveHypForEachSlot_1, slotQueues := slotQueues_1,
        slotQueues_size := slotQueues_size_1 } →
    slots = slots_1 ∧
      conclusionDeps = conclusionDeps_1 ∧
        variableMap = variableMap_1 ∧
          completeMatches = completeMatches_1 ∧ haveHypForEachSlot = haveHypForEachSlot_1 ∧ slotQueues = slotQueues_1
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedVarId.default : Lean.IR.VarId
-- Mathlib.Analysis.Convex.Function
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is concave it suffices to
verify the inequality `a • f x + b • f y ≤ f (a • x + b • y)` for `x < y` and positive `a`, `b`. The
main use case is `E = ℝ` however one can apply it, e.g., to `ℝ^n` with lexicographic order.  -/
LinearOrder.concaveOn_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β]
  [inst_7 : LinearOrder E] {s : Set E} {f : E → β},
  Convex 𝕜 s →
    (∀ ⦃x : E⦄,
        x ∈ s →
          ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)) →
      ConcaveOn 𝕜 s f
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.lcm_apply_mul_gcd_apply : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {x y : ℕ}, f (x.lcm y) * f (x.gcd y) = f x * f y
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.eq_1 : ∀ (n a b : ℕ), (a ≡ b [MOD n]) = (a % n = b % n)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbot_zero : ∀ {α : Type u} [inst : Zero α], WithBot.unbot 0 ⋯ = 0
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toFun_eq_coe : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {f : CentroidHom α}, (↑f.toAddMonoidHom).toFun = ⇑f
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] (X : CategoryTheory.Idempotents.Karoubi A),
  CategoryTheory.Epi ((CategoryTheory.Abelian.LeftResolution.karoubi.π Λ).app X)
-- Batteries.Lean.AttributeExtra
Lean.ParametricAttributeExtra.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (attr : Lean.ParametricAttribute α) (base : Std.HashMap Lean.Name α),
  sizeOf { attr := attr, base := base } = 1 + sizeOf attr + sizeOf base
-- Std.Data.DTreeMap.Internal.Model
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getEntryGE?ₘ : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)