mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_div : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x y : WithVal v), (x / y).ofVal = x.ofVal / y.ofVal
-- Mathlib.Algebra.Category.Grp.Ulift
CommGrpCat.uliftFunctorFullyFaithful.eq_1 : CommGrpCat.uliftFunctorFullyFaithful =
  {
    preimage := fun {X Y} f =>
      CommGrpCat.ofHom (MulEquiv.ulift.toMonoidHom.comp ((CommGrpCat.Hom.hom f).comp MulEquiv.ulift.symm.toMonoidHom)),
    map_preimage := @CommGrpCat.uliftFunctorFullyFaithful._proof_1,
    preimage_map := @CommGrpCat.uliftFunctorFullyFaithful._proof_2 }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.pullbackRestrictIsoRestrict_hom_ι : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict f U).hom
      ((TopologicalSpace.Opens.map f.base).obj U).ι =
    CategoryTheory.Limits.pullback.fst f U.ι
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.rightHomologyIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp S₁.rightHomologyIso.inv (CategoryTheory.ShortComplex.rightHomologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) S₂.rightHomologyIso.inv
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.integral_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure], 0 < ∫ (x : E), ↑f x ∂μ
-- Mathlib.Algebra.FreeMonoid.Basic
/-- An induction principle for free monoids which mirrors
induction on lists, with cases analogous to the empty list and cons  -/
FreeAddMonoid.inductionOn' : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Prop} (a : FreeAddMonoid α),
  motive 0 → (∀ (b : α) (a : FreeAddMonoid α), motive a → motive (FreeAddMonoid.of b + a)) → motive a
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerEquiv_apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [inst_3 : IsUltrametricDist E] [inst_4 : CompleteSpace E] (f : C(ℤ_[p], E)),
  ⇑((PadicInt.mahlerEquiv E) f) = fun n => (fwdDiff 1)^[n] (⇑f) 0
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_re : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.re ((starRingEnd K) z) = RCLike.re z
-- Mathlib.Order.RelIso.Basic
RelIso.relIsoCongr_symm_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ ≃r s₂) (a : α₁),
  ((e₁.relIsoCongr e₂).symm f₂) a = e₂.symm (f₂ (e₁ a))
