mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.whiskering_map_app_right : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u') [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : CategoryTheory.Functor C D} (η : X ⟶ Y) (A : CategoryTheory.SimplicialObject.Augmented C),
  (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).map η).app A).right =
    η.app (CategoryTheory.SimplicialObject.Augmented.point.obj A)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
_private.Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet.0.Associates.FactorSet.prod.match_1.splitter : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    (motive : Associates.FactorSet α → Sort u_2) →
      (x : Associates.FactorSet α) →
        (Unit → motive none) → ((s : Multiset { a // Irreducible a }) → motive (some s)) → motive x
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_lcm : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a.lcm b).factorization = a.factorization ⊔ b.factorization
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_toSubsemiring : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  (Algebra.adjoin R s).toSubsemiring = Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s)
-- Mathlib.Algebra.Free
FreeAddSemigroup.of_head : ∀ {α : Type u} (x : α), (FreeAddSemigroup.of x).head = x
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.single.linearMap_apply : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] (a : Γ) (a_1 : V),
  (HahnSeries.single.linearMap a) a_1 = (↑(HahnSeries.single.addMonoidHom a)).toFun a_1
-- Mathlib.Order.Basic
update_le_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i}
  {i : ι} {a : π i}, Function.update y i a ≤ x ↔ a ≤ x i ∧ ∀ (j : ι), j ≠ i → y j ≤ x j
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGE!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited α],
          Std.DTreeMap.Internal.Impl.getKeyGE! k t₁ = Std.DTreeMap.Internal.Impl.getKeyGE! k t₂
-- Mathlib.Topology.Homotopy.Basic
/-- Post-compose a homotopy relative to a set by a continuous function.  -/
ContinuousMap.HomotopyRel.compContinuousMap : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {S : Set X} →
              {f₀ f₁ : C(X, Y)} → f₀.HomotopyRel f₁ S → (g : C(Y, Z)) → (g.comp f₀).HomotopyRel (g.comp f₁) S
