mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.Data.ForwardRuleMatches
_private.Aesop.Tree.Data.ForwardRuleMatches.0.Aesop.ForwardRuleMatches.eraseHyps.go : Std.HashSet Lean.FVarId → Lean.PHashSet Aesop.ForwardRuleMatch → Lean.PHashSet Aesop.ForwardRuleMatch
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between any initial object and the zero object.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → {X : C} → CategoryTheory.Limits.IsInitial X → (0 ≅ X)
-- Mathlib.Analysis.Normed.Group.Hom
/-- A Lipschitz continuous additive homomorphism is a normed additive group homomorphism.  -/
NormedAddGroupHom.ofLipschitz : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    [inst : SeminormedAddCommGroup V₁] →
      [inst_1 : SeminormedAddCommGroup V₂] →
        (f : V₁ →+ V₂) → {K : NNReal} → LipschitzWith K ⇑f → NormedAddGroupHom V₁ V₂
-- Init.Data.UInt.Lemmas
UInt16.toFin_div : ∀ (a b : UInt16), (a / b).toFin = a.toFin / b.toFin
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the values of a hash map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.valuesIter : {α β : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → (Std.DHashMap α fun x => β) → Std.Iter β
-- Mathlib.Algebra.Order.Sub.Basic
tsub_le_tsub_iff_left : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α} [AddLeftReflectLE α], c ≤ a → (a - b ≤ a - c ↔ c ≤ b)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_δ_of_mono : ∀ {n : ℕ} (θ : { len := n } ⟶ { len := n + 1 }) [CategoryTheory.Mono θ], ∃ i, θ = SimplexCategory.δ i
-- Mathlib.Order.Filter.Pointwise
Filter.sub_le_sub_left : ∀ {α : Type u_2} [inst : Sub α] {f g₁ g₂ : Filter α}, g₁ ≤ g₂ → f - g₁ ≤ f - g₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁_trans : ∀ {q q' : Turing.PartrecToTM2.Λ'},
  q' ∈ Turing.PartrecToTM2.trStmts₁ q → Turing.PartrecToTM2.trStmts₁ q' ⊆ Turing.PartrecToTM2.trStmts₁ q
-- Init.GrindInstances.ToInt
Lean.Grind.instDivUInt8UintOfNatNat : Lean.Grind.ToInt.Div UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.CategoryTheory.Category.ULift
/-- A type-level equivalence `(C ⥤ D) ≃ (C ⥤ (ULiftHom.{v'} (ULift.{u'} D)))`. Note that this is
not ensured by a categorical equivalence, and so needs special treatment.  -/
CategoryTheory.ULiftHomULiftCategory.equivCongrLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D ≃ CategoryTheory.Functor C (CategoryTheory.ULiftHom (ULift.{u', u₂} D))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).getKey? a =
        if compare k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- The one-point extension of an arbitrary topological space `X`  -/
OnePoint : Type u_3 → Type u_3
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, p ≠ 0 → ↑p.roots.card ≤ p.degree
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- In a semisimple Lie algebra, the atoms are independent.  -/
LieAlgebra.IsSemisimple.sSupIndep_isAtom : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsSemisimple R L], sSupIndep {I | IsAtom I}
-- Init.Data.Nat.Basic
/-- Alias for `Nat.le_total`.  -/
Nat.le_or_ge : ∀ (m n : ℕ), m ≤ n ∨ n ≤ m
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.sheafifyCocone_ι_app_val_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [inst_3 : CategoryTheory.HasWeakSheafify J D] {F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)}
  (E : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf J D))) (k : K)
  {Z : CategoryTheory.Functor Cᵒᵖ D}
  (h : (((CategoryTheory.Functor.const K).obj (CategoryTheory.Sheaf.sheafifyCocone E).pt).obj k).obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sheaf.sheafifyCocone E).ι.app k).hom h =
    CategoryTheory.CategoryStruct.comp (E.ι.app k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J E.pt) h)
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.div_mul_cancel_left : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a : α}, IsUnit a → ∀ (b : α), a / (a * b) = b⁻¹
-- Lean.Elab.Tactic.ElabTerm
_private.Lean.Elab.Tactic.ElabTerm.0.Lean.Elab.Tactic.withCollectingNewGoalsFrom.go : Lean.Elab.Tactic.TacticM Lean.Expr →
  Lean.Name → Lean.Name → Bool → Lean.Elab.Tactic.TacticM (Lean.Expr × List Lean.MVarId)
-- Init.System.ST
/-- Runs an `EST` computation, in which mutable state and exceptions are the only side effects.
 -/
