mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₁ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₁ =
    (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₁
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.comp_eq_aeval : ∀ {R : Type u} [inst : CommSemiring R] {p q : Polynomial R}, p.comp q = (Polynomial.aeval q) p
-- Mathlib.Algebra.Lie.InvariantForm
LieAlgebra.InvariantForm.restrict_nondegenerate : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L]
  (Φ : LinearMap.BilinForm K L),
  Φ.Nondegenerate →
    LinearMap.BilinForm.lieInvariant L Φ →
      Φ.IsRefl →
        (∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥I) →
          ∀ (I : LieIdeal K L), IsAtom I → (Φ.restrict (LieIdeal.toLieSubalgebra K L I).toSubmodule).Nondegenerate
-- Std.Time.Date.Unit.Year
/-- Checks if the given date is valid for the specified year, month, and day.
 -/
Std.Time.Year.Offset.Valid : Std.Time.Year.Offset → Std.Time.Month.Ordinal → Std.Time.Day.Ordinal → Prop
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_natDegree_eq_zero_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → p.coeff q.natDegree = 0
-- Mathlib.Algebra.Torsor.Defs
AddTorsor.nonempty : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : AddGroup G} [self : AddTorsor G P], Nonempty P
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.functor_obj : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : ModuleCat R),
  (ModuleCat.exteriorPower.functor R n).obj M = M.exteriorPower n
-- Lean.Parser.Do
Lean.Parser.Term.doLet.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : ℕ),
  FirstOrder.Language.BoundedFormula.falsum.freeVarFinset = ∅
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- Let

`N := LocallyConstant (π C (ord I · < o)) ℤ`

`M := LocallyConstant C ℤ`

`P := LocallyConstant (C' C ho) ℤ`

`ι := GoodProducts (π C (ord I · < o))`

`ι' := GoodProducts (C' C ho')`

`v : ι → N := GoodProducts.eval (π C (ord I · < o))`

Then `SumEval C ho` is the map `u` in the diagram below. It is linearly independent if and only if
`GoodProducts.eval C` is, see `linearIndependent_iff_sum`. The top row is the exact sequence given
by `succ_exact` and `succ_mono`. The left square commutes by `GoodProducts.square_commutes`.
```
0 --→ N --→ M --→  P
      ↑     ↑      ↑
     v|    u|      |
      ι → ι ⊕ ι' ← ι'
```
 -/
Profinite.NobelingProof.GoodProducts.SumEval : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
            ↑(Profinite.NobelingProof.GoodProducts
                    (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ⊕
                ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) →
              LocallyConstant ↑C ℤ
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
_private.Mathlib.Algebra.Module.StablyFree.FreeOfInvertible.0.exteriorPower.cofactorLinear.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {n : ℕ} (bN : Module.Basis (Fin n) R N),
  exteriorPower.cofactorLinear✝ bN =
    { toFun := fun x => (bN.det.compLinearMap (LinearMap.snd R M N)).smulRight x.1, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Given `c : E →L[R] S`, `c.smulRightₗ` is the linear map from `F` to `E →L[R] F`
sending `f` to `fun e => c e • f`. See also `ContinuousLinearMap.smulRightL`.  -/
ContinuousLinearMap.smulRightₗ : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      {M : Type u_4} →
        {M₂ : Type u_5} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : Semiring T] →
                [inst_3 : Module R S] →
                  [inst_4 : AddCommMonoid M₂] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module S M₂] →
                        [IsScalarTower R S M₂] →
                          [inst_8 : TopologicalSpace S] →
                            [inst_9 : TopologicalSpace M₂] →
                              [ContinuousSMul S M₂] →
                                [inst_11 : TopologicalSpace M] →
                                  [inst_12 : AddCommMonoid M] →
                                    [inst_13 : Module R M] →
                                      [inst_14 : ContinuousAdd M₂] →
                                        [inst_15 : Module T M₂] →
                                          [inst_16 : ContinuousConstSMul T M₂] →
                                            [inst_17 : SMulCommClass R T M₂] →
                                              [SMulCommClass S T M₂] → (M →L[R] S) → M₂ →ₗ[T] M →L[R] M₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_one : ∀ {x z : ℝ}, 0 ≤ x → x < 1 → 0 < z → x ^ z < 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.corootForm_apply_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (x y : N), (P.CorootForm x) y = ∑ i, (P.root' i) x * (P.root' i) y
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_roo : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_roo._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
    List.filter (fun e => decide ((cmp e.1 lowerBound).isGT = true ∧ (cmp e.1 upperBound).isLT = true)) t.toList
