mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Multiplication in a non-unital normed algebra as a continuous bilinear map.  -/
ContinuousLinearMap.mul : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] → [IsScalarTower 𝕜 R R] → [SMulCommClass 𝕜 R R] → R →L[𝕜] R →L[𝕜] R
-- Mathlib.Algebra.CharP.Two
CharTwo.list_sum_mul_self : ∀ {R : Type u_1} [inst : CommSemiring R] [CharP R 2] (l : List R), l.sum * l.sum = (List.map (fun x => x * x) l).sum
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingleton_apply_apply : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : Subsingleton ι] (i : ι) (f : M →L[R] N) (x : ι → M),
  ((ContinuousAlternatingMap.ofSubsingleton R M N i) f) x = f (x i)
-- Mathlib.Util.Superscript
/-- Constructs a mapping (intended for compile time use). Panics on violated invariants.  -/
Mathlib.Tactic.Superscript.mkMapping : String → String → Mathlib.Tactic.Superscript.Mapping
-- Mathlib.Data.Finset.Sym
Finset.replicate_mem_sym : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → ∀ (n : ℕ), Sym.replicate n a ∈ s.sym n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Order.ScottContinuity
/-- The join operation is Scott continuous  -/
ScottContinuous.sup₂ : ∀ {β : Type u_2} [inst : SemilatticeSup β], ScottContinuous fun b => b.1 ⊔ b.2
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_normalizer_of_normal : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.Normal], K ≤ AddSubgroup.normalizer ↑H
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_algebraMap : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : ℝ),
  ((algebraMap ℝ A) r)⁻ = (algebraMap ℝ A) r⁻
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.getD a fallback = t[a]?.getD fallback
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instToExprIProp : Lean.ToExpr Mathlib.Tactic.ITauto.IProp
-- Init.Data.String.Defs
String.Pos.Raw.IsValid.le_rawEndPos : ∀ {s : String} {off : String.Pos.Raw}, String.Pos.Raw.IsValid s off → off ≤ s.rawEndPos
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `U`, the
logarithmic derivative of a finite product of meromorphic functions is the sum of the logarithmic
derivatives.
 -/
MeromorphicOn.logDeriv_finprod_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_3} {F : ι → 𝕜 → 𝕜'},
  (Function.mulSupport F).Finite →
    (∀ (i : ι), MeromorphicOn (F i) U) →
      (∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤) →
        logDeriv (∏ᶠ (i : ι), F i) =ᶠ[Filter.codiscreteWithin U] ∑ᶠ (i : ι), logDeriv (F i)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.wordProd_mul_getD_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (j : ℕ),
  cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instCommMonoid : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] → [inst_2 : CommMonoid Y] → [inst_3 : MulDistribMulAction N Y] → CommMonoid (X →ₑ[σ] Y)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid.  -/
