mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ClusterPt
ClusterPt.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (F : Filter X), ClusterPt x F = (nhds x ⊓ F).NeBot
-- Mathlib.Data.Multiset.Fintype
Multiset.image_toEnumFinset_fst : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Finset.image Prod.fst m.toEnumFinset = m.toFinset
-- Mathlib.Algebra.Order.IsBotOne
/-- A typeclass expressing that the `1` of a type is a bottom element. In a partial `OrderBot`, this
is equivalent to `⊥ = 1`.  -/
IsBotOneClass : (α : Type u_1) → [LE α] → [One α] → Prop
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_of_not_continuousOn : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R] {s : Set X}
  [inst_3 : Zero ↑s] {f : X → R} {g : ContinuousMapZero (↑s) R},
  ¬ContinuousOn f s → ContinuousMapZero.mkD (s.domRestrict f) g = g
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCocone` commutes with `precomposeEquivalence`  -/
CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F G : CategoryTheory.Functor J C} →
                {α : F ≅ G} →
                  {c : CategoryTheory.Limits.Cocone F} →
                    H.mapCocone ((CategoryTheory.Limits.Cocone.precomposeEquivalence α).functor.obj c) ≅
                      (CategoryTheory.Limits.Cocone.precomposeEquivalence
                              (CategoryTheory.Functor.isoWhiskerRight α H)).functor.obj
                        (H.mapCocone c)
-- Mathlib.Data.Set.Pairwise.Basic
/-- See also `Function.injective_iff_pairwise_ne`  -/
Set.injOn_iff_pairwise_ne : ∀ {α : Type u_1} {ι : Type u_4} {f : ι → α} {s : Set ι}, Set.InjOn f s ↔ s.Pairwise fun x1 x2 => f x1 ≠ f x2
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.val_add : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (f g : AdicCompletion I M), ↑(f + g) = ↑f + ↑g
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The multiplicative map forgetting that a bounded continuous function is bounded.  -/
BoundedContinuousFunction.toContinuousMapMonoidHom : (α : Type u) →
  (R : Type u_2) →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Monoid R] →
          [inst_3 : BoundedMul R] → [inst_4 : ContinuousMul R] → BoundedContinuousFunction α R →* C(α, R)
-- Init.Data.String.Termination
String.Pos.next_induction : ∀ {s : String} {C : s.Pos → Prop} (p : s.Pos), (∀ (x : s.Pos) (h : x ≠ s.endPos), C (x.next h) → C x) → C s.endPos → C p
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.getHandlers : Lean.Environment → Lean.NameMap Lean.Linter.MissingDocs.Handler
-- Std.Http.Data.Status
Std.Http.instBEqCustomStatus : BEq Std.Http.CustomStatus
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_le : ∀ {α : Type u_1} {s : Set (Set α)} {m : MeasurableSpace α},
  (∀ t ∈ s, MeasurableSet t) → MeasurableSpace.generateFrom s ≤ m
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.deg_lt_aleph0 : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  Cardinal.mk
      (Field.Emb
        ↥(IntermediateField.adjoin F
            (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i))
        ↥(↥(IntermediateField.adjoin F
                (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E ''
                  Set.Iio i)))⟮(Field.Emb.Cardinal.wellOrderedBasis F E) (Field.Emb.Cardinal.leastExt F E i)⟯) <
    Cardinal.aleph0
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_rat_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (x + ↑r) ↔ LiouvilleWith p x
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
/-- If `S` is `R`-smooth, there exists a cover by basic opens `D(sᵢ)` such that
`S[1/sᵢ]` is `R`-standard-smooth.  -/
Algebra.Smooth.exists_span_eq_top_isStandardSmooth : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Algebra.Smooth R S],
  ∃ s, Ideal.span s = ⊤ ∧ ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Creates a new variable in the cutsat module.  -/
Lean.Meta.Grind.Arith.Cutsat.mkVar : Lean.Expr → Lean.Meta.Grind.GoalM Int.Internal.Linear.Var
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.hasMultiplicativeReduction_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  WeierstrassCurve.HasMultiplicativeReduction R W ↔
    WeierstrassCurve.IsMinimal R W ∧
      (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1 ∧
        (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ = 1
-- Init.Data.Nat.ToString
Nat.repr_eq_repr_append_repr : ∀ {n : ℕ}, 10 ≤ n → n.repr = (n / 10).repr ++ (n % 10).repr
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerBifunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] (α : Type tᵒᵖ),
  CategoryTheory.Limits.FormalCoproduct.powerBifunctor.obj α =
    CategoryTheory.Limits.FormalCoproduct.powerFunctor (Opposite.unop α)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to
zero, the probability measures giving mass at most `uₙ` to the complement of `Kₙ` form a
compact set.  -/
isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E},
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Lean.Meta.Inductive
/-- Return true if the types of the given constructors are compatible.  -/
Lean.Meta.compatibleCtors : Lean.Name → Lean.Name → Lean.MetaM Bool
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.toSpanSingleton_surjective : ∀ (R : Type u_2) [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M]
  {m : M}, m ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M m)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) (T : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).obj T =
    CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₁)
      (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₂)
      (n.negOnePow •
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map T.mor₃)
          ((CategoryTheory.shiftFunctorComm C 1 n).hom.app T.obj₁))
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.not_isIrreducible_of_subsingleton : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Subsingleton M],
  ¬P.IsIrreducible
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] (f : E →L[𝕜] E) {c : NNReal}, 0 < c → (∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖inner 𝕜 (f x) x‖) → IsUnit f
-- Mathlib.Analysis.Complex.Tietze
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If `e : C(X, Y)` is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ` of the same norm such that `g ∘ e = f`.  -/
BoundedContinuousFunction.exists_norm_eq_domRestrict_eq : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s : Set X},
  IsClosed s →
    ∀ (𝕜 : Type v) [inst_2 : RCLike 𝕜] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
      [FiniteDimensional 𝕜 E] (f : BoundedContinuousFunction (↑s) E), ∃ g, ‖g‖ = ‖f‖ ∧ g.domRestrict s = f