-- Mathlib.Algebra.Homology.LocalCohomology
localCohomology.SelfLERadical.inhabited : {R : Type u} → [inst : CommRing R] → (J : Ideal R) → Inhabited (localCohomology.SelfLERadical J)
-- Init.Data.String.Substring
/-- Removes trailing whitespace from a substring by moving its end position to the last non-whitespace
character, or to its start position if there is no non-whitespace character.

“Whitespace” is defined as characters for which `Char.isWhitespace` returns `true`.
 -/
Substring.Raw.trimRight : Substring.Raw → Substring.Raw
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.basis_repr_apply : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] (x : QuadraticAlgebra R a b),
  ⇑((QuadraticAlgebra.basis a b).repr x) = ![x.re, x.im]
-- Mathlib.NumberTheory.Real.Irrational
Irrational.div_cases : ∀ {x y : ℝ}, Irrational (x / y) → Irrational x ∨ Irrational y
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.sign.match_1.eq_3 : ∀ (motive : ℤ → Sort u_1) (a : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n.succ)) (h_2 : Unit → motive (Int.ofNat 0))
  (h_3 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.negSucc a with
    | Int.ofNat n.succ => h_1 n
    | Int.ofNat 0 => h_2 ()
    | Int.negSucc a => h_3 a) =
    h_3 a
-- Mathlib.Algebra.Group.Action.End
/-- The additive action induced by a hom to `Additive (Function.End α)`

See note [reducible non-instances].  -/
AddAction.ofEndHom : {M : Type u_2} → {α : Type u_5} → [inst : AddMonoid M] → (M →+ Additive (Function.End α)) → AddAction M α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_neg_coe_eq_self_iff : ∀ {θ : ℝ}, |(-↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ Real.pi
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ φ_1 : CategoryTheory.Functor C D) (e_φ : φ = φ_1) (hφ : Function.Injective φ.obj)
  (S S_1 : CategoryTheory.Subgroupoid C),
  S = S_1 → CategoryTheory.Subgroupoid.map φ hφ S = CategoryTheory.Subgroupoid.map φ_1 ⋯ S_1
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
/-- The composition of `(J ⥤ C) ⥤ Karoubi (J ⥤ C)` and `Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C)`
equals the functor `(J ⥤ C) ⥤ (J ⥤ Karoubi C)` given by the composition with
`toKaroubi C : C ⥤ Karoubi C`.  -/
CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C],
  (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Functor J C)).comp
      (CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding J C) =
    (CategoryTheory.Functor.whiskeringRight J C (CategoryTheory.Idempotents.Karoubi C)).obj
      (CategoryTheory.Idempotents.toKaroubi C)
-- Mathlib.Data.Int.ModEq
Int.ModEq.instIsTrans : ∀ {n : ℤ}, IsTrans ℤ n.ModEq
-- Mathlib.Topology.UniformSpace.Defs
/-- The uniformity is a filter on α × α (inferred from an ambient uniform space
structure on α).  -/
Uniformity.term𝓤 : Lean.ParserDescr
-- Std.Http.Internal.Char
Std.Http.Internal.Char.quotedPairChar.eq_2 : Std.Http.Internal.Char.quotedPairChar ' ' = (true || Std.Http.Internal.Char.vchar ' ')
-- Init.Prelude
/-- Places an element of a type into the quotient that equates terms according to the provided relation.

Given `v : α` and relation `r : α → α → Prop`, `Quot.mk r v : Quot r` is like `v`, except all
observations of `v`'s value must respect `r`.

`Quot.mk` is a built-in primitive:
 * `Quot` is the built-in quotient type.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.sound` asserts the equality of elements related by `r`.
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`.
 -/
