mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Server.GoTo
Lean.Server.GoToContext.mk.inj : ∀ {doc : Lean.Server.DocumentMeta} {kind : Lean.Server.GoToKind} {infoTree? : Option Lean.Elab.InfoTree}
  {originInfo? : Option Lean.Elab.Info} {children : Lean.PersistentArray Lean.Elab.InfoTree}
  {doc_1 : Lean.Server.DocumentMeta} {kind_1 : Lean.Server.GoToKind} {infoTree?_1 : Option Lean.Elab.InfoTree}
  {originInfo?_1 : Option Lean.Elab.Info} {children_1 : Lean.PersistentArray Lean.Elab.InfoTree},
  { doc := doc, kind := kind, infoTree? := infoTree?, originInfo? := originInfo?, children := children } =
      { doc := doc_1, kind := kind_1, infoTree? := infoTree?_1, originInfo? := originInfo?_1, children := children_1 } →
    doc = doc_1 ∧ kind = kind_1 ∧ infoTree? = infoTree?_1 ∧ originInfo? = originInfo?_1 ∧ children = children_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The opposite morphism in `ShortComplex Cᵒᵖ` associated to a morphism in `ShortComplex C`  -/
CategoryTheory.ShortComplex.opMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → (S₂.op ⟶ S₁.op)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules.
Then there is a linear map from `⨂ᵢ Hom(sᵢ, Hom(tᵢ, t'ᵢ))` to `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))`
defined by `⨂ᵢ fᵢ ↦ ⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.

This is `TensorProduct.homTensorHomMap` for two arbitrary families of modules.
 -/
PiTensorProduct.piTensorHomMap₂ : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              {t' : ι → Type u_12} →
                [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                  [inst_4 : (i : ι) → Module R (t i)] →
                    [inst_5 : (i : ι) → AddCommMonoid (t' i)] →
                      [inst_6 : (i : ι) → Module R (t' i)] →
                        (PiTensorProduct R fun i => s i →ₗ[R] t i →ₗ[R] t' i) →ₗ[R]
                          (PiTensorProduct R fun i => s i) →ₗ[R]
                            (PiTensorProduct R fun i => t i) →ₗ[R] PiTensorProduct R fun i => t' i
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_univ : ∀ {α : Type u_1} [inst : Preorder α], Set.univ.OrdConnected
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.linearEquiv_of_ne_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N},
  f ≠ 0 → ∃ S, Nonempty (N ≃ₗ[R] ↥S)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This is the `List.sum` version of `add_neg_rev`  -/
List.sum_neg_reverse : ∀ {G : Type u_7} [inst : AddGroup G] (L : List G), -L.sum = (List.map (fun x => -x) L).reverse.sum
-- Mathlib.Algebra.Lie.Prod
LieHom.fst_prod : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂), (LieHom.fst R L₁ L₂).comp (f.prod g) = f
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.functor_map : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C)
  {X Y : ↑h.smallCategoryOfSet.obj} (a : ↑(h.hom X Y)), h.functor.map a = h.homEquiv a
-- Mathlib.Topology.Sheaves.Sheafify
TopCat.Presheaf.stalkToFiber_injective : ∀ {X : TopCat} (F : TopCat.Presheaf (Type v) X) (x : ↑X),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.stalkToFiber x))
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddLeftCancelSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddLeftCancelSemigroup M] → AddLeftCancelSemigroup (l.Germ M)
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- A single element `EffectiveEpiFamily` consists of an `EffectiveEpi`
 -/
CategoryTheory.effectiveEpiStructOfEffectiveEpiFamilySingleton : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B X : C} →
      (f : X ⟶ B) → [CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => f] → CategoryTheory.EffectiveEpiStruct f
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond.eq_2 : ∀ (n : ℕ), Nat.stirlingSecond 0 n.succ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The cofork built from `coequalizer.π f g` is colimiting.  -/
CategoryTheory.Limits.coequalizerIsCoequalizer : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.coequalizer.π f g) ⋯)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H},
  MDiff[s] ↑I
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.findAux_root : ∀ {self : Batteries.UnionFind} {x : Fin self.size}, (self.findAux x).root = self.root x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- A pair of finsets of vertices is `ε`-uniform (aka `ε`-regular) iff their edge density is close
to the density of any big enough pair of subsets. Intuitively, the edges between them are
random-like.  -/
SimpleGraph.IsUniform : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [Field 𝕜] → [LinearOrder 𝕜] → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset α → Finset α → Prop
-- Mathlib.Analysis.InnerProductSpace.Basic
ext_inner_left : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, (∀ (v : E), inner 𝕜 v x = inner 𝕜 v y) → x = y
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.DelabM : Type → Type
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.collect : Lean.Expr → Lean.Meta.Grind.EMatch.InstanceMap → Array Lean.Meta.Grind.EMatchTheorem
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_baseChange : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] M) (A : Type u_6) [inst_5 : CommRing A] [inst_6 : Algebra R A],
  (LinearMap.trace A (TensorProduct R A M)) (LinearMap.baseChange A f) = (algebraMap R A) ((LinearMap.trace R M) f)
-- Mathlib.Order.Heyting.Basic
sdiff_sup_sdiff_cancel : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, b ≤ a → c ≤ b → a \ b ⊔ b \ c = a \ c
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- Given a monoidal category `C`, a localization functor `L : C ⥤ D` with respect
to `W : MorphismProperty C` which satisfies `W.IsMonoidal`, and a choice
of object `unit : D` with an isomorphism `L.obj (𝟙_ C) ≅ unit`, this is a
type synonym for `D` on which we define the localized monoidal category structure.  -/
CategoryTheory.LocalizedMonoidal : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (L : CategoryTheory.Functor C D) →
            (W : CategoryTheory.MorphismProperty C) →
              [W.IsMonoidal] →
                [L.IsLocalization W] →
                  {unit : D} → (L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) → Type u_2
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.notMem_support_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ},
  m ∉ p.support ↔ MvPolynomial.coeff m p = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.le_pi_iff : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → MulOneClass (M i)] {I : Set ι} {S : (i : ι) → Submonoid (M i)}
  {J : Submonoid ((i : ι) → M i)}, J ≤ Submonoid.pi I S ↔ ∀ i ∈ I, J ≤ Submonoid.comap (Pi.evalMonoidHom M i) (S i)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_eq_div_iff_mul_eq_mul_of_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] {x y z t : R}, y ≠ 0 → t ≠ 0 → y ∣ x → t ∣ z → (x / y = z / t ↔ t * x = y * z)
-- Mathlib.Topology.Algebra.ConstMulAction
smul_mem_nhds_smul_iff : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] {t : Set α} (g : G) {a : α}, g • t ∈ nhds (g • a) ↔ t ∈ nhds a
-- Mathlib.Topology.Constructions
Continuous.update : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i} [inst_1 : DecidableEq ι],
  Continuous f → ∀ (i : ι) {g : X → A i}, Continuous g → Continuous fun a => Function.update (f a) i (g a)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The set of vertices in a connected component of a graph.  -/
SimpleGraph.ConnectedComponent.supp : {V : Type u} → {G : SimpleGraph V} → G.ConnectedComponent → Set V
-- Mathlib.ModelTheory.DirectLimit
/-- **Alias** of `DirectedSystem.map_self'`. -/
FirstOrder.Language.DirectedSystem.map_self : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] ⦃i : ι⦄ (x : F i), (f i i ⋯) x = x
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_unitGroupMulEquiv_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A.unitGroup), ↑↑(A.unitGroupMulEquiv a) = ↑↑a
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.mk : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        {d : F.WellOrderInductionData} →
          [inst_2 : OrderBot J] →
            {val₀ : F.obj (Opposite.op ⊥)} →
              {j : J} →
                (val : F.obj (Opposite.op j)) →
                  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val = val₀ →
                    (∀ (i : J) (hi : i < j),
                        (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val =
                          d.succ i ⋯
                            ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val)) →
                      (∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
                          (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) val =
                            d.lift i hi
                              ⟨fun x =>
                                match x with
                                | Opposite.op ⟨k, hk⟩ =>
                                  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) val,
                                ⋯⟩) →
                        d.Extension val₀ j
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.DTreeMap.getKeyGT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option α
-- Init.Data.String.Iter.Basic
/-- Convenience function for turning an iterator into a list of strings, provided the output of the
iterator implements `ToString`.
 -/
