mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.length_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Fold a function on the values from left to right (in increasing order).  -/
RBTree.RBMap.foldl : {α : Type u} → {β : Type v} → {σ : Type w} → {cmp : α → α → Ordering} → (σ → α → β → σ) → σ → RBTree.RBMap α β cmp → σ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.map_app_objEquiv_symm_δ_index : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper],
  (CategoryTheory.ConcreteCategory.hom (c.map.app (Opposite.op { len := c.dim })))
      (SSet.stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) =
    (↑c.s).simplex
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.compContinuousLinearMap.eq_1 : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F]
  [inst_10 : ContinuousConstSMul 𝕜 F] [inst_11 : AddCommMonoid G] [inst_12 : Module 𝕜 G] [inst_13 : TopologicalSpace G]
  [inst_14 : ContinuousAdd G] [inst_15 : ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
  (n : ℕ), p.compContinuousLinearMap u n = (p n).compContinuousLinearMap fun x => u
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.ker_eq : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] (i : K →+* L) (p : ℕ)
  [inst_2 : ExpChar L p] [inst_3 : PerfectRing L p] [IsPerfectClosure i p], RingHom.ker i = pNilradical K p
-- Mathlib.Order.Hom.Bounded
/-- `id` as a `TopHom`.  -/
TopHom.id : (α : Type u_2) → [inst : Top α] → TopHom α α
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.epi_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting), CategoryTheory.Epi S.g
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The degree of `L` over `K` is equal to the number of unramified places over `v` plus twice the
number of ramified places over `v`.  -/
NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) [NumberField K] [NumberField L],
  (NumberField.InfinitePlace.unramifiedPlacesOver L v).ncard +
      2 * (NumberField.InfinitePlace.ramifiedPlacesOver L v).ncard =
    Module.finrank K L
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.diff_eq_diff! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF),
  t₁.diff t₂ ⋯ = t₁.diff! t₂
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- `trim` sends the supremum of two outer measures to the supremum of the trimmed measures.  -/
MeasureTheory.OuterMeasure.trim_sup : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m₁ m₂ : MeasureTheory.OuterMeasure α), (m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim
-- Std.Async.IO
Std.Async.IO.AsyncStream.stop : {α : Type} → {β : outParam Type} → [self : Std.Async.IO.AsyncStream α β] → α → IO Unit
-- Mathlib.CategoryTheory.Functor.Const
/-- The functor sending `X : C` to the constant functor `J ⥤ C` sending everything to `X`.
 -/
CategoryTheory.Functor.const : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] → CategoryTheory.Functor C (CategoryTheory.Functor J C)
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
CategoryTheory.Limits.filtered_colim_preservesFiniteLimits : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  [Small.{v, u₂} K] [CategoryTheory.FinCategory J] [CategoryTheory.IsFiltered K] {C : Type u}
  [inst_5 : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_6 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_7 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfShape J C] [inst_9 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [CategoryTheory.Limits.ReflectsLimitsOfShape J (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget C)],
  CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim
-- Lean.DocString.Syntax
Lean.Doc.Syntax.link_target.quot : Lean.ParserDescr
-- Mathlib.Analysis.Convex.EGauge
le_egauge_inter : ∀ {𝕜 : Type u_1} [inst : NNNorm 𝕜] {E : Type u_2} [inst_1 : SMul 𝕜 E] (s t : Set E) (x : E),
  max (egauge 𝕜 s x) (egauge 𝕜 t x) ≤ egauge 𝕜 (s ∩ t) x
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.tail.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (h : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.tail le h =
    (Batteries.BinomialHeap.Imp.Heap.tail? le h).getD Batteries.BinomialHeap.Imp.Heap.nil
-- Mathlib.Data.Finset.Insert
Finset.coe_cons : ∀ {α : Type u_1} {a : α} {s : Finset α} {h : a ∉ s}, ↑(Finset.cons a s h) = insert a ↑s
-- Mathlib.Logic.Embedding.Basic
/-- Restrict both domain and codomain of an embedding.  -/
Function.Embedding.subtypeMap : {α : Sort u_1} →
  {β : Sort u_2} →
    {p : α → Prop} → {q : β → Prop} → (f : α ↪ β) → (∀ ⦃x : α⦄, p x → q (f x)) → { x // p x } ↪ { y // q y }
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsCircuit.closure_sdiff_singleton_eq`. -/
Matroid.IsCircuit.closure_diff_singleton_eq : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → ∀ (e : α), M.closure (C \ {e}) = M.closure C
-- Mathlib.Algebra.Group.Defs
mul_right_inj : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] (a : G) {b c : G}, a * b = a * c ↔ b = c
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_filterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} {o : Type w → Type u_2}
  [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o] [inst_5 : Std.Do.WPMonad o ps]
  [inst_6 : MonadAttach n] [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT n o] [LawfulMonadLiftT n o]
  [Std.Iterators.Finite α Id] [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → n (ULift.{w, 0} Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out)
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.filterM f it) init g ⦃Q⦄
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfList_cons : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {hd : α} {tl : List α},
  Std.HashMap.Raw.unitOfList (hd :: tl) = (∅.insertIfNew hd ()).insertManyIfNewUnit tl
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.extendIsoEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {X : C} (i : s.pt ⟶ X)
  [inst_2 : CategoryTheory.IsIso i],
  CategoryTheory.Limits.IsColimit.extendIsoEquiv i =
    equivOfSubsingletonOfSubsingleton (CategoryTheory.Limits.IsColimit.extendIso i)
      (CategoryTheory.Limits.IsColimit.ofExtendIso i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.mkReplaceIndFVars : Array Lean.Elab.Command.InductiveView →
  Array Lean.Expr → List Lean.Name → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Ring.Defs
/-- Zero is a right absorbing element for multiplication  -/
NonUnitalNonAssocSemiring.mul_zero : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a : α), a * 0 = 0
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_zero : ∀ {A : Type u_1} [inst : Semiring A] (v : A →+* ℂ), Polynomial.mapMahlerMeasure 0 v = 0
-- Init.Data.String.Lemmas.Basic
String.Slice.utf8ByteSize_eq_size_toByteArray_copy : ∀ {s : String.Slice}, s.utf8ByteSize = s.copy.toByteArray.size
-- Mathlib.Algebra.Group.Indicator
Set.indicator_add' : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f g : α → M),
  s.indicator (f + g) = s.indicator f + s.indicator g
-- Mathlib.Algebra.Homology.FullSubcategory
HomologicalComplex.liftObjectProperty_X : ∀ {ι : Type u_1} {c : ComplexShape ι} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V]
  [inst_1 : CategoryTheory.Preadditive V] (P : CategoryTheory.ObjectProperty V) (K : HomologicalComplex V c)
  (hK : ∀ (n : ι), P (K.X n)) (n : ι),
  (HomologicalComplex.liftObjectProperty P K hK).X n = { obj := K.X n, property := ⋯ }
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- The action fulfils a normality condition on products that lie in `H`.
This ensures that the action descends to an action on the quotient `G ⧸ H`.  -/
MulAction.QuotientAction.inv_mul_mem : ∀ {G : Type u} {X : Type v} {inst : Group G} {inst_1 : Monoid X} {inst_2 : MulAction X G} {H : Subgroup G}
  [self : MulAction.QuotientAction X H] (b : X) {a a' : G}, a⁻¹ * a' ∈ H → (b • a)⁻¹ * b • a' ∈ H
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_left_inj₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a b : M₀} {n : ℕ}
  [MulPosMono M₀], 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_biUnion_finset : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} (t : Finset ι) {s : ι → Set X},
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Function.onFun Disjoint s) →
      (∀ i ∈ t, MeasureTheory.IntegrableOn f (s i) μ) →
        ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.coe_compRingHom_apply : ∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R), q.compRingHom p = p.comp q
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂_apply : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ σ₂ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) (i : n) (j : m),
  (LinearMap.toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.reverse.eq_1 : ∀ {T : Type u_1} (g : ContextFreeGrammar T),
  g.reverse =
    { NT := g.NT, initial := g.initial, rules := Finset.map { toFun := ContextFreeRule.reverse, inj' := ⋯ } g.rules }
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_le_of_prod_range_le : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : CommMonoid α] [inst_2 : TopologicalSpace α] {c : α} [ClosedIicTopology α]
  {f : ℕ → α}, Multipliable f → (∀ (n : ℕ), ∏ i ∈ Finset.range n, f i ≤ c) → ∏' (n : ℕ), f n ≤ c
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.neg : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'}, MDiffAt f z → MDiffAt (-f) z
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (t : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((sz : ℕ) →
              (k' : α) →
                (v' : β) →
                  (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')) →
            motive t
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instLattice : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Lattice (ClopenUpperSet α)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonServerInfo.toJson : Lean.Lsp.ServerInfo → Lean.Json
-- Lean.Meta.Sym.AlphaShareCommon
/-- When `true`, `shareCommonAlpha` and `shareCommonAlphaInc` throw when hash-consing
a new reducible constant that the `unfoldReducible` preprocessing step should
have unfolded (see `isUnfoldReducibleCandidate`).
 -/
Lean.Meta.Sym.AlphaShareCommon.Context.checkReducible : Lean.Meta.Sym.AlphaShareCommon.Context → Bool
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_le_right_iff_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {a b : E} {r : k}, r < 1 → ((AffineMap.lineMap a b) r ≤ b ↔ a ≤ b)
-- Init.Data.SInt.Lemmas
Int16.left_eq_add : ∀ {a b : Int16}, a = a + b ↔ b = 0
-- Init.Data.String.Length
String.length_singleton : ∀ {c : Char}, (String.singleton c).length = 1
-- Mathlib.Data.Set.Finite.Basic
Set.card_insert : ∀ {α : Type u} {a : α} (s : Set α) [inst : Fintype ↑s],
  a ∉ s → ∀ {d : Fintype ↑(insert a s)}, Fintype.card ↑(insert a s) = Fintype.card ↑s + 1
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
/-- The category of internal monoid objects in `Type`
is equivalent to the category of "native" bundled monoids.
 -/
monTypeEquivalenceMon : CategoryTheory.Mon (Type u) ≌ MonCat
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPUnicode : Lean.Options → Bool
-- Init.Data.Int.DivMod.Bootstrap
Int.lt_mul_ediv_self_add : ∀ {x k : ℤ}, 0 < k → x < k * (x / k) + k
-- Mathlib.Algebra.Order.Floor.Defs
/-- `Int.floor a` is the greatest integer `z` such that `z ≤ a`. It is denoted with `⌊a⌋`.  -/
Int.floor : {α : Type u_2} → [inst : Ring α] → [inst_1 : LinearOrder α] → [FloorRing α] → α → ℤ
-- Mathlib.Algebra.Ring.Identities
/-- Brahmagupta's identity, see <https://en.wikipedia.org/wiki/Brahmagupta%27s_identity>
 -/
sq_add_mul_sq_mul_sq_add_mul_sq : ∀ {R : Type u_1} [inst : CommRing R] {x₁ x₂ y₁ y₂ n : R},
  (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt16
-- Mathlib.RingTheory.OreLocalization.Basic
/-- Another characterization of the addition on the Ore localization, bundling up all witnesses
and conditions into a sigma type.  -/
OreLocalization.oreDivAddChar' : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddMonoid X] →
            [inst_3 : DistribMulAction R X] →
              (r r' : X) →
                (s s' : ↥S) →
                  (r'' : R) ×'
                    (s'' : ↥S) ×' ↑s'' * ↑s = r'' * ↑s' ∧ r /ₒ s + r' /ₒ s' = (s'' • r + r'' • r') /ₒ (s'' * s)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_lt_of_le_of_pos_of_nonneg`. -/
mul_lt_mul_of_pos_of_nonneg' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
  [MulPosStrictMono α], a < b → c ≤ d → 0 < c → 0 ≤ b → a * c < b * d
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.congr_simp : ∀ (M : Type u_1) [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  MulArchimedeanClass M = MulArchimedeanClass M
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The naturality of the iterated slice equivalence up to isomorphism.  -/
CategoryTheory.Over.iteratedSliceForwardNaturalityIso : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {f g : CategoryTheory.Over X} →
        (p : f ⟶ g) →
          f.iteratedSliceForward.comp (CategoryTheory.Over.map (CategoryTheory.Over.Hom.left p)) ≅
            (CategoryTheory.Over.map p).comp g.iteratedSliceForward
-- Mathlib.Algebra.Homology.Embedding.Connect
_private.Mathlib.Algebra.Homology.Embedding.Connect.0.CochainComplex.ConnectData.d.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (h_1 : (n m : ℕ) → motive (Int.ofNat n) (Int.ofNat m))
  (h_2 : (n m : ℕ) → motive (Int.negSucc n) (Int.negSucc m)) (h_3 : Unit → motive (Int.negSucc 0) (Int.ofNat 0))
  (h_4 : (a a_1 : ℕ) → motive (Int.ofNat a) (Int.negSucc a_1))
  (h_5 : (a a_1 : ℕ) → motive (Int.negSucc a) (Int.ofNat a_1)),
  (match Int.negSucc 0, Int.ofNat 0 with
    | Int.ofNat n, Int.ofNat m => h_1 n m
    | Int.negSucc n, Int.negSucc m => h_2 n m
    | Int.negSucc 0, Int.ofNat 0 => h_3 ()
    | Int.ofNat a, Int.negSucc a_1 => h_4 a a_1
    | Int.negSucc a, Int.ofNat a_1 => h_5 a a_1) =
    h_3 ()
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on connected spaces.  -/
intermediate_value_univ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] [PreconnectedSpace X] (a b : X) {f : X → α}, Continuous f → Set.Icc (f a) (f b) ⊆ Set.range f
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.decidableMemMker : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : MonoidHomClass F M N] → [DecidableEq N] → (f : F) → DecidablePred fun x => x ∈ MonoidHom.mker f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_rio : ∀ {b : ℕ}, (*...b).size = b
-- Mathlib.Tactic.Rify
Mathlib.Tactic.Rify.ratCast_ne : ∀ (a b : ℚ), a ≠ b ↔ ↑a ≠ ↑b
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_of_isEmpty' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [IsEmpty 𝓨], ProbabilityTheory.avgRisk ℓ P κ π = 0
-- Mathlib.Data.Set.Basic
Set.Nonempty.left : ∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty → s.Nonempty
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt.vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x <ᵥ y → x ≤ᵥ y
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- See `ramificationIdx_tower'` for a version that only assumes local flatness.  -/
Ideal.ramificationIdx_tower : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.LiesOver q] [Module.Flat S T], r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S
-- Mathlib.RingTheory.Regular.IsSMulRegular
LinearEquiv.isSMulRegular_congr : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (e : M ≃ₗ[R] N) (r : R), IsSMulRegular M r ↔ IsSMulRegular N r
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_algebraMap : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (v : AbsoluteValue R S) (w : AbsoluteValue T S) (x : WithAbs v),
  ((algebraMap (WithAbs v) (WithAbs w)) x).ofAbs = (algebraMap R T) x.ofAbs
-- Mathlib.Tactic.Push
/-- Set `distrib` to true in `push Not` and related tactics.  -/
Mathlib.Tactic.Push.push_neg.use_distrib : Lean.Option Bool
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- **Alias** of `CategoryTheory.MorphismProperty.HasPullbacks.hasPullback`. -/
CategoryTheory.MorphismProperty.hasPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.HasPullbacks]
  {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S), P f → CategoryTheory.Limits.HasPullback f g
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_rco' : ∀ {m n k : ℕ}, List.map (fun x => k + x) (m...n).toList = ((k + m)...k + n).toList
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FiniteType.of_finitePresentation : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A →ₐ[R] B}, f.FinitePresentation → f.FiniteType
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinderHom_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {i j : (CategoryTheory.PreOneHypercover.cylinder f g).I₀} (k : (CategoryTheory.PreOneHypercover.cylinder f g).I₁ i j),
  (CategoryTheory.PreOneHypercover.cylinderHom f g).s₁ k = k.down
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.version.getPatch : Unit → ℕ
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mul_subset_closure : ∀ {M : Type u_3} [inst : Monoid M] {s t u : Set M}, s ⊆ u → t ⊆ u → s * t ⊆ ↑(Submonoid.closure u)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (l l_1 : Std.ExtTreeMap α β cmp),
  l = l_1 → ∀ (a a_1 : α), a = a_1 → l.contains a = l_1.contains a_1
-- Init.Data.Option.Lemmas
Option.get_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Bool} {f : (x : α) → p x = true → β} {o : Option α}
  {h : ∀ (a : α), o = some a → p a = true} {h' : (Option.pmap f o h).isSome = true},
  (Option.pmap f o h).get h' = f (o.get ⋯) ⋯
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.toEquiv_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), ↑(Matrix.reindexAlgEquiv R A e) = Matrix.reindex e e
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.aeval_algHom_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (ϕ : AdjoinRoot f →ₐ[R] S), (Polynomial.aeval (ϕ (AdjoinRoot.root f))) f = 0
-- Mathlib.Algebra.Free
FreeAddMagma.hom_ext_iff : ∀ {α : Type u} {β : Type v} [inst : Add β] {f g : FreeAddMagma α →ₙ+ β},
  f = g ↔ ⇑f ∘ FreeAddMagma.of = ⇑g ∘ FreeAddMagma.of