multiset_prod_mem : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [SubmonoidClass B M]
  (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.prod ∈ S
-- Mathlib.RingTheory.HahnSeries.Lex
FiniteArchimedeanClass.congr_simp : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  FiniteArchimedeanClass M = FiniteArchimedeanClass M
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticAt.zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {n : ℤ}, AnalyticAt 𝕜 f z → f z ≠ 0 → AnalyticAt 𝕜 (f ^ n) z
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCategory : CategoryTheory.Category.{u, u + 1} CommMonCat
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.instHasZeroMorphisms.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D],
  CategoryTheory.AddMon.instHasZeroMorphisms =
    { zero := CategoryTheory.AddMon.instZeroHom, comp_zero := ⋯, zero_comp := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
/-- `addOrderOf a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `n • a = 0` if it
exists. Otherwise, i.e. if `a` is of infinite order, then `addOrderOf a` is `0` by convention.  -/
addOrderOf : {G : Type u_1} → [AddMonoid G] → G → ℕ
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sigma_eq_one_iff : ∀ (k n : ℕ), (ArithmeticFunction.sigma k) n = 1 ↔ n = 1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x * a) ⁻¹' Set.Ioc b c = Set.Ioc (b / a) (c / a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.symm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → m₂.Equiv m₁
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapGrp_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapGrp.unitIso =
    CategoryTheory.Functor.mapGrpIdIso.symm ≪≫
      CategoryTheory.Functor.mapGrpNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapGrpCompIso
-- Std.Data.DTreeMap.Internal.WF.Defs
_private.Std.Data.DTreeMap.Internal.WF.Defs.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (k : α) (motive : Option (β k) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β k) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.ODE.PicardLindelof
ODE.FunSpace.compProj_of_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal}
  {α : ODE.FunSpace t₀ x₀ r L} {t : ℝ} (ht : t ∈ Set.Icc tmin tmax), α.compProj t = α.toFun ⟨t, ht⟩
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalysisNoDot : Lean.Options → Bool
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for unsigned shift right on `BitVec`.  -/
BitVec.reduceUShiftRight : Lean.Meta.Simp.DSimproc
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_eq_zero_iff : ∀ {α : Type u}, Cardinal.mk α = 0 ↔ IsEmpty α
-- Mathlib.Data.FunLike.Module
FunLike.mulAction.eq_1 : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [inst : SMul M F] [inst_1 : Monoid M]
  [inst_2 : MulAction M β] [inst_3 : IsSMulApply M F α β],
  FunLike.mulAction = Function.Injective.mulAction DFunLike.coe ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] (F G : CategoryTheory.Functor C V) (c : C) {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (X_1 : C),
  ((((CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map f).app X_1 =
    (CategoryTheory.MonoidalClosed.pre (F.map f.unop)).app
      (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 c))
-- Mathlib.CategoryTheory.ComposableArrows.One
CategoryTheory.ComposableArrows.functorArrows_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (i j n : ℕ)
  (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.functorArrows._auto_1)
  (hj : autoParam (j ≤ n) CategoryTheory.ComposableArrows.functorArrows._auto_3)
  (S : CategoryTheory.ComposableArrows C n),
  (CategoryTheory.ComposableArrows.functorArrows C i j n hij hj).obj S =
    CategoryTheory.ComposableArrows.mk₁ (S.map' i j hij hj)
-- Mathlib.Order.Partition.Basic
/-- A `Partition` of an element `s` of a `CompleteLattice` is a collection of
independent nontrivial elements whose supremum is `s`.  -/
Partition : {α : Type u_1} → [CompleteLattice α] → α → Type u_1
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- `LinearEquiv.lTensor M f : M ⊗ N ≃ₗ M ⊗ P` is the natural linear equivalence
induced by `f : N ≃ₗ P`.  -/
LinearEquiv.lTensor : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      {N : Type u_8} →
        {P : Type u_9} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] → (N ≃ₗ[R] P) → TensorProduct R M N ≃ₗ[R] TensorProduct R M P
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_C_mul : ∀ {R : Type u} [inst : Semiring R] (a : R) (p : Polynomial R),
  Polynomial.derivative (Polynomial.C a * p) = Polynomial.C a * Polynomial.derivative p
-- Mathlib.Order.Hom.Basic
OrderHomClass.coe_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {F : Type u_6} [inst_2 : FunLike F α β]
  [inst_3 : OrderHomClass F α β] (f : F), ⇑↑f = ⇑f
-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.beq : {α : Type u} →
  (self : Std.Packages.PreorderOfLEArgs α) →
    let this := self.le;
    let this := self.decidableLE;
    BEq α
-- Mathlib.Order.Antisymmetrization
instTransAntisymmRelLeLt : {α : Type u_1} →
  [inst : Preorder α] → Trans (AntisymmRel fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.mem_sInf_iff : ∀ {α : Type u_1} [inst : LE α] {S : Set (UpperSet α)} {a : α}, a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.sigmoid_pos : ∀ (x : ℝ), 0 < unitInterval.sigmoid x
-- Mathlib.Order.Monotone.Defs
Monotone.prodMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : Preorder δ] {f : α → γ} {g : β → δ}, Monotone f → Monotone g → Monotone (Prod.map f g)
-- Mathlib.RingTheory.Localization.BaseChange
Algebra.algebraMapSubmonoid_isUnit_le_isUnit : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S],
  Algebra.algebraMapSubmonoid S (IsUnit.submonoid R) ≤ IsUnit.submonoid S
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- One half of **Jordan's inequality**.

In the range `[0, π / 2]`, we have a linear lower bound on `sin`. The other half is given by
`Real.sin_le`.
 -/
Real.mul_le_sin : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi / 2 → 2 / Real.pi * x ≤ Real.sin x
-- Init.System.IO
/-- Sets the POSIX-style permissions for a file.
 -/
IO.setAccessRights : System.FilePath → IO.FileRight → IO Unit
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.IsIdempotent.isIso_whiskerLeft_r_ι : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {Φ : CategoryTheory.Abelian.Preradical C}
  [self : Φ.IsIdempotent], CategoryTheory.IsIso (Φ.r.whiskerLeft Φ.ι)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Every semilinear map between two topological modules, where the source has the module
topology, is continuous.  -/
IsModuleTopology.continuous_of_linearMapₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Semiring R]
  [inst_1 : Semiring S] {A : Type u_3} [inst_2 : AddCommMonoid A] [inst_3 : Module R A] [aA : TopologicalSpace A]
  [IsModuleTopology R A] {B' : Type u_5} [inst_5 : AddCommMonoid B'] [inst_6 : Module S B'] [aB' : TopologicalSpace B']
  [ContinuousAdd B'] [ContinuousSMul S B'] {σ : R →+* S}, Continuous ⇑σ → ∀ (φ : A →ₛₗ[σ] B'), Continuous ⇑φ
-- Mathlib.GroupTheory.PushoutI
/-- A word in `CoprodI` is reduced if none of its letters are in the base group.  -/
Monoid.PushoutI.Reduced : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] → [inst_1 : Group H] → ((i : ι) → H →* G i) → Monoid.CoprodI.Word G → Prop
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_counitIso_hom_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightIso L i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_intCast : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (↑n) (↑n + 1))
-- Mathlib.Order.Category.LinOrd
_private.Mathlib.Order.Category.LinOrd.0.LinOrd.Hom.mk : {X Y : LinOrd} → (↑X →o ↑Y) → X.Hom Y
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.dual_id : ∀ {α : Type u_2} [inst : Max α] [inst_1 : Bot α], SupBotHom.dual (SupBotHom.id α) = InfTopHom.id αᵒᵈ
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.applyFunBinderHeuristic : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Topology.QuasiSeparated
QuasiSeparatedSpace.of_isTopologicalBasis : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} {b : ι → Set α},
  TopologicalSpace.IsTopologicalBasis (Set.range b) → (∀ (i j : ι), IsCompact (b i ∩ b j)) → QuasiSeparatedSpace α
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constSMul : ∀ {G : Type u_1} (P : Type u_2) [inst : Group G] [inst_1 : Torsor G P] (v : G), ⇑(Equiv.constSMul P v) = fun x => v • x
-- Mathlib.Topology.Irreducible
closure_sUnion_irreducibleComponents_sdiff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (irreducibleComponents X).Finite → ∀ Z ∈ irreducibleComponents X, closure (⋃₀ (irreducibleComponents X \ {Z}))ᶜ = Z
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.leadingTerm f = (MvPolynomial.monomial (m.degree f)) (m.leadingCoeff f)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.exists_nonneg : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {c : ℝ} {f : α → E}
  {g' : α → F'} {l : Filter α}, Asymptotics.IsBigOWith c l f g' → ∃ c' ≥ 0, Asymptotics.IsBigOWith c' l f g'
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.comp_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] {F : C → D}
  {X Y Z : CategoryTheory.InducedCategory D F} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Std.Data.ExtDTreeMap.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.Const.getThenInsertIfNew? : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → β → Option β × Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.HasOrthogonalProjection.exists_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} {inst : RCLike 𝕜} {inst_1 : NormedAddCommGroup E} {inst_2 : InnerProductSpace 𝕜 E}
  {K : Submodule 𝕜 E} [self : K.HasOrthogonalProjection] (v : E), ∃ w ∈ K, v - w ∈ Kᗮ
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSub.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (p : ι → P),
  s.weightedVSub p = s.weightedVSubOfPoint p (Classical.choice ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.liftCycles_shift_homologyπ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ}
  (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ)
  (hj : (ComplexShape.up ℤ).next i = j)
  (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0)
  (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j') {Z : C}
  (h : HomologicalComplex.homology ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf)
      (CategoryTheory.CategoryStruct.comp
        (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) h) =
    CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j'
        hj' ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i')
        (CategoryTheory.CategoryStruct.comp
          (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K) h))
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  a < b →
    ∀ {fa fb : E},
      (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
        IntervalIntegrable f' MeasureTheory.volume a b →
          Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds fa) →
            Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds fb) → ∫ (y : ℝ) in a..b, f' y = fb - fa
-- Init.Data.Format.Basic
/-- A monad that can be used to incrementally render `Format` objects.
 -/
Std.Format.MonadPrettyFormat : (Type → Type) → Type
-- Mathlib.Data.List.Sigma
List.mem_dlookup_kunion_middle : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ l₃ : List (Sigma β)},
  b ∈ List.dlookup a (l₁.kunion l₃) → a ∉ l₂.keys → b ∈ List.dlookup a ((l₁.kunion l₂).kunion l₃)
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.eq_ge_of_eq_gt`.

---

If two different elements of the `upperCentralSeries` of a group `G` are equal, then
they are all equal, starting from the smaller index.  -/
upperCentralSeries.eq_ge_of_eq_gt : ∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
  a ≠ b →
    a ≤ c →
      Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b →
        Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G c
-- Std.Http.Data.Method
/-- Update a version-controlled resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-7.1
 -/
Std.Http.Method.update : Std.Http.Method
-- Init.Grind.PP
Lean.Grind.nodeDefUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.rightFunctor.congr_simp : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V],
  CategoryTheory.Preadditive.RightFreyd.rightFunctor V = CategoryTheory.Preadditive.RightFreyd.rightFunctor V