-- Init.Data.String.PosRaw
String.Pos.Raw.add_char_right_comm : ∀ (p : String.Pos.Raw) (c₁ c₂ : Char), p + c₁ + c₂ = p + c₂ + c₁
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.Core.withCurrHeartbeatsImp : {α : Type} → Lean.CoreM α → Lean.CoreM α
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
_private.Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers.0.CategoryTheory.Limits.parallelFamily.match_1.eq_2 : ∀ {J : Type u_1} (motive : (x y : CategoryTheory.Limits.WalkingParallelFamily J) → (x ⟶ y) → Sort u_2) (j : J)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingParallelFamily J) →
      motive x x (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x))
  (h_2 :
    (j : J) →
      motive CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one
        (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)),
  (match CategoryTheory.Limits.WalkingParallelFamily.zero, CategoryTheory.Limits.WalkingParallelFamily.one,
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j with
    | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one),
      CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => h_2 j) =
    h_2 j
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOptionValue.default : Lean.LeanOptionValue
-- Qq.Macro
Qq.Impl.whnfR : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Convex.Jensen
StrictConcaveOn.lt_map_sum_iff_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i) ↔ ∃ j ∈ t, ∃ k ∈ t, w j ≠ 0 ∧ w k ≠ 0 ∧ p j ≠ p k)
-- Mathlib.Data.Finsupp.Fin
/-- `cons` for maps `Fin n →₀ M`. See `Fin.cons` for more details.  -/
Finsupp.cons : {n : ℕ} → {M : Type u_1} → [inst : Zero M] → M → (Fin n →₀ M) → Fin (n + 1) →₀ M
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- The bijection `Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE` when
`e₁` and `e₂` are complementary embeddings of complex shapes.  -/
ComplexShape.Embedding.AreComplementary.Boundary.equiv : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} →
              {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → Subtype e₁.BoundaryLE ≃ Subtype e₂.BoundaryGE
-- Mathlib.Analysis.Normed.Lp.Matrix
Matrix.ofLp_toLpLin : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (p q : ENNReal) (A : Matrix m n R) (x : WithLp p (n → R)),
  (((Matrix.toLpLin p q) A) x).ofLp = (Matrix.toLin' A) x.ofLp
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceRev : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zero : ∀ {M₀ : Type u_7} [inst : CommMonoidWithZero M₀] [Nontrivial M₀], IsPrimitiveRoot 0 0
-- Mathlib.Logic.Function.Conjugate
/-- If `f` commutes with `g`, then `Option.map f` commutes with `Option.map g`.  -/
Function.Commute.option_map : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute (Option.map f) (Option.map g)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instPartialOrder.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupSeminorm.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪a ⊗ₜ (b ⊗ₜ c), x⟫ = ⟪a ⊗ₜ (b ⊗ₜ c), y⟫` for all
`a, b, c`.

See also `ext_iff_inner_left_threefold` for when `x, y : E ⊗ F ⊗ G`.  -/
TensorProduct.ext_iff_inner_left_threefold' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] {x y : TensorProduct 𝕜 E (TensorProduct 𝕜 F G)},
  x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) x = inner 𝕜 (a ⊗ₜ[𝕜] (b ⊗ₜ[𝕜] c)) y
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.closed_range_of_antilipschitz : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {σ : 𝕜 →+* 𝕜'} {σ' : 𝕜' →+* 𝕜}
  [inst_4 : RingHomInvPair σ σ'] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜' F]
  [CompleteSpace E] {f : E →SL[σ] F} {c : NNReal}, AntilipschitzWith c ⇑f → (↑f).range.topologicalClosure = (↑f).range
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.normalizer_bot_eq_maxTrivSubmodule : ∀ (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],
  ⊥.normalizer = LieModule.maxTrivSubmodule R L M
-- Mathlib.Order.Lattice
inf_congr_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b ⊓ c ≤ a → a ⊓ c ≤ b → a ⊓ c = b ⊓ c
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variable to equation constraint used to eliminate it. `solved` variables should not occur in
`diseqs`, `lowers`, or `uppers`.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.elimEqs : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray (Option Lean.Meta.Grind.Arith.Linear.EqCnstr)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.mk.inj : ∀ {J : Type u} {inst : LinearOrder J} {inst_1 : SuccOrder J} {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {succ : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))}
  {map_succ :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ j hj x) = x}
  {lift : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)}
  {map_lift :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift j hj x) =
        ↑x (Opposite.op ⟨i, hi⟩)}
  {succ_1 : (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))}
  {map_succ_1 :
    ∀ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (succ_1 j hj x) = x}
  {lift_1 : (j : J) → Order.IsSuccLimit j → ↑(⋯.functor.op.comp F).sections → F.obj (Opposite.op j)}
  {map_lift_1 :
    ∀ (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j),
      (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (lift_1 j hj x) =
        ↑x (Opposite.op ⟨i, hi⟩)},
  { succ := succ, map_succ := map_succ, lift := lift, map_lift := map_lift } =
      { succ := succ_1, map_succ := map_succ_1, lift := lift_1, map_lift := map_lift_1 } →
    succ = succ_1 ∧ lift = lift_1
-- Mathlib.Algebra.Order.SuccPred
Order.succ_eq_add_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : One α] [inst_3 : SuccAddOrder α] (x : α),
  Order.succ x = x + 1
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.prodMk : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f₁ : α → β} {f₂ : α → γ}, UniformContinuous f₁ → UniformContinuous f₂ → UniformContinuous fun a => (f₁ a, f₂ a)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.mul_toMatrix' : ∀ {n : Type u_11} {m : Type u_12} {n' : Type u_13} {R : Type u_16} [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype n'] [inst_6 : DecidableEq n']
  (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R),
  M * (LinearMap.toMatrix₂' R) B = (LinearMap.toMatrix₂' R) (B ∘ₗ Matrix.toLin' M.transpose)
-- Mathlib.CategoryTheory.Skeletal
/-- From a functor `C ⥤ D`, construct a map of skeletons `Skeleton C → Skeleton D`.  -/
CategoryTheory.Functor.mapSkeleton : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → CategoryTheory.Functor (CategoryTheory.Skeleton C) (CategoryTheory.Skeleton D)
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.linearEquiv_of_le_sSup : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsSimpleModule R ↥N] (s : Set (Submodule R M)) [simple : ∀ (m : ↑s), IsSimpleModule R ↥↑m],
  N ≤ sSup s → ∃ S ∈ s, Nonempty (↥N ≃ₗ[R] ↥S)
-- Mathlib.Order.Filter.ENNReal
ENNReal.liminf_mul_const_of_ne_top : ∀ {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ → Filter.liminf (fun x => u x * a) f = a * Filter.liminf u f
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- The map from `Matrix n n R` to bilinear forms on `n → R`.

This is an auxiliary definition for the equivalence `Matrix.toBilin'`.  -/
Matrix.toBilin'Aux : {R₁ : Type u_1} →
  [inst : CommSemiring R₁] → {n : Type u_5} → [Fintype n] → Matrix n n R₁ → LinearMap.BilinForm R₁ (n → R₁)
-- Mathlib.GroupTheory.Index
AddSubgroup.FiniteIndex.mk : ∀ {G : Type u_3} [inst : AddGroup G] {H : AddSubgroup G}, H.index ≠ 0 → H.FiniteIndex
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_iff_ne_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isSome = true ↔ t ≠ ∅
-- Init.Grind.AC
/-- `superpose_ac_idempotent` for the non-commutative case. It is similar to `superpose_head_idempotent` but for the "tail"-case
 -/
Lean.Grind.AC.superpose_tail_idempotent : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.IdempotentOp ctx.op}
  (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_tail_idempotent_cert x lhs₁ rhs₁ rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs
-- Mathlib.Algebra.Lie.Basic
/-- The inverse function of an equivalence of Lie modules  -/
LieModuleEquiv.invFun : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → (M ≃ₗ⁅R,L⁆ N) → N → M
-- Lean.Util.SCC
Lean.SCC.State.stack : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SCC.State α → List α
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_finite_of_isCompact_invariant : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} [inst : UniformSpace X],
  IsCompact F → Set.MapsTo T F F → U ∈ uniformity X → Dynamics.coverEntropyEntourage T F U < ⊤
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.TSyntax.getHexNumSize.go : String → String.Pos.Raw → ℕ → ℕ
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation.polynomial`. -/
FunctionField.inftyValuation.polynomial : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {p : Polynomial F},
  p ≠ 0 → RatFunc.inftyValuationDef F ((algebraMap (Polynomial F) (RatFunc F)) p) = WithZero.exp ↑p.natDegree
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Asymptotics.IsBigO.hasFDerivAt : ∀ {𝕜 : 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] {f : E → F}
  {x₀ : E} {n : ℕ}, (f =O[nhds x₀] fun x => ‖x - x₀‖ ^ n) → 1 < n → HasFDerivAt f 0 x₀
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.instIsInnerPairingSuccCastSucc : ∀ {m : ℕ} (k : Fin m) (n : ℕ), (SSet.prodStdSimplex.pairing k.castSucc.succ n).IsInner
-- Mathlib.Data.Fintype.Card
Finset.card_univ : ∀ {α : Type u_1} [inst : Fintype α], Finset.univ.card = Fintype.card α
-- Mathlib.Tactic.Core
/-- Extract the arguments from a `simpArgs` syntax as an array of syntaxes  -/
Mathlib.Tactic.getSimpArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)
-- Init.Omega.IntList
Lean.Omega.IntList.get_cons_succ : ∀ {x : ℤ} {xs : List ℤ} {i : ℕ}, Lean.Omega.IntList.get (x :: xs) (i + 1) = Lean.Omega.IntList.get xs i
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The Cauchy completion of a ring with absolute value.  -/
CauSeq.Completion.Cauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [IsStrictOrderedRing α] → {β : Type u_2} → [inst_3 : Ring β] → (abv : β → α) → [IsAbsoluteValue abv] → Type u_2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂},
  (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.instOrElseParenthesizerM : {α : Type} → OrElse (Lean.PrettyPrinter.ParenthesizerM α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_eq_get!_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α},
  Std.ExtDHashMap.Const.get! m a = (Std.ExtDHashMap.Const.get? m a).get!
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Field R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A] (s : S) (h1 : 1 ∉ s)
  (a : Unitization R ↥s),
  ↑((NonUnitalSubalgebra.unitizationAlgEquiv s h1) a) = (algebraMap R A) a.toProd.1 + ↑a.toProd.2
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_sub_coe : ∀ (L : PeriodPair) (z : ℂ) (l : ↥L.lattice), L.weierstrassP (z - ↑l) = L.weierstrassP z
-- Mathlib.Data.Rel
Set.preimage_eq_core : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), f ⁻¹' s = (Function.graph f).core s