runEST : {ε α : Type} → ((σ : Type) → EST ε σ α) → Except ε α
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabInferInstanceAs : Lean.Elab.Term.TermElab
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- Hausdorff dimension of a set in an (e)metric space.  -/
dimH : {X : Type u_2} → [EMetricSpace X] → Set X → ENNReal
-- Mathlib.CategoryTheory.IsConnected
/-- The setoid given by the equivalence relation `Zigzag`. A quotient for this
setoid is a connected component of the category.
 -/
CategoryTheory.Zigzag.setoid : (J : Type u₂) → [CategoryTheory.Category.{v₁, u₂} J] → Setoid J
-- Mathlib.LinearAlgebra.Projection
Submodule.quotientEquivOfIsCompl_apply_mk : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : E), (p.quotientEquivOfIsCompl q h) (Submodule.Quotient.mk x) = (q.projectionOnto p ⋯) x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts of shape `J` if it preserves biproducts of `f` for every
`f : J → C`.  -/
CategoryTheory.Limits.PreservesBiproductsOfShape.preserves : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {J : Type w₁}
  {F : CategoryTheory.Functor C D} {inst_4 : F.PreservesZeroMorphisms}
  [self : CategoryTheory.Limits.PreservesBiproductsOfShape J F] {f : J → C},
  CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.Data.Sum.Order
Sum.instIsWellOrderLex : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsWellOrder α r] [IsWellOrder β s],
  IsWellOrder (α ⊕ β) (Sum.Lex r s)
-- Mathlib.Analysis.Analytic.Constructions
/-- Finite products of analytic functions are analytic  -/
Finset.analyticWithinAt_fun_prod : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_9} [inst_3 : NormedCommRing A] [inst_4 : NormedAlgebra 𝕜 A] {f : α → E → A}
  {c : E} {s : Set E} (N : Finset α),
  (∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z => ∏ n ∈ N, f n z) s c
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_divRight : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul G] (g : G),
  MeasurableEmbedding fun x => x / g
-- Mathlib.LinearAlgebra.FreeProduct.Basic
_private.Mathlib.LinearAlgebra.FreeProduct.Basic.0.LinearAlgebra.FreeProduct.rel.match_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α] (s : Finset α) (a : α),
  s.truncatedInf a = if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.get!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} [inst_1 : Inhabited (β k)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.get! k = t₂.get! k
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.natFloor_logb_natCast : ∀ (b n : ℕ), ⌊Real.logb ↑b ↑n⌋₊ = Nat.log b n
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Unweighted mean inequality, version for two elements of `ℝ≥0` and real exponents.  -/
NNReal.rpow_add_le_mul_rpow_add_rpow : ∀ (z₁ z₂ : NNReal) {p : ℝ}, 1 ≤ p → (z₁ + z₂) ^ p ≤ 2 ^ (p - 1) * (z₁ ^ p + z₂ ^ p)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- A (local) presentation of a sheaf of module `M` is a finite presentation
if each given presentation of `M.over (X i)` is a finite presentation.  -/
SheafOfModules.QuasicoherentData.IsFinitePresentation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.QuasicoherentData → Prop
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleRange_of_le : ∀ {n : ℕ} {i j : Fin n} [inst : NeZero n], i ≤ j → j.cycleRange i = if i = j then 0 else i + 1
-- Init.SimpLemmas
Bool.not_false : (!false) = true
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_sq : Real.goldenRatio ^ 2 = Real.goldenRatio + 1
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.leftInverse_of_rightInverse : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N}
  {g : N →ₗ[R] M}, Function.RightInverse ⇑f ⇑g → Function.LeftInverse ⇑f ⇑g
-- Lean.Parser.Syntax
Lean.Parser.optPrecedence.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.RootsOfUnity.Basic
Units.val_set_image_rootsOfUnity_one : ∀ {R : Type u_4} [inst : CommMonoid R], Units.val '' ↑(rootsOfUnity 1 R) = {1}
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {Z : CategoryTheory.Functor (CategoryTheory.ShortComplex C) C} (h : CategoryTheory.ShortComplex.π₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₁Toπ₂
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.π₂Toπ₃ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_list_prod : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R ≃+* S) (l : List R),
  f l.prod = (List.map (⇑f) l).prod
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- A semigroup with a partial order and satisfying `LeftCancelSemigroup`
(i.e. `a * c < b * c → a < b`) is a `LeftCancelSemigroup`.  -/
Contravariant.toLeftCancelSemigroup : {α : Type u_1} → [inst : Semigroup α] → [inst_1 : PartialOrder α] → [MulLeftReflectLE α] → LeftCancelSemigroup α
-- Mathlib.Analysis.Complex.RealDeriv
DifferentiableAt.real_of_complex : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {z : ℂ},
  DifferentiableAt ℂ f z → DifferentiableAt ℝ f z
