mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.cfcAbs_cfcAbs : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A),
  CFC.abs (CFC.abs a) = CFC.abs a
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isLittleO_atTop_of_degree_lt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜], P.degree < Q.degree → (fun x => Polynomial.eval x P) =o[Filter.atTop] fun x => Polynomial.eval x Q
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) {X Y : C} (φ : X ⟶ Y),
  ((t.eTriangleLTGE.obj i).map φ).hom₁ = (t.eTruncLT.obj i).map φ
-- Mathlib.Algebra.Ring.Ext
Semiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : Semiring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Algebra.Quaternion
Quaternion.instMulAction : {S : Type u_1} →
  {R : Type u_3} → [inst : CommRing R] → [inst_1 : Monoid S] → [MulAction S R] → MulAction S (Quaternion R)
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The token for the `⏳️` HTML that represents the state of the ongoing computations.  -/
Mathlib.Tactic.ClickSuggestions.Context.statusToken : Mathlib.Tactic.ClickSuggestions.Context → ProofWidgets.RefreshToken
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.SingleFunctors.postcomp.eq_1 : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A],
  F.postcomp G =
    { functor := fun a => (F.functor a).comp G,
      shiftIso := fun n a a' ha' =>
        (F.functor a').associator G (CategoryTheory.shiftFunctor E n) ≪≫
          (F.functor a').isoWhiskerLeft (CategoryTheory.Functor.commShiftIso G n).symm ≪≫
            ((F.functor a').associator (CategoryTheory.shiftFunctor D n) G).symm ≪≫
              CategoryTheory.Functor.isoWhiskerRight (F.shiftIso n a a' ha') G,
      shiftIso_zero := ⋯, shiftIso_add := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.leftIso_inv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (e : ψ ≅ ψ'),
  (CategoryTheory.Limits.CatCospanTransform.leftIso e).inv = e.inv.left
-- Mathlib.MeasureTheory.Measure.Stieltjes
subsingleton_botSet : ∀ {R : Type u_1} [inst : LinearOrder R], botSet.Subsingleton
-- Init.Data.UInt.Lemmas
UInt64.ofNat_uInt16ToNat : ∀ (n : UInt16), UInt64.ofNat n.toNat = n.toUInt64
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_append : ∀ {m n : ℕ}, m < n → (m<...=n).toList = (m<...=n - 1).toList ++ [n]
-- Init.Data.Array.Bootstrap
Array.foldlM_toList : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {init : β} {xs : Array α},
  List.foldlM f init xs.toList = Array.foldlM f init xs
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  (∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0) → v.AbsolutelyContinuous w
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.succ_lt_iSup_of_ne_iSup : ∀ {ι : Type u_3} {f : ι → Ordinal.{u}} [Small.{u, u_3} ι],
  (∀ (i : ι), f i ≠ iSup f) → ∀ {a : Ordinal.{u}}, a < iSup f → Order.succ a < iSup f
-- Init.Core
Substring.Raw.mk.injEq : ∀ (str : String) (startPos stopPos : String.Pos.Raw) (str_1 : String) (startPos_1 stopPos_1 : String.Pos.Raw),
  ({ str := str, startPos := startPos, stopPos := stopPos } =
      { str := str_1, startPos := startPos_1, stopPos := stopPos_1 }) =
    (str = str_1 ∧ startPos = startPos_1 ∧ stopPos = stopPos_1)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.algebraMap_injective : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → Function.Injective ⇑(algebraMap R A)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.mono : ∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) {c₁ c₂ : NNReal} {l₁ l₂ : BoxIntegral.IntegrationParams}
  {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I},
  l₁ ≤ l₂ → c₁ ≤ c₂ → (∀ x ∈ BoxIntegral.Box.Icc I, r₁ x ≤ r₂ x) → l₁.MemBaseSet I c₁ r₁ π → l₂.MemBaseSet I c₂ r₂ π
-- Mathlib.Algebra.Group.Commute.Units
Commute.units_inv_right_iff : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {u : Mˣ}, Commute a ↑u⁻¹ ↔ Commute a ↑u
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryLT! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α → α × β
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_vadd_left_iff : ∀ {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} {v : V}, v ∈ s.direction → (s.WSameSide (v +ᵥ x) y ↔ s.WSameSide x y)
-- Mathlib.CategoryTheory.Square
/-- The natural transformation `F.mapSquare ⟶ G.mapSquare` induces
by a natural transformation `F ⟶ G`.  -/
CategoryTheory.NatTrans.mapSquare : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} → (F ⟶ G) → (F.mapSquare ⟶ G.mapSquare)
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.mk.inj : ∀ {isHoverPosOnStop : Bool} {size : ℕ} {isVariableInfo isPartialTermInfo isHoverPosOnStop_1 : Bool} {size_1 : ℕ}
  {isVariableInfo_1 isPartialTermInfo_1 : Bool},
  { isHoverPosOnStop := isHoverPosOnStop, size := size, isVariableInfo := isVariableInfo,
        isPartialTermInfo := isPartialTermInfo } =
      { isHoverPosOnStop := isHoverPosOnStop_1, size := size_1, isVariableInfo := isVariableInfo_1,
        isPartialTermInfo := isPartialTermInfo_1 } →
    isHoverPosOnStop = isHoverPosOnStop_1 ∧
      size = size_1 ∧ isVariableInfo = isVariableInfo_1 ∧ isPartialTermInfo = isPartialTermInfo_1
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
/-- The topological abelianization of `absoluteGaloisGroup`, that is, the quotient of
`absoluteGaloisGroup` by the topological closure of its commutator subgroup.  -/
Field.absoluteGaloisGroupAbelianization : (K : Type u_1) → [Field K] → Type u_1
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- If `R` is a ring that has enough roots of unity and `n ≠ 0`, then for each
`a ≠ 1` in `ZMod n`, there exists a Dirichlet character `χ` mod `n` with values in `R`
such that `χ a ≠ 1`.  -/
DirichletCharacter.exists_apply_ne_one_of_hasEnoughRootsOfUnity : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [Nontrivial R] ⦃a : ZMod n⦄, a ≠ 1 → ∃ χ, χ a ≠ 1
-- Aesop.Tree.Check
_private.Aesop.Tree.Check.0.Aesop.MVarClusterRef.mvarClusterId : Aesop.MVarCluster → BaseIO String
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.zero_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (v : V), 0 v = 0
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C}
  [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.Small] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), CategoryTheory.Presieve.IsSheafFor P E.presieve₀
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.alterKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)),
  Std.Internal.List.alterKey k f l =
    match f (Std.Internal.List.getValueCast? k l) with
    | none => Std.Internal.List.eraseKey k l
    | some v => Std.Internal.List.insertEntry k v l
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a fallback : α},
  (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_mul_iff_one_le_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulMono α]
  [PosMulReflectLE α], 0 < a → (a ≤ a * b ↔ 1 ≤ b)
