mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.LocalSubring
LocalSubring.map_maximalIdeal_eq_top_of_isMax : ∀ {K : Type u_3} [inst : Field K] {R : LocalSubring K},
  IsMax R →
    ∀ {S : Subring K} (hS : R.toSubring < S),
      Ideal.map (Subring.inclusion ⋯) (IsLocalRing.maximalIdeal ↥R.toSubring) = ⊤
-- Mathlib.Algebra.Group.TypeTags.Basic
ofAdd_sub : ∀ {α : Type u} [inst : Sub α] (x y : α), Multiplicative.ofAdd (x - y) = Multiplicative.ofAdd x / Multiplicative.ofAdd y
-- Mathlib.Data.Seq.Parallel
Computation.Corec.f.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (x : α ⊕ β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)) (val : β),
  x = Sum.inr val →
    (match x with
      | Sum.inl a => h_1 a
      | Sum.inr val => h_2 val) ≍
      h_2 val
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y}
  (toMapFactorizationData :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f)
  (s : Y ⟶ toMapFactorizationData.Z)
  (s_p :
    autoParam (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam)
  (cofibration_s :
    autoParam (HomotopicalAlgebra.Cofibration s)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam)
  (toMapFactorizationData_1 :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f)
  (s_1 : Y ⟶ toMapFactorizationData_1.Z)
  (s_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 toMapFactorizationData_1.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam)
  (cofibration_s_1 :
    autoParam (HomotopicalAlgebra.Cofibration s_1)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam),
  ({ toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p, cofibration_s := cofibration_s } =
      { toMapFactorizationData := toMapFactorizationData_1, s := s_1, s_p := s_p_1,
        cofibration_s := cofibration_s_1 }) =
    (toMapFactorizationData = toMapFactorizationData_1 ∧ s ≍ s_1)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_uIcc_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.uIcc a b, f (Fin.castAdd m i)
-- Mathlib.Data.Sum.Order
/-- `orderDual` is distributive over `⊕` up to an order isomorphism.  -/
OrderIso.sumDualDistrib : (α : Type u_10) → (β : Type u_11) → [inst : LE α] → [inst_1 : LE β] → (α ⊕ β)ᵒᵈ ≃o αᵒᵈ ⊕ βᵒᵈ
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_index : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K : Set G},
  IsCompact K →
    ∀ (g : G) {V : Set G},
      (interior V).Nonempty →
        MeasureTheory.Measure.haar.index ((fun h => g * h) '' K) V = MeasureTheory.Measure.haar.index K V
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.of_counit : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : Ring X] [inst_2 : Bialgebra R X],
  CoalgebraStruct.counit = CoalgebraStruct.counit
-- Mathlib.Order.UpperLower.Closure
lowerClosure_sUnion : ∀ {α : Type u_1} [inst : Preorder α] (S : Set (Set α)), lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s
-- Mathlib.CategoryTheory.Limits.Preserves.Over
CategoryTheory.Limits.instPreservesCofilteredLimitsOfSizeOverForget : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C},
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{u_2, u_3, v_1, v_1, max u_1 v_1, u_1}
    (CategoryTheory.Over.forget X)
-- Mathlib.FieldTheory.SeparableClosure
/-- If `K / E / F` is a field extension tower, then `E` adjoin `separableClosure F K` is contained
in `separableClosure E K`.  -/
separableClosure.adjoin_le : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K],
  IntermediateField.adjoin E ↑(separableClosure F K) ≤ separableClosure E K
-- Mathlib.Data.Set.Monotone
/-- **Alias** of the forward direction of `strictMono_domRestrict`. -/
StrictMono.of_domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMono (s.domRestrict f) → StrictMonoOn f s
-- Mathlib.Analysis.Convex.EGauge
egauge.eq_1 : ∀ (𝕜 : Type u_1) [inst : ENorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] (s : Set E) (x : E),
  egauge 𝕜 s x = ⨅ c, ⨅ (_ : x ∈ c • s), ‖c‖ₑ
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.mk.injEq : ∀ (parent : Lean.Name) (components : List String) (parent_1 : Lean.Name) (components_1 : List String),
  ({ parent := parent, components := components } = { parent := parent_1, components := components_1 }) =
    (parent = parent_1 ∧ components = components_1)
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.inclusion_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M} (h : p ≤ p'), Function.Injective ⇑(Submodule.inclusion h)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- When `f.ker ⊓ I` is a sub-dp-ideal of `I`, this is the induced divided power structure on
the ideal `I.map f` of the target.  -/
DividedPowers.Quotient.OfSurjective.dividedPowers : {A : Type u_1} →
  [inst : CommRing A] →
    {I : Ideal A} →
      (hI : DividedPowers I) →
        {B : Type u_2} →
          [inst_1 : CommRing B] →
            {f : A →+* B} →
              {J : Ideal B} →
                Function.Surjective ⇑f → J = Ideal.map f I → hI.IsSubDPIdeal (RingHom.ker f ⊓ I) → DividedPowers J
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_single_mul : ∀ {m : Type u_9} {n : Type u_10} {R : Type u_11} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : NonUnitalNonAssocSemiring R] [inst_4 : Fintype m] (i : n) (j : m) (a : R) (x : Matrix m n R),
  (Matrix.single i j a * x).trace = a • x j i
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `image.preComp f g` is a monomorphism.
 -/