-- Init.Data.UInt.Bitwise
UInt64.toUSize_or : ∀ (a b : UInt64), (a ||| b).toUSize = a.toUSize ||| b.toUSize
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.card_le_card_of_forall_subsingleton' : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {s : Finset α} {t : Finset β},
  (∀ b ∈ t, ∃ a ∈ s, r a b) → (∀ a ∈ s, {b | b ∈ t ∧ r a b}.Subsingleton) → t.card ≤ s.card
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equivalence `WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ` sending left to left and right to
right.
 -/
CategoryTheory.Limits.walkingParallelPairOpEquiv : CategoryTheory.Limits.WalkingParallelPair ≌ CategoryTheory.Limits.WalkingParallelPairᵒᵖ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.semilatticeSup.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Etale.Kaehler
KaehlerDifferential.isLocalizedModule_map : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [IsLocalization M T], IsLocalizedModule M (KaehlerDifferential.map R R S T)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ : ∀ {x y : SimplexCategoryGenRel} {e : x ⟶ y},
  SimplexCategoryGenRel.P_σ e → CategoryTheory.IsSplitEpi (SimplexCategoryGenRel.toSimplexCategory.map e)
-- Batteries.Data.Float.Basic
/-- Returns `v, exp` integers such that `f = v * 2^exp`.
(`e` is not minimal, but `v.abs` will be at most `2^24 - 1`.)
Returns `none` when `f` is not finite (i.e. `inf`, `-inf` or a `nan`).  -/
Float32.toRatParts : Float32 → Option (ℤ × ℤ)
-- Mathlib.Order.Category.Semilat
SemilatSupCat.of.inj : ∀ {X : Type u} {isSemilatticeSup : SemilatticeSup X} {isOrderBot : OrderBot X} {X_1 : Type u}
  {isSemilatticeSup_1 : SemilatticeSup X_1} {isOrderBot_1 : OrderBot X_1},
  { X := X, isSemilatticeSup := isSemilatticeSup, isOrderBot := isOrderBot } =
      { X := X_1, isSemilatticeSup := isSemilatticeSup_1, isOrderBot := isOrderBot_1 } →
    X = X_1 ∧ isSemilatticeSup ≍ isSemilatticeSup_1 ∧ isOrderBot ≍ isOrderBot_1
-- Init.Data.Vector.Attach
Vector.toArray_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ a ∈ xs, P a},
  (Vector.pmap f xs H).toArray = Array.pmap f xs.toArray ⋯
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The explicit finite coproduct cocone is a colimit cocone.  -/
CompHausLike.finiteCoproduct.isColimit : {P : TopCat → Prop} →
  {α : Type w} →
    [inst : Finite α] →
      (X : α → CompHausLike P) →
        [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] →
          CategoryTheory.Limits.IsColimit (CompHausLike.finiteCoproduct.cofan X)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_one : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β], ⇑1 = 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.isCompl_corootSpan_ker_corootForm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], IsCompl (P.corootSpan R) (LinearMap.ker P.CorootForm)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.braiding_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.SymmetricCategory C] (M N : CategoryTheory.Mon C), (β_ M N).inv.hom = (β_ M.X N.X).inv
