mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WithBot
/-- The order on `WithTop α`, defined by `x ≤ ⊤` and `a ≤ b → ↑a ≤ ↑b`.

Equivalently, `x ≤ y` can be defined as `∀ b : α, y = ↑b → ∃ a : α, x = ↑a ∧ a ≤ b`,
see `le_iff_forall`. The definition as an inductive predicate is preferred since it
cannot be accidentally unfolded too far.  -/
WithTop.instLE : {α : Type u_1} → [LE α] → LE (WithTop α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon_k_eq_mulMon : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon_k k m p = Lean.Grind.CommRing.Poly.mulMon k m p
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toAddMonoidHom_coe : ∀ {R : Type u_1} {S : Type u_5} {M₁ : Type u_9} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {modM₁ : Module R M₁} {modM₂ : Module S M₂} {σ : R →+* S}
  (f : M₁ →ₛₗ[σ] M₂), ⇑f.toAddMonoidHom = ⇑f
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RoiSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Roi α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Roi α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Topology.MetricSpace.Bilipschitz
/-- If `f : α → β` is bilipschitz, then the pullback of the bornology on `β` through `f` agrees
with the bornology on `α`.

This can be used to provide the replacement equality when applying
`PseudoMetricSpace.replaceBornology`, which can be useful when following the forgetful inheritance
pattern when creating type synonyms.

Important Note: if `α` is some synonym of a type `β` (at default transparency), and `f : α ≃ β` is
some bilipschitz equivalence, then instead of writing:
```
instance : Bornology α := inferInstanceAs (Bornology β)
```
Users should instead write something like:
```
instance : Bornology α := Bornology.induced (f : α → β)
```
in order to avoid abuse of the definitional equality `α := β`.  -/
isBounded_iff_of_bilipschitz : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K₁ K₂ : NNReal}
  {f : α → β},
  AntilipschitzWith K₁ f → LipschitzWith K₂ f → ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
-- Mathlib.LinearAlgebra.Dimension.LinearMap
/-- The rank of the composition of two maps is less than the minimum of their ranks.  -/
LinearMap.lift_rank_comp_le : ∀ {K : Type u} {V : Type v} {V' : Type v'} {V'' : Type v''} [inst : Semiring K] [inst_1 : AddCommMonoid V]
  [inst_2 : Module K V] [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [inst_5 : AddCommMonoid V'']
  [inst_6 : Module K V''] (g : V →ₗ[K] V') (f : V' →ₗ[K] V''),
  Cardinal.lift.{v', v''} (f ∘ₗ g).rank ≤ min (Cardinal.lift.{v', v''} f.rank) (Cardinal.lift.{v'', v'} g.rank)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Order.DirectedInverseSystem
_private.Mathlib.Order.DirectedInverseSystem.0.DirectLimit.lift₂Aux : {ι : Type u_1} →
  [inst : Preorder ι] →
    {F₁ : ι → Type u_2} →
      {F₂ : ι → Type u_3} →
        {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} →
          (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)] →
                {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} →
                  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) →
                    [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] →
                      [DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] →
                        [IsDirectedOrder ι] →
                          {C : Sort u_9} →
                            (ih : (i : ι) → F₁ i → F₂ i → C) →
                              (∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i),
                                  ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) →
                                (z : (i : ι) × F₁ i) →
                                  (w : (i : ι) × F₂ i) →
                                    { x //
                                      ∀ (i : ι) (hzi : z.fst ≤ i) (hwi : w.fst ≤ i),
                                        x = ih i ((f₁ z.fst i hzi) z.snd) ((f₂ w.fst i hwi) w.snd) }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp k (t.maxKey ⋯)).isLE = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ Std.DHashMap.Const.alter m k f ↔ (f (Std.DHashMap.Const.get? m k)).isSome = true
-- Mathlib.Order.ULift
ULift.instLE_mathlib : {α : Type u} → [LE α] → LE (ULift.{v, u} α)
-- Init.Data.List.Lemmas
List.map_eq_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l = [] ↔ l = []
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.MLListImpl.brecOn_1.go : {m : Type u → Type u} →
  {α : Type u} →
    {motive_1 : MLList.MLListImpl✝ m α → Sort u_1} →
      {motive_2 : Thunk (MLList.MLListImpl✝ m α) → Sort u_1} →
        (t : Thunk (MLList.MLListImpl✝ m α)) →
          ((t : MLList.MLListImpl✝ m α) → MLList.MLListImpl.below✝ t → motive_1 t) →
            ((t : Thunk (MLList.MLListImpl✝ m α)) → MLList.MLListImpl.below_1✝ t → motive_2 t) →
              motive_2 t ×' MLList.MLListImpl.below_1✝ t
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Reindexing both indices along equivalences preserves the absolute of the determinant.