Std.Iter.toStringList : {α β : Type} → [Std.Iterator α Id β] → [ToString β] → Std.Iter β → List String
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.unchanged.sizeOf_spec : sizeOf Aesop.NormSeqResult.unchanged = 1
-- Mathlib.RingTheory.Localization.Integral
/-- `S` is algebraic over `R` iff a fraction ring of `S` is algebraic over `R`  -/
IsFractionRing.isAlgebraic_iff' : ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_4)
  [inst_3 : Field K] [IsDomain R] [inst_5 : Algebra R K] [inst_6 : Algebra S K] [Module.IsTorsionFree R K]
  [IsFractionRing S K] [IsScalarTower R S K], Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limMap_eq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {G : CategoryTheory.Functor J C} (α : F ⟶ G), CategoryTheory.Limits.limMap α = CategoryTheory.Limits.lim.map α
-- Mathlib.Tactic.GRewrite.Core
/-- Update the local contexts of the metavariables to include the variables introduced by the
`gcongr` lemma. This is a bit of a hack.

Returns whether we have done a rewrite in this subgoal, in which case it has been closed.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.processGCongrHypothesis : Lean.MVarId → Bool → Mathlib.Tactic.GRewrite.Config → Mathlib.Tactic.GRewrite.GRewriteM✝ Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DTreeMap.Const.get? (Std.DTreeMap.Const.insertMany t l) k = Std.DTreeMap.Const.get? t k
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RocSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_nil : ∀ {m n : ℤ}, n ≤ m → (m<...=n).toArray = #[]
-- Lean.Syntax
Lean.Syntax.MonadTraverser.goLeft : {m : Type → Type} → [t : Lean.Syntax.MonadTraverser m] → m Unit
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.encard_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} [H.FiniteIndex],
  AddSubgroup.IsComplement (↑H) T → T.encard = ↑H.index
