mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Algebra.IsAlgebraic.isTranscendenceBasis_of_le_trdeg_of_finite : ∀ (R : Type u_1) {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [NoZeroDivisors A]
  [FaithfulSMul R A] {ι : Type w} [Finite ι] (x : ι → A) [Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A],
  Cardinal.mk ι ≤ Algebra.trdeg R A → IsTranscendenceBasis R x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.DTreeMap.Const.get! (Std.DTreeMap.filter f t) k =
    ((Std.DTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Init.Data.Array.Bootstrap
Array.toList_push : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x).toList = xs.toList ++ [x]
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.counitBialgHom_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (x : A),
  (Bialgebra.counitBialgHom R A) x = CoalgebraStruct.counit x
-- Mathlib.Logic.Pairwise
pairwise_fin_succ_iff_of_isSymm : ∀ {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} [Std.Symm R],
  Pairwise R ↔ (∀ (j : Fin n), R 0 j.succ) ∧ Pairwise fun i j => R i.succ j.succ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α}, k ∈ m → (m.insertManyIfNewUnit l).getKey? k = m.getKey? k
-- Mathlib.Topology.DiscreteSubset
codiscrete_le_cofinite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], Filter.codiscrete X ≤ Filter.cofinite
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instSep : Sep ZFSet.{u_1} ZFSet.{u_1}
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_ite_eq : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] (i : ι)
  (t : Finset ι) (z : ι → E) [inst_3 : DecidableEq ι], i ∈ t → t.centerMass (fun j => if i = j then 1 else 0) z = z i
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.instMonadHashMapCacheAdapterExprStructEqExprM : Lean.MonadHashMapCacheAdapter Lean.ExprStructEq Lean.Expr Lean.MetavarContext.MkBinding.M
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
/-- **Nested intervals lemma**: if `f` is a monotone sequence, `g` is an antitone sequence, and
`f n ≤ g n` for all `n`, then `⨆ n, f n` belongs to all the intervals `[f n, g n]`.  -/
Monotone.ciSup_mem_iInter_Icc_of_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] [inst_1 : Preorder β]
  [IsDirectedOrder β] {f g : β → α}, Monotone f → Antitone g → f ≤ g → ⨆ n, f n ∈ ⋂ n, Set.Icc (f n) (g n)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.descSigma_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} {φ : F ⟶ G} {K : HomologicalComplex C c}
  (x y : (α : G ⟶ K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0),
  x = y ↔ x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j
-- Init.Data.Ord.Basic
/-- Uses a decidable less-than relation and Boolean equality to find an `Ordering`.

In particular, if `x < y` then the result is `Ordering.lt`. If `x == y` then the result is
`Ordering.eq`. Otherwise, it is `Ordering.gt`.

`compareOfLessAndEq` uses `DecidableEq` instead of `BEq`.
 -/
compareOfLessAndBEq : {α : Type u_1} → (x y : α) → [inst : LT α] → [Decidable (x < y)] → [BEq α] → Ordering
-- Mathlib.Order.Ideal
Order.Ideal.finsetSup_mem_iff : ∀ {P : Type u_2} [inst : SemilatticeSup P] [inst_1 : OrderBot P] (t : Order.Ideal P) {ι : Type u_3} {f : ι → P}
  {s : Finset ι}, s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
-- Mathlib.RingTheory.MvPowerSeries.Derivative
_private.Mathlib.RingTheory.MvPowerSeries.Derivative.0.MvPowerSeries.pderivFun_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ} (f g : MvPowerSeries σ R),
  MvPowerSeries.pderivFun i (f * g) = f • MvPowerSeries.pderivFun i g + g • MvPowerSeries.pderivFun i f
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadIso.mk_inv_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Monad C}
  (f : M.toFunctor ≅ N.toFunctor)
  (f_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (M.η.app X) (f.hom.app X) = N.η.app X)
      CategoryTheory.MonadIso.mk._auto_1)
  (f_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (M.μ.app X) (f.hom.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (M.map (f.hom.app X)) (f.hom.app (N.obj X))) (N.μ.app X))
      CategoryTheory.MonadIso.mk._auto_3),
  (CategoryTheory.MonadIso.mk f f_η f_μ).inv.toNatTrans = f.inv
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_inv_s₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  {i j : F.I₀} (k : F.I₁ i j),
  (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.s₁ k =
    s₁.symm ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) k)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instHashablePoly.hash : Lean.Grind.CommRing.Poly → UInt64
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.Nonnegg.eq_1 : ∀ (c d a b : ℕ), Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.ofNat b) = True
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.map_nsmul_piAntidiag_univ : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0),
  Finset.map { toFun := fun x => n • x, inj' := ⋯ } (Finset.univ.piAntidiag m) =
    {f ∈ Finset.univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.of.eq_1 : ∀ {α : Type u_1} (x : α), FreeAddMonoid.of x = FreeAddMonoid.ofList [x]
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedFunDecl : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.FunDecl a)
-- Lean.Elab.AutoBound
Lean.Elab.instInhabitedAutoBoundImplicitContext : Inhabited Lean.Elab.AutoBoundImplicitContext
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_inv_two : ↑2⁻¹ = 2⁻¹
-- Mathlib.SetTheory.Lists
Lists.lt_sizeof_cons' : ∀ {α : Type u_1} {b : Bool} (a : Lists' α b) (l : Lists' α true), sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.isPullback_colon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C),
  CategoryTheory.IsPullback (Φ.colon Ψ).ι (Φ.colonπ Ψ) Φ.π
    (CategoryTheory.CategoryStruct.comp (Φ.quotient.whiskerLeft Ψ.ι) Φ.quotient.rightUnitor.hom)
-- Mathlib.Data.Set.Image
Set.compl_range_some : ∀ (α : Type u_5), (Set.range some)ᶜ = {none}
-- Mathlib.Data.List.Lattice
List.mem_inter_of_mem_of_mem : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α], a ∈ l₁ → a ∈ l₂ → a ∈ l₁ ∩ l₂
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.instDecidableEqDyadic.decEq.match_1.eq_3 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (n k : ℤ) (hn : n % 2 = 1) (h_1 : Unit → motive Dyadic.zero Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive Dyadic.zero (Dyadic.ofOdd n k hn))
  (h_3 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn) Dyadic.zero)
  (h_4 :
    (a a_1 : ℤ) →
      (a_2 : a % 2 = 1) → (b b_1 : ℤ) → (b_2 : b % 2 = 1) → motive (Dyadic.ofOdd a a_1 a_2) (Dyadic.ofOdd b b_1 b_2)),
  (match Dyadic.ofOdd n k hn, Dyadic.zero with
    | Dyadic.zero, Dyadic.zero => h_1 ()
    | Dyadic.zero, Dyadic.ofOdd n k hn => h_2 n k hn
    | Dyadic.ofOdd n k hn, Dyadic.zero => h_3 n k hn
    | Dyadic.ofOdd a a_1 a_2, Dyadic.ofOdd b b_1 b_2 => h_4 a a_1 a_2 b b_1 b_2) =
    h_3 n k hn