Quot.mk : {α : Sort u} → (r : α → α → Prop) → α → Quot r
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Puts a parametric numeric literal in `grind` normal form.

`grind` represents `BitVec` and `Fin` literals using `OfNat.ofNat` (see
`isOfNatFinBitVecLiteral`), but a term may spell one as `BitVec.ofNat` (e.g., `1#2`) or
`Fin.mk`. Ground patterns are internalized without full normalization, and a non-canonical
literal reaching the E-graph breaks the invariant that distinct interpreted nodes denote
distinct values, which `addEqStep` relies on to detect `valueInconsistency`.

**TODO**: delete this function. The normalizer should do this, instead of enumerating literal
kinds here. Waiting on the port of `Sym.dsimp` to `grind`. The same hardcoding is in
`AC.mkStruct` for identity elements, and should be deleted with it.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.canonLit : Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Tactic.OpenPrivate
/-- Elaborator for `open private`.  -/
Lean.Elab.Command.elabOpenPrivate : Lean.Elab.Command.CommandElab
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.prop : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) (t : ↑unitInterval), P (F.curry t)
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_isTopologicalBasis_isOpen_isPreconnected : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ TopologicalSpace.IsTopologicalBasis {s | IsOpen s ∧ IsPreconnected s}
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.le_iff_forall_le : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α], Order.IsSuccLimit a → (a ≤ b ↔ ∀ c < a, c ≤ b)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- We say the coproduct of the family `Xᵢ` is disjoint, if whenever we have a pullback diagram of the
form
```
Z  ⟶ X₁
↓    ↓
X₂ ⟶ ∐ X
```
`Z` is initial.
 -/
CategoryTheory.Limits.CoproductDisjoint : {C : Type u} → [CategoryTheory.Category.{v, u} C] → {ι : Type u_1} → (ι → C) → Prop
-- Init.Core
/-- `Subrelation q r` means that `q ⊆ r` or `∀ x y, q x y → r x y`.
It is the analogue of the subset relation on relations.
 -/
Subrelation : {α : Sort u} → (α → α → Prop) → (α → α → Prop) → Prop
-- Batteries.Data.ByteArray
/-- Inner loop for `mapMUnsafe`.  -/
ByteArray.mapMUnsafe.loop : {m : Type → Type u_1} → [Monad m] → (UInt8 → m UInt8) → ByteArray → USize → USize → m ByteArray
-- Mathlib.Dynamics.Newton
Polynomial.isFixedPt_newtonMap_of_aeval_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S}, (Polynomial.aeval x) P = 0 → Function.IsFixedPt P.newtonMap x
-- Init.Core
/-- Task priority.

Tasks with higher priority will always be scheduled before tasks with lower priority. Tasks with a
priority greater than `Task.Priority.max` are scheduled on dedicated threads.
 -/
Task.Priority : Type
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.mem_of_self : ∀ {α : Type u_1} {m : α}, m ∈ FreeAddMonoid.of m
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Restriction of scalars is left adjoint to coextension of scalars.  -/
ModuleCat.restrictCoextendScalarsAdj : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] → [inst_1 : Ring S] → (f : R →+* S) → ModuleCat.restrictScalars f ⊣ ModuleCat.coextendScalars f
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback : ∀ {P X Y Z : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g → ∀ (s : Set ↥X), ⇑snd '' ⇑fst ⁻¹' s = ⇑g ⁻¹' ⇑f '' s
-- Mathlib.Computability.DFA
/-- DFAs are closed under union.  -/
DFA.union : {α : Type u} → {σ1 σ2 : Type v} → DFA α σ1 → DFA α σ2 → DFA α (σ1 × σ2)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommGroupOfAddOpposite : {M : Type u_1} → [AddCommGroup Mᵃᵒᵖ] → AddCommGroup Mᵈᵃᵃ
-- Mathlib.MeasureTheory.Function.UnifTight
/-- If two functions agree a.e., then one is tight iff the other is tight.  -/
MeasureTheory.unifTight_congr_ae : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal} {g : ι → α → β},
  (∀ (n : ι), f n =ᵐ[μ] g n) → (MeasureTheory.UnifTight f p μ ↔ MeasureTheory.UnifTight g p μ)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_symm_C_C : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (x : R),
  (MvPolynomial.optionEquivLeft R S₁).symm (Polynomial.C (MvPolynomial.C x)) = MvPolynomial.C x