CategoryTheory.Limits.image.preComp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasImage g]
  [inst_2 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.Mono (CategoryTheory.Limits.image.preComp f g)
-- Init.SimpLemmas
have_val_congr' : ∀ {α : Sort u} {β : Sort v} {a a' : α} {f : α → β}, a = a' → f a = f a'
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for modulo on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalMod : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- The minimal submodule that contains all strata.

This is the domain of our "base" embedding into Hahn series, which we will extend into a full
embedding.  -/
HahnEmbedding.ArchimedeanStrata.baseDomain : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] → HahnEmbedding.ArchimedeanStrata K M → Submodule K M
-- Mathlib.GroupTheory.Focal
/-- The Transfer homomorphism is surjective from `G` to `P/P*`.  -/
Subgroup.transferFocal_surjective : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [inst_2 : (↑P).FiniteIndex],
  Function.Surjective ⇑(↑P).transferFocal
-- Std.Http.Data.Status
/-- 426 Upgrade Required
 -/
Std.Http.Status.upgradeRequired : Std.Http.Status
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_apply_le_one : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f : α → M} {a : α},
  (a ∈ s → f a ≤ 1) → s.mulIndicator f a ≤ 1
-- Std.Http.Protocol.H1.Reader
/-- Marks that no more input will be provided (connection closed).
 -/
Std.Http.Protocol.H1.Reader.markNoMoreInput : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_comap_inl : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M) (q : Submodule R M₂),
  Submodule.comap (LinearMap.inl R M M₂) (p.prod q) = p
-- Mathlib.Data.Set.Card
Set.encard_pair : ∀ {α : Type u_1} {x y : α}, x ≠ y → {x, y}.encard = 2
-- Mathlib.CategoryTheory.IsomorphismClasses
/-- An object `X` is isomorphic to an object `Y` if `X ≅ Y` is nonempty.  -/
CategoryTheory.IsIsomorphic : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → C → Prop
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.isDomain : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [IsDomain A] [inst_3 : Algebra R A]
  (S : Subalgebra R A), IsDomain ↥S
-- Mathlib.Topology.Algebra.LinearTopology
/-- If `R` is commutative and left-linearly topologized, it is also right-linearly topologized.  -/
IsLinearTopology.instMulOpposite : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R], IsLinearTopology Rᵐᵒᵖ R
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.lieAlgebraOf_apply : ∀ (R : Type u) (ι : Type v) [inst : CommRing R] (L : ι → Type w) [inst_1 : (i : ι) → LieRing (L i)]
  [inst_2 : (i : ι) → LieAlgebra R (L i)] [inst_3 : DecidableEq ι] (j : ι) (a : L j),
  (DirectSum.lieAlgebraOf R ι L j) a = (DirectSum.of L j) a
-- Batteries.Lean.HashSet
/-- `O(n)`. Returns `true` if `f` returns `true` for all elements of the set.
 -/