-- Mathlib.LinearAlgebra.CrossProduct
cross_anticomm : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), -(crossProduct v) w = (crossProduct w) v
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_of_nonneg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [PosSMulMono α β], b₁ ≤ b₂ → 0 ≤ a → a • b₁ ≤ a • b₂
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT`. -/
Topology.CWComplex.iUnion_cellFrontier_subset_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (l : ℕ),
  ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeletonLT C ↑l)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some '' Set.Ioi a = Set.Ioo ↑a ⊤
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.prodMultiplicative_symm_apply : ∀ (G : Type u_2) (H : Type u_3) [inst : Add G] [inst_1 : Add H] (x : Multiplicative G × Multiplicative H),
  (MulEquiv.prodMultiplicative G H).symm x =
    match x with
    | (x, y) => Multiplicative.ofAdd (Multiplicative.toAdd x, Multiplicative.toAdd y)
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- The (multiplicative) universal property of `WithZero`.  -/
WithZero.lift' : {α : Type u_1} → {β : Type u_2} → [inst : MulOneClass α] → [inst_1 : MulZeroOneClass β] → (α →* β) ≃ (WithZero α →*₀ β)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.rootMultiplicity_expand_pow : ∀ {R : Type u} [inst : CommRing R] {p n : ℕ} [ExpChar R p] {f : Polynomial R} {r : R},
  Polynomial.rootMultiplicity r ((Polynomial.expand R (p ^ n)) f) = p ^ n * Polynomial.rootMultiplicity (r ^ p ^ n) f
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.linearEquivFunOnFinite_symm_coe : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M] (f : α →₀ M), (Finsupp.linearEquivFunOnFinite R M α).symm ⇑f = f
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addEquiv_trans : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid O] (e₁ : M ≃+ N) (e₂ : N ≃+ O),
  Finsupp.mapRange.addEquiv (e₁.trans e₂) = (Finsupp.mapRange.addEquiv e₁).trans (Finsupp.mapRange.addEquiv e₂)
-- Mathlib.Order.Interval.Basic
/-- The closed intervals in an order.

We represent intervals either as `⊥` or a nonempty interval given by its endpoints `fst`, `snd`.
To convert intervals to the set of elements between these endpoints, use the coercion
`Interval α → Set α`.  -/
Interval : (α : Type u_6) → [LE α] → Type u_6
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence.  -/
CategoryTheory.Over.homMk_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V W : CategoryTheory.Over X}
  (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (w_f : CategoryTheory.CategoryStruct.comp f V.hom = U.hom)
  (w_g : CategoryTheory.CategoryStruct.comp g W.hom = V.hom),
  CategoryTheory.Over.homMk (CategoryTheory.CategoryStruct.comp f g) ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk f w_f) (CategoryTheory.Over.homMk g w_g)
-- Lean.Meta.Tactic.Cases
/-- Convert `s` into an array of `CasesSubgoal`, by attaching the corresponding constructor name,
and adding the substitution `majorFVarId -> ctor_i us params fields` into each subgoal.  -/
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.toCasesSubgoals : Array Lean.Meta.InductionSubgoal →
  Array Lean.Name → Lean.FVarId → List Lean.Level → Array Lean.Expr → Array Lean.Meta.CasesSubgoal
-- Mathlib.Topology.Sheaves.Stalks
/-- For a presheaf `F` on a space `X`, a continuous map `f : X ⟶ Y` induces a morphisms between the
stalk of `f _ * F` at `f x` and the stalk of `F` at `x`.
 -/
TopCat.Presheaf.stalkPushforward : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} →
        (f : X ⟶ Y) →
          (F : TopCat.Presheaf C X) →
            (x : ↑X) →
              ((TopCat.Presheaf.pushforward C f).obj F).stalk ((CategoryTheory.ConcreteCategory.hom f) x) ⟶ F.stalk x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_top : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (x : G), x ∈ ⊤
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.hasFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃ₗᵢ[𝕜] F), HasFDerivAt (⇑iso) (↑↑iso) x
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The right-hand side of the diagram commutes.  -/
GroupExtension.Equiv.rightHom_comm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S'),
  ⇑S'.rightHom ∘ ⇑self.toMulEquiv = ⇑S.rightHom
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
Real.deriv_log' : deriv Real.log = Inv.inv
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.pairwise_toList_le : ∀ {α : Type u} {r : Std.Rii α} [inst : LE α] [inst_1 : Std.PRange.Least? α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxi.IsAlwaysFinite α],
  List.Pairwise (fun a b => a ≤ b) r.toList
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleMap_preimage_codiscrete : ∀ {c : ℂ} {R : ℝ},
  R ≠ 0 → Filter.map (circleMap c R) (Filter.codiscrete ℝ) ≤ Filter.codiscreteWithin (Metric.sphere c |R|)
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.bvar.sizeOf_spec : ∀ (idx : ℕ), sizeOf (Lean.Meta.ArrowPropResult.bvar✝ idx) = 1 + sizeOf idx
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_add : ∀ (R : Type u) {M : Type v} [inst : AddZeroClass R] [inst_1 : Add M] (m₁ m₂ : M),
  TrivSqZeroExt.inr (m₁ + m₂) = TrivSqZeroExt.inr m₁ + TrivSqZeroExt.inr m₂
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_7 : ∀ (q₁ q₂ : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ (q₁.pred q₂) =
    insert (q₁.pred q₂)
      (Turing.PartrecToTM2.trStmts₁ q₁ ∪ insert (Turing.PartrecToTM2.unrev q₂) (Turing.PartrecToTM2.trStmts₁ q₂))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.CoeExpansionTrace.mk : List Lean.Name → Lean.Elab.Term.CoeExpansionTrace
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (x : Rep.leftRegular k G ⟶ A),
  (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.homResolutionIso A g hg).hom.f i)) x =
    (Rep.homEquiv x) (MonoidAlgebra.single 1 1)
-- Mathlib.Order.Filter.ENNReal
ENNReal.ofReal_limsup : ∀ {α : Type u_1} {f : Filter α} {u : α → ℝ},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) ENNReal.ofReal_limsup._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) ENNReal.ofReal_limsup._auto_3 →
      ENNReal.ofReal (Filter.limsup u f) = Filter.limsup (fun a => ENNReal.ofReal (u a)) f
-- Init.Data.Array.Lemmas
Array.foldrM_start_stop : ∀ {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [inst : Monad m] {xs : Array α} {f : α → β → m β} {b : β}
  {start stop : ℕ}, Array.foldrM f b xs start stop = Array.foldrM f b (xs.extract stop start)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstr.p : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Grind.Linarith.Poly
-- Mathlib.Topology.Order.ExtendFrom
eq_lim_at_right_extendFrom_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {lb : β} [T2Space β],
  a < b → Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds lb) → extendFrom (Set.Ioo a b) f b = lb
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Option.all (fun x => x == a) (Std.Internal.List.getKey? a l) = true
-- Mathlib.Algebra.Prime.Defs
Prime.irreducible : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M}, Prime p → Irreducible p
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the forward component of the right unitor isomorphism.  -/
Bimod.RightUnitorBimod.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        {R S : CategoryTheory.Mon C} → (P : Bimod R S) → Bimod.TensorBimod.X P (Bimod.regular S) ⟶ P.X
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (A : CategoryTheory.Endofunctor.Algebra F) → Inhabited (A.Hom A)
-- Init.Control.Lawful.Instances
ExceptT.run_restoreM : ∀ {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : Monad m] (x : stM m (ExceptT ε m) α), (restoreM x).run = pure x
-- Init.Data.Array.MapIdx
Array.zipIdx_toArray : ∀ {α : Type u_1} {l : List α} {k : ℕ}, l.toArray.zipIdx k = (l.zipIdx k).toArray
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC_nc : Lean.Grind.CommRing.Expr → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.coe_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [inst_3 : CompleteSpace A] (φ : A →ₐ[𝕜] 𝕜), ⇑φ.toContinuousLinearMap = ⇑φ
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.BundledIterM.iterator : {m : Type w → Type w'} → {β : Type w} → (self : Std.BundledIterM m β) → Std.IterM m β
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedInjectiveTheorem : Inhabited Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.Topology.Algebra.Monoid.Defs
SeparatelyContinuousMul.continuous_const_mul : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Mul M} [self : SeparatelyContinuousMul M] {a : M},
  Continuous fun x => a * x
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The bundled additive group giving the filtered colimit of a diagram.  -/
AddGrpCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddGrpCat → AddGrpCat
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkYoneda.{w, v, u} =
    { obj := fun X => CategoryTheory.FunctorToTypes.shrink.{w, v, v, u} (CategoryTheory.yoneda.obj X),
      map := fun {X Y} f => CategoryTheory.FunctorToTypes.shrinkMap (CategoryTheory.yoneda.map f), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forget_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U ⟶ V},
  (CategoryTheory.Over.forget X).map f = CategoryTheory.Over.Hom.left f
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.PreservesSheafification.le : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {A : Type u_1}
  {B : Type u_2} {inst_1 : CategoryTheory.Category.{v_1, u_1} A} {inst_2 : CategoryTheory.Category.{v_2, u_2} B}
  {F : CategoryTheory.Functor A B} [self : J.PreservesSheafification F],
  J.W ≤ J.W.inverseImage ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F)
-- Mathlib.Data.Finsupp.Order
Finsupp.instPosSMulMono : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : Zero β]
  [inst_3 : Preorder β] [inst_4 : SMulZeroClass α β] [PosSMulMono α β], PosSMulMono α (ι →₀ β)
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging `tac; grind` into just `grind` if that also solves the goal.  -/
Mathlib.TacticAnalysis.mergeWithGrind : Mathlib.TacticAnalysis.Config
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.instRespectsIsoTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.RespectsIso
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : CategoryTheory.Limits.HasCokernel S.f],
  (CategoryTheory.ShortComplex.HomologyData.ofHasCokernel S hg).iso =
    CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel S hg).H
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ModelWithCorners.Simps.apply : (𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_5) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] → (H : Type u_6) → [inst_3 : TopologicalSpace H] → ModelWithCorners 𝕜 E H → H → E
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.toContinuousSemilinearMapClass : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
  [inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂] [SemilinearIsometryClass 𝓕 σ₁₂ E E₂],
  ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.initState : Lean.Server.StatefulRequestHandler → Dynamic
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.minValueSealed_def : Int64.minValueSealed✝ = Int64.minValue
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_sub : ∀ {R : Type u_1} [inst : Ring R] (f g : Polynomial R) (N : ℕ),
  Polynomial.reflect N (f - g) = Polynomial.reflect N f - Polynomial.reflect N g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isSMulIntInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Init.Data.AC
Lean.Data.AC.Context.mergeIdem_nonEmpty : ∀ (e : List ℕ), e ≠ [] → Lean.Data.AC.mergeIdem e ≠ []
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.iUnion_Ioo_of_tendsto : ∀ {ι : Type u_1} [Finite ι] {I : BoxIntegral.Box ι} {J : ℕ → BoxIntegral.Box ι},
  Monotone J →
    Filter.Tendsto (BoxIntegral.Box.lower ∘ J) Filter.atTop (nhds I.lower) →
      Filter.Tendsto (BoxIntegral.Box.upper ∘ J) Filter.atTop (nhds I.upper) →
        ⋃ n, BoxIntegral.Box.Ioo (J n) = BoxIntegral.Box.Ioo I
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.srangeRestrict.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {N : Type u_5} [inst_1 : Mul N] (f : M →ₙ* N),
  f.srangeRestrict = f.codRestrict f.srange ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.mul' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸}
  {a' b' : E →L[𝕜] 𝔸},
  HasFDerivAt a a' x → HasFDerivAt b b' x → HasFDerivAt (a * b) (a x • b' + MulOpposite.op (b x) • a') x
-- Mathlib.Data.Set.Restrict
Set.domRestrict₂_def : ∀ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t), Set.domRestrict₂ hst = fun f x => f ⟨↑x, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_eq_elem_of_card_eq_one : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {A : Matrix n n R},
  Fintype.card n = 1 → ∀ (k : n), A.det = A k k
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- Similar to `rank_quotient_add_rank_le` but for `finrank` and a finite `M`.  -/
Module.finrank_quotient_add_finrank_le : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] (N : Submodule R M), Module.finrank R (M ⧸ N) + Module.finrank R ↥N ≤ Module.finrank R M
-- Lean.Elab.Util
Lean.Elab.adaptMacro : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadMacroAdapter m] →
      [Lean.MonadEnv m] →
        [Lean.MonadRecDepth m] →
          [Lean.MonadError m] →
            [Lean.MonadResolveName m] →
              [Lean.MonadTrace m] →
                [Lean.MonadOptions m] →
                  [Lean.AddMessageContext m] → [MonadLiftT IO m] → Lean.Macro → Lean.Syntax → m Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.card_eq : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') [inst : Fintype V]
  [inst_1 : Fintype W], Fintype.card V = Fintype.card W
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (t acc : List α) (h_1 : (acc : List α) → motive [] acc)
  (h_2 : (a : α) → (t acc : List α) → motive (a :: t) acc),
  (match a :: t, acc with
    | [], acc => h_1 acc
    | a :: t, acc => h_2 a t acc) =
    h_2 a t acc
-- Batteries.Data.BitVec.Lemmas
BitVec.getMsbD_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ), (BitVec.ofFnLE f).getMsbD i = if h : i < n then f ⟨i, h⟩.rev else false
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The second of two points lies in their affine span.  -/
right_mem_affineSpan_pair : ∀ (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] (p₁ p₂ : P), p₂ ∈ line[k, p₁, p₂]
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.ProbabilityTheory.incrementsToRestrict_increments_orderEmbOfFinWithBot_ae_eq_restrict : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : LinearOrder T] [inst_1 : Bot T] (R : Type u_4) [inst_2 : Semiring R] [inst_3 : AddCommGroup E]
  [inst_4 : Module R E] [inst_5 : TopologicalSpace E] [inst_6 : ContinuousAdd E] {X : T → Ω → E},
  (∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0) →
    ∀ (I : Finset T),
      (fun ω => I.restrict fun x => X x ω) =ᵐ[P]
        ⇑(ProbabilityTheory.incrementsToRestrict✝ R I) ∘ fun ω i =>
          X (Finset.orderEmbOfFinWithBot✝ I i.succ) ω - X (Finset.orderEmbOfFinWithBot✝ I i.castSucc) ω
-- Mathlib.NumberTheory.FunctionField
/-- The function field analogue of `NumberField.ringOfIntegers`:
`FunctionField.ringOfIntegers F K` is the integral closure of `F[X]` in `K`.

We don't actually assume `K` is a function field over `F` in the definition,
only when proving its properties.
 -/
FunctionField.ringOfIntegers : (F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] → [inst_1 : Field K] → [inst_2 : Algebra (Polynomial F) K] → Subalgebra (Polynomial F) K
-- Mathlib.Algebra.Notation.Defs
VSub.mk : {G : outParam (Type u_1)} → {P : Type u_2} → (P → P → G) → VSub G P
-- Mathlib.Algebra.Algebra.Equiv
/-- Each element of the group defines an algebra equivalence.

This is a stronger version of `MulSemiringAction.toRingEquiv` and
`DistribMulAction.toLinearEquiv`.  -/
MulSemiringAction.toAlgEquiv : {G : Type u_2} →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Group G] → [inst_4 : MulSemiringAction G A] → [SMulCommClass G R A] → G → A ≃ₐ[R] A
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instIsLeftAdjointOpensOpensFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Hom.opensFunctor f).IsLeftAdjoint
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_of_isMaximal : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R} [I.IsMaximal] [J.IsMaximal], I ≠ J → IsCoprime I J
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.iSupLift_mk : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Type u_4} [inst_5 : Nonempty ι] (K : ι → Subalgebra R A)
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T ≤ iSup K}
  {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T), (Subalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
-- Std.Time.Date.Unit.Year
Std.Time.Year.instToStringOffset : ToString Std.Time.Year.Offset
-- Lean.PrettyPrinter.Formatter
/-- We use `EStateM` to be able to abort pretty printing once we get to the end of a line.  -/
Lean.PrettyPrinter.OneLine.M : Type → Type