mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Given `i` and `j` in `Fin (n + 1)` such that `i < j`,
this is the isomorphism from `Δ[1]` to the face
of `Δ[n]` corresponding to `{i, j}`.  -/
SSet.stdSimplex.facePairIso : {n : ℕ} → (i j : Fin (n + 1)) → i < j → (SSet.stdSimplex.obj { len := 1 } ≅ (SSet.stdSimplex.face {i, j}).toSSet)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Represent a section of rewrites as `MessageData`.  -/
Mathlib.Tactic.LibraryRewrite.SectionToMessageData : Array (Mathlib.Tactic.LibraryRewrite.Rewrite × Lean.Name) × Bool → Lean.MetaM (Option Lean.MessageData)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- Given a fiber functor `F` and a connected object `X` of `C`. Then `X` is Galois if and only if
the natural action of `Aut X` on `F.obj X` is transitive.  -/
CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected X],
  CategoryTheory.PreGaloisCategory.IsGalois X ↔ MulAction.IsPretransitive (CategoryTheory.Aut X) (F.obj X).obj
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote.mk.sizeOf_spec : ∀ (name : Lean.StrLit), sizeOf { name := name } = 1 + sizeOf name
-- Mathlib.Algebra.Opposites
/-- A recursor for `AddOpposite`. Use as `induction x`.  -/
AddOpposite.rec' : {α : Type u_1} → {F : αᵃᵒᵖ → Sort u_3} → ((X : α) → F (AddOpposite.op X)) → (X : αᵃᵒᵖ) → F X
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxc.HasSize α] [inst_1 : Std.PRange.Least? α] (r : Std.Ric α),
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some least => Std.Rxc.HasSize.size least r.upper
-- Init.Data.Bool
Bool.xor_comm : ∀ (x y : Bool), (x ^^ y) = (y ^^ x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → ∀ {h' : k' ∈ Std.TreeMap.ofList l cmp}, (Std.TreeMap.ofList l cmp).getKey k' h' = k
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.instDiscreteTopologyQuotient : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), DiscreteTopology (Quotient S.toSetoid)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.lt_pred : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  Order.IsPredPrelimit b → b < a → b < Order.pred a
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_7} [inst_1 : Unique ι] (f : R →ₗ[R] R) (i j : ι),
  (LinearMap.toMatrix (Module.Basis.singleton ι R) (Module.Basis.singleton ι R)) f i j = f 1
