mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X] [IrreducibleSpace ↥X], CategoryTheory.IsIso (X.irreducibleComponentι Z hZ)
-- Init.Core
/-- `insert x ∅ = {x}`  -/
LawfulSingleton : (α : Type u) → (β : Type v) → [EmptyCollection β] → [Insert α β] → [Singleton α β] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.mapId_inv_app_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P : CategoryTheory.MorphismProperty T}
  (Q : CategoryTheory.MorphismProperty T) [inst_1 : Q.IsMultiplicative] [inst_2 : P.IsStableUnderComposition]
  [inst_3 : P.IsMultiplicative] [inst_4 : Q.RespectsIso] (X : T)
  (f : optParam (X ⟶ X) (CategoryTheory.CategoryStruct.id X))
  (hf : autoParam (f = CategoryTheory.CategoryStruct.id X) CategoryTheory.MorphismProperty.Under.mapId._auto_1)
  (X_1 : P.Under Q X),
  ((CategoryTheory.MorphismProperty.Under.mapId Q X f hf).inv.app X_1).right =
    CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.holo' : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (self : CuspForm Γ k), MDiff ⇑self.toSlashInvariantForm
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.nnnorm_eq_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι), ‖b i‖₊ = 1
-- Lean.Environment
/-- Finds the constant in the collection that is a prefix of `declName`, if any.  -/
_private.Lean.Environment.0.Lean.AsyncConsts.findPrefix? : Lean.AsyncConsts✝ → Lean.Name → Option Lean.AsyncConst✝
-- Mathlib.Data.Matrix.Mul
not_injective_dotProduct_left : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α),
  ¬Function.Injective (dotProduct a)
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
/-- The ideal of elements that are not units.  -/
ValuativeRel.«term𝓂[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mk : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          (X : ι → V) →
            (d : (i j : ι) → X i ⟶ X j) →
              autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam →
                autoParam
                    (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0)
                    HomologicalComplex.d_comp_d'._autoParam →
                  HomologicalComplex V c
-- Mathlib.Data.Ordmap.Ordset
Ordnode.erase.eq_2 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α) (sz : ℕ) (l : Ordnode α) (y : α) (r : Ordnode α),
  Ordnode.erase x (Ordnode.node sz l y r) =
    match cmpLE x y with
    | Ordering.lt => (Ordnode.erase x l).balanceR y r
    | Ordering.eq => l.glue r
    | Ordering.gt => l.balanceL y (Ordnode.erase x r)
-- Aesop.Script.OptimizeSyntax
_private.Aesop.Script.OptimizeSyntax.0.Aesop.addIdents : Std.HashSet Lean.Name → Lean.Syntax → Std.HashSet Lean.Name
-- Mathlib.GroupTheory.Rank
Group.rank_eq_zero_iff : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Group.FG G], Group.rank G = 0 ↔ Subsingleton G
-- Lean.Parser.Types
Lean.Parser.InputContext.fileName : Lean.Parser.InputContext → String
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a commutative semigroup, if it admits a surjective map that preserves
`*` from a commutative semigroup. See note [reducible non-instances].  -/
Function.Surjective.commSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : CommSemigroup M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x * y) = f x * f y) → CommSemigroup M₂
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.orElse_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ε : Type u} {x : ExceptT ε m α} {h : Unit → ExceptT ε m α}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  ⦃(Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)⦄ OrElse.orElse x h ⦃Q⦄
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Reinterpret a `LinearIsometryEquiv` as a `Homeomorph`.  -/
LinearIsometryEquiv.toHomeomorph : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₜ E₂
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getZero : Lean.Meta.Grind.Arith.Linear.LinearM Lean.Expr
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.length_sigma : ∀ {α : Type u_2} {σ : α → Type u_8} (l₁ : List α) (l₂ : (a : α) → List (σ a)),
  (l₁.sigma l₂).length = (List.map (fun a => (l₂ a).length) l₁).sum