-- Init.System.IOError
/-- An argument to an I/O operation was invalid.

This corresponds to the POSIX errors `ELOOP`, `ENAMETOOLONG`, `EDESTADDRREQ`, `EILSEQ`, `EINVAL`, `EDOM`, `EBADF`
`ENOEXEC`, `ENOSTR`, `ENOTCONN`, and `ENOTSOCK`.
 -/
IO.Error.invalidArgument : Option String → UInt32 → String → IO.Error
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
/-- **Alias** of `MeasureTheory.Measure.absolutelyContinuous_of_le`. -/
LE.le.absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ.AbsolutelyContinuous ν
-- Init.Data.String.Lemmas.Splits
_private.Init.Data.String.Lemmas.Splits.0.String.Pos.ofEqAppend.eq_1 : ∀ {s t₁ t₂ : String} (h : s = t₁ ++ t₂), String.Pos.ofEqAppend h = ((t₁ ++ t₂).pos t₁.rawEndPos ⋯).cast ⋯
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `mkOrList [x1, x2, ...]` is defined as `x1 ∨ (x2 ∨ ...)`, or `False` if the list is empty.  -/
Mathlib.Tactic.MkIff.mkOrList : List Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.map_comp_includeLeft : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A →ₐ[S] C) (g : B →ₐ[R] D),
  (Algebra.TensorProduct.map f g).comp Algebra.TensorProduct.includeLeft = Algebra.TensorProduct.includeLeft.comp f
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientiInfEmbedding.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {ι : Type u_2} (f : ι → AddSubgroup α),
  AddSubgroup.quotientiInfEmbedding f = { toFun := fun q i => AddSubgroup.quotientMapOfLE ⋯ q, inj' := ⋯ }
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.instFunLikeSubtypeRingHomαContinuousCoe : (R S : TopCommRingCat) → FunLike { f // Continuous ⇑f } R.α S.α
-- Mathlib.Algebra.Category.Ring.Limits
/-- The forgetful functor from commutative rings to types preserves all limits.
(That is, the underlying types could have been computed instead as limits in the category of types.)
 -/
CommRingCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommRingCat)
-- Mathlib.Order.Interval.Finset.Defs
/-- A noncomputable constructor from the finiteness of all closed intervals.  -/
LocallyFiniteOrder.ofFiniteIcc : {α : Type u_1} → [inst : Preorder α] → (∀ (a b : α), (Set.Icc a b).Finite) → LocallyFiniteOrder α
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldInfo.lctx : Lean.Elab.FieldInfo → Lean.LocalContext
-- Mathlib.Tactic.Linarith.Parsing
/-- `ExprMap` is used to record atomic expressions which have been seen while processing inequality
expressions.
 -/
Mathlib.Tactic.Linarith.ExprMap : Type
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatEq.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).isUnsatEq = (k != 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d)
  (K : CategoryTheory.Limits.Multifork I),
  (I.toPiForkFunctor hc hd).obj K = CategoryTheory.Limits.Multifork.toPiFork hc hd K
-- Mathlib.SetTheory.Ordinal.Notation
ONote.sub.eq_2 : ∀ (x : ONote), (x = ONote.zero → False) → x.sub ONote.zero = x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.smul_mk : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : SMul S R] (s : S) (x y : R),
  s • { re := x, im := y } = { re := s • x, im := s • y }
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.of_subsingleton : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  s.Subsingleton → BoundedVariationOn f s
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.ofMeasurable.congr_simp : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m m_1 : (s : Set α) → MeasurableSet s → ENNReal) (e_m : m = m_1)
  (m0 : m ∅ ⋯ = 0)
  (mU :
    ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯),
  MeasureTheory.Measure.ofMeasurable m m0 mU = MeasureTheory.Measure.ofMeasurable m_1 ⋯ ⋯