For the `simp` version of this lemma, see `abs_det_submatrix_equiv_equiv`;
this one is unsuitable because `Matrix.reindex_apply` unfolds `reindex` first.
 -/
Matrix.abs_det_reindex : ∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type u_3} [inst_4 : CommRing R] [inst_5 : LinearOrder R] [IsStrictOrderedRing R]
  (e₁ e₂ : m ≃ n) (A : Matrix m m R), |((Matrix.reindex e₁ e₂) A).det| = |A.det|
-- Lean.Elab.PreDefinition.Structural.FindRecArg
_private.Lean.Elab.PreDefinition.Structural.FindRecArg.0.Lean.Elab.Structural.getIndexMinPos : Array Lean.Expr → Array Lean.Expr → ℕ
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The range of a morphism of simplicial sets, as a subcomplex.  -/
SSet.Subcomplex.range : {X Y : SSet} → (X ⟶ Y) → Y.Subcomplex
-- Init.Data.UInt.Bitwise
UInt32.xor_self : ∀ {a : UInt32}, a ^^^ a = 0
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.mk.injEq : ∀ (ctxInfo : Lean.Elab.ContextInfo) (tacticInfo : Lean.Elab.TacticInfo) (useAfter indented : Bool) (priority : ℕ)
  (ctxInfo_1 : Lean.Elab.ContextInfo) (tacticInfo_1 : Lean.Elab.TacticInfo) (useAfter_1 indented_1 : Bool)
  (priority_1 : ℕ),
  ({ ctxInfo := ctxInfo, tacticInfo := tacticInfo, useAfter := useAfter, indented := indented, priority := priority } =
      { ctxInfo := ctxInfo_1, tacticInfo := tacticInfo_1, useAfter := useAfter_1, indented := indented_1,
        priority := priority_1 }) =
    (ctxInfo = ctxInfo_1 ∧
      tacticInfo = tacticInfo_1 ∧ useAfter = useAfter_1 ∧ indented = indented_1 ∧ priority = priority_1)
-- Mathlib.Algebra.Group.Submonoid.Units
/-- The equivalence between the greatest subgroup of units contained within `T` and `T` itself.  -/
Subgroup.unitsEquivSelf : {G : Type u_2} → [inst : Group G] → (H : Subgroup G) → ↥H.units ≃* ↥H
-- Mathlib.Algebra.Lie.Engel
LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_top : ∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [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]
  {I : LieIdeal R L} {x : L},
  R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤ →
    ∀ {n i j : ℕ},
      (LieModule.toEnd R L M) x ^ n = 0 →
        LieModule.lowerCentralSeries R L M i ≤ I.lcs M j → LieModule.lowerCentralSeries R L M (i + n) ≤ I.lcs M (j + 1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
cfcHom_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] [inst_7 : NormedSpace ℝ A] (a : A)
  (f : X → C(↑(spectrum 𝕜 a), 𝕜)),
  MeasureTheory.Integrable f μ →
    ∀ (ha : autoParam (p a) cfcHom_integral._auto_1), ∫ (x : X), (cfcHom ha) (f x) ∂μ = (cfcHom ha) (∫ (x : X), f x ∂μ)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.any_map : ∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'} {p : β' → Bool},
  Std.Iter.any p (Std.Iter.map f it) = Std.Iter.any (fun x => p (f x)) it
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **third isomorphism theorem** for algebras. See `quotQuotEquivQuotSupₐ` for version
that does not assume an inclusion of ideals.  -/
DoubleQuot.quotQuotEquivQuotOfLEₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] → {I J : Ideal A} → I ≤ J → ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] A ⧸ J
-- Mathlib.Analysis.Convex.EGauge
mem_of_egauge_lt_one : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {x : E}, Balanced 𝕜 s → egauge 𝕜 s x < 1 → x ∈ s
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.hasExactLimitsOfShape_discrete_finite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [inst_3 : Finite J],
  CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete J) C
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Path.notMem_edges_of_loop : ∀ {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v}, e ∉ (↑p).edges
-- Mathlib.Analysis.Analytic.ChangeOrigin
HasFPowerSeriesWithinOnBall.analyticOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → AnalyticOn 𝕜 f (insert x s ∩ Metric.eball x r)
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The two words of length `M i i'` that alternate between `i` and `i'` have the same product.
This is known as the "braid relation" or "Artin-Tits relation".  -/
CoxeterSystem.wordProd_braidWord_eq : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B),
  cs.wordProd (CoxeterSystem.braidWord M i i') = cs.wordProd (CoxeterSystem.braidWord M i' i)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `some t` if `t` is the solver term for `ext` associated with `e`.
 -/