-- Lean.Environment
Lean.ConstantKind.recursor.sizeOf_spec : sizeOf Lean.ConstantKind.recursor = 1
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_mul_le : ∀ {n m : ℕ}, 2 ≤ n → n * m ≤ m → m = 0
-- Std.Http.Internal.LowerCase
Std.Http.Internal.instDecidableIsLowerCase : {s : String} → Decidable (Std.Http.Internal.IsLowerCase s)
-- Init.Data.Vector.Find
Vector.find?_eq_some_iff_getElem : ∀ {α : Type} {n : ℕ} {xs : Vector α n} {p : α → Bool} {b : α},
  Vector.find? p xs = some b ↔ p b = true ∧ ∃ i, ∃ (h : i < n), xs[i] = b ∧ ∀ (j : ℕ) (hj : j < i), (!p xs[j]) = true
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_of_coprime : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → ∀ (i : ℕ), i.Coprime k → IsPrimitiveRoot (ζ ^ i) k
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.cmpEq.lt_congr_right : ∀ {α : Type u_1} {cmp : α → α → Ordering} {y z x : α},
  RBTree.RBNode.cmpEq cmp y z → (RBTree.RBNode.cmpLT cmp x y ↔ RBTree.RBNode.cmpLT cmp x z)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.forIn'_toArray_eq_forIn' : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.Rxo.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_8 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)},
  forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isFinitelySemisimple_sub_algebraMap_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, (f - (algebraMap R (Module.End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple
-- Mathlib.NumberTheory.Ostrowski
/-- There exists a minimal positive integer with absolute value smaller than 1.  -/
Rat.AbsoluteValue.exists_minimal_nat_zero_lt_and_lt_one : ∀ {f : AbsoluteValue ℚ ℝ},
  f.IsNontrivial → (∀ (n : ℕ), f ↑n ≤ 1) → ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
-- Std.Data.ByteSlice
/-- Extracts a byte from the byte slice, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array. The
default value is 0.
 -/
ByteSlice.get! : ByteSlice → ℕ → UInt8
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rio.toArray_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_5 : Std.Rxo.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rio α}, r.iter.toArray = r.toArray
-- Lean.Data.LBool
Lean.LBool.neg : Lean.LBool → Lean.LBool
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_eq_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x : ↑(Set.Icc 0 1)},
  ↑x = 1 ↔ x = 1
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The natural action of `SpecialLinearGroup R V` on `V`.  -/
SpecialLinearGroup.instDistribMulAction : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → DistribMulAction (SpecialLinearGroup R V) V
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDiv : {α : Type u_1} → [Div α] → Div (Colex α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.instEssSurjOverToOver : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T) [F.EssSurj], (CategoryTheory.CostructuredArrow.toOver F X).EssSurj
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι_assoc : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData} (h : I ≤ J) {Z : AlgebraicGeometry.Scheme} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h)
      (CategoryTheory.CategoryStruct.comp I.subschemeι h_1) =
    CategoryTheory.CategoryStruct.comp J.subschemeι h_1
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.getPendingMVarErrorMessage.interpretedAsParameters : List Lean.Name → Lean.MessageData
-- Lean.Elab.Deriving.Util
/-- Make fresh, hygienic names for every parameter and index of an inductive declaration.

For example, `inductive Foo {α : Type} : Nat → Type` will give something like ``#[`α✝, `a✝]``.  -/
Lean.Elab.Deriving.mkInductArgNames : Lean.InductiveVal → Lean.Elab.TermElabM (Array Lean.Name)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderivWithin_csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x →
      fderivWithin ℂ (fun x => Complex.sin (f x)) s x = Complex.cos (f x) • fderivWithin ℂ f s x
-- Std.Http.Protocol.H1.Writer
/-- Writes accumulated user data to output using fixed-size encoding.
 -/
Std.Http.Protocol.H1.Writer.writeFixedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → ℕ → Std.Http.Protocol.H1.Writer dir × ℕ
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.refine_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S T : J.Cover X} (x : CategoryTheory.Meq P T) (e : S ⟶ T) (I : S.Arrow),
  ↑(x.refine e) I = ↑x { Y := I.Y, f := I.f, hf := ⋯ }
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_2 : HAdd Std.Time.Nanosecond.Offset Std.Time.Minute.Offset Std.Time.Nanosecond.Offset
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toAdditionalRules : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      Aesop.Frontend.RuleExpr → Aesop.Frontend.RuleConfig → Aesop.RuleSetName → m (Array Aesop.Frontend.RuleConfig)
-- Std.Do.SPred.SPred
/-- Implication in `SPred`: states that satisfy `Q` whenever they satisfy `P` satisfy `spred(P → Q)`.
 -/