-- Init.Data.Array.InsertionSort
_private.Init.Data.Array.InsertionSort.0.Array.insertionSort.swapLoop : {α : Type u_1} → (α → α → Bool) → (xs : Array α) → (j : ℕ) → j < xs.size → Array α
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right]
  (a :
    CategoryTheory.Limits.Cofork
      (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
      (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))),
  (I.multicoforkEquivSigmaCofork.inverse.obj a).pt = a.pt
-- Mathlib.Data.QPF.Univariate.Basic
/-- does `abs` preserve `supp`?  -/
QPF.SuppPreservation : {F : Type u → Type u} → [q : QPF F] → Prop
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.relIndex_span_span_nat_mul : ∀ {K : Type u_1} [inst : Field K] [NumberField K] (m : ℕ) {n : ℕ},
  n ≠ 0 →
    ∀ (a : NumberField.RingOfIntegers K),
      (Submodule.toAddSubgroup (Ideal.span {↑m})).relIndex (Submodule.toAddSubgroup (Ideal.span {↑m, a})) =
        (Submodule.toAddSubgroup (Ideal.span {↑n * ↑m})).relIndex
          (Submodule.toAddSubgroup (Ideal.span {↑(n * m), ↑n * a}))
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- Send a continuous bilinear form to an abstract bilinear form (forgetting continuity).  -/
ContinuousLinearMap.toBilinForm : {𝕜 : Type u_2} →
  {E : Type u_5} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [inst_3 : TopologicalSpace E] → (E →L[𝕜] E →L[𝕜] 𝕜) → LinearMap.BilinForm 𝕜 E
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `inv_mul_le_iff_le_mul`. -/
inv_mul_le_of_le_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a ≤ b * c → b⁻¹ * a ≤ c
-- Mathlib.NumberTheory.Padics.Complex
/-- `PadicAlgCl p` is an algebraic extension of `ℚ_[p]`.  -/
PadicAlgCl.isAlgebraic : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Algebra.IsAlgebraic ℚ_[p] (PadicAlgCl p)
-- Mathlib.RingTheory.Smooth.Quotient
KaehlerDifferential.kerToTensor.eq_1 : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B],
  KaehlerDifferential.kerToTensor R A B =
    { toFun := fun x => 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.nnnorm_holder_apply_apply_le : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q r : ENNReal} [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  (f : ↥(MeasureTheory.Lp E p μ)) (g : ↥(MeasureTheory.Lp F q μ)),
  ‖ContinuousLinearMap.holder r B f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊
-- Mathlib.Topology.Separation.Regular
NormalSpace.of_compactSpace_r1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] [R1Space X], NormalSpace X
-- Mathlib.GroupTheory.GroupAction.Pointwise
IsAddUnit.preimage_vadd_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : AddMonoid M] [inst_1 : AddAction M α]
  [inst_2 : AddAction M β] [inst_3 : FunLike F α β] [AddActionHomClass F M α β] (f : F) {c : M},
  IsAddUnit c → ∀ (t : Set β), ⇑f ⁻¹' (c +ᵥ t) = c +ᵥ ⇑f ⁻¹' t
-- Mathlib.Analysis.Normed.Group.Defs
AddGroupSeminorm.toSeminormedAddCommGroup.eq_1 : ∀ {E : Type u_5} [inst : AddCommGroup E] (f : AddGroupSeminorm E),
  f.toSeminormedAddCommGroup =
    { toNorm := f.toSeminormedAddGroup.toNorm, toAddGroup := f.toSeminormedAddGroup.toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := f.toSeminormedAddGroup.toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Data.Rat.Sqrt
/-- Square root function on rational numbers, defined by taking the (integer) square root of the
numerator and the square root (on natural numbers) of the denominator.  -/
Rat.sqrt : ℚ → ℚ
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.support_mul : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] [inst_1 : DecidableEq α] {g₁ g₂ : α →₀ β},
  (g₁ * g₂).support ⊆ g₁.support ∩ g₂.support