Std.HashSet.allM : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {m : Type → Type u_2} → [Monad m] → Std.HashSet α → (α → m Bool) → m Bool
-- Aesop.RuleTac.Basic
Aesop.CasesPattern : Type
-- Mathlib.Algebra.Opposites
MulOpposite.op.eq_1 : ∀ {α : Type u_1}, MulOpposite.op = PreOpposite.op'
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.mvarIds : Lean.Meta.RewriteResult → List Lean.MVarId
-- Mathlib.CategoryTheory.Discrete.SumsProducts
/-- A product of discrete categories is discrete.  -/
CategoryTheory.IsDiscrete.prod : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_3)
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [CategoryTheory.IsDiscrete C] [CategoryTheory.IsDiscrete D],
  CategoryTheory.IsDiscrete (C × D)
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingFirst_zero : Nat.stirlingFirst 0 0 = 1
-- Mathlib.RingTheory.Length
Module.length_eq_rank : ∀ (K : Type u_5) (M : Type u_6) [inst : DivisionRing K] [inst_1 : AddCommGroup M] [inst_2 : Module K M],
  Module.length K M = Cardinal.toENat (Module.rank K M)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.single 1` as a `RingHom`  -/
MonoidAlgebra.singleOneRingHom : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [inst_1 : MulOneClass M] → R →+* MonoidAlgebra R M
-- Mathlib.Order.RelIso.Basic
/-- `Quotient.out` as a relation embedding between the lift of a relation and the relation.  -/
Quotient.outRelEmbedding : {α : Type u_1} →
  {x : Setoid α} →
    {r : α → α → Prop} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) → Quotient.lift₂ r H ↪r r
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.eval₂_reverse_mul_pow : ∀ {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 * x ^ f.natDegree = Polynomial.eval₂ i x f
-- Aesop.Util.UnionFind
Aesop.UnionFind.mk.inj : ∀ {α : Type u_1} {inst : BEq α} {inst_1 : Hashable α} {parents sizes : Array USize} {toRep : Std.HashMap α USize}
  {parents_1 sizes_1 : Array USize} {toRep_1 : Std.HashMap α USize},
  { parents := parents, sizes := sizes, toRep := toRep } =
      { parents := parents_1, sizes := sizes_1, toRep := toRep_1 } →
    parents = parents_1 ∧ sizes = sizes_1 ∧ toRep = toRep_1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- An equation between morphisms gives a comparison map between the images
(which momentarily we prove is an iso).
 -/
CategoryTheory.Limits.image.eqToHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f f' : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasImage f] →
          [inst_2 : CategoryTheory.Limits.HasImage f'] →
            f = f' → (CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.image f')
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.Status.noConfusionType : Sort v✝ → Lean.Util.ParamMinimizer.Status → Lean.Util.ParamMinimizer.Status → Sort v✝
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂] (i₁₂ i₁₂' : I₁₂) {Z : C}
  (h : L.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂)
      (CategoryTheory.CategoryStruct.comp (L.D₁ c₁₂ i₁₂ i₁₂') h) =
    CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂') h)
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atBot_eq_generate_of_not_bddBelow : ∀ {α : Type u_3} [inst : LinearOrder α] {s : Set α}, ¬BddBelow s → Filter.atBot = Filter.generate (Set.Iic '' s)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- **Alias** of `norm_add_sq_real`.

---

Expand the square  -/
norm_add_pow_two_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * inner ℝ x y + ‖y‖ ^ 2
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with product greater than one must have positive length.  -/
List.length_pos_of_one_lt_prod : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : Preorder M] (L : List M), 1 < L.prod → 0 < L.length
-- Mathlib.RingTheory.Jacobson.Ring
Ideal.radical_eq_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [H : IsJacobsonRing R] (I : Ideal R), I.radical = I.jacobson
-- Mathlib.Algebra.Group.Defs
mul_comm : ∀ {G : Type u_1} [inst : CommMagma G] (a b : G), a * b = b * a
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} {X Y : CategoryTheory.Limits.Cocone F.rightOp} (f : X ⟶ Y),
  CategoryTheory.Limits.coconeRightOpOfConeEquiv.inverse.map f = Opposite.op { hom := f.hom.unop, w := ⋯ }
-- Init.Grind.Interactive
/-- The `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded.

* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
 -/
Lean.Parser.Tactic.Grind.have : Lean.ParserDescr
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.evalSuggest : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.limitCone_π_app_hom : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (F : CategoryTheory.Functor J (CategoryTheory.Mon C))
  (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Mon.forget C))) (hc : CategoryTheory.Limits.IsLimit c)
  (j : J), ((CategoryTheory.Mon.limitCone F c hc).π.app j).hom = c.π.app j
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.lift_apply : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommGroup G] (f : M →+ G)
  (x : Algebra.GrothendieckAddGroup M),
  (Algebra.GrothendieckAddGroup.lift f) x =
    f ((AddLocalization.addMonoidOf ⊤).sec x).1 - f ↑((AddLocalization.addMonoidOf ⊤).sec x).2
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.toCostructuredArrow_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) {X Y : F.Elementsᵒᵖ}
  (f : X ⟶ Y),
  (CategoryTheory.CategoryOfElements.toCostructuredArrow F).map f =
    CategoryTheory.CostructuredArrow.homMk (↑f.unop).unop ⋯
-- Lean.DocString.Add
/-- Adds a docstring to the environment. If `isVerso` is `false`, then the docstring is interpreted as
Markdown.
 -/