-- Init.Data.Rat.Lemmas
Rat.neg_normalize : ∀ (n : ℤ) (d : ℕ) (z : d ≠ 0), -Rat.normalize n d z = Rat.normalize (-n) d z
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.erase_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp.congr_simp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} {M₁ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] {M₃ : Type u_7}
  [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃] [inst_9 : Module R₁ M₁] [inst_10 : Module R₂ M₂]
  [inst_11 : Module R₃ M₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g g_1 : M₂ →SL[σ₂₃] M₃),
  g = g_1 → ∀ (f f_1 : M₁ →SL[σ₁₂] M₂), f = f_1 → g ∘SL f = g_1 ∘SL f_1
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instFinite : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α],
  Std.Iterators.Finite (Std.Rxi.Iterator α) Id
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If Cᵒᵖ is cofiltered or empty, then C is filtered or empty.  -/
CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ],
  CategoryTheory.IsFilteredOrEmpty C
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.flip_quotDualCoannihilatorToDual_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (W : Submodule R (Module.Dual R M)), Function.Injective ⇑W.quotDualCoannihilatorToDual.flip
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Representable presheaves are (trivially) ind-objects.  -/
CategoryTheory.Limits.isIndObject_yoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.Limits.IsIndObject (CategoryTheory.yoneda.obj X)
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.RingMode.SOP.sizeOf_spec : sizeOf Mathlib.Tactic.RingNF.RingMode.SOP = 1
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- The scalar product `ψ • s` of a differentiable function `ψ : M → 𝕜` and a section `s` of a
vector bundle `V → M` is differentiable once `s` is differentiable on an open set containing
`tsupport ψ`.

See `ContMDiffOn.smul_section_of_tsupport` for the analogous result about `C^n` sections.  -/
MDifferentiableOn.smul_section_of_tsupport : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B}
  {s : (x : B) → E x} {ψ : B → 𝕜},
  MDiff[u] ψ → IsOpen u → tsupport ψ ⊆ u → MDiff[u] (T% s) → MDiff fun x => ⟨x, (ψ • s) x⟩
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_restrict : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M) {s t : Set α},
  MeasurableSet s → MeasurableSet t → (v.restrict t).restrict s = v.restrict (s ∩ t)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instMonoid : {R : Type u_1} →
  {A : Type u_6} →
    {ι : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] → {𝒜 : ι → Submodule R A} → [inst_5 : GradedAlgebra 𝒜] → Monoid (𝒜 →ₐᵍ[R] 𝒜)