Lean.Meta.Grind.SolverExtension.getTerm : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.ENode → Option Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_def : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹ = Ring.inverse A.det • A.adjugate
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The full configuration in the full shift `A^G`.  -/
SymbolicDynamics.FullShift.Pattern.config : {A : Type u_1} → {G : Type u_2} → [inst : Inhabited A] → SymbolicDynamics.FullShift.Pattern A G → G → A
-- Mathlib.Geometry.Manifold.Instances.Real
instZeroEuclideanHalfSpace : {n : ℕ} → [inst : NeZero n] → Zero (EuclideanHalfSpace n)
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.lift` preserves the identity functor.  -/
CategoryTheory.MonoOver.liftId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      CategoryTheory.MonoOver.lift (CategoryTheory.Functor.id (CategoryTheory.Over X)) ⋯ ≅
        CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.inv_image : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (U : Y.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor e.inv).obj U = (TopologicalSpace.Opens.map e.hom.base).obj U
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasStrictDerivAt.const_smul` -/
HasStrictDerivAt.fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun i => c • f i) (c • f') x
-- Mathlib.Data.Finset.Sort
Finset.image_orderEmbOfFin_univ : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k),
  Finset.image (⇑(s.orderEmbOfFin h)) Finset.univ = s
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.Tendsto.eventually_ne_atTop' : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α},
  Filter.Tendsto f l Filter.atTop → ∀ (c : α), ∀ᶠ (x : α) in l, x ≠ c
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instDistribMulActionSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          {X : Type u_4} →
            [inst_3 : AddMonoid X] → [DistribMulAction L X] → (F : IntermediateField K L) → DistribMulAction (↥F) X
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_eq_zero_or_add_one_sub_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  Int.fract a = 0 ∨ Int.fract a = a + 1 - ↑⌈a⌉
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.pure_bind : ∀ {α β : Type u} (f : α → FreeGroup β) (x : α), pure x >>= f = f x
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.odd_card_of_char_ne_two : ∀ {F : Type u_3} [inst : Field F] [inst_1 : Fintype F], ringChar F ≠ 2 → Fintype.card F % 2 = 1
-- Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
/-- The natural homeomorphism between nonzero elements of a normed space `E`
and `Metric.sphere (0 : E) 1 × Set.Ioi (0 : ℝ)`.

The forward map sends `⟨x, hx⟩` to `⟨‖x‖⁻¹ • x, ‖x‖⟩`,
the inverse map sends `(x, r)` to `r • x`.

One may think about it as generalization of polar coordinates to any normed space.
See also `homeomorphSphereProd` for a version that works for a sphere of any positive radius.  -/
homeomorphUnitSphereProd : (E : Type u_1) → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → ↑{0}ᶜ ≃ₜ ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] (n : ℕ),
  AddSubgroup.upperCentralSeries G n = (AddSubgroup.upperCentralSeriesAux G n).fst
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.brecOn.go : {motive : Mathlib.Tactic.Conv.Path → Sort u} →
  (t : Mathlib.Tactic.Conv.Path) →
    ((t : Mathlib.Tactic.Conv.Path) → Mathlib.Tactic.Conv.Path.below t → motive t) →
      motive t ×' Mathlib.Tactic.Conv.Path.below t
-- Init.System.ST
ST.Prim.Ref.modifyGet : {σ α β : Type} → ST.Ref σ α → (α → β × α) → ST σ β
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.ext_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {h₁ h₂ : α ≃ᵢ β},
  h₁ = h₂ ↔ ∀ (x : α), h₁ x = h₂ x
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.smulAux'_im : ∀ (g : GL (Fin 2) ℝ) (z : ℂ),
  (UpperHalfPlane.smulAux' g z).im =
    |↑(Matrix.GeneralLinearGroup.det g)| * z.im / Complex.normSq (UpperHalfPlane.denom g z)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.utf8GetAux?.eq_1 : ∀ (x x_1 : String.Pos.Raw), String.Pos.Raw.utf8GetAux? [] x x_1 = none
-- Lean.Meta.Canonicalizer
Lean.Meta.Canonicalizer.instHashableExprVisited : Hashable Lean.Meta.Canonicalizer.ExprVisited
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.dist_gm_am_le : ∀ {x y : NNReal}, dist (NNReal.sqrt (x * y)) ((x + y) / 2) ≤ dist x y / 2
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.functor_obj : ∀ {I : Type u} [inst : CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat}
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (i : I),
  (Profinite.Extend.functor c).obj i = CategoryTheory.StructuredArrow.mk (c.π.app i)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Adding top to the type of finite classes yields the type of all classes.  -/
FiniteMulArchimedeanClass.withTopOrderIso : (M : Type u_1) →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] → WithTop (FiniteMulArchimedeanClass M) ≃o MulArchimedeanClass M
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonRpcKeepAliveParams : Lean.ToJson Lean.Lsp.RpcKeepAliveParams
-- Mathlib.GroupTheory.OrderOfElement
nsmul_finEquivZMultiples_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} (hx : IsOfFinAddOrder x) (a : ↥(AddSubgroup.zmultiples x)),
  ↑((finEquivZMultiples hx).symm a) • x = ↑a