Std.Do.SPred.imp : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Std.Do.SPred σs
-- Std.Data.HashSet.Raw
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.HashSet.Raw.forIn : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → (α → β → m (ForInStep β)) → β → Std.HashSet.Raw α → m β
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = false → (Std.DHashMap.Const.alter m k f).contains k' = m.contains k'
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.smul_X : ∀ {A : Type u_1} [inst : CommRing A] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra A R] {τ : Type u_3} (a : A)
  (t : τ), PowerSeries.HasSubst (a • MvPowerSeries.X t)
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.numNodes : Lean.PersistentArray.Stats → ℕ
-- Mathlib.Algebra.Order.ToIntervalMod
QuotientAddGroup.equivIcoMod_zero : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), (QuotientAddGroup.equivIcoMod hp a) 0 = ⟨toIcoMod hp a 0, ⋯⟩
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `Measurable.mul` -/
Measurable.fun_mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f g : α → M}
  [MeasurableMul₂ M], Measurable f → Measurable g → Measurable fun i => f i * g i
-- Mathlib.Data.NNReal.Defs
NNReal.abs_eq : ∀ (x : NNReal), |↑x| = ↑x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (φ : W.RightFraction X Y) {Z : C} (h : φ.leftFraction.Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp φ.leftFraction.s h) =
    CategoryTheory.CategoryStruct.comp φ.s (CategoryTheory.CategoryStruct.comp φ.leftFraction.f h)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_add_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n
-- Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
NonarchimedeanGroup.exists_openSubgroup_separating : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [NonarchimedeanGroup G] [T2Space G] {a b : G},
  a ≠ b → ∃ V, Disjoint (a • ↑V) (b • ↑V)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- Changing the origin of a formal multilinear series `p`, so that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense.
 -/