Lean.addDocStringOf : Bool → Lean.Name → Lean.Syntax → Lean.TSyntax `Lean.Parser.Command.docComment → Lean.Elab.TermElabM Unit
-- Init.Data.Array.Basic
/-- Applies the monadic action `f` to every element in the array, left-to-right, and returns the array
of results.
 -/
Array.mapM : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m β) → Array α → m (Array β)
-- Mathlib.Order.RelIso.Basic
/-- `Sum.inr` as a relation embedding into `Sum.LiftRel r s`.  -/
RelEmbedding.sumLiftRelInr : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → s ↪r Sum.LiftRel r s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = false → (k' ∈ Std.ExtDHashMap.Const.alter m k f ↔ k' ∈ m)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_eq_empty_of_lt : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b < a → Finset.Icc a b = ∅
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.localizedModuleFunctor_map : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R) {X Y : ModuleCat R} (f : X ⟶ Y),
  (ModuleCat.localizedModuleFunctor S).map f = ModuleCat.localizedModuleMap S f
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.finsuppProd : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Zero β] (c : Con M) (h h' : ι → β → M)
  {f g : ι →₀ β},
  (∀ (i : ι), c (h i 0) 1) →
    (∀ (i : ι), c (h' i 0) 1) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.prod h) (g.prod h')
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionOfComplement.trans_F : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5} {F' : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F]
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {H : Type u_7} [inst_9 : TopologicalSpace H]
  {G : Type u_9} [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G}
  {M : Type u_11} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] {N : Type u_13}
  [inst_13 : TopologicalSpace N] [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersionOfComplement F I J n f → ∀ (e : F ≃L[𝕜] F'), Manifold.IsImmersionOfComplement F' I J n f
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_const_add : ∀ {E : Type u_3} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace ℝ E] [BorelSpace E] (r t : E),
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => r + x) μ) t =
    MeasureTheory.charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)
-- Mathlib.Algebra.Star.MonoidHom
/-- Promote a bijective star monoid homomorphism to a star monoid equivalence.  -/
StarMulEquiv.ofBijective : {A : Type u_2} →
  {B : Type u_3} →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : Star A] → [inst_3 : Star B] → (f : A →⋆* B) → Function.Bijective ⇑f → A ≃⋆* B
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_inter_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom : ∀ {ι : Type u_2} {R : ι → Type u_1} [inst : (i : ι) → CommRing (R i)] (s : Set ((i : ι) → R i)),
  s.Finite → (∀ (i : ι), Ideal.span (⇑(Pi.evalRingHom (fun x => R x) i) '' s) = ⊤) → Ideal.span s = ⊤
-- Init.Data.Int.Lemmas
Int.neg_mul_neg : ∀ (a b : ℤ), -a * -b = a * b
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval_gate : ∀ {α : Type} {a : α → Bool} {g : Std.Tactic.BVDecide.Gate} {x y : Std.Tactic.BVDecide.BoolExpr α},
  Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.gate g x y) =
    g.eval (Std.Tactic.BVDecide.BoolExpr.eval a x) (Std.Tactic.BVDecide.BoolExpr.eval a y)
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σ[A]` of a finset `A` in a group is `|A + A| / |A|`.  -/
Combinatorics.Additive.«termσ[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Defs
/-- The additive inverse of one multiplied by an element of a ring is the element's additive
inverse.  -/
neg_one_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), -1 * a = -a
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_iInf_le : ∀ {G : Type u_1} [inst : AddGroup G] {L : AddSubgroup G} {ι : Type u_3} [inst_1 : Fintype ι] (f : ι → AddSubgroup G),
  (⨅ i, f i).relIndex L ≤ ∏ i, (f i).relIndex L
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAdd : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Add γ] → [ContinuousAdd γ] → Add (α →ₘ[μ] γ)
-- Aesop.Script.Tactic
Aesop.Script.Tactic.mk.injEq : ∀ (uTactic : Aesop.Script.UTactic) (sTactic? : Option Aesop.Script.STactic) (uTactic_1 : Aesop.Script.UTactic)
  (sTactic?_1 : Option Aesop.Script.STactic),
  ({ uTactic := uTactic, sTactic? := sTactic? } = { uTactic := uTactic_1, sTactic? := sTactic?_1 }) =
    (uTactic = uTactic_1 ∧ sTactic? = sTactic?_1)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_StateT_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u_3} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {σ α : Type u} {post : α → σ → Pred}
  {epost : EPred} (x : StateT σ m α) (h : ε → StateT σ m α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost = fun s =>
    Std.Internal.Do.wp (MonadExceptOf.tryCatch (x.run s) fun e => (h e).run s)
      (fun x =>
        match x with
        | (a, s') => post a s')
      epost
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.of.eq_1 : ∀ (M : Type u) [inst : Semigroup M], Semigrp.of M = { carrier := M, str := inst }
-- Mathlib.NumberTheory.Real.Irrational
/-- There is an irrational number `r` between any two reals `x < r < y`.  -/
exists_irrational_btwn : ∀ {x y : ℝ}, x < y → ∃ r, Irrational r ∧ x < r ∧ r < y
-- Init.Data.List.Basic
List.modifyTailIdx.go : {α : Type u} → (List α → List α) → ℕ → List α → List α