-- Mathlib.Algebra.Lie.Nilpotent
/-- For a nilpotent Lie module `M` of a Lie algebra `L`, the first term in the lower central series
of `M` contains a non-zero element on which `L` acts trivially unless the entire action is trivial.

Taking `M = L`, this provides a useful characterisation of Abelian-ness for nilpotent Lie
algebras.  -/
LieModule.disjoint_lowerCentralSeries_maxTrivSubmodule_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [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]
  [LieModule.IsNilpotent L M],
  Disjoint (LieModule.lowerCentralSeries R L M 1) (LieModule.maxTrivSubmodule R L M) ↔ LieModule.IsTrivial L M
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.isEmpty = false),
  t.maxEntry h = t_1.maxEntry ⋯
-- Batteries.Data.ByteArray
Fin.cast.eq_1 : ∀ {n m : ℕ} (eq : n = m) (i : Fin n), Fin.cast eq i = ⟨↑i, ⋯⟩
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Regular.Pi
Pi.isAddRegular_iff : ∀ {ι : Type u_1} {R : ι → Type u_3} [inst : (i : ι) → Add (R i)] {a : (i : ι) → R i},
  IsAddRegular a ↔ ∀ (i : ι), IsAddRegular (a i)
-- Init.Data.Option.Monadic
Option.bindM.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Pure m] (f : α → m (Option β)) (val : α),
  Option.bindM f (some val) = f val
-- Lean.CoreM
Lean.Core.CoreM.run' : {α : Type} → Lean.CoreM α → Lean.Core.Context → Lean.Core.State → EIO Lean.Exception α
-- Lean.Environment
Lean.ConstantKind.opaque.sizeOf_spec : sizeOf Lean.ConstantKind.opaque = 1
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.inv_hom_id_apply : ∀ {X Y : TopCat} (f : X ≅ Y) (y : ↑Y),
  (CategoryTheory.ConcreteCategory.hom f.hom) ((CategoryTheory.ConcreteCategory.hom f.inv) y) = y
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one : ∀ (n : ℕ) [inst : NeZero n] {s : ℂ},
  s ≠ 1 →
    deriv (DirichletCharacter.LFunctionTrivChar₁ n) s =
      (s - 1) * deriv (DirichletCharacter.LFunctionTrivChar n) s + DirichletCharacter.LFunctionTrivChar n s
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.coe_substAlgHom : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a), ⇑(PowerSeries.substAlgHom ha) = PowerSeries.subst a
-- Std.Http.Internal.IndexMultiMap
Std.Internal.instReprIndexMultiMap.repr : {α : Type u_1} →
  {β : Type u_2} →
    {inst : BEq α} → {inst_1 : Hashable α} → [Repr α] → [Repr β] → Std.Internal.IndexMultiMap α β → ℕ → Std.Format
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_monomial_monomial : ∀ {R : Type u_1} [inst : CommSemiring R] (n m : ℕ) (r : R),
  Polynomial.Bivariate.swap ((Polynomial.monomial n) ((Polynomial.monomial m) r)) =
    (Polynomial.monomial m) ((Polynomial.monomial n) r)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
AlgebraicGeometry.Scheme.AffineZariskiSite.cocone_pt : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.AffineZariskiSite.cocone X).pt = X
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- Getting back the natural number from the objects.  -/
FreeSimplexQuiver.len : FreeSimplexQuiver → ℕ
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withSimpTheorems : {α : Type} → Lean.Meta.SimpTheoremsArray → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_pred_singleton : ∀ {a : ℕ}, 0 < a → Finset.Ico (a - 1) a = {a - 1}
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.star_apply : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : StarRing R'] (χ : MulChar R R')
  (a : R), (star χ) a = star (χ a)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.getThenInsertIfNew? k v).1 = m.get? k
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.leftOpRightOpEquiv_unitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ),
  (CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.StrictBackwardPattern.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat],
  (∀ {s : String.Slice} (h : s.isEmpty = false) (q : s.Pos),
      String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h = some q → q ≠ s.endPos) →
    String.Slice.Pattern.StrictBackwardPattern pat
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- The image of the `GoodProducts` for `π C (ord I · < o)` in `LocallyConstant C ℤ`. The name `smaller`
refers to the setting in which we will use this, when we are mapping in `GoodProducts` from a
smaller set, i.e. when `o` is a smaller ordinal than the one `C` is "contained" in.
 -/
