mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_neg : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D : LieDerivation R L M), ⇑(-D) = -⇑D
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.coe_comp : ∀ {X Y Z : Semigrp} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The algebraic closure of `F` in `E` is algebraic over `F`.  -/
algebraicClosure.isAlgebraic : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Algebra.IsAlgebraic F ↥(algebraicClosure F E)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.mk.inj : ∀ {proof : Lean.Expr} {xs : Array Lean.Expr} {proof_1 : Lean.Expr} {xs_1 : Array Lean.Expr},
  { proof := proof, xs := xs } = { proof := proof_1, xs := xs_1 } → proof = proof_1 ∧ xs = xs_1
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_eq_lcm_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidableEq α], s.lcm f = (Finset.image f s).lcm id
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.mk.injEq : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (I : Type u) (s : I → M.sections)
  (epi : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s)) SheafOfModules.GeneratingSections.epi._autoParam)
  (I_1 : Type u) (s_1 : I_1 → M.sections)
  (epi_1 : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s_1)) SheafOfModules.GeneratingSections.epi._autoParam),
  ({ I := I, s := s, epi := epi } = { I := I_1, s := s_1, epi := epi_1 }) = (I = I_1 ∧ s ≍ s_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α},
  k ∈ ↑(t.insertMany l ⋯) → (List.map Sigma.fst l).contains k = false → k ∈ t
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le : ∀ {𝕜 : Type u} {ι : Type v} (E : ι → Type wE) {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : ContinuousMultilinearMap 𝕜 E₁ G), ‖g.compContinuousLinearMapLRight‖ ≤ ‖g‖
-- Mathlib.Tactic.CategoryTheory.IsoReassoc
/-- Given an equation `f = g` between isomorphisms `X ≅ Y` in a category,
produce the equation `∀ {Z} (h : Y ≅ Z), f ≪≫ h = g ≪≫ h`,
but with compositions fully right associated, identities removed, and functors applied.
 -/
Mathlib.Tactic.Reassoc.reassocExprIso : Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filterMap f m).contains k = true → m.contains k = true
-- Mathlib.CategoryTheory.Limits.Creates
/-- Define the lift of a cocone: For a cocone `c` for `K ⋙ F`, give a cocone for
`K` which is a lift of `c`, i.e. the image of it under `F` is (iso) to `c`.

We will then use this as part of the definition of creation of colimits:
every limit cocone has a lift.

Note this definition is really only useful when `c` is a colimit already.
 -/