-- Lean.Data.SMap
Lean.SMap.stage₁ : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → Bool
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.of_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} {n : ℕ}, IsOfFinAddOrder (n • a) → n ≠ 0 → IsOfFinAddOrder a
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet.precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} {ι' : Type u_6}
  {g : ι' → ι}, Function.Injective g → ProbabilityTheory.iIndepSet s μ → ProbabilityTheory.iIndepSet (s ∘ g) μ
-- Lean.Meta.Tactic.ElimInfo
/-- Gets an eliminator appropriate for the provided array of targets.
If `induction` is `true` then returns a matching eliminator defined using the `@[induction_eliminator]` attribute
and otherwise returns one defined using the `@[cases_eliminator]` attribute.

The `@[induction_eliminator]` attribute is for the `induction` tactic
and the `@[cases_eliminator]` attribute is for the `cases` tactic.
 -/
Lean.Meta.getCustomEliminator? : Array Lean.Expr → Bool → Lean.MetaM (Option Lean.Name)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.chartedSpace_chartAt : ∀ {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace F]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)] {HB : Type u_7}
  [inst_3 : TopologicalSpace HB] [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B] [inst_6 : FiberBundle F E]
  (x : Bundle.TotalSpace F E),
  chartAt (ModelProd HB F) x =
    (trivializationAt F E x.proj).trans ((chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey? = t.keys.getLast?
-- Mathlib.Algebra.DualNumber
DualNumber.lift_apply_apply : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) })
  (a : DualNumber A), (DualNumber.lift fe) a = (↑fe).1 (TrivSqZeroExt.fst a) + (↑fe).1 (TrivSqZeroExt.snd a) * (↑fe).2
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type s} [inst_3 : CategoryTheory.SmallCategory K] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K D]
  {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D))
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W))))
  (i : (Opposite.unop W).Arrow) (k : K) {Z : D} (h : (F.obj k).obj (Opposite.op i.Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (E.π.app k)
        (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i))
      h
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N], ⇑0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany!_list_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {l : List ((a : α) × β a)}, (↑(t.insertMany! l)).size ≤ t.size + l.length
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instIsNegApplyForall : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂], IsNegApply (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, a ∈ t → t.get? a = some (t.getD a fallback)
-- Std.Sync.Channel
/-- Create a new channel. If:
- `capacity` is `none` it will be unbounded (the default)
- `capacity` is `some 0` it will always force a rendezvous between sender and receiver
- `capacity` is `some n` with `n > 0` it will use a buffer of size `n` and begin blocking once it
  is filled
 -/
Std.CloseableChannel.Sync.new : {α : Type} → optParam (Option ℕ) none → BaseIO (Std.CloseableChannel.Sync α)
-- Lean.HeadIndex
Lean.HeadIndex.lit.inj : ∀ {litVal litVal_1 : Lean.Literal}, Lean.HeadIndex.lit litVal = Lean.HeadIndex.lit litVal_1 → litVal = litVal_1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instHasZeroObjectLocalization : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C]
  (W : CategoryTheory.MorphismProperty C) [W.HasLeftCalculusOfFractions] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasZeroObject W.Localization
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel : ∀ {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] {S : CategoryTheory.ShortComplex C} [CategoryTheory.Balanced C],
  S.Exact →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.PreservesZeroMorphisms] [(S.map F).HasHomology],
      CategoryTheory.Mono S.f →
        CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F → (S.map F).Exact
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- Bundled monotone right-continuous real functions, used to construct Stieltjes measures.  -/
StieltjesFunction : (R : Type u_1) → [LinearOrder R] → [TopologicalSpace R] → Type u_1
-- Mathlib.GroupTheory.Coset.Basic
rightCosetEquivalence_rel : ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (RightCosetEquivalence s)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_one_of_forall_eq_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
  (∀ x ∈ s, f x = 1) → ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ)
  (m n p : ℤ)
  (h : autoParam (m + n = p) CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_add_unitIso_hom_app_eq._auto_1),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.hom.app
                ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app
              (Opposite.unop
                ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).functor.obj
                  ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))).op
          ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op))
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- **Alias** of `PositiveLinearMap.ofClass`.

---