Profinite.NobelingProof.GoodProducts.smaller : {I : Type u} →
  (C : Set (I → Bool)) → [inst : LinearOrder I] → [WellFoundedLT I] → Ordinal.{u} → Set (LocallyConstant ↑C ℤ)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedDelayedTheoremInstance.default : Lean.Meta.Grind.DelayedTheoremInstance
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt : ∀ {α : Type u_1} [inst : Monoid α] {a b : α},
  FiniteMultiplicity a b → ∀ {n : ℕ}, multiplicity a b < n → emultiplicity a b < ↑n
-- Mathlib.Data.Finsupp.Defs
Finsupp.zero_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {a : α}, 0 a = 0
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
Cardinal.SharplyLT.lt : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [inst_1 : Fact κ₂.IsRegular], κ₁.SharplyLT κ₂ → κ₁ < κ₂
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.leftUnitor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Discrete PUnit.{w + 1} × C),
  (CategoryTheory.prod.leftUnitor C).obj X = X.2
-- Mathlib.GroupTheory.Congruence.Basic
/-- The **first isomorphism theorem for monoids**.  -/
Con.quotientKerEquivRange : {M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass P] → (f : M →* P) → (Con.ker f).Quotient ≃* ↥(MonoidHom.mrange f)
-- Mathlib.RingTheory.RingHom.Flat
RingHom.flat_algebraMap_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).Flat ↔ Module.Flat R S
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `a` and `b`, then `fderiv` derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)`
equals `(u, v) ↦ v • cb - u • ca`.  -/
intervalIntegral.fderiv_integral : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
        ContinuousAt f a →
          ContinuousAt f b →
            fderiv ℝ (fun p => ∫ (x : ℝ) in p.1..p.2, f x) (a, b) =
              (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)
-- Mathlib.Order.Filter.Prod
Filter.pure_prod : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : Filter β}, pure a ×ˢ f = Filter.map (Prod.mk a) f
-- Std.Http.Data.Status
/-- 302 Found
 -/
Std.Http.Status.found : Std.Http.Status
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s t : Set E), gaugeRescale s t 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss.0.Polynomial.Chebyshev.exp_sub_one_ne_zero : ∀ {n : ℕ} {k : ℤ}, n ≠ 0 → ¬2 * ↑n ∣ k → Complex.exp (↑k / ↑n * ↑Real.pi * Complex.I) ≠ 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCall.from : Lean.Lsp.CallHierarchyIncomingCall → Lean.Lsp.CallHierarchyItem
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.proj : Lean.Name → ℕ → ℕ → Lean.Meta.DiscrTree.Key
-- Init.Data.SInt.Bitwise
Int16.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : Int16}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- In a monoid whose only unit is `1`, a product is equal to `1` iff all factors are `1`.  -/
Finset.prod_eq_one_iff : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} [Subsingleton Mˣ],
  ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1
-- Lean.Data.Name
Lean.Name.getPrefix : Lean.Name → Lean.Name
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanIleanInfoParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanIleanInfoParams
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.mk : {n : ℕ} →
  {X : SSet.Truncated (n + 1)} →
    (spineToSimplex :
        (m : ℕ) →
          (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
            X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h })) →
      (∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex m ⋯ = id) →
        (∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex m ⋯ ∘ X.spine m h = id) → X.StrictSegal
-- Mathlib.Tactic.DeriveTraversable
/-- For a sum type `inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ...`
``traverseField `Foo f `α `(x : List α)`` synthesizes
`traverse f x` as part of traversing `foo1`.  -/
Mathlib.Deriving.Traversable.traverseField : Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM (Bool × Lean.Expr)
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.orbit.eq_or_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (a b : X),
  AddAction.orbit G a = AddAction.orbit G b ∨ Disjoint (AddAction.orbit G a) (AddAction.orbit G b)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
neg_le_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), -a ≤ |a|
-- Mathlib.Order.CompleteLattice.Basic
sup_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [Nonempty ι] {f : ι → α} {a : α}, a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x
-- Init.Data.BitVec.Lemmas
BitVec.cast_append_right : ∀ {w v v' : ℕ} (h : w + v = w + v') (x : BitVec w) (y : BitVec v), BitVec.cast h (x ++ y) = x ++ BitVec.cast ⋯ y
-- Init.Data.Ord.Basic
/-- The lexicographic order on pairs.  -/
lexOrd : {α : Type u_1} → {β : Type u_2} → [Ord α] → [Ord β] → Ord (α × β)