FormalMultilinearSeries.changeOrigin : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → FormalMultilinearSeries 𝕜 E F → E → FormalMultilinearSeries 𝕜 E F
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivaryOn_neg_right`. -/
AntivaryOn.of_neg_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : AddCommGroup β]
  [inst_2 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f (-g) s → MonovaryOn f g s
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₁.src : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Obj
-- Lean.Meta.Sym.Canon
/-- Returns `true` if `shouldCanon pinfos i arg` is not `.visit`.
This is a helper function used to implement mbtc.
 -/
Lean.Meta.Sym.Canon.isSupport : Array Lean.Meta.ParamInfo → ℕ → Lean.Expr → Lean.MetaM Bool
-- Init.Data.UInt.Lemmas
UInt16.lt_or_eq_of_le : ∀ {a b : UInt16}, a ≤ b → a < b ∨ a = b
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.sum.eq_2 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (v : Fin 1 → α), FinVec.sum v = v 0
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `MulEquivClass F α β`
into an actual `OrderMonoidIso`. This is declared as the default coercion from `F` to `α ≃*o β`.  -/
OrderMonoidIsoClass.toOrderMonoidIso : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulOneClass α] →
            [inst_3 : MulOneClass β] →
              [inst_4 : EquivLike F α β] → [OrderIsoClass F α β] → [MulEquivClass F α β] → F → α ≃*o β
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.hc : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ), FermatLastTheoremForThreeGen.Solution'.c✝ self ≠ 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NNReal.instContinuousMap.UniqueHom : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [IsSemitopologicalRing A] [T2Space A], ContinuousMap.UniqueHom NNReal A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_maxKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      cmp ((Std.DTreeMap.Raw.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- The orthogonal projection onto a subspace.  -/
Submodule.orthogonalProjection : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E →L[𝕜] ↥K
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.PromiseCheckedResult.mk : Lean.Environment → Lean.Environment → IO.Promise Lean.Kernel.Environment → Lean.Environment.PromiseCheckedResult
-- Mathlib.Topology.MetricSpace.IsometricSMul
instIsIsometricVAddAddOpposite : ∀ {M : Type u} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : VAdd M X] [IsIsometricVAdd M X],
  IsIsometricVAdd M Xᵃᵒᵖ
-- Lean.Server.CodeActions.Attr
_private.Lean.Server.CodeActions.Attr.0.Lean.CodeAction.mkHoleCodeAction.unsafe_1 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.HoleCodeAction
-- Mathlib.Algebra.Lie.Loop
/-- A linear isomorphism to finitely supported functions.  -/
LieAlgebra.LoopAlgebra.toFinsupp : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieAlgebra.loopAlgebra R A L ≃ₗ[R] A →₀ L
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_le_toReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toReal ≤ b.toReal ↔ a ≤ b)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹.Nonempty ↔ s.Nonempty
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toBitVec = OfNat.ofNat n
-- Std.Data.DTreeMap.Internal.Operations
/-- The key.  -/
Std.DTreeMap.Internal.Impl.RawView.k : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl.RawView α β → α
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.tr_ret_cons₁ : ∀ (fs : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.tr (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)) =
    Turing.TM2.Stmt.goto fun x =>
      Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.main Turing.PartrecToTM2.K'.aux
        (Turing.PartrecToTM2.move₂ (fun s => decide (s = Turing.PartrecToTM2.Γ'.consₗ)) Turing.PartrecToTM2.K'.stack
          Turing.PartrecToTM2.K'.main
          (Turing.PartrecToTM2.move₂ (fun x => false) Turing.PartrecToTM2.K'.aux Turing.PartrecToTM2.K'.stack
            (Turing.PartrecToTM2.trNormal fs k.cons₂)))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m.insertManyIfNewUnit [] = m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The natural isomorphism `R ⊗[R₀] S₀ ≃ₐ[R] S`.  -/
Algebra.Presentation.tensorModelOfHasCoeffsEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {P : Algebra.Presentation R S ι σ} →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] →
                          [inst_7 : P.HasCoeffs R₀] →
                            TensorProduct R₀ R (Algebra.Presentation.ModelOfHasCoeffs R₀) ≃ₐ[R] S
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivAt.mul'` -/
HasFDerivAt.fun_mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸}
  {a' b' : E →L[𝕜] 𝔸},
  HasFDerivAt a a' x → HasFDerivAt b b' x → HasFDerivAt (fun i => a i * b i) (a x • b' + MulOpposite.op (b x) • a') x
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.Type.enoughInjectives : CategoryTheory.EnoughInjectives (Type u₁)
-- Aesop.Search.SearchM
Aesop.modifyTree : {Q : Type} → [inst : Aesop.Queue Q] → (Aesop.Tree → Aesop.Tree) → Aesop.SearchM Q Unit
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubmonoid.mem_even : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a : M}, a ∈ AddSubmonoid.even M ↔ Even a
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given a "bowtie" of morphisms
```
 k₁   k₂
 |\  /|
 | \/ |
 | /\ |
 |/  \∣
 vv  vv
 j₁  j₂
```
in a cofiltered category, we can construct an object `s` and two morphisms
from `s` to `k₁` and `k₂`, making the resulting squares commute.
 -/
CategoryTheory.IsCofiltered.bowtie : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j₁ j₂ k₁ k₂ : C}
  (f₁ : k₁ ⟶ j₁) (g₁ : k₂ ⟶ j₁) (f₂ : k₁ ⟶ j₂) (g₂ : k₂ ⟶ j₂),
  ∃ s α β,
    CategoryTheory.CategoryStruct.comp α f₁ = CategoryTheory.CategoryStruct.comp β g₁ ∧
      CategoryTheory.CategoryStruct.comp α f₂ = CategoryTheory.CategoryStruct.comp β g₂
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_neg_add_iff_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α}, 0 < -b + a ↔ b < a
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- Given a free group basis of `G` over `ι`, there is a canonical bijection between maps from `ι`
to a group `H` and morphisms from `G` to `H`.  -/
FreeGroupBasis.lift : {ι : Type u_1} →
  {G : Type u_3} → {H : Type u_4} → [inst : Group G] → [inst_1 : Group H] → FreeGroupBasis ι G → (ι → H) ≃ (G →* H)
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.mono : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α},
  IsCompactlyGenerated.BooleanGenerators S → ∀ {T : Set α}, T ⊆ S → IsCompactlyGenerated.BooleanGenerators T
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMapM.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Data.Set.Function
Set.surjOn_iff_exists_bijOn_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t ↔ ∃ s' ⊆ s, Set.BijOn f s' t
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityInt32HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_coe : ∀ (n : ℕ), ↑↑n = ↑n