Reinterpret an element of a type of positive linear maps as a positive linear map.  -/
PositiveLinearMapClass.toPositiveLinearMap : {F : Type u_1} →
  {R : Type u_2} →
    {E₁ : Type u_3} →
      {E₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid E₁] →
            [inst_2 : PartialOrder E₁] →
              [inst_3 : AddCommMonoid E₂] →
                [inst_4 : PartialOrder E₂] →
                  [inst_5 : Module R E₁] →
                    [inst_6 : Module R E₂] →
                      [inst_7 : FunLike F E₁ E₂] →
                        [LinearMapClass F R E₁ E₂] → [OrderHomClass F E₁ E₂] → F → E₁ →ₚ[R] E₂
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.NamedLinter.toLinter : Batteries.Tactic.Lint.NamedLinter → Batteries.Tactic.Lint.Linter
-- Mathlib.CategoryTheory.Action.Limits
/-- Auxiliary construction for the `Abelian (Action V G)` instance.  -/
Action.abelianAux : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {G : Type u_2} → [inst_1 : Monoid G] → Action V G ≌ CategoryTheory.Functor (CategoryTheory.SingleObj G) V
-- Mathlib.GroupTheory.EckmannHilton
/-- If a type carries two unital binary operations that distribute over each other,
then these operations are equal.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`.  -/
EckmannHilton.mul : ∀ {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X},
  EckmannHilton.IsUnital m₁ e₁ →
    EckmannHilton.IsUnital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → m₁ = m₂
-- Lean.Elab.Term.TermElabM
/-- Similar to `Lean.Elab.Term.elabTerm`, but ensures that the type of the elaborated term is `expectedType?`
by inserting coercions if necessary.

If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
Otherwise, it throws the error.
 -/
Lean.Elab.Term.elabTermEnsuringType : Lean.Syntax →
  Option Lean.Expr →
    optParam Bool true → optParam Bool true → optParam (Option String) none → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_span_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂),
  Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.median.eq_1 : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.median i = line[k, s.points i, s.faceOppositeCentroid i]
-- Std.Tactic.Do.Syntax
/-- If `true`, `vcgen` checks failed `BackwardRule.apply` calls by retrying after
`unfoldReducible`-normalizing the goal. If the rule then succeeds, an earlier step
forgot a normalization; `vcgen` raises a hard error pointing at the offending
rule and the missing reduction. Off by default; only consulted by `vcgen`.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.debug : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Init.Data.List.Nat.Modify
List.getElem?_modify_eq : ∀ {α : Type u_1} (f : α → α) (i : ℕ) (l : List α), (l.modify i f)[i]? = f <$> l[i]?
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instCommutativeJoin : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.Commutative fun x1 x2 => Lean.Order.join x1 x2
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.mem_interedges_iff : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {s t : Finset α} {x : α × α},
  x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- **Alias** of `FourierTransform.fourierInvCLM_apply`. -/
TemperedDistribution.fourierTransformInvCLM_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransformInv E F] [inst_6 : FourierInvAdd E F]
  [inst_7 : FourierInvSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourierInv E F] (f : E),
  (FourierTransform.fourierInvCLM R E) f = FourierTransformInv.fourierInv f
-- Mathlib.GroupTheory.Nilpotent
instNormalOfIsNilpotentOfFactPrime : ∀ {G : Type u_1} [hG : Group G] [Finite G] [Group.IsNilpotent G] {p : ℕ} [Fact (Nat.Prime p)] {P : Sylow p G},
  (↑P).Normal
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
/-- The power series expansion of `Real.sin`.  -/
Real.hasSum_sin : ∀ (r : ℝ), HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1).factorial) (Real.sin r)
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_3.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → 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
-- Aesop.BuiltinRules.Subst
Aesop.BuiltinRules.prepareIffs : Lean.MVarId → Array Lean.FVarId → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Analysis.Analytic.Composition
Composition.length_gather : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length), (a.gather b).length = b.length
-- Lean.Util.NumApps
Lean.Expr.NumApps.State.mk : Lean.PtrSet Lean.Expr → Lean.NameMap ℕ → Lean.Expr.NumApps.State
-- Mathlib.Algebra.Polynomial.Inductions
Polynomial.recOnHorner.eq_def : ∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Sort u_1} (p : Polynomial R) (M0 : M 0)
  (MC : (p : Polynomial R) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (p + Polynomial.C a))
  (MX : (p : Polynomial R) → p ≠ 0 → M p → M (p * Polynomial.X)),
  p.recOnHorner M0 MC MX =
    if hp : p = 0 then ⋯ ▸ M0
    else
      have wf := ⋯;
      ⋯.mpr
        (if hcp0 : p.coeff 0 = 0 then ⋯.mpr (⋯.mpr (⋯.mpr (MX p.divX ⋯ (p.divX.recOnHorner M0 MC MX))))
        else
          MC (p.divX * Polynomial.X) (p.coeff 0) ⋯ hcp0
            (if hpX0 : p.divX = 0 then
              have this := ⋯.mpr (⋯.mpr M0);
              this
            else MX p.divX hpX0 (p.divX.recOnHorner M0 MC MX)))
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.InferControlInfo.ofOptionSeq : Option Lean.DoSeq → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} →
        (toPreOneHypercover : CategoryTheory.PreOneHypercover S) →
          toPreOneHypercover.sieve₀ ∈ J S →
            (∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁)
                (p₂ : W ⟶ toPreOneHypercover.X i₂),
                CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) =
                    CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) →
                  toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W) →
              J.OneHypercover S
-- Mathlib.Algebra.Torsor.Basic
Prod.mk_sdiv_mk : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (p₁ p₂ : P) (p₁' p₂' : P'),
  (p₁, p₁') /ₛ (p₂, p₂') = (p₁ /ₛ p₂, p₁' /ₛ p₂')
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_eq_of_eq : ∀ {a b : UInt8}, a = b → a.toBitVec = b.toBitVec
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) →
        [inst_2 : P.IsMonoidal] →
          [inst_3 : CategoryTheory.MonoidalClosed C] →
            [P.IsMonoidalClosed] → CategoryTheory.MonoidalClosed P.FullSubcategory
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character is quadratic as a multiplicative character.  -/
quadraticChar_isQuadratic : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F], (quadraticChar F).IsQuadratic
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The direction of the span of the result of adding a point to a nonempty affine subspace is the
sup of the direction of that subspace and of any one difference between that point and a point in
the subspace.  -/
AffineSubspace.direction_affineSpan_insert : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p₁ p₂ : P},
  p₁ ∈ s → (affineSpan k (insert p₂ ↑s)).direction = k ∙ (p₂ -ᵥ p₁) ⊔ s.direction
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_succ : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + i = m) SimplexCategory.δ₀Iter_succ._auto_1),
  SimplexCategory.δ₀Iter (i + 1) ⋯ =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i h) (SimplexCategory.δ 0)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
/-- The under category has any connected limit which the original category has.  -/
CategoryTheory.Under.hasColimitsOfShape_of_isConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {B : C} [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Under B)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.partSize_le : ∀ {n : ℕ} (c : OrderedFinpartition n) (m : Fin c.length), c.partSize m ≤ n
-- Mathlib.Data.DFinsupp.BigOperators
/-- **Alias** of `DFinsupp.finsetSum_apply`. -/
DFinsupp.finset_sum_apply : ∀ {ι : Type u} {β : ι → Type v} {α : Type u_1} [inst : (i : ι) → AddCommMonoid (β i)] (s : Finset α)
  (g : α → Π₀ (i : ι), β i) (i : ι), (∑ a ∈ s, g a) i = ∑ a ∈ s, (g a) i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.Subcomplex.Pairing.strongInnerAnodyneExtensions : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [h₁ : P.IsRegular] [h₂ : P.IsInner],
  SSet.strongInnerAnodyneExtensions A.ι
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- A morphism in the CoGrothendieck construction `∫ᶜ F` between two points `X Y : ∫ᶜ F` consists of
a morphism in the base category `base : X.base ⟶ Y.base` and
a morphism in a fiber `f.fiber : X.fiber ⟶ (F.map base.op.toLoc).obj Y.fiber`.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      F.CoGrothendieck → F.CoGrothendieck → Type (max v₁ v₂)
-- Mathlib.Analysis.Real.Hyperreal
/-- A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega`. -/
Hyperreal.omega : ℝ*
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbol.brecOn_3.go : {motive_1 : Lean.Lsp.DocumentSymbol → Sort u} →
  {motive_2 : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol → Sort u} →
    {motive_3 : Option (Array Lean.Lsp.DocumentSymbol) → Sort u} →
      {motive_4 : Array Lean.Lsp.DocumentSymbol → Sort u} →
        {motive_5 : List Lean.Lsp.DocumentSymbol → Sort u} →
          (t : Array Lean.Lsp.DocumentSymbol) →
            ((t : Lean.Lsp.DocumentSymbol) → t.below → motive_1 t) →
              ((t : Lean.Lsp.DocumentSymbolAux Lean.Lsp.DocumentSymbol) →
                  Lean.Lsp.DocumentSymbol.below_1 t → motive_2 t) →
                ((t : Option (Array Lean.Lsp.DocumentSymbol)) → Lean.Lsp.DocumentSymbol.below_2 t → motive_3 t) →
                  ((t : Array Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_3 t → motive_4 t) →
                    ((t : List Lean.Lsp.DocumentSymbol) → Lean.Lsp.DocumentSymbol.below_4 t → motive_5 t) →
                      motive_4 t ×' Lean.Lsp.DocumentSymbol.below_3 t
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.w_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (φ : f ⟶ g) {Z : T}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp f.hom h
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_le_one : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] {a : α}, a⁺ᵐ ≤ 1 ↔ a ≤ 1