mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.FileWorker.SignatureHelp
_private.Lean.Server.FileWorker.SignatureHelp.0.Lean.Server.FileWorker.SignatureHelp.findSignatureHelp?.determineCandidateKind : Lean.FileMap →
  Option Lean.Lsp.SignatureHelpContext →
    String.Pos.Raw →
      Lean.Syntax →
        Lean.Syntax →
          Option Lean.Server.FileWorker.SignatureHelp.CandidateKind × Lean.Server.FileWorker.SignatureHelp.SearchControl
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_nonneg_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A] (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) cfcₙ_nonneg_iff._auto_1 →
    autoParam (f 0 = 0) cfcₙ_nonneg_iff._auto_3 →
      autoParam (p a) cfcₙ_nonneg_iff._auto_5 → (0 ≤ cfcₙ f a ↔ ∀ x ∈ quasispectrum R a, 0 ≤ f x)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k},
  Std.ExtDHashMap.Const.get (m.erase k) a h' = Std.ExtDHashMap.Const.get m a ⋯
-- Mathlib.Tactic.MinImports
/-- `getAllDependencies cmd id` takes a `Syntax` input `cmd` and returns the `NameSet` of all the
declaration names that are implied by
* the `SyntaxNodeKinds`,
* the attributes of `cmd` (if there are any),
* the identifiers contained in `cmd`,
* if `cmd` adds a declaration `d` to the environment, then also all the module names implied by `d`.

The argument `id` is expected to be an identifier.
It is used either for the internally generated name of a "nameless" `instance` or when parsing
an identifier representing the name of a declaration.

Note that the return value does not contain dependencies of the dependencies;
you can use `Lean.NameSet.transitivelyUsedConstants` to get those.
 -/
Mathlib.Command.MinImports.getAllDependencies : Lean.Syntax → Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.NameSet
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.instSMulCommClass : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V],
  SMulCommClass (SpecialLinearGroup R V) R V
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- When `F : C ⥤ D` is an additive functor, this is
the functor `C ⥤ HomotopyCategory D (ComplexShape.down ℕ)` which
sends `X : C` to `F` applied to a projective resolution of `X`.  -/
CategoryTheory.Functor.leftDerivedToHomotopyCategory : {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.Abelian C] →
          [CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                [F.Additive] → CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))
-- Mathlib.Topology.Inseparable
specializes_pi : ∀ {ι : Type u_5} {A : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (A i)] {f g : (i : ι) → A i},
  f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.instEssSurjSkeletonFromSkeleton : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.fromSkeleton C).EssSurj
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.adj_edge : ∀ {V : Type u_1} (s t : V) {v w : V}, (SimpleGraph.edge s t).Adj v w ↔ s(s, t) = s(v, w) ∧ v ≠ w
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The ring seminorm underlying an algebra norm.  -/
AlgebraNorm.toRingSeminorm' : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} → [inst_1 : Ring S] → [inst_2 : Algebra R S] → AlgebraNorm R S → RingSeminorm S
-- Mathlib.Algebra.Order.Monovary
antivary_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → (Antivary f g⁻¹ ↔ Monovary f g)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.IsCoreflexivePair.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B},
  (∃ s,
      CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.id A ∧
        CategoryTheory.CategoryStruct.comp g s = CategoryTheory.CategoryStruct.id A) →
    CategoryTheory.IsCoreflexivePair f g