-- Init.Data.List.Monadic
List.foldlM_filter : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {p : α → Bool}
  {g : β → α → m β} {l : List α} {init : β},
  List.foldlM g init (List.filter p l) = List.foldlM (fun x y => if p y = true then g x y else pure x) init l
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.Context.mk.sizeOf_spec : ∀ (userName : Lean.Name) (explicitPatternVars : Array Lean.FVarId),
  sizeOf { userName := userName, explicitPatternVars := explicitPatternVars } =
    1 + sizeOf userName + sizeOf explicitPatternVars
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.sub_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  (s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)) (x : ↥(Opposite.unop V)),
  ↑(s - t) x = ↑s x - ↑t x
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly₂.poly : ∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R}
  [self : WittVector.IsPoly₂ p f],
  ∃ φ,
    ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : WittVector p R),
      (f x y).coeff = fun n => WittVector.peval (φ n) ![x.coeff, y.coeff]
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_sub`. -/
ContinuousLinearMap.coe_sub : ∀ {R : Type u_1} [inst : Ring R] {R₂ : Type u_2} [inst_1 : Ring R₂] {M : Type u_4} [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] {M₂ : Type u_5} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂]
  [inst_6 : Module R M] [inst_7 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_8 : IsTopologicalAddGroup M₂]
  (f g : M →SL[σ₁₂] M₂), ↑(f - g) = ↑f - ↑g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → t.isEmpty = false
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.pair_sdiff_right`. -/
Set.pair_diff_right : ∀ {α : Type u_1} {a b : α}, a ≠ b → {a, b} \ {b} = {a}
-- Aesop.Tree.TreeM
Aesop.getAndIncrementNextGoalId : Aesop.TreeM Aesop.GoalId
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instFunLike : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (φ : M →* N) →
          (A : Type u_4) →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                (B : Type u_5) → [inst_4 : Monoid B] → [inst_5 : MulDistribMulAction N B] → FunLike (A →ₑ*[φ] B) A B
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Auxiliary definition for `inclusion`.  -/
CategoryTheory.FreeBicategory.inclusionMapCompAux : {B : Type u} →
  [inst : Quiver B] →
    {a b c : B} →
      (f : Quiver.Path a b) →
        (g : Quiver.Path b c) →
          (CategoryTheory.FreeBicategory.preinclusion B).map
              (CategoryTheory.CategoryStruct.comp { as := f } { as := g }) ≅
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := f })
              ((CategoryTheory.FreeBicategory.preinclusion B).map { as := g })
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_zero_pos : ∀ (x : ℝ), 0 < x ^ 0
-- Lean.Parser.Term
Lean.Parser.Term.fromTerm.formatter : Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go : (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
  Std.Tactic.BVDecide.BVLogicalExpr → Std.Tactic.BVDecide.BVExpr.Cache aig → Std.Tactic.BVDecide.Return aig
-- Mathlib.RingTheory.LocalProperties.ProjectiveDimension
ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R)
  [Module.Finite R ↑M],
  CategoryTheory.projectiveDimension M =
    ⨆ p, CategoryTheory.projectiveDimension (M.localizedModule p.asIdeal.primeCompl)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.exists_of_mem_join : ∀ {α : Type u} {a : α} {S : Stream'.WSeq (Stream'.WSeq α)}, a ∈ S.join → ∃ s ∈ S, a ∈ s
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `f` is continuous on the circle `|z - c| = R`, `R > 0`, the `‖f z‖` is less than or equal to
`C : ℝ` on this circle, and this norm is strictly less than `C` at some point `z` of the circle,
then `‖∮ z in C(c, R), f z‖ < 2 * π * R * C`.  -/
circleIntegral.norm_integral_lt_of_norm_le_const_of_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R C : ℝ},
  0 < R →
    ContinuousOn f (Metric.sphere c R) →
      (∀ z ∈ Metric.sphere c R, ‖f z‖ ≤ C) →
        (∃ z ∈ Metric.sphere c R, ‖f z‖ < C) → ‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * Real.pi * R * C
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_C : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R),
  (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r) = f r
-- Lean.Elab.App
/-- Returns a named argument that depends on the next argument, otherwise `none`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.findNamedArgDependsOn? : Lean.Expr → List Lean.Elab.Term.NamedArg → Lean.MetaM (Option Lean.Elab.Term.NamedArg)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).left =
    CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm
-- Mathlib.Order.Filter.Extr
IsExtrFilter.comp_tendsto : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {l : Filter α} {g : δ → α} {l' : Filter δ}
  {b : δ}, IsExtrFilter f l (g b) → Filter.Tendsto g l' l → IsExtrFilter (f ∘ g) l' b
-- Lean.Server.GoTo
Lean.Server.GoToM.run : {α : Type} → Lean.Server.GoToContext → Lean.Elab.ContextInfo → Lean.LocalContext → Lean.Server.GoToM α → IO α
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.dValue.eq_1 : ∀ (N : ℕ), Behrend.dValue N = ⌊↑N ^ (↑(Behrend.nValue N))⁻¹ / 2⌋₊
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_empty`. -/
Set.diff_empty : ∀ {α : Type u_1} {s : Set α}, s \ ∅ = s
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.noChange.sizeOf_spec : sizeOf Lean.Meta.TacticResultCNM.noChange = 1
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology : ∀ (S : LightProfinite), Countable (TopologicalSpace.Clopens ↑S.toTop)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter'.spec' : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g : L ≃+* L) {t : Lˣ},
  t ∈ rootsOfUnity n L → g ↑t = ↑t ^ (↑((modularCyclotomicCharacter' L n) g)).val
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The product of two arithmetic functions defines the same function as the Dirichlet convolution
of the functions defined by them.  -/
ArithmeticFunction.coe_mul : ∀ {R : Type u_1} [inst : Semiring R] (f g : ArithmeticFunction R), LSeries.convolution ⇑f ⇑g = ⇑(f * g)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (val_1 : ℤ) (x_1 n_1 : Lean.Grind.Linarith.Var),
  (Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen c_1 val_1 x_1 n_1) =
    (c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1)
-- Mathlib.Control.ULiftable
instULiftableReaderTULift : {s : Type u₀} →
  {m : Type u₀ → Type u_5} →
    {m' : Type (max u₀ u_6) → Type u_7} → [ULiftable m m'] → ULiftable (ReaderT s m) (ReaderT (ULift.{u_6, u₀} s) m')
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.imageStrongEpiMonoFactorisation f).m = CategoryTheory.Abelian.image.ι f
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.indepSet_of_mem : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s t : Set Ω} (S T : Set (Set Ω)) {_m0 : MeasurableSpace Ω},
  s ∈ S →
    t ∈ T →
      MeasurableSet s →
        MeasurableSet t →
          ∀ (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α) [ProbabilityTheory.IsZeroOrMarkovKernel κ],
            ProbabilityTheory.Kernel.IndepSets S T κ μ → ProbabilityTheory.Kernel.IndepSet s t κ μ
-- Mathlib.Order.Filter.AtTopBot.Finset
Filter.atTop_finset_eq_iInf : ∀ {α : Type u_3}, Filter.atTop = ⨅ x, Filter.principal (Set.Ici {x})
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis.eRk_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.eRk X = I.encard
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {Kg : NNReal} {g : β → γ},
  AntilipschitzWith Kg g → ∀ {Kf : NNReal} {f : α → β}, AntilipschitzWith Kf f → AntilipschitzWith (Kf * Kg) (g ∘ f)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid_apply_coe : ∀ {M : Type u_4} [inst : AddMonoid M] (x : AddUnits M), ↑(AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid x) = ↑x
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- Indexed version of `exists_lt_of_lt_csSup`.
When `b < iSup f`, there is an element `i` such that `b < f i`.
 -/
exists_lt_of_lt_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {b : α} [Nonempty ι] {f : ι → α},
  b < iSup f → ∃ i, b < f i
-- Init.Data.AC
Lean.Data.AC.List.two_step_induction : {motive : List ℕ → Sort u} →
  (l : List ℕ) →
    motive [] → ((a : ℕ) → motive [a]) → ((a b : ℕ) → (l : List ℕ) → motive (b :: l) → motive (a :: b :: l)) → motive l
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.UnifEigenvalues.instCoeOut : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {f : Module.End R M} → (k : ℕ∞) → CoeOut (f.UnifEigenvalues k) R
-- Mathlib.Data.Nat.Pairing
Nat.add_le_pair : ∀ (m n : ℕ), m + n ≤ Nat.pair m n
-- Std.Async.Basic
/-- Runs all computations in an `Array` concurrently and returns all results as an array.
 -/
Std.Async.Async.concurrentlyAll : {α : Type} → Array (Std.Async.Async α) → optParam Task.Priority Task.Priority.default → Std.Async.Async (Array α)
-- Mathlib.Algebra.Group.Shrink
Shrink.instZero.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Zero α], Shrink.instZero = (equivShrink α).symm.zero
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.summable_of_eq_zero_or_self : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f g : β → α}
  [CompleteSpace α], Summable f → (∀ (b : β), g b = 0 ∨ g b = f b) → Summable g
-- Mathlib.Probability.Process.Adapted
MeasureTheory.StronglyAdapted.smul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [inst_2 : (i : ι) → SMul ℝ (β i)] [∀ (i : ι), ContinuousConstSMul ℝ (β i)] (c : ℝ),
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f (c • u)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.from_single_hom_ext_iff : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (HomologicalComplex.single V c j).obj A ⟶ K},
  f = g ↔ f.f j = g.f j
-- Mathlib.Order.RelClasses
instIsStrictOrderLt : ∀ {α : Type u} [inst : Preorder α], IsStrictOrder α fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_sub_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] {s t : Finset α} {f : α → β} {a : β}, (s - t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x - y) ≤ a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β},
  (Std.DTreeMap.Const.modify t k f).minKey? = Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.comul_eq_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.ComonObj A],
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
      (CategoryTheory.CategoryStruct.id A)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X) = 1 + sizeOf X
-- Mathlib.RingTheory.Algebraic.Integral
/-- [Stacks Tag 0G1M](https://stacks.math.columbia.edu/tag/0G1M) -/
Algebra.IsAlgebraic.rank_fractionRing_polynomial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S],
  Module.rank (FractionRing (Polynomial R)) (FractionRing (Polynomial S)) = Module.rank R S
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNegZeroClass : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [NegZeroClass G] → NegZeroClass (l.Germ G)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
val_inv_cfcUnits : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p]
  [inst_10 : ContinuousInv₀ R] (f : R → R) (a : A) (hf' : ∀ x ∈ spectrum R a, f x ≠ 0)
  (hf : autoParam (ContinuousOn f (spectrum R a)) cfcUnits._auto_1) (ha : autoParam (p a) cfcUnits._auto_3),
  ↑(cfcUnits f a hf' hf ha)⁻¹ = cfc (fun x => (f x)⁻¹) a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) h)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.homologyMap_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology],
  CategoryTheory.ShortComplex.homologyMap φ₁ = CategoryTheory.ShortComplex.homologyMap φ₂
-- Init.Data.Array.Lemmas
Array.flatten.eq_1 : ∀ {α : Type u} (xss : Array (Array α)), xss.flatten = Array.foldl (fun acc xs => acc ++ xs) #[] xss
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  (h' : a ∈ t), t.getKey? a = some (t.getKey a h')
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_X_sub_C_pow_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (r : R) (m n : ℕ),
  f.natDegree ≤ m → f.resultant ((Polynomial.X - Polynomial.C r) ^ n) m n = (-1) ^ (m * n) * Polynomial.eval r f ^ n
-- Init.Data.Float.Model.Format.Basic
/-- The smallest exponent possible for a number using the given specification,
including subnormals.
 -/
Float.Model.Format.minExponent : Float.Model.Format → ℤ
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.card_bot : ∀ {M : Type u_1} [inst : AddMonoid M] {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.mulRight.eq_1 : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : SeparatelyContinuousMul G] (a : G),
  Homeomorph.mulRight a = { toEquiv := Equiv.mulRight a, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Lean.Widget.TaggedText
Lean.Widget.instInhabitedTaggedText.default : {α : Type u} → Lean.Widget.TaggedText α
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic'_symm_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)) (x : EuclideanSpace ℝ (Fin n)),
  ↑(↑(stereographic' n v).symm x) =
    have U := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr;
    (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • 4 • ↑(U.symm x) + (‖↑(U.symm x)‖ ^ 2 + 4)⁻¹ • (‖↑(U.symm x)‖ ^ 2 - 4) • ↑v
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.siftedSum_eq_sum_support_mul_ite : ∀ {s : BoundingSieve}, BoundingSieve.siftedSum = ∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.not_continuousAt_deriv_qaryEntropy_zero : ∀ {q : ℕ}, ¬ContinuousAt (deriv (Real.qaryEntropy q)) 0
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_insert_of_notMem' : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (f : α → β)
  (comm : (↑(insert a s)).Pairwise (Function.onFun Commute f)),
  a ∉ s → (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.erased : Lean.Meta.SimpTheorems → Lean.PHashSet Lean.Meta.Origin
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration.method : Lean.Lsp.Registration → String
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInrCompInverseAssociator_inv_app_down : ∀ (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] (X : E),
  ((CategoryTheory.sum.inrCompInrCompInverseAssociator C D E).inv.app X).down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inr X)).down
      (CategoryTheory.CategoryStruct.id (Sum.inr X)).down
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddMonoidOfContinuousAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β],
  ContinuousMap.instAddMonoidOfContinuousAdd =
    { toAddSemigroup := ContinuousMap.instAddSemigroupOfContinuousAdd, toZero := ContinuousMap.instZero, zero_add := ⋯,
      add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.LinearAlgebra.Span.Basic
/-- See `Submodule.span_smul_eq` (in `RingTheory.Ideal.Operations`) for
`span R (r • s) = r • span R s` that holds for arbitrary `r` in a `CommSemiring`.  -/
Submodule.span_smul_eq_of_isUnit : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M)
  (r : R), IsUnit r → Submodule.span R (r • s) = Submodule.span R s
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.remainingToString : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → it.remainingToString = String.ofList r
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_digits : ∀ (b n : ℕ), Nat.ofDigits b (b.digits n) = n