-- Init.Data.Option.List
Option.toList_map : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → β}, (Option.map f o).toList = List.map f o.toList
-- Mathlib.Algebra.Group.Defs
/-- Addition is right cancellative (i.e. right regular).  -/
IsRightCancelAdd.add_right_cancel : ∀ {G : Type u} {inst : Add G} [self : IsRightCancelAdd G] (a : G), IsAddRightRegular a
-- Mathlib.RingTheory.Invariant.Basic
Algebra.IsInvariant.orbit_eq_primesOver : ∀ (A : Type u_1) (B : Type u_2) (G : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] [SMulCommClass G A B]
  (P : Ideal A) (Q : Ideal B) [hP : Q.LiesOver P] [hQ : Q.IsPrime], MulAction.orbit G Q = P.primesOver B
-- Mathlib.Data.Nat.Bitwise
Nat.lor_comm : ∀ (n m : ℕ), n ||| m = m ||| n
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.totalDegree_trunc' : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] {n : σ →₀ ℕ} (φ : MvPowerSeries σ R),
  ((MvPowerSeries.trunc' R n) φ).totalDegree ≤ Finsupp.degree n
-- Std.Http.Server.Config
/-- Maximum number of extensions on a single chunk-size line (default: 16).
 -/
Std.Http.Config.maxChunkExtensions : Std.Http.Config → ℕ
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The `q`-expansion of a function on the upper half plane with strict period `h`, bundled as a
`PowerSeries`. The `m`-th coefficient is the Taylor coefficient of the `cuspFunction` at `q = 0`,
where `q = exp(2πiτ/h)` is the local parameter at the cusp.  -/
UpperHalfPlane.qExpansion : ℝ → (UpperHalfPlane → ℂ) → PowerSeries ℂ
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
deriv_comp_const_add : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a x : 𝕜), deriv (fun x => f (a + x)) x = deriv f (a + x)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.periods : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → Set (ι → ℕ)
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.integral_map_cast_poissonMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {R : Type u_2} [inst_1 : NatCast R] [inst_2 : MeasurableSpace R]
  [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] (r : NNReal) [Countable R] [MeasurableSingletonClass R]
  (f : R → E),
  ∫ (x : R), f x ∂MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r) =
    ∑' (n : ℕ), (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • f ↑n
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of a finite set is
finite-dimensional.  -/
finiteDimensional_direction_affineSpan_of_finite : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, s.Finite → FiniteDimensional k ↥(affineSpan k s).direction
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndInv.eq_1 : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  (A : Rep.{u, u, u} k G) (B : Rep.{u, u, u} k H),
  Rep.coinvariantsTensorIndInv φ A B =
    ModuleCat.ofHom
      (Representation.Coinvariants.lift
        (((CategoryTheory.MonoidalCategory.curriedTensor (Rep.{u, u, u} k G)).obj A).obj (Rep.res φ B)).ρ
        (TensorProduct.lift ((Rep.ind φ A).coinvariantsTensorMk B ∘ₗ Representation.IndV.mk φ A.ρ 1)) ⋯)