-- Mathlib.Data.Sym.Basic
/-- A function `α → β` induces a function `Sym α n → Sym β n` by applying it to every element of
the underlying `n`-tuple.  -/
Sym.map : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → β) → Sym α n → Sym β n
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass (Lex M) N α
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Does the set (approximately) contain the element `x`? That is,
is there an element that is equivalent to `x` in the order?

```
1 ∈ {1, 2, 3} = true
4 ∈ {1, 2, 3} = false
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
(1, 1) ∈ {(0, 1), (1, 2)} = true
(3, 1) ∈ {(0, 1), (1, 2)} = false
```  -/
Ordnode.mem : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Bool
-- Init.Data.Array.Lemmas
Array.not_mem_empty : ∀ {α : Type u_1} (a : α), a ∉ #[]
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_add_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f m₁ s₁ + IsLocalizedModule.mk' f m₂ s₂ = IsLocalizedModule.mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_1eq_certC : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange_mono : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {p q : Submodule R M},
  p ≤ q → Submodule.baseChange A p ≤ Submodule.baseChange A q
-- Lean.Compiler.IR.Basic
Lean.IR.instAlphaEqvVarId : Lean.IR.AlphaEqv Lean.IR.VarId
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_symm : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x y : X ⊕ Y}, f ∈ GromovHausdorff.candidates X Y → f (x, y) = f (y, x)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.hom_ext_iff : ∀ {α : Type u} {R : Type v} [inst : CommRing R] {f g : FreeCommRing α →+* R},
  f = g ↔ ∀ (x : α), f (FreeCommRing.of x) = g (FreeCommRing.of x)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {α₁ : Type u_6} {g : α₁ → α} {x : FreeMonoid α₁},
  (FreeMonoid.map f) ((FreeMonoid.map g) x) = (FreeMonoid.map (f ∘ g)) x
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_rename_app : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (p : MvPowerSeries σ R),
  (MvPowerSeries.killCompl e) ((MvPowerSeries.rename ⇑e) p) = p
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  x ∈ NumberField.mixedEmbedding.fundamentalCone K →
    ∀ (u : (NumberField.RingOfIntegers K)ˣ),
      u • x ∈ NumberField.mixedEmbedding.fundamentalCone K ↔ u ∈ NumberField.Units.torsion K
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_eq_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ},
  0 ≤ a → (⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_coe : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous SetLike.coe
-- Mathlib.Computability.Encoding
/-- A decoding function from `List Bool` to the positive binary numbers.  -/
Computability.decodePosNum : List Bool → PosNum
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.forget_faithful : ∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S],
  (CategoryTheory.DifferentialObject.forget S C).Faithful
-- Mathlib.AlgebraicTopology.DoldKan.Equivalence
CategoryTheory.Abelian.DoldKan.equivalence_inverse : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A],
  CategoryTheory.Abelian.DoldKan.equivalence.inverse = CategoryTheory.Abelian.DoldKan.Γ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_mapRange_index : ∀ {α : Type u_1} {M : Type u_8} {M' : Type u_9} {N : Type u_10} [inst : Zero M] [inst_1 : Zero M']
  [inst_2 : CommMonoid N] {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N},
  (∀ (a : α), h a 0 = 1) → (Finsupp.mapRange f hf g).prod h = g.prod fun a b => h a (f b)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_surjective : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  Function.Surjective ⇑(DirectSum.lmap f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOnFilter.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {l' : Filter β} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformlyOnFilter f g l l' →
    TendstoUniformlyOnFilter f' g' l l' → TendstoUniformlyOnFilter (f - f') (g - g') l l'
-- Mathlib.Data.Fin.Fin2
Fin2.last.eq_2 : ∀ (k : ℕ), Fin2.last = Fin2.last.fs
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.containsKey_inner_toList : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {c : Std.DTreeMap.Internal.Cell α β (compare k)},
  c.contains = true → Std.Internal.List.containsKey k c.inner.toList = true