-- Mathlib.Control.Random
/-- Execute `RandT m α` using the global `stdGenRef` as RNG and the given `seed`.  -/
IO.runRandWith : {m : Type u_1 → Type u_2} → [Monad m] → {α : Type u_1} → ℕ → RandT m α → m α
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β), (↑f.toMonoidHom).toFun = ⇑f
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The algebra isomorphism between multivariable polynomials in variables `S₁` of multivariable
polynomials in variables `S₂` and multivariable polynomials in variables `S₂` of multivariable
polynomials in variables `S₁`.  -/
MvPolynomial.commAlgEquiv : (R : Type u_2) →
  (S₁ : Type u_3) →
    (S₂ : Type u_4) →
      [inst : CommSemiring R] → MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R)
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instMonad : Monad WithOne
-- Mathlib.Order.Atoms
OrderDual.instIsCoatomistic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [h : IsAtomistic α], IsCoatomistic αᵒᵈ
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix_eq_fix : ∀ {α : Sort u_2} {C : α → Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] {R : α → α → Prop}
  {F : (a : α) → ((a' : α) → R a' a → C a') → C a} (wf : WellFounded R) {a : α},
  WellFounded.partialExtrinsicFix R F a = wf.fix F a
-- Mathlib.Data.Fintype.EquivFin
/-- This instance also provides `[Finite s]` for `s : Set α`.  -/
Subtype.finite : ∀ {α : Sort u_4} [Finite α] {p : α → Prop}, Finite { x // p x }
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_ne_top : ∀ {r : NNReal}, ↑r ≠ ⊤
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).natTrailingDegree = n
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.ext_fun : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β},
  (∀ (a : α) (f : β → ENNReal), Measurable f → ∫⁻ (b : β), f b ∂κ a = ∫⁻ (b : β), f b ∂η a) → κ = η
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.iteratedDeriv_charFun : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {n : ℕ} {t : ℝ},
  MeasureTheory.MemLp id (↑n) μ →
    iteratedDeriv n (MeasureTheory.charFun μ) t =
      Complex.I ^ n * ∫ (x : ℝ), ↑x ^ n * Complex.exp (↑t * ↑x * Complex.I) ∂μ
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.comp_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Zero β] (g : C(β, γ)), g.comp 0 = ContinuousMap.const α (g 0)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- Turn a measure into the corresponding element of the space of measures equipped with the
Lévy-Prokhorov metric.  -/
MeasureTheory.LevyProkhorov.ofMeasure : {α : Type u_2} → α → MeasureTheory.LevyProkhorov α
-- Mathlib.RingTheory.PowerSeries.Ideal
/-- A prime ideal `P` of `R⟦X⟧` is finitely generated if and only if `P.map constantCoeff` is
finitely generated.  -/
PowerSeries.fg_iff_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {P : Ideal (PowerSeries R)} [P.IsPrime],
  P.FG ↔ (Ideal.map PowerSeries.constantCoeff P).FG
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `G : C → D` is a faithful functor which sends t to a colimit cocone,
then it suffices to check that the induced maps for the image of t
can be lifted to maps of `C`.  -/
CategoryTheory.Limits.IsColimit.ofFaithful : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            {D : Type u₄} →
              [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
                (G : CategoryTheory.Functor C D) →
                  [G.Faithful] →
                    (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) →
                      (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) →
                        (∀ (s : CategoryTheory.Limits.Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)) →
                          CategoryTheory.Limits.IsColimit t
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.instSFiniteHSMulMeasure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {R : Type u_2}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R), MeasureTheory.SFinite (c • μ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : β k → β k},
  (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Given three points on a circle, twice the radius of that circle may be expressed explicitly as
the distance between two of those points divided by the absolute value of the sine of the angle
at the third point (a version of the law of sines or sine rule).  -/
EuclideanGeometry.Sphere.dist_div_sin_oangle_eq_two_mul_radius : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s → p₁ ≠ p₂ → p₁ ≠ p₃ → p₂ ≠ p₃ → dist p₁ p₃ / |(EuclideanGeometry.oangle p₁ p₂ p₃).sin| = 2 * s.radius
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.continuousSMul : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [RingHomSurjective σ] [RingHomIsometric σ] [inst_9 : TopologicalSpace F]
  [inst_10 : IsTopologicalAddGroup F] [inst_11 : ContinuousSMul 𝕜₂ F], ContinuousSMul 𝕜₂ (E →SL[σ] F)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_le_prod_map : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [MulLeftMono α] (f : α → α),
  (∀ x ∈ s, x ≤ f x) → s.prod ≤ (Multiset.map f s).prod
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- **Ptolemy's inequality**: in a quadrangle `ABCD`, `|AC| * |BD| ≤ |AB| * |CD| + |BC| * |AD|`. If
`ABCD` is a convex cyclic polygon, then this inequality becomes an equality, see
`EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical`.  -/
EuclideanGeometry.mul_dist_le_mul_dist_add_mul_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [NormedAddTorsor V P] (a b c d : P), dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.support_subset : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  Function.support ⇑f ⊆ ↑K
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.oreEqv.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type u_2)
  [inst_2 : MulAction R X],
  OreLocalization.oreEqv S X = { r := fun rs rs' => ∃ u v, u • rs'.1 = v • rs.1 ∧ ↑u * ↑rs'.2 = v * ↑rs.2, iseqv := ⋯ }
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.mk : (toBddDistLat : BddDistLat) → [isFintype : Fintype ↑toBddDistLat.toDistLat] → FinBddDistLat
-- Mathlib.Topology.SeparatedMap
T2Space.isSeparatedMap : ∀ {X : Type u_1} {Y : Sort u_2} [inst : TopologicalSpace X] [T2Space X] (f : X → Y), IsSeparatedMap f
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.prod_finset_product' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) → ∀ {f : γ → α → β}, ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a
-- Batteries.Data.String.Legacy
String.Pos.Raw.next.eq_1 : ∀ (s : String) (p : String.Pos.Raw), String.Pos.Raw.next s p = p + String.Pos.Raw.get s p