mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.MutualInductive
/-- Checks that `u` has at most one universe level metavariable.
If it has a level metavariable, then applies the `simplifyResultingUniverse`
procedure to it and checks that the result is of the form `?m + k`.
Returns the simplified universe — this is used as an upper bound when collecting constraints
to solve for a least `?m`.

Throws an exception if `u` has metavariables and isn't of the right form for inference.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.processResultingUniverseForInference : Lean.Level → Lean.Elab.TermElabM Lean.Level
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_pos : ∀ {a : Cardinal.{u_1}}, 0 < a.ord ↔ 0 < a
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.cases : Lean.Name → Bool → Lean.Meta.Grind.Entry
-- Mathlib.RingTheory.Localization.Basic
Localization.algEquiv_symm_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  (Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = IsLocalization.mk' (Localization M) x y
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgEquiv_apply : ∀ (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (e : A ≃ₐ[R] B)
  (a : AddMonoidAlgebra A M),
  (AddMonoidAlgebra.mapAlgEquiv R M e) a = (↑↑(AddMonoidAlgebra.mapAlgHom M ↑e).toRingHom).toFun a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Mathlib.Logic.Function.Basic
Function.Surjective.hasRightInverse : ∀ {α : Sort u} {β : Sort v} {f : α → β}, Function.Surjective f → Function.HasRightInverse f
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.not_a_field : ∀ (R : Type u) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsLocalRing.maximalIdeal R ≠ ⊥
-- Init.Data.String.Basic
String.Pos.lt_next : ∀ {s : String} {p : s.Pos} {h : p ≠ s.endPos}, p < p.next h
-- Mathlib.Analysis.Convex.Gauge
gauge_def : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E},
  gauge s x = sInf {r | r ∈ Set.Ioi 0 ∧ x ∈ r • s}
-- Mathlib.CategoryTheory.Action.Basic
Action.res_obj_V : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] (f : G →* H) (M : Action V H), ((Action.res V f).obj M).V = M.V
-- Mathlib.Data.ZMod.Basic
ZMod.mul_inv_eq_gcd : ∀ {n : ℕ} (a : ZMod n), a * a⁻¹ = ↑(a.val.gcd n)
-- Init.Data.Rat.Lemmas
Rat.divInt.eq_def : ∀ (x x_1 : ℤ),
  Rat.divInt x x_1 =
    match x, x_1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => Rat.normalize (-n) d.succ ⋯
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- The identity `HomObj F F A`.  -/
CategoryTheory.Functor.HomObj.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F : CategoryTheory.Functor C D} → (A : CategoryTheory.Functor C (Type w)) → F.HomObj F A
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.nondegComplex_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (a : ℕ), s.nondegComplex.X a = s.N a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z) =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X Z
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.precomp_map_right : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).right = CategoryTheory.CategoryStruct.id X.right
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'_eq_zipWithLeft'TR.go : ∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → Option β → γ) (acc : Array γ) (as : List α) (bs : List β),
  List.zipWithLeft'TR.go f as bs acc =
    match List.zipWithLeft' f as bs with
    | (l, r) => (acc.toList ++ l, r)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- A `Functor.PushoutObjObj` structure for a functor `F : C₁ ⥤ C₂ ⥤ C₃` and
morphisms `f₁ : X₁ ⟶ Y₁` and `f₂ : X₂ ⟶ Y₂` when `X₁` is initial and both
`F.flip.obj X₂` and `F.flip.obj Y₂` preserve the initial object.  -/
CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {X₁ Y₁ : C₁} →
                (f₁ : X₁ ⟶ Y₁) →
                  {X₂ Y₂ : C₂} →
                    (f₂ : X₂ ⟶ Y₂) →
                      [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                            (F.flip.obj X₂)] →
                        [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
                              (F.flip.obj Y₂)] →
                          CategoryTheory.Limits.IsInitial X₁ → F.PushoutObjObj f₁ f₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- A way to create isomorphisms in the category of formal coproducts, by creating an `Equiv`
between the indexing sets, and then correspondingly isomorphisms of each component.  -/
CategoryTheory.Limits.FormalCoproduct.isoOfComponents : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : CategoryTheory.Limits.FormalCoproduct C} → (e : X.I ≃ Y.I) → ((i : X.I) → X.obj i ≅ Y.obj (e i)) → (X ≅ Y)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instDiv.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Div M],
  Filter.Germ.instDiv = { div := Filter.Germ.map₂ fun x1 x2 => x1 / x2 }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintLabelPart : Lean.ToJson Lean.Lsp.InlayHintLabelPart
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq : ∀ {R : Type r} [inst : CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R}, P 2 = Q 2 → Q 2 ≠ 0 → (P ≈ Q ↔ P = Q)
-- Mathlib.AlgebraicGeometry.Morphisms.IsIso
AlgebraicGeometry.isIso_SpecMap_iff : ∀ {R S : CommRingCat} {f : R ⟶ S},
  CategoryTheory.IsIso (AlgebraicGeometry.Spec.map f) ↔ Function.Bijective ⇑(CommRingCat.Hom.hom f)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowingε₀_one : ONote.fastGrowingε₀ 1 = 2