-- Mathlib.Tactic.Core
/-- Introduce variables, using rintro patterns from a specified list.  -/
Lean.MVarId.rintroWithPats : Lean.MVarId →
  List (Lean.TSyntax `rintroPat) →
    optParam (Option ℕ) none → Lean.MetaM (List Lean.MVarId × List (Lean.TSyntax `rintroPat))
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOnNhd.eval_linearMap : ∀ {𝕜 : Type u_1} {E : Type u_2} {B : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedCommRing B] [inst_4 : NormedAlgebra 𝕜 B] {σ : Type u_5} [CompleteSpace 𝕜]
  [T2Space E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] σ → B) (p : MvPolynomial σ B),
  AnalyticOnNhd 𝕜 (fun x => (MvPolynomial.eval (f x)) p) Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pullbackConeOfRightIso f g).π.app CategoryTheory.Limits.WalkingCospan.left =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingCospan).obj
            (CategoryTheory.Limits.pullbackConeOfRightIso f g).pt).obj
        CategoryTheory.Limits.WalkingCospan.left)
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- The absolute norm of an ideal `P` above a rational prime `p` is
`|p| ^ ((span {p}).inertiaDeg' P)`.
See `absNorm_eq_pow_inertiaDeg'` for a version with `p` of type `ℕ`.  -/
Ideal.absNorm_eq_pow_inertiaDeg : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ}
  (P : Ideal R) [P.LiesOver (Ideal.span {p})], Prime p → Ideal.absNorm P = p.natAbs ^ (Ideal.span {p}).inertiaDeg' P
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited ((a : α) × β a)] {k : α}, t₁.Equiv t₂ → t₁.getEntryGE! k = t₂.getEntryGE! k
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote'_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote' ctx p = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.unop_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.HomologyData), h.unop.left = h.right.unop
-- Mathlib.FieldTheory.SeparableDegree
/-- A monic polynomial over a field `F` of exponential characteristic `q` has separable degree one
if and only if it is of the form `(X ^ (q ^ n) - C y) ^ m` for some non-zero natural number `m`,
some natural number `n`, and some element `y` of `F`.  -/
Polynomial.Monic.natSepDegree_eq_one_iff : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q],
  f.Monic → (f.natSepDegree = 1 ↔ ∃ m n y, m ≠ 0 ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.uniqueGalOne : {F : Type u_1} → [inst : Field F] → Unique (Polynomial.Gal 1)
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.ContextualizedCompletionInfo.hoverInfo : Lean.Server.Completion.ContextualizedCompletionInfo → Lean.Server.Completion.HoverInfo
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.op_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], MulOpposite.op (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constAddMonoidHom_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : AddZeroClass β] (a : β) (a_1 : α),
  (Pi.constAddMonoidHom α β) a a_1 = Function.const α a a_1
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.target_inter_preimage_symm_source_eq : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e f : Bundle.Pretrivialization F proj), f.target ∩ ↑f.symm ⁻¹' e.source = (e.baseSet ∩ f.baseSet) ×ˢ Set.univ
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inl_aut : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G) (n : N),
  SemidirectProduct.inl ((φ g) n) = SemidirectProduct.inr g * SemidirectProduct.inl n * SemidirectProduct.inr g⁻¹