CategoryTheory.LiftableCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J C) →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.Limits.Cocone (K.comp F) → Type (max (max (max u₁ v₁) v₂) w)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_destruct_map : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  (s : Stream'.Seq (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)),
  s.destruct =
    Option.map
      (fun x =>
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct s)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If `E` and `F` are isomorphic pre-`1`-hypercovers and `G` is a presheaf,
the multifork for `E` is exact if and only if the multifork for `F` is exact.  -/
CategoryTheory.PreOneHypercover.isLimitEquivOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {S : C} →
          {E F : CategoryTheory.PreOneHypercover S} →
            (E ≅ F) →
              (G : CategoryTheory.Functor Cᵒᵖ A) →
                CategoryTheory.Limits.IsLimit (E.multifork G) ≃ CategoryTheory.Limits.IsLimit (F.multifork G)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.base_subset`. -/
Topology.CWComplex.Subcomplex.base_subset : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C), D ⊆ ↑E
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_iInf : ∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} {S : ι → Subfield K}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Std.Http.Data.URI.Encoding
/-- Converts a nibble (4-bit value, 0-15) to its hexadecimal digit representation. Returns '0'-'9' for
values 0-9, and 'A'-'F' for values 10-15.
 -/
Std.Http.URI.hexDigit : UInt8 → UInt8
-- Mathlib.Order.Cover
Bool.wcovBy_iff : ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
/-- Any standard Borel space is measurably equivalent to a subset of the reals.  -/
MeasureTheory.exists_subset_real_measurableEquiv : ∀ (α : Type u_1) [inst : MeasurableSpace α] [StandardBorelSpace α], ∃ s, MeasurableSet s ∧ Nonempty (α ≃ᵐ ↑s)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
/-- Negative part of a simple function.  -/
MeasureTheory.SimpleFunc.negPart : {α : Type u_1} →
  {E : Type u_2} →
    [LinearOrder E] →
      [Zero E] → [inst : MeasurableSpace α] → [Neg E] → MeasureTheory.SimpleFunc α E → MeasureTheory.SimpleFunc α E
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.mem_S'_iff : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × OnePoint X)
  (y : (x : OnePoint X) → ↑(Prod.snd ∘ π ⁻¹' {x})),
  y ∈ InternalProjectivityProof.S'✝ π ↔ ∀ (n m : OnePoint X), (π ↑(y n)).1 = (π ↑(y m)).1
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.fullyFaithfulForgetToAddMonCat.eq_1 : AddCommMonCat.fullyFaithfulForgetToAddMonCat =
  { preimage := fun {X Y} f => AddCommMonCat.ofHom (AddMonCat.Hom.hom f),
    map_preimage := @AddCommMonCat.fullyFaithfulForgetToAddMonCat._proof_1,
    preimage_map := @AddCommMonCat.fullyFaithfulForgetToAddMonCat._proof_2 }
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheoremType.id.sizeOf_spec : sizeOf Mathlib.Meta.FunProp.LambdaTheoremType.id = 1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.instIsFractionRingSubtypeMem : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), IsFractionRing (↥A) K
-- Mathlib.Order.Concept
upperPolar_anti : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop), Antitone (upperPolar r)
-- Mathlib.Lean.Expr.Rat
/-- Test if an expression represents an explicit number written in normal form:
* A "natural number in normal form" is an expression `OfNat.ofNat n`, even if it is not of type `ℕ`,
  as long as `n` is a literal.
* An "integer in normal form" is an expression which is either a natural number in number form,
  or `-n`, where `n` is a natural number in normal form.
* A "rational in normal form" is an expressions which is either an integer in normal form,
  or `n / d` where `n` is an integer in normal form, `d` is a natural number in normal form,
  `d ≠ 1`, and `n` and `d` are coprime (in particular, we check that `(mkRat n d).den = d`).
 -/
Lean.Expr.isExplicitNumber : Lean.Expr → Bool
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.filterMap_eq_toIter_filterMap_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {f : β → Option γ},
  Std.Iter.filterMap f it = (Std.IterM.filterMap f it.toIterM).toIter
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K K' : ChainComplex C ℕ} (f : K ⟶ K') {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [inst_2 : CategoryTheory.Mono i] {Z : C}
  (h : K'.X Δ.len ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
      (CategoryTheory.CategoryStruct.comp (f.f Δ.len) h) =
    CategoryTheory.CategoryStruct.comp (f.f Δ'.len)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i) h)
-- Std.Data.DHashMap.Basic
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.DHashMap.containsThenInsert : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → (a : α) → β a → Bool × Std.DHashMap α β
-- Mathlib.Algebra.Group.Defs
/-- **Alias** of the reverse direction of `isMulCommutative_iff`. -/
IsMulCommutative.of_comm : ∀ {M : Type u_2} [inst : Mul M], (∀ (a b : M), a * b = b * a) → IsMulCommutative M
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonTextDocumentSyncOptions : Lean.ToJson Lean.Lsp.TextDocumentSyncOptions
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso.eq_1 : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w),
  h.orderMonoidIso =
    { toFun := h.valueGroup₀Fun, invFun := ⋯.valueGroup₀Fun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
      map_le_map_iff' := ⋯ }
-- Mathlib.Algebra.CubicDiscriminant
Cubic.roots.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (P : Cubic R), P.roots = P.toPoly.roots
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_right_iff : ∀ {R : Type u_1} [inst : CommRing R] (x y : R), IsRelPrime x (-y) ↔ IsRelPrime x y
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_zero_right : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x : E}, inner A x 0 = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_sUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {S : Set (Set α)},
  S.Countable → S.Pairwise Disjoint → (∀ s ∈ S, MeasurableSet s) → μ (⋃₀ S) = ∑' (s : ↑S), μ ↑s
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Algebra.instSMulCommClassCarrier : ∀ {S₀ : Type u₀} [inst : CommSemiring S₀] {S : Type u} [inst_1 : Ring S] [inst_2 : Algebra S₀ S] {M : ModuleCat S},
  SMulCommClass S S₀ ↑M
-- Lean.Data.Lsp.Extra
Lean.Lsp.DependencyBuildMode.always.sizeOf_spec : sizeOf Lean.Lsp.DependencyBuildMode.always = 1
-- Mathlib.Analysis.Normed.Group.Basic
mem_sphere_iff_norm' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, b ∈ Metric.sphere a r ↔ ‖b / a‖ = r
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.fold.eq_2 : ∀ {σ : Sort u_1} {α : Type u_2} (v₀ : σ) (f : σ → α → σ → σ) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α),
  RBTree.RBNode.fold v₀ f (RBTree.RBNode.node c l v r) = f (RBTree.RBNode.fold v₀ f l) v (RBTree.RBNode.fold v₀ f r)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The image of a monomorphism is isomorphic to the source.  -/
CategoryTheory.Limits.imageMonoIsoSource : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (f : X ⟶ Y) → [inst_1 : CategoryTheory.Mono f] → CategoryTheory.Limits.image f ≅ X
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).size =
        if Std.DTreeMap.Internal.Impl.contains k t = true then t.size else t.size + 1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasurableEmbedding.integral_map_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {β : Type u_9}
  [inst_6 : MeasurableSpace β] {φ : X → β},
  MeasurableEmbedding φ → ∀ {f : β → E}, ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_atTop : ∀ (f : CircleDeg1Lift), Filter.Tendsto (⇑f) Filter.atTop Filter.atTop
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_one_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B} {a : A},
  (MonoidWithZeroHom.ValueGroup₀.restrict₀ f) a = 1 ↔ f a = 1
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.isUniformEmbedding_comp : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : Zero R]
  [inst_3 : UniformSpace R] {Y : Type u_3} [inst_4 : UniformSpace Y] [inst_5 : Zero Y] (g : ContinuousMapZero Y R),
  IsUniformEmbedding ⇑g → IsUniformEmbedding fun x => g.comp x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.toArray.size = t.size
-- Mathlib.Data.Finset.Sups
Finset.Nonempty.sups : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] {s t : Finset α},
  s.Nonempty → t.Nonempty → (s ⊻ t).Nonempty
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.count_D_lt_count_U_of_lt_firstReturn : ∀ {p : DyckWord} {i : ℕ},
  i < p.firstReturn → List.count DyckStep.D (List.take (i + 1) ↑p) < List.count DyckStep.U (List.take (i + 1) ↑p)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instOrderBotValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → OrderBot (ValuativeRel.ValueGroupWithZero R)
-- Init.Data.List.Lemmas
List.contains_cons : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α}, (a :: l).contains b = (b == a || l.contains b)
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_nat_cast : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (n k : ℕ),
  (ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)
-- Mathlib.Topology.UnitInterval
unitInterval.instLinearOrderedCommMonoidWithZeroElemReal : LinearOrderedCommMonoidWithZero ↑unitInterval
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF → ∀ {a : α} {h' : a ∈ t}, Std.DTreeMap.Raw.Const.get t a h' = Std.DTreeMap.Raw.Const.get! t a
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.ElementarySubstructure M),
  L.ElementarilyEquivalent (↥S) M
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate.match_1.splitter : {α : Type u_1} →
  (motive : List α × List α → Sort u_2) → (x : List α × List α) → ((l₁ l₂ : List α) → motive (l₁, l₂)) → motive x
-- Std.Data.ExtHashMap.Basic
/-- If there is no mapping for the given key, inserts the given mapping into the map. Otherwise,
returns the map unaltered.
 -/
Std.ExtHashMap.insertIfNew : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → Std.ExtHashMap α β
-- Mathlib.Algebra.Order.Field.Basic
Bound.div_lt_one_of_pos_of_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α}, 0 < b → a < b → a / b < 1
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support has a global maximum.  -/
Continuous.exists_forall_ge_of_hasCompactSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [Nonempty β] [inst_5 : Zero α] {f : β → α},
  Continuous f → HasCompactSupport f → ∃ x, ∀ (y : β), f y ≤ f x
-- Mathlib.RingTheory.AdicCompletion.Exactness
/-- In each step, a preimage is constructed from the preimage of the previous step by
adding this delta.  -/
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapExactAuxDelta : {R : Type u} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type u} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {f : M →ₗ[R] N} →
                    Function.Injective ⇑f →
                      {k : ℕ} →
                        (∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)) →
                          (x : AdicCompletion.AdicCauchySequence I N) →
                            {n : ℕ} →
                              {d : N} →
                                d ∈ I ^ (k + n + 1) • ⊤ →
                                  {y yₙ : M} →
                                    f y = ↑x (k + n + 1) - d →
                                      f yₙ - ↑x (k + n) ∈ I ^ (k + n) • ⊤ →
                                        ↑{d | f (yₙ + ↑d) - ↑x (k + n + 1) ∈ I ^ (k + n + 1) • ⊤}
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.addGroupEquivQuotientProdAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α},
  AddSubgroup.addGroupEquivQuotientProdAddSubgroup =
    Trans.trans
      (Trans.trans
        (Trans.trans (Equiv.sigmaFiberEquiv QuotientAddGroup.mk).symm
          (Equiv.sigmaCongrRight fun L => ⋯.mpr (id (⋯.mpr (Equiv.refl { x // Quotient.mk'' x = L })))))
        (Equiv.sigmaCongrRight fun x => AddSubgroup.leftCosetEquivAddSubgroup (Quotient.out x)))
      (Equiv.sigmaEquivProd (α ⧸ s) ↥s)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ max a b → Set.Ico a b ∪ Set.Ici c = Set.Ici (min a c)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.eval₂_reverse_eq_zero_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : CommSemiring S] (i : R →+* S) (x : S)
  [inst_2 : Invertible x] (f : Polynomial R), Polynomial.eval₂ i (⅟x) f.reverse = 0 ↔ Polynomial.eval₂ i x f = 0
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.modEq_nsmul_cases`.

---

If `a ≡ b [PMOD p]`, then mod `n • p` there are `n` cases.  -/
AddCommGroup.ModEq.nsmul_cases : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (n : ℕ),
  n ≠ 0 → a ≡ b [PMOD p] → ∃ i < n, a ≡ b + i • p [PMOD n • p]
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.instFintypeCarrierObjTopCatForget₂ContinuousMapToTop : (X : FinTopCat) → Fintype ↑((CategoryTheory.forget₂ FinTopCat TopCat).obj X)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.toFractionRing_eq : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  RatFunc.toFractionRing =
    ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (RatFunc K) (FractionRing (Polynomial K)))