-- Plausible.Sampleable
Plausible.NoShrink.mk : {α : Type u_1} → α → Plausible.NoShrink α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_list_eq_foldl : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtDHashMap.Const.insertManyIfNewUnit m l = List.foldl (fun acc a => acc.insertIfNew a ()) m l
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b < slope f a c`.  -/
lineMap_lt_map_iff_slope_lt_slope : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  a < b →
    0 < r →
      r < 1 →
        ((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
          slope f ((AffineMap.lineMap a b) r) b < slope f a ((AffineMap.lineMap a b) r))
-- Lean.Expr
/-- `.fvar fvarId` is now the preferred form.
This function is seldom used, free variables are often automatically created using the
telescope functions (e.g., `forallTelescope` and `lambdaTelescope`) at `MetaM`.
 -/
Lean.mkFVar : Lean.FVarId → Lean.Expr
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))),
  CategoryTheory.Presheaf.imageSieve f s =
    (CategoryTheory.Subfunctor.range (CategoryTheory.Functor.whiskerRight f (CategoryTheory.forget A))).sieveOfSection s
-- Mathlib.Computability.TuringMachine.Computable
/-- The initial configuration corresponding to a list in the input alphabet.  -/
Turing.initList : (tm : Turing.FinTM2) → List (tm.Γ tm.k₀) → tm.Cfg
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.Mon C), M.id.hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instDivisionRing : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → DivisionRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → DivisionRing (DirectLimit G f)
-- Lean.Elab.AutoBound
Lean.Elab.instInhabitedAutoBoundImplicitContext.default : Lean.Elab.AutoBoundImplicitContext
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.forIn'.loop.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Tactic.Linarith.Frontend
/-- Prove goals which are not linear comparisons by first calling `exfalso`.  -/
Mathlib.Tactic.Linarith.LinarithConfig.exfalso : Mathlib.Tactic.Linarith.LinarithConfig → Bool
-- Mathlib.Order.Ideal
Order.Ideal.IsMaximal.isCoatom : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  I.IsMaximal → IsCoatom I
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).inv.right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.right).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.right
        (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.eq_4 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (ca : Computation α)
  (cb : Computation β), Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRccSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Rcc.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RccSlice α β)
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The right chart for the topological space `[x, y]`, defined on `(x,y]` and sending `y` to `0` in
`EuclideanHalfSpace 1`.
 -/
IccRightChart : (x y : ℝ) → [h : Fact (x < y)] → OpenPartialHomeomorph (↑(Set.Icc x y)) (EuclideanHalfSpace 1)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation less-than relation, defined as `x <ᵥ y ↔ ¬ y ≤ᵥ x`.  -/
ValuativeRel.vlt : {R : Type u_1} → [inst : Semiring R] → [ValuativeRel R] → R → R → Prop
-- Mathlib.Order.Basic
eq_of_le_of_forall_lt_imp_le_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, a₂ ≤ a₁ → (∀ (a : α), a₂ < a → a₁ ≤ a) → a₁ = a₂
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instFaithfulForget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommMon.forget C).Faithful
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α}, m.getKeyD a fallback = (m.getKey? a).getD fallback
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ActionToRep_obj_V : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (X : Action (ModuleCat k) G),
  ↑((Rep.ActionToRep k G).obj X) = ↑X.V
-- Mathlib.Probability.Process.Stopping
MeasureTheory.memLp_stoppedValue_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Nonempty ι] {μ : MeasureTheory.Measure Ω}
  {τ : Ω → WithTop ι} {E : Type u_4} {p : ENNReal} {u : ι → Ω → E} [inst_1 : PartialOrder ι]
  {ℱ : MeasureTheory.Filtration ι m} [inst_2 : NormedAddCommGroup E],
  MeasureTheory.IsStoppingTime ℱ τ →
    (∀ (n : ι), MeasureTheory.MemLp (u n) p μ) →
      ∀ {s : Finset ι}, (∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) → MeasureTheory.MemLp (MeasureTheory.stoppedValue u τ) p μ
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.vaddConst_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (p : P₁) (v : V₁), (ContinuousAffineEquiv.vaddConst k p) v = v +ᵥ p
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] (F : CategoryTheory.Functor C D)
  [CategoryTheory.PreservesPullbacksOfInclusions F] {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f CategoryTheory.Limits.coprod.inl) F
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty, it suffices to show
that all values of `f` are at most some nonnegative number `a` to show that `⨆ i, f i ≤ a`.

See also `ciSup_le`.  -/
Real.iSup_le : ∀ {ι : Sort u_1} {f : ι → ℝ} {a : ℝ}, (∀ (i : ι), f i ≤ a) → 0 ≤ a → ⨆ i, f i ≤ a
-- Mathlib.Order.Filter.Map
Filter.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {m' : β → γ},
  Filter.map m' (Filter.map m f) = Filter.map (m' ∘ m) f
-- Lean.Elab.Tactic.ElabTerm
/-- Execute `k`, and collect new "holes" in the resulting expression.

* `parentTag` and `tagSuffix` are used to tag untagged goals with `Lean.Elab.Tactic.tagUntaggedGoals`.
* If `allowNaturalHoles` is true, then `_`'s are allowed and create new goals.
 -/
Lean.Elab.Tactic.withCollectingNewGoalsFrom : Lean.Elab.Tactic.TacticM Lean.Expr →
  Lean.Name → Lean.Name → optParam Bool false → Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.isSheaf_of_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  {P : CategoryTheory.Functor Cᵒᵖ (Type v)},
  (∀ {X : C}, ∀ S ∈ J X, CategoryTheory.Presieve.YonedaSheafCondition P S) → CategoryTheory.Presieve.IsSheaf J P