-- Mathlib.Order.Filter.AtTopBot.CountablyGenerated
Filter.atBot.isCountablyGenerated : ∀ {α : Type u_1} [inst : Preorder α] [Countable α], Filter.atBot.IsCountablyGenerated
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).size = t.size
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Filter.eventually_all_finset`. -/
Finset.eventually_all : ∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
  (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R],
  MaximalSpectrum.asIdeal ∘ ⇑IsArtinianRing.primeSpectrumEquivMaximalSpectrum = PrimeSpectrum.asIdeal
-- Mathlib.Algebra.GroupWithZero.Defs
zero_ne_mul_self : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a : M₀}, 0 ≠ a * a ↔ a ≠ 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.category.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C},
  CategoryTheory.Limits.Cone.category =
    { Hom := fun A B => CategoryTheory.Limits.ConeMorphism A B,
      id := fun B => { hom := CategoryTheory.CategoryStruct.id B.pt, w := ⋯ },
      comp := fun {X Y Z} f g => { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, w := ⋯ }, id_comp := ⋯,
      comp_id := ⋯, assoc := ⋯ }
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_inter_eq_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.ext_iff : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  (x y : ↥L'), x = y ↔ ↑x = ↑y
-- Init.Data.Array.Lemmas
Array.filterMap_append : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : α → Option β} {stop : ℕ},
  stop = xs.size + ys.size → Array.filterMap f (xs ++ ys) 0 stop = Array.filterMap f xs ++ Array.filterMap f ys
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sOppSide_point_excenter_singleton : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [n.AtLeastTwo]
  (i : Fin (n + 1)), (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide (s.points i) (s.excenter {i})
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- Assuming the base ring has a linear topology, the powers of a `MvPowerSeries` converge to 0
iff its constant coefficient is topologically nilpotent.

See also `MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent`.  -/
MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsLinearTopology R R]
  (f : MvPowerSeries σ R),
  Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) ↔ IsTopologicallyNilpotent (MvPowerSeries.constantCoeff f)
-- Mathlib.Topology.UniformSpace.Compact
IsClosed.relImage_of_isCompact : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → ∀ {t : Set α}, IsCompact t → IsClosed (s.image t)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.destruct_eq_cons : ∀ {α : Type u} {s : Stream'.Seq α} {a : α} {s' : Stream'.Seq α}, s.destruct = some (a, s') → s = Stream'.Seq.cons a s'
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_norm_left`. -/
Asymptotics.IsBigOWith.of_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) g → Asymptotics.IsBigOWith c l f' g
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.instCoeOutContinuousAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → CoeOut (A ≃A[R] B) (A →A[R] B)
-- Lean.Parser.Do
Lean.Parser.Term.doWhile : Lean.Parser.Parser
-- Mathlib.Data.Set.Finite.Range
Set.fintypeRange : {α : Type u} → {ι : Sort w} → [DecidableEq α] → (f : ι → α) → [Fintype (PLift ι)] → Fintype ↑(Set.range f)
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_hom_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_1}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (g : G) {X : C} (x : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.PreGaloisCategory.toAut F G) g).hom.app X)) x = g • x
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.whiskerLeft_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a' ⟶ F.obj a) (g : a ⟶ b),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map g)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app b)))
-- Mathlib.FieldTheory.SeparableClosure
Field.instNeZeroInsepDegree : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], NeZero (Field.insepDegree F E)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_diff : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF),
  t₂.WF →
    (t₁.diff t₂ ⋯).toListModel.Perm
      (List.filter (fun p => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.ofLeftInverse.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) {g : N → M}
  (h : Function.LeftInverse g ⇑f),
  MulEquiv.ofLeftInverse f h =
    { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(MulMemClass.subtype f.srange), left_inv := h, right_inv := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_le_natCast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : ℕ},
  ↑m ≤ ↑n ↔ m ≤ ↑n
-- Init.Data.String.Basic
String.toList_comp_ofList : String.toList ∘ String.ofList = id
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {a : α} [inst_1 : Inhabited α],
  ∅.getKey! a = default
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {s : Set E}, AnalyticWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 f (insert x s) x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsPath → ¬p.Nil → p.toSubgraph.neighborSet v = {p.penultimate}
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.not_adj_iff_part_eq : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} {s t : V}
  (h : G.IsTuranMaximal r) [inst_2 : DecidableEq V], ¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α}, (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a
-- Mathlib.Algebra.Polynomial.Basic
/-- Replace the coefficient of a `p : R[X]` at a given degree `n : ℕ`
by a given value `a : R`. If `a = 0`, this is equal to `p.erase n`
If `p.natDegree < n` and `a ≠ 0`, this increases the degree to `n`.  -/
Polynomial.update : {R : Type u} → [inst : Semiring R] → Polynomial R → ℕ → R → Polynomial R
-- Mathlib.Data.List.Induction
List.reverseRec.eq_1 : ∀ {α : Type u_1} {motive : List α → Sort u_2} (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])),
  List.reverseRec nil append_singleton [] = nil
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.natDegree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
instMeasurableEqOfSecondCountableTopologyOfT2Space : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α] [T2Space α], MeasurableEq α
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.pow : ∀ {G : Type u_1} [inst : Monoid G] {a : G} {n : ℕ}, IsOfFinOrder a → IsOfFinOrder (a ^ n)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mk.injEq : ∀ (mvar key : Lean.Expr) (mctx : Lean.MetavarContext) (subgoals : List Lean.Expr) (size : ℕ) (mvar_1 key_1 : Lean.Expr)
  (mctx_1 : Lean.MetavarContext) (subgoals_1 : List Lean.Expr) (size_1 : ℕ),
  ({ mvar := mvar, key := key, mctx := mctx, subgoals := subgoals, size := size } =
      { mvar := mvar_1, key := key_1, mctx := mctx_1, subgoals := subgoals_1, size := size_1 }) =
    (mvar = mvar_1 ∧ key = key_1 ∧ mctx = mctx_1 ∧ subgoals = subgoals_1 ∧ size = size_1)
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation maps balls to balls and scales the radius by `ratio f`.  -/
Dilation.mapsTo_eball : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r : ENNReal),
  Set.MapsTo (⇑f) (Metric.eball x r) (Metric.eball (f x) (↑(Dilation.ratio f) * r))
