mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.shift_distinguished_triangle : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  ∀ T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C,
    ∀ (n : ℤ),
      (CategoryTheory.Pretriangulated.Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj T ∈
        HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Mathlib.Data.Matrix.Basic
Matrix.zero_le_one_elem : ∀ {n : Type u_3} {α : Type u_11} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] [inst_3 : Preorder α]
  [ZeroLEOneClass α] (i j : n), 0 ≤ 1 i j
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero : ∀ (R : Type u_1) {L : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : Fintype ι] (b : Module.Basis ι R L) (x : L)
  [inst_6 : DecidableEq ι],
  LieAlgebra.IsRegular R x ↔
    (MvPolynomial.eval ⇑(b.repr x)) (((↑(LieAlgebra.ad R L)).polyCharpoly b).coeff (LieAlgebra.rank R L)) ≠ 0
-- Mathlib.Tactic.DepRewrite
/-- Apply `rw!` to the goal.  -/
Mathlib.Tactic.DepRewrite.Conv.depRwTarget : Lean.Syntax → Bool → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.map_comp : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (k : ℕ) {A : Type w}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] {B : Type w} [inst_5 : CommRing B] [inst_6 : Algebra R B] (f : A →ₐ[R] B)
  {C : Type w} [inst_7 : CommRing C] [inst_8 : Algebra R C] (g : B →ₐ[R] C)
  (N : Module.Grassmannian A (TensorProduct R A M) k),
  Module.Grassmannian.map (g.comp f) N = Module.Grassmannian.map g (Module.Grassmannian.map f N)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_div_Iio : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => a / x) ⁻¹' Set.Iio b = Set.Ioi (a / b)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasStrictDerivAt.mul` -/
HasStrictDerivAt.fun_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasStrictDerivAt c c' x → HasStrictDerivAt d d' x → HasStrictDerivAt (fun i => c i * d i) (c' * d x + c x * d') x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_toArray_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [CompactSpace Y] [inst_4 : Zero Y] {s : Set X}
  [inst_5 : TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(Y, E)],
  MeasurableSet s →
    ∀ (f : X → Y → E) (g : ContinuousMapZero Y E),
      ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
        (∀ᵐ (x : X) ∂μ.restrict s, f x 0 = 0) →
          MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMapZero.mkD (f x) g) (μ.restrict s)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.coe_of : ∀ (α : Type u_1) [inst : BooleanAlgebra α] [inst_1 : Fintype α], ↑(FinBoolAlg.of α).toBoolAlg = α