-- Init.Prelude
Nat.mul_pos : ∀ {n m : ℕ}, 0 < n → 0 < m → 0 < n * m
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `PartitionOfUnity ι X s` that is subordinate to `U`.  -/
PartitionOfUnity.exists_isSubordinate : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X] [ParacompactSpace X],
  IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
-- Mathlib.LinearAlgebra.RootSystem.BaseChange
RootPairing.restrictScalars_coe_coroot : ∀ {ι : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field L] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module L M] [inst_4 : Module L N] (P : RootPairing ι L M N) (K : Type u_5)
  [inst_5 : Field K] [inst_6 : Algebra K L] [inst_7 : Module K M] [inst_8 : Module K N] [inst_9 : IsScalarTower K L M]
  [inst_10 : IsScalarTower K L N] [inst_11 : P.IsBalanced] [inst_12 : P.IsValuedIn K] (i : ι),
  ↑((P.restrictScalars' K).coroot i) = P.coroot i
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_C_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (r : R) (f : PowerSeries R),
  (PowerSeries.trunc n) (PowerSeries.C r * f) = Polynomial.C r * (PowerSeries.trunc n) f
-- Init.Data.String.Basic
String.Pos.sliceFrom_inj : ∀ {s : String} {p₀ pos pos' : s.Pos} {h : p₀ ≤ pos} {h' : p₀ ≤ pos'},
  p₀.sliceFrom pos h = p₀.sliceFrom pos' h' ↔ pos = pos'
-- Mathlib.CategoryTheory.Monad.Coequalizer
/-- The cofork map in the coequalizer diagram we will construct.  -/
CategoryTheory.Monad.FreeCoequalizer.π : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {T : CategoryTheory.Monad C} → (X : T.Algebra) → T.free.obj X.A ⟶ X
-- Init.Data.Array.Basic
/-- Removes all the elements that satisfy a predicate from the end of an array.

The longest contiguous sequence of elements that all satisfy the predicate is removed.

Examples:
* `#[0, 1, 2, 3, 4].popWhile (· > 2) = #[0, 1, 2]`
* `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]`
* `(#[] : Array Nat).popWhile (· > 2) = #[]`
 -/
Array.popWhile : {α : Type u} → (α → Bool) → Array α → Array α
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.isMaximal_of_mem_primesOver : ∀ {A : Type u_1} [inst : CommRing A] {p : Ideal A} [p.IsMaximal] {B : Type u_2} [inst_2 : CommRing B]
  [inst_3 : Algebra A B] [Algebra.IsIntegral A B] {P : Ideal B}, P ∈ p.primesOver B → P.IsMaximal
-- Mathlib.RingTheory.RingHom.Smooth
/-- A ring homomorphism `f : R →+* S` is formally smooth
if `S` is formally smooth as an `R` algebra.  -/
RingHom.FormallySmooth : {R : Type u_1} → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_add_succ_right_eq_push' : ∀ {m n : ℕ}, (m...m + (n + 1)).toArray = (m...m + n).toArray.push (m + n)