-- Lean.Parser.Command
Lean.Parser.Command.openHiding : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.map_swap : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] {S : Type u_4}
  [inst_2 : NonAssocSemiring S] (f : R →+* S) (i j : n), (Matrix.swap R i j).map ⇑f = Matrix.swap S i j
-- Mathlib.GroupTheory.OrderOfElement
powersEquivPowers_apply : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [inst_1 : Finite G] {x y : G} (h : orderOf x = orderOf y) (n : ℕ),
  (powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩
-- Mathlib.Data.EReal.Inv
EReal.monotone_div_right_of_nonneg : ∀ {b : EReal}, 0 ≤ b → Monotone fun a => a / b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_neg : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x : ℚ}, ↑(-x) = -↑x
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulMono.to_covariantClass_pos_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulMono α],
  CovariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpComp_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor Cᵒᵖ D)
  (G : CategoryTheory.Functor D E) (X : C),
  (F.rightOpComp G).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.op X))))
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_sUnion_of_mem : ∀ {x y z : ZFSet.{u_1}}, y ∈ z → z ∈ x → y ∈ x.sUnion
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.lt_map_map_zero : ∀ (f g : CircleDeg1Lift), f 0 + g 0 - 1 < f (g 0)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
  {h' : Std.Internal.List.containsKey a l = true},
  Std.Internal.List.DistinctKeys l →
    ∀ (h : l.Perm l'), Std.Internal.List.getKey a l h' = Std.Internal.List.getKey a l' ⋯