-- Mathlib.LinearAlgebra.StdBasis
/-- The basis on `η → R` where the `i`th basis vector is `Function.update 0 i 1`.  -/
Pi.basisFun : (R : Type u_2) → (η : Type u_4) → [inst : Semiring R] → [Finite η] → Module.Basis η R (η → R)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiable_id : ∀ {𝕜 : 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], MDiff id
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.DTreeMap.Raw.valuesArray : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → Array β
-- Mathlib.CategoryTheory.Triangulated.Yoneda
/-- [Stacks Tag 0149](https://stacks.math.columbia.edu/tag/0149) -/
CategoryTheory.Pretriangulated.instIsHomologicalOppositeAddCommGrpCatObjFunctorPreadditiveYoneda : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C] (B : C),
  (CategoryTheory.preadditiveYoneda.obj B).IsHomological
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.inst : ∀ {R : Type u} [inst : CommRing R], Algebra.FormallySmooth R R
-- Mathlib.Data.Nat.Bitwise
_private.Mathlib.Data.Nat.Bitwise.0.Nat.bitwise.eq_1 : ∀ (f : Bool → Bool → Bool) (n m : ℕ),
  Nat.bitwise f n m =
    if n = 0 then if f false true = true then m else 0
    else
      if m = 0 then if f true false = true then n else 0
      else
        have n' := n / 2;
        have m' := m / 2;
        let b₁ := n % 2 = 1;
        let b₂ := m % 2 = 1;
        have r := Nat.bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactors : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {a b : R},
  a ∈ UniqueFactorizationMonoid.normalizedFactors b →
    Ideal.span {a} ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {b})
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- the addition of two morphisms is mapped to the sum of their images  -/
CategoryTheory.Functor.Additive.map_add : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.Preadditive C}
  {inst_3 : CategoryTheory.Preadditive D} {F : CategoryTheory.Functor C D} [self : F.Additive] {X Y : C} {f g : X ⟶ Y},
  F.map (f + g) = F.map f + F.map g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, a ∉ t → t.getKey! a = default
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} [inst_1 : SizeOf C]
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (r : X ⟶ R)
  (reflexivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₁ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₁._autoParam)
  (reflexivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp r p₂ = CategoryTheory.CategoryStruct.id X)
      CategoryTheory.ReflexiveRelation.reflexivity₂._autoParam),
  sizeOf { toJointlyMono₂ := toJointlyMono₂, r := r, reflexivity₁ := reflexivity₁, reflexivity₂ := reflexivity₂ } =
    1 + sizeOf toJointlyMono₂ + sizeOf r + sizeOf reflexivity₁ + sizeOf reflexivity₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.mem_succ_succ_iff : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : LT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo hi a : α},
  (a ∈ (Std.PRange.succ lo)<...=Std.PRange.succ hi) ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo<...=hi
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- A morphism from the cone point of any other cone to the weak limit object.  -/
CategoryTheory.Limits.weakLimit.lift : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasWeakLimit F] →
            (c : CategoryTheory.Limits.Cone F) → c.pt ⟶ CategoryTheory.Limits.weakLimit F
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_self : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Ico a a = ∅
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.invOf_diagonal_eq : ∀ {n : Type u'} [inst : Fintype n] [inst_1 : DecidableEq n] {α : Type u_2} [inst_2 : Semiring α] (v : n → α)
  [inst_3 : Invertible v] [inst_4 : Invertible (Matrix.diagonal v)], ⅟(Matrix.diagonal v) = Matrix.diagonal ⅟v
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.nextn.match_1.eq_2 : ∀ (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) (ss : Substring.Raw) (i : ℕ) (p : String.Pos.Raw)
  (h_1 : (x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p)
  (h_2 : (ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p),
  (match ss, i.succ, p with
    | x, 0, p => h_1 x p
    | ss, i.succ, p => h_2 ss i p) =
    h_2 ss i p
-- Init.Data.UInt.Lemmas
UInt16.ofNat_usizeSize_sub_one : UInt16.ofNat (USize.size - 1) = 65535
-- Std.Http.Server.Config
Std.Http.Config.mk.sizeOf_spec : ∀ (maxConnections maxRequests maxHeaders maxHeaderBytes : ℕ) (lingeringTimeout : Std.Time.Millisecond.Offset)
  (keepAliveTimeout : { x // x > 0 }) (headerTimeout : Std.Time.Millisecond.Offset) (enableKeepAlive : Bool)
  (maximumRecvSize defaultPayloadBytes : ℕ) (generateDate : Bool) (serverName : Option Std.Http.Header.Value)
  (maxUriLength maxStartLineLength maxHeaderNameLength maxHeaderValueLength maxSpaceSequence maxLeadingEmptyLines
    maxChunkExtNameLength maxChunkExtValueLength maxChunkLineLength maxChunkSize maxBodySize maxReasonPhraseLength
    maxTrailerHeaders maxChunkExtensions : ℕ),
  sizeOf
      { maxConnections := maxConnections, maxRequests := maxRequests, maxHeaders := maxHeaders,
        maxHeaderBytes := maxHeaderBytes, lingeringTimeout := lingeringTimeout, keepAliveTimeout := keepAliveTimeout,
        headerTimeout := headerTimeout, enableKeepAlive := enableKeepAlive, maximumRecvSize := maximumRecvSize,
        defaultPayloadBytes := defaultPayloadBytes, generateDate := generateDate, serverName := serverName,
        maxUriLength := maxUriLength, maxStartLineLength := maxStartLineLength,
        maxHeaderNameLength := maxHeaderNameLength, maxHeaderValueLength := maxHeaderValueLength,
        maxSpaceSequence := maxSpaceSequence, maxLeadingEmptyLines := maxLeadingEmptyLines,
        maxChunkExtNameLength := maxChunkExtNameLength, maxChunkExtValueLength := maxChunkExtValueLength,
        maxChunkLineLength := maxChunkLineLength, maxChunkSize := maxChunkSize, maxBodySize := maxBodySize,
        maxReasonPhraseLength := maxReasonPhraseLength, maxTrailerHeaders := maxTrailerHeaders,
        maxChunkExtensions := maxChunkExtensions } =
    1 + sizeOf maxConnections + sizeOf maxRequests + sizeOf maxHeaders + sizeOf maxHeaderBytes +
                                                sizeOf lingeringTimeout +
                                              sizeOf keepAliveTimeout +
                                            sizeOf headerTimeout +
                                          sizeOf enableKeepAlive +
                                        sizeOf maximumRecvSize +
                                      sizeOf defaultPayloadBytes +
                                    sizeOf generateDate +
                                  sizeOf serverName +
                                sizeOf maxUriLength +
                              sizeOf maxStartLineLength +
                            sizeOf maxHeaderNameLength +
                          sizeOf maxHeaderValueLength +
                        sizeOf maxSpaceSequence +
                      sizeOf maxLeadingEmptyLines +
                    sizeOf maxChunkExtNameLength +
                  sizeOf maxChunkExtValueLength +
                sizeOf maxChunkLineLength +
              sizeOf maxChunkSize +
            sizeOf maxBodySize +
          sizeOf maxReasonPhraseLength +
        sizeOf maxTrailerHeaders +
      sizeOf maxChunkExtensions
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_roo : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  Std.Slice.size (Std.Roo.Sliceable.mkSlice xs lo<...hi) = min hi xs.size - (lo + 1)
-- Std.Time.Date.PlainDate
Std.Time.instInhabitedPlainDate : Inhabited Std.Time.PlainDate
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.resolve : {α : Type} → Std.Broadcast.Consumer✝ α → Bool → BaseIO Unit
-- Mathlib.Data.Real.ConjExponents
/-- The conjugate exponent of `p` is `q = p / (p-1)`, so that `p⁻¹ + q⁻¹ = 1`.  -/
Real.conjExponent : ℝ → ℝ
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Entails.mk : {α : Type u} → {β : Type v} → ((α → Bool) → β → Prop) → Std.Tactic.BVDecide.LRAT.Internal.Entails α β
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.CompactOpens α), IsOpen ↑s
-- Mathlib.RingTheory.Regular.ProjectiveDimension
ModuleCat.projectiveDimension_quotient_eq_add_length_of_isWeaklyRegular : ∀ {R : Type u} [inst : CommRing R] [Small.{v, u} R] [inst_2 : IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R)
  [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular (↑M) rs →
    (∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) →
      CategoryTheory.projectiveDimension (ModuleCat.of R (↑M ⧸ Ideal.ofList rs • ⊤)) =
        CategoryTheory.projectiveDimension M + ↑rs.length
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.d_single : ∀ {k G : Type u} [inst : CommRing k] {n : ℕ} (c : Fin (n + 1) → G) (r : k),
  (Rep.standardComplex.d k G n) (MonoidAlgebra.single c r) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) (r * (-1) ^ ↑p)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformContinuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun x => x.1 ×ˢ x.2
-- Mathlib.Order.Sublattice
Sublattice.bot_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (M : Sublattice β), ⊥.prod M = ⊥
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_zero : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α}, xs.insertIdx 0 x ⋯ = Vector.cast ⋯ (#v[x] ++ xs)
-- Lean.Elab.Binders
/-- The dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually
reserve the latter for propositions. Also written as `Π x : α, β` (the "Pi-type")
in the literature.  -/
Lean.Elab.Term.elabDepArrow : Lean.Elab.Term.TermElab
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.emb_ne_emb_of_ne : ∀ {n : ℕ} (c : OrderedFinpartition n) {i j : Fin c.length} {a : Fin (c.partSize i)} {b : Fin (c.partSize j)},
  i ≠ j → c.emb i a ≠ c.emb j b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.comm_comp_lTensor_comp_comm_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_8} {P : Type u_9} {Q : Type u_10} [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] (g : N →ₗ[R] P),
  ↑(TensorProduct.comm R Q P) ∘ₗ LinearMap.lTensor Q g ∘ₗ ↑(TensorProduct.comm R N Q) = LinearMap.rTensor Q g
-- Init.Data.UInt.Lemmas
USize.toNat_div : ∀ (a b : USize), (a / b).toNat = a.toNat / b.toNat
-- Mathlib.Analysis.Seminorm
Seminorm.closedBall_bot : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {r : ℝ}
  (x : E), 0 < r → ⊥.closedBall x r = Set.univ
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.diff.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.diff m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.diff ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Std.Sat.AIG.CachedLemmas
/-- If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`.
 -/
Std.Sat.AIG.denote_mkGate_cached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput}
  {hit :
    Std.Sat.AIG.CacheHit aig.decls
      (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input.lhs.gate input.lhs.invert)
        (Std.Sat.AIG.Fanin.mk input.rhs.gate input.rhs.invert))},
  aig.cache.get?
        (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input.lhs.gate input.lhs.invert)
          (Std.Sat.AIG.Fanin.mk input.rhs.gate input.rhs.invert)) =
      some hit →
    ⟦assign, { aig := aig, ref := { gate := hit.idx, invert := false, hgate := ⋯ } }⟧ = ⟦assign, aig.mkGate input⟧
-- Mathlib.Logic.Unique
nonempty_unique : ∀ (α : Sort u) [Subsingleton α] [Nonempty α], Nonempty (Unique α)
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- Any point is a periodic point of period `0`.  -/
Function.isPeriodicPt_zero : ∀ {α : Type u_1} (f : α → α) (x : α), Function.IsPeriodicPt f 0 x
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- Two-sided-ideals corresponds to congruence relations on a ring.  -/
TwoSidedIdeal.orderIsoRingCon : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal R ≃o RingCon R
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.splitter : {β : Type u_1} →
  (motive : List β → Sort u_2) →
    (l : List β) → (Unit → motive []) → ((x : β) → (xs : List β) → motive (x :: xs)) → motive l
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear equivs on the right respects higher differentiability.  -/
ContinuousLinearEquiv.contDiff_comp_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E),
  ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- If a monic polynomial `f : k[X]` splits in `K`,
then it has as many roots (counting multiplicity) as its degree.  -/
AlgebraicClosure.finEquivRoots : {k : Type u} →
  [inst : Field k] →
    {K : Type u_1} →
      [inst_1 : Field K] →
        [inst_2 : DecidableEq K] →
          {i : k →+* K} →
            {f : AlgebraicClosure.Monics k} →
              (Polynomial.map i ↑f).Splits → Fin (↑f).natDegree ≃ ↥(Polynomial.map i ↑f).roots.toEnumFinset
-- Mathlib.Order.Fin.Tuple
/-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`.  -/
finSuccAboveOrderIso : {n : ℕ} → (p : Fin (n + 1)) → Fin n ≃o { x // x ≠ p }
-- Mathlib.CategoryTheory.Abelian.Exact
/-- A functor which preserves exactness preserves epimorphisms.  -/
CategoryTheory.Functor.preservesEpimorphisms_of_map_exact : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Abelian A] [inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
  [inst_4 : L.PreservesZeroMorphisms],
  (∀ (S : CategoryTheory.ShortComplex A), S.Exact → (S.map L).Exact) → L.PreservesEpimorphisms
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_toUSize : ∀ (n : UInt32), n.toUSize.toUInt8 = n.toUInt8
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.visit : Lean.Expr → StateRefT' IO.RealWorld Lean.Meta.FunInd.Collector.Cache Lean.Meta.FunInd.Collector.M Unit
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
polarCoord_symm_apply : ∀ (p : ℝ × ℝ), ↑polarCoord.symm p = (p.1 * Real.cos p.2, p.1 * Real.sin p.2)
-- Aesop.RuleTac.Forward
_private.Aesop.RuleTac.Forward.0.Aesop.RuleTac.assertForwardHyp.tacticBuilder : Lean.MVarId → Lean.Meta.Hypothesis → Lean.FVarId × Lean.MVarId → Aesop.Script.TacticBuilder
-- Mathlib.Data.Nat.Prime.Defs
Nat.instDecidablePredPrime : DecidablePred Prime
-- Mathlib.SetTheory.Lists
Lists.of'.eq_1 : ∀ {α : Type u_1} (l : Lists' α true), Lists.of' l = ⟨true, l⟩
-- Mathlib.Topology.Category.LightProfinite.Extend
LightProfinite.Extend.cocone_ι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C)
  (S : LightProfinite) (i : CategoryTheory.CostructuredArrow FintypeCat.toLightProfinite.op (Opposite.op S)),
  (LightProfinite.Extend.cocone G S).ι.app i = G.map i.hom
-- Init.Data.List.Basic
/-- Returns a list of the numbers with the given length `len`, starting at `start` and increasing by
`step` at each element.

In other words, `List.range' start len step` is `[start, start+step, ..., start+(len-1)*step]`.

Examples:
 * `List.range' 0 3 (step := 1) = [0, 1, 2]`
 * `List.range' 0 3 (step := 2) = [0, 2, 4]`
 * `List.range' 0 4 (step := 2) = [0, 2, 4, 6]`
 * `List.range' 3 4 (step := 2) = [3, 5, 7, 9]`
 -/
List.range' : ℕ → ℕ → optParam ℕ 1 → List ℕ
-- Mathlib.Tactic.Bound.Attribute
/-- Check if an expression is zero  -/
Mathlib.Tactic.Bound.isZero : {u : Lean.Level} → {α : Q(Type u)} → Q(«$α») → Lean.MetaM Bool
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.cons.inj : ∀ {α : Type u} {rank : ℕ} {val : α} {node : Batteries.BinomialHeap.Imp.HeapNode α}
  {next : Batteries.BinomialHeap.Imp.Heap α} {rank_1 : ℕ} {val_1 : α} {node_1 : Batteries.BinomialHeap.Imp.HeapNode α}
  {next_1 : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.cons rank val node next =
      Batteries.BinomialHeap.Imp.Heap.cons rank_1 val_1 node_1 next_1 →
    rank = rank_1 ∧ val = val_1 ∧ node = node_1 ∧ next = next_1
-- Aesop.Forward.RuleInfo
/-- The previous premises that the premise of this slot depends on.  -/
Aesop.Slot.deps : Aesop.Slot → Std.HashSet Aesop.PremiseIndex
-- Mathlib.CategoryTheory.Opposites
/-- An equivalence between `Cᵒᵖ` and `D` gives an equivalence between `C` and `Dᵒᵖ`.  -/
CategoryTheory.Equivalence.rightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (Cᵒᵖ ≌ D) → (C ≌ Dᵒᵖ)
-- Batteries.Data.ByteArray
/-- Unsafe optimized implementation of `mapM`.

This function is unsafe because it relies on the implementation limit that the size of an array is
always less than `USize.size`.
 -/
ByteArray.mapMUnsafe : {m : Type → Type u_1} → [Monad m] → ByteArray → (UInt8 → m UInt8) → m ByteArray
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instPowCauchyNat : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Pow (CauSeq.Completion.Cauchy abv) ℕ
-- Mathlib.FieldTheory.Minpoly.Field
/-- If `L/K` is a field extension and an element `y` of `K` is a root of the minimal polynomial
of an element `x ∈ L`, then `y` maps to `x` under the field embedding.  -/
minpoly.root : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [IsDomain B] [inst_3 : Algebra A B] {x : B},
  IsIntegral A x → ∀ {y : A}, (minpoly A x).IsRoot y → (algebraMap A B) y = x
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- The full level `N` congruence subgroup of `SL(2, ℤ)` of matrices that reduce to the identity
modulo `N`.  -/
CongruenceSubgroup.«termΓ(_)» : Lean.ParserDescr