-- Mathlib.Data.Fin.VecNotation
/-- `![]` is the vector with no entries.  -/
Matrix.vecEmpty : {α : Type u} → Fin 0 → α
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Construct a new empty tree.  -/
RBTree.mkRBSet : (α : Type u) → (cmp : α → α → Ordering) → RBTree.RBSet α cmp
-- Mathlib.Order.Compare
cmpUsing.eq_1 : ∀ {α : Type u} (lt : α → α → Prop) [inst : DecidableRel lt] (a b : α),
  cmpUsing lt a b = if lt a b then Ordering.lt else if lt b a then Ordering.gt else Ordering.eq
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.absNorm_ne_zero`.

---

The norm of a maximal ideal as an element of `ℝ≥0` is `≠ 0`  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  [Module.Finite ℤ R] [inst_3 : Module.Free ℤ R], ↑(Ideal.absNorm v.asIdeal) ≠ 0
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go.match_13.eq_2 : ∀ (motive : Std.Sat.AIG.Decl ℕ → Sort u_1) (idx : ℕ)
  (h_1 : Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx_1 : ℕ) → Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → motive (Std.Sat.AIG.Decl.atom idx_1))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match heq : Std.Sat.AIG.Decl.atom idx with
    | Std.Sat.AIG.Decl.false => h_1 heq
    | Std.Sat.AIG.Decl.atom idx_1 => h_2 idx_1 heq
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs heq) =
    h_2 idx ⋯
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The type copy of `E →SL[σ] F` endowed with the weak operator topology, denoted as
`E →SWOT[σ] F`. Likewise, when `σ := RingHom.id 𝕜`, the notation `E →WOT[𝕜] F` is available.  -/
ContinuousLinearMapWOT.«term_→WOT[_]_» : Lean.TrailingParserDescr
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Extension : Type → Type
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.liftInclusion_of : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M) {i : ι} (x : ↥(S i)),
  (FirstOrder.Language.DirectLimit.liftInclusion S)
      ((FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x))
          (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i)
        x) =
    (S i).subtype x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] {kf : CategoryTheory.Limits.KernelFork S.g}
  (hkf : CategoryTheory.Limits.IsLimit kf) {Z : C} (h : S.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) h) =
    CategoryTheory.CategoryStruct.comp S.iCycles h
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.mk' : {X : SSet} → (toS : X.S) → toS.simplex ∈ X.nonDegenerate toS.dim → X.N
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.Hom.toImage_imageι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toImage f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.imageι f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_eq_some : ∀ {n : ℕ} {i j : Fin (n + 1)} {k : Fin n}, (finSuccEquiv' i) j = some k ↔ j = i.succAbove k
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_right_cancel' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (c : G), a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p]