-- Mathlib.Data.List.Sort
List.insertionSort_cons_eq_take_drop : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (a : α) (l : List α),
  List.insertionSort r (a :: l) =
    List.takeWhile (fun b => decide ¬r a b) (List.insertionSort r l) ++
      a :: List.dropWhile (fun b => decide ¬r a b) (List.insertionSort r l)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisors.ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [Nontrivial M₀], x ∈ nonZeroDivisors M₀ → x ≠ 0
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapNatIso_functor_obj_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T T' : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapNatIso i).functor.obj X).right = X.right
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.rfind : ∀ {O : Set (ℕ →. ℕ)} {f : ℕ →. ℕ},
  Nat.RecursiveIn O f → Nat.RecursiveIn O fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a n)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.map_zero_eq_self_iff : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D]
  {x z : Topology.RelCWComplex.cell C 0},
  ↑(Topology.RelCWComplex.map 0 x) ![] = ↑(Topology.RelCWComplex.map 0 z) ![] ↔ x = z
-- Init.System.ST
EST.bind : {ε σ α β : Type} → EST ε σ α → (α → EST ε σ β) → EST ε σ β
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h : α) (l : List α) (h_1 : (h : α) → (l : List α) → motive (h :: l))
  (h_2 : Unit → motive []),
  (match h :: l with
    | h :: l => h_1 h l
    | [] => h_2 ()) =
    h_1 h l
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsRightAdjointTopCatToGeneratedByTopCat : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)], TopCat.toGeneratedByTopCat.IsRightAdjoint
-- Mathlib.Analysis.Calculus.FDeriv.Comp
HasFDerivWithinAt.comp_hasFDerivAt_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {f' : E →L[𝕜] F} (x : E) {g : F → G}
  {g' : F →L[𝕜] G} {t : Set F} {y : F},
  HasFDerivWithinAt g g' t y →
    HasFDerivAt f f' x → (∀ᶠ (x' : E) in nhds x, f x' ∈ t) → y = f x → HasFDerivAt (g ∘ f) (g' ∘SL f') x
-- Lean.Widget.UserWidget
Lean.Widget.ToModule : Type u → Type u
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingEquiv_single`. -/
MonoidAlgebra.mapRangeRingEquiv_single : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Monoid M]
  (e : R ≃+* S) (r : R) (m : M),
  (MonoidAlgebra.mapRingEquiv M e) (MonoidAlgebra.single m r) = MonoidAlgebra.single m (e r)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.id_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.AddMon C), M.id.hom = CategoryTheory.CategoryStruct.id M.X
-- Init.Data.ByteArray.Basic
ByteArray.forInUnsafe.loop : {β : Type v} → {m : Type v → Type w} → [Monad m] → ByteArray → (UInt8 → β → m (ForInStep β)) → USize → USize → β → m β
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.mul_coe_eq_smul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (r : R) (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], a * ↑r = r • a
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_mul_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R} (z : R), x ≤ᵥ y → x * z ≤ᵥ y * z
-- Mathlib.Order.UpperLower.Prod
LowerSet.mem_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {x : α × β} {s : LowerSet α} {t : LowerSet β},
  x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], (t₁ ∪ t₂)[k]! = t₂.getD k t₁[k]!
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.center_toSubsemigroup : ∀ (M : Type u_1) [inst : MulOneClass M], (Submonoid.center M).toSubsemigroup = Subsemigroup.center M
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveView : Inhabited Lean.Elab.Command.InductiveView
-- Mathlib.Order.Minimal
OrderIso.map_minimal_mem : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o ↑t)
  (hx : Minimal (fun x => x ∈ s) x), Minimal (fun x => x ∈ t) ↑(f ⟨x, ⋯⟩)
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOneClass N], instInhabitedMonoidHom = { default := 1 }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.addRightMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddRightStrictMono N], AddRightMono (Lex (α →₀ N))
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.isUnit_or_isUnit_of_isUnit_add : ∀ {R : Type u_1} [inst : Semiring R] [IsLocalRing R] {a b : R}, IsUnit (a + b) → IsUnit a ∨ IsUnit b
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.pure_bind : ∀ {α β : Type u} (f : α → FreeAddGroup β) (x : α), pure x >>= f = f x
-- Mathlib.Topology.Compactness.SigmaCompact
instSigmaCompactSpaceSigmaOfCountable : ∀ {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
  [∀ (i : ι), SigmaCompactSpace (X i)], SigmaCompactSpace ((i : ι) × X i)
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.List.of_findIdx?_eq_some.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Algebra.Lie.EngelSubalgebra
/-- Engel subalgebras are self-normalizing.
See `LieSubalgebra.normalizer_eq_self_of_engel_le` for a proof that Lie-subalgebras
containing an Engel subalgebra are also self-normalizing,
provided that the ambient Lie algebra is Artinian.  -/
LieSubalgebra.normalizer_engel : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x : L),
  (LieSubalgebra.engel R x).normalizer = LieSubalgebra.engel R x
-- Mathlib.Tactic.ProdAssoc
/-- A helper type to keep track of universe levels and types in iterated products.  -/
Lean.Expr.ProdTree : Type
-- Mathlib.Tactic.CongrExclamation
/-- Try to apply `pi_congr`. This is similar to `Lean.MVar.congrImplies?`.
 -/
Lean.MVarId.congrPi? : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.compUliftCoyonedaCompWhiskeringLeft_inv_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : Cᵒᵖ) (X_1 : C)
  (x : (CategoryTheory.uliftCoyoneda.{v₂, v₁, u₁}.obj (Opposite.op (Opposite.unop X))).obj X_1),
  ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftCoyonedaCompWhiskeringLeft.inv.app X).app X_1)) x).down =
    F.map x.down
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixedPoints_addSubmonoid_iSup : ∀ (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst_1 : AddAction M α] {ι : Sort u_3} {P : ι → AddSubmonoid M},
  AddAction.fixedPoints (↥(iSup P)) α = ⋂ i, AddAction.fixedPoints (↥(P i)) α
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Int.Internal.Linear.Poly.gcdAll : Int.Internal.Linear.Poly → ℕ
-- Mathlib.Algebra.Category.Ring.Instances
isLocalHom_of_isIso : ∀ {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f], IsLocalHom (CommRingCat.Hom.hom f)
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_one_norm' : ∀ {E : Type u_2} [inst : SeminormedGroup E], LipschitzWith 1 norm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne : ∀ {n m : ℕ},
  n ≠ m →
    ∫ (x : ℝ),
        Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) *
          Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m) ∂Polynomial.Chebyshev.measureT =
      0
-- Init.Sym.Lemmas
Lean.Sym.String.eq_eq_false : ∀ (a b : String), decide (a = b) = false → (a = b) = False
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_top : ∀ {α : Type u_1} [inst : Zero α], ⊤.untop₀ = 0
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_zero_right : ∀ (b : Ordinal.{u_1}), Ordinal.log b 0 = 0
-- Mathlib.Data.Real.Basic
Real.mk_inf : ∀ (a b : CauSeq ℚ abs), Real.mk (a ⊓ b) = min (Real.mk a) (Real.mk b)