-- Init.Data.String.Defs
/-- The underlying strings.  -/
String.Slice.str : String.Slice → String
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_subtype_le_map_subtype : ∀ {G : Type u_1} [inst : AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'},
  AddSubgroup.map G'.subtype H ≤ AddSubgroup.map G'.subtype K ↔ H ≤ K
-- Mathlib.Topology.Algebra.Group.Basic
/-- If `G` is an additive group with topological negation, then it is homeomorphic to
its additive units.  -/
toAddUnits_homeomorph : {G : Type w} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [ContinuousNeg G] → G ≃ₜ AddUnits G
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_neg`. -/
MonovaryOn.neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  MonovaryOn f g s → MonovaryOn (-f) (-g) s
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset : ∀ {A B : GrpCat} (f : A ⟶ B) (x : ↑B),
  ((GrpCat.SurjectiveOfEpiAuxs.h f) x)
      (GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩) =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toDiv : {G₀ : Type u_2} → [self : CommGroupWithZero G₀] → Div G₀
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_mul_cancel : ∀ {a b : ℤ}, b ∣ a → a.tdiv b * b = a
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The sequence of compact sets that form a compact exhaustion.  -/
CompactExhaustion.toFun : {X : Type u_4} → [inst : TopologicalSpace X] → CompactExhaustion X → ℕ → Set X
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- A variant of `SkewMonoidAlgebra.ofCoeff_injective` in terms of `Iff`.  -/
SkewMonoidAlgebra.ofCoeff_inj : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : G →₀ k}, { coeff := a } = { coeff := b } ↔ a = b
-- Mathlib.Data.Multiset.Fold
Multiset.fold_add : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b₁ b₂ : α) (s₁ s₂ : Multiset α),
  Multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
-- Lean.Elab.App
Lean.Elab.Term.synthesizeAppInstMVars : Array Lean.MVarId → Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.toCostructuredArrow_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (d : D) (X : (CategoryTheory.StructuredArrow d F)ᵒᵖ),
  (CategoryTheory.StructuredArrow.toCostructuredArrow F d).obj X =
    CategoryTheory.CostructuredArrow.mk (Opposite.unop X).hom.op
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- If `f` and `g` are locally Lipschitz, so is the induced map `f × g` to the product type.  -/
LocallyLipschitz.prodMk : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β},
  LocallyLipschitz f → ∀ {g : α → γ}, LocallyLipschitz g → LocallyLipschitz fun x => (f x, g x)
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- The l2-operator norm of a nonempty permutation matrix is equal to 1.
Note that this is not true for the empty case, since the empty matrix has l2-operator norm 0.
See `Matrix.permMatrix_l2_opNorm_le` for the inequality version of the empty case.
 -/
Matrix.permMatrix_l2_opNorm_eq : ∀ {n : Type u_1} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n] {𝕜 : Type u_3} [inst_2 : RCLike 𝕜]
  [Nonempty n], ‖Equiv.Perm.permMatrix 𝕜 σ‖ = 1
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_p : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ‖↑p‖ = (↑p)⁻¹
-- Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular
CategoryTheory.Functor.reflects_preregular : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.PreservesEffectiveEpis]
  [F.ReflectsEffectiveEpis] [F.EffectivelyEnough] [CategoryTheory.Preregular D] [F.Full] [F.Faithful],
  CategoryTheory.Preregular C
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_le_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g₁ g₂ : Filter β}, g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂
-- Init.Data.List.Monadic
List.filterMapM_loop_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m (Option β)}
  {l : List α} {acc : List β},
  List.filterMapM.loop f l acc = (fun x => acc.reverse ++ x) <$> List.filterMapM.loop f l []
-- Mathlib.Algebra.Ring.GeomSum
Commute.geom_sum₂_mul : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_eq_top_iff : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = ⊤ ↔ I = ⊤
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_uIoo : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.uIoo i j = Set.uIoo ↑i ↑j
-- Mathlib.Algebra.Homology.Homotopy
/-- homotopy is closed under composition (on the right)  -/
Homotopy.compRight : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D E : HomologicalComplex V c} →
            {e f : C ⟶ D} →
              Homotopy e f →
                (g : D ⟶ E) → Homotopy (CategoryTheory.CategoryStruct.comp e g) (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.set_mul_normal_comm : ∀ {G : Type u_2} [inst : Group G] (S : Set G) (N : Subgroup G) [hN : N.Normal], S * ↑N = ↑N * S
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.SplitCandidate.some.inj : ∀ {c : Lean.Meta.Grind.SplitInfo} {numCases : ℕ} {isRec tryPostpone : Bool} {c_1 : Lean.Meta.Grind.SplitInfo}
  {numCases_1 : ℕ} {isRec_1 tryPostpone_1 : Bool},
  Lean.Meta.Grind.SplitCandidate.some✝ c numCases isRec tryPostpone =
      Lean.Meta.Grind.SplitCandidate.some✝ c_1 numCases_1 isRec_1 tryPostpone_1 →
    c = c_1 ∧ numCases = numCases_1 ∧ isRec = isRec_1 ∧ tryPostpone = tryPostpone_1
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.reinsertAux.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (data : Array (Std.DHashMap.Internal.AssocList α β))
  (motive : { u // u.toNat < data.size } → Sort u_3) (i : USize) (h : i.toNat < data.size)
  (h_1 : (i : USize) → (h : i.toNat < data.size) → motive ⟨i, h⟩),
  (match ⟨i, h⟩ with
    | ⟨i, h⟩ => h_1 i h) =
    h_1 i h
-- Mathlib.Order.Lattice
inf_lt_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b < a ↔ ¬a ≤ b
-- Mathlib.Topology.MetricSpace.HausdorffAlexandroff
Real.fromBinary_continuous : Continuous Real.fromBinary
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.hcomp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H I : CategoryTheory.Functor D E} (α : F ≅ G) (β : H ≅ I), (CategoryTheory.NatIso.hcomp α β).inv = α.inv ◫ β.inv
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α]
  (discr lhs rhs : aig.Ref),
  sizeOf { discr := discr, lhs := lhs, rhs := rhs } = 1 + sizeOf discr + sizeOf lhs + sizeOf rhs
-- Mathlib.Order.RelSeries
LTSeries.nonempty_of_finiteDimensionalOrder : ∀ (α : Type u_1) [inst : Preorder α] [FiniteDimensionalOrder α], Nonempty α
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.summable_coe : ∀ {α : Type u_2} {L : SummationFilter α} {f : α → NNReal}, Summable (fun a => ↑(f a)) L ↔ Summable f L
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.map_unattach_toListRev_attachWith : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Prop} {n : Type u_1 → Type u_2} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [Monad n] {it : Std.IterM m β} {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out}
  [Std.Iterators.Finite α m] [LawfulMonad m], List.unattach <$> (it.attachWith P hP).toListRev = it.toListRev
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infiniteNeg_add_infinitePos : ∀ {x y : ℝ*}, ¬x.InfiniteNeg → y.InfinitePos → (x + y).InfinitePos
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
integral_comp_pi_polarCoord_symm : ∀ {ι : Type u_1} [inst : Fintype ι] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : (ι → ℝ × ℝ) → E),
  (∫ (p : ι → ℝ × ℝ) in Set.univ.pi fun x => polarCoord.target, (∏ i, (p i).1) • f fun i => ↑polarCoord.symm (p i)) =
    ∫ (p : ι → ℝ × ℝ), f p
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_lt_natCast' : ∀ {n : ℕ} {r : ℝ}, r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_mul_pow_le_factorial : ∀ {m n : ℕ}, m.factorial * (m + 1) ^ n ≤ (m + n).factorial
-- Mathlib.Data.List.Basic
List.IsPrefix.mem_iff_idxOf_lt_length : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁ <+: l₂ → ∀ (a : α), a ∈ l₁ ↔ List.idxOf a l₂ < l₁.length
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_univ_of_tendsto_atBot_atBot : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] [Nonempty R],
  Filter.Tendsto (↑f) Filter.atBot Filter.atBot → f.measure Set.univ = ⊤
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.div : ∀ {α : Type u_1} {M : Type u_3} [inst : DivisionMonoid M] {f g : α → M},
  Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport g → Function.HasFiniteMulSupport (f / g)
-- Mathlib.Order.Sublattice
Sublattice.subsingleton_iff : ∀ {α : Type u_2} [inst : Lattice α], Subsingleton (Sublattice α) ↔ IsEmpty α
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.ofList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {l : List (α × β)}, (Std.HashMap.Raw.ofList l).WF
-- Mathlib.Tactic.Simps.Basic
Simps.ProjectionRule.erase.inj : ∀ {a : Lean.Name} {a_1 : Lean.Syntax} {a_2 : Lean.Name} {a_3 : Lean.Syntax},
  Simps.ProjectionRule.erase a a_1 = Simps.ProjectionRule.erase a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Order.Defs.LinearOrder
le_max_left : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a ≤ max a b
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.map_mul_eq_map_mconv_map₀' : ∀ {Ω : Type u_7} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {M : Type u_10} [inst : Monoid M]
  [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] {f g : Ω → M},
  AEMeasurable f μ →
    AEMeasurable g μ →
      MeasureTheory.SigmaFinite (MeasureTheory.Measure.map f μ) →
        MeasureTheory.SigmaFinite (MeasureTheory.Measure.map g μ) →
          ProbabilityTheory.IndepFun f g μ →
            MeasureTheory.Measure.map (f * g) μ = (MeasureTheory.Measure.map f μ).mconv (MeasureTheory.Measure.map g μ)
-- Mathlib.Algebra.Group.Defs
CommSemigroup.ext_iff : ∀ {G : Type u} {x y : CommSemigroup G}, x = y ↔ Mul.mul = Mul.mul
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_mul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Mul M] (f g : α → M), ↑(f * g) = ↑f * ↑g
-- Std.Http.Data.Status
Std.Http.Status.serviceUnavailable.sizeOf_spec : sizeOf Std.Http.Status.serviceUnavailable = 1
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_natIso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (i : F ≅ F'), F.Initial ↔ F'.Initial
-- Mathlib.Order.Atoms.Finite
/-- It is important that `IsSimpleOrder` is the last type-class argument of this instance,
so that type-class inference fails quickly if it doesn't apply.

Note that as of 2025-08-13, this is false. Could someone investigate?  -/
IsSimpleOrder.instFintypeOfDecidableEq : {α : Type u_1} → [inst : LE α] → [inst_1 : BoundedOrder α] → [IsSimpleOrder α] → [DecidableEq α] → Fintype α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.insertManyIfNewUnit_list_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ : Std.TreeMap α Unit cmp} {l : List α},
  (t₁.insertManyIfNewUnit l).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) t₁ l)
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalₐ_liftAlgHom : ∀ {S : Type u_5} [inst : CommRing S] (I : Ideal S) {R : Type u_6} {A : Type u_7} [inst_1 : CommRing R]
  [inst_2 : CommRing A] [inst_3 : Algebra R A] [inst_4 : Algebra R S] (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n)
  (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m) (n : ℕ) (x : A),
  (AdicCompletion.evalₐ I n) ((AdicCompletion.liftAlgHom I f ⋯) x) = (f n) x
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.coverPreserving_overPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CoverPreserving (J.over Y) (J.over X) (CategoryTheory.Over.pullback f)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_diagonal_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] [NoZeroDivisors R] [Nontrivial R] {d : n → R},
  (Matrix.diagonal d).PosDef ↔ ∀ (i : n), 0 < d i
-- Mathlib.Order.SymmDiff
bihimp_eq_left : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a b : α}, bihimp a b = a ↔ b = ⊤
-- Mathlib.Data.Rat.Cast.Order
Rat.natCast_le_cast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ}, ↑m ≤ ↑n ↔ ↑m ≤ n
-- Mathlib.RingTheory.Extension.Basic
/-- A map between extensions induce a map between kernels.  -/
Algebra.Extension.Hom.mapKer : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            (f : P.Hom P') →
                              [alg : Algebra P.Ring P'.Ring] →
                                algebraMap P.Ring P'.Ring = f.toRingHom → ↥P.ker →ₗ[P.Ring] ↥P'.ker