mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- When the affine space is also a vector space, the affine span is contained within the linear
span.  -/
affineSpan_le_toAffineSubspace_span : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : Set V},
  affineSpan k s ≤ ↑(Submodule.span k s)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insert_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {p : α × β},
  insert p t = t.insert p.1 p.2
-- Mathlib.Topology.UniformSpace.Defs
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is symmetric.  -/
Filter.Tendsto.uniformity_symm : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] {l : Filter β} {f : β → α × α},
  Filter.Tendsto f l (uniformity α) → Filter.Tendsto (fun x => ((f x).2, (f x).1)) l (uniformity α)
-- Init.Data.Fin.Lemmas
Fin.pos' : ∀ {n : ℕ} [Nonempty (Fin n)], 0 < n
-- Init.Data.Int.DivMod.Lemmas
Int.lt_mul_tdiv_self_add : ∀ {x k : ℤ}, 0 < k → x < k * x.tdiv k + k
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.mkQ_comp_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N] {n : ℕ}, (I ^ a n • ⊤).mkQ ∘ₗ IsAdicComplete.StrictMono.lift I ha f ⋯ = f n
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_right' : ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → a * c ≡ b * c [ZMOD n * c]
-- Std.Http.Data.Headers
Std.Http.Headers.instSingletonProdNameValue : Singleton (Std.Http.Header.Name × Std.Http.Header.Value) Std.Http.Headers
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instCommMonoid : CommMonoid Cardinal.{u}
-- Mathlib.Topology.Defs.Filter
/-- The "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the
intersection of `s` and a neighborhood of `x`.  -/
Topology.«term𝓝[_]_» : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hasForgetToCommMonCat : CategoryTheory.HasForget₂ CommGrpCat CommMonCat
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsFragment.nonempty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  K < 1 → S.Nonempty → Finset.IsFragment✝ K S A → A.Nonempty
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.IterM.step_drop.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.ExtDTreeMap.maxKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.MonadicRightAdjoint.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {R : CategoryTheory.Functor D C} →
          (L : CategoryTheory.Functor C D) →
            (adj : L ⊣ R) → (CategoryTheory.Monad.comparison adj).IsEquivalence → CategoryTheory.MonadicRightAdjoint R
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.associator_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b) (β : b ⟶ c)
  (γ : c ⟶ d),
  (CategoryTheory.Bicategory.associator α β γ).hom.τr = (CategoryTheory.Bicategory.associator γ.r β.r α.r).hom
-- Lean.ProjFns
/-- Number of parameters in the child structure.  -/
Lean.AuxParentProjectionInfo.numParams : Lean.AuxParentProjectionInfo → ℕ
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` preserves terminal objects (G4).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.aeval_val_relationOfHasCoeffs : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (r : σ),
  (MvPolynomial.aeval P.val) (Algebra.Presentation.relationOfHasCoeffs R₀ r) = 0
-- Mathlib.LinearAlgebra.Orientation
Orientation.reindex.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] (M : Type u_2)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {ι : Type u_4} {ι' : Type u_5} (e : ι ≃ ι'),
  Orientation.reindex R M e = Module.Ray.map (AlternatingMap.domDomCongrₗ R e)
-- Mathlib.Data.ENat.Pow
ENat.epow_right_mono : ∀ {x : ℕ∞}, x ≠ 0 → Monotone fun y => x ^ y
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- A collection of entries that will be inserted into the discrimination trees.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries : Type
-- Lean.Meta.Tactic.SolveByElim
/-- Configuration structure to control the behaviour of `solve_by_elim`:
* transparency mode for calls to `apply`
* whether to use `symm` on hypotheses and `exfalso` on the goal as needed,
* see also `BacktrackConfig` for hooks allowing flow control.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig : Type
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonEmpty : Lean.FromJson Empty
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.limitCompWhiskeringRightIsoLimitComp.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [inst_5 : CategoryTheory.Limits.PreservesLimitsOfShape J F]
  (G : CategoryTheory.Functor J (CategoryTheory.Functor C D)),
  CategoryTheory.limitCompWhiskeringRightIsoLimitComp F G =
    (CategoryTheory.preservesLimitIso ((CategoryTheory.Functor.whiskeringRight C D E).obj F) G).symm
-- Mathlib.Algebra.Module.ZMod
/-- The `ZMod n`-module structure on commutative monoids whose elements have order dividing `n ≠ 0`.
Also implies a group structure via `Module.addCommMonoidToAddCommGroup`.
See note [reducible non-instances].  -/
AddCommMonoid.zmodModule : {n : ℕ} → {M : Type u_1} → [NeZero n] → [inst : AddCommMonoid M] → (∀ (x : M), n • x = 0) → Module (ZMod n) M
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Formal Taylor series associated to a function within a set.  -/
ftaylorSeriesWithin : (𝕜 : Type u) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E → F) → Set E → E → FormalMultilinearSeries 𝕜 E F
-- Mathlib.RingTheory.Localization.Defs
Localization.monoidOf_eq_algebraMap : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (x : R),
  (Localization.monoidOf M) x = (algebraMap R (Localization M)) x
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_one_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left),
  CategoryTheory.ComposableArrows.Precomp.map F f 1 1 ⋯ = F.map (CategoryTheory.CategoryStruct.id ⟨0, ⋯⟩)
-- Mathlib.Order.SupIndep
sSupIndep.eq_1 : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sSupIndep s = ∀ ⦃a : α⦄, a ∈ s → Disjoint a (sSup (s \ {a}))
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.inradius_pos : ∀ {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), 0 < s.inradius
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.merge_eq_mergeTR : @List.merge = @List.MergeSort.Internal.mergeTR
-- Lean.Data.Json.FromToJson.Basic
Lean.Prod.fromJson? : {α : Type u} → {β : Type v} → [Lean.FromJson α] → [Lean.FromJson β] → Lean.Json → Except String (α × β)
-- Init.Data.UInt.Lemmas
UInt8.toFin_toUSize : ∀ (n : UInt8), n.toUSize.toFin = Fin.castLE UInt8.size_le_usizeSize n.toFin
-- Lean.Widget.TaggedText
Lean.Widget.instFromJsonTaggedText.fromJson : {α : Type} → [Lean.FromJson α] → Lean.Json → Except String (Lean.Widget.TaggedText α)
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
/-- The cone associated to the weak pullback of `f` and `g`  -/
CategoryTheory.Limits.weakPullback.cone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) → (g : Y ⟶ Z) → [CategoryTheory.Limits.HasWeakPullback f g] → CategoryTheory.Limits.PullbackCone f g
-- Init.Data.String.Lemmas.FindPos
_private.Init.Data.String.Lemmas.FindPos.0.String.Slice.Pos.prevn.eq_def : ∀ {s : String.Slice} (p : s.Pos) (n : ℕ),
  p.prevn n =
    match n with
    | 0 => p
    | n.succ => if h : p ≠ s.startPos then (p.prev h).prevn n else p
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instSecondCountableTopology : ∀ {M : Type u_1} [inst : TopologicalSpace M] [SecondCountableTopology M], SecondCountableTopology Mᵈᵐᵃ
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- Adding an edge increases the clique number by at most one.  -/
SimpleGraph.CliqueFree.sup_edge : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ},
  G.CliqueFree n → ∀ (v w : α), (G ⊔ SimpleGraph.edge v w).CliqueFree (n + 1)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwLemma.mk : Mathlib.Tactic.ClickSuggestions.Premise → Bool → Lean.Name → Mathlib.Tactic.ClickSuggestions.GrwLemma
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).H = c.pt
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.eq_1 : ∀ (𝕜 : Type u) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (x : E),
  ContDiffWithinAt 𝕜 none f s x =
    ∃ u ∈ nhdsWithin x (insert x s), ∃ p, HasFTaylorSeriesUpToOn ⊤ f p u ∧ ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} {φ₁ φ₂ : R ⟶ R'}, φ₁.f = φ₂.f → φ₁ = φ₂
-- Mathlib.Data.Finset.Sups
Finset.map_sups : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : SemilatticeSup α] [inst_3 : SemilatticeSup β] [inst_4 : FunLike F α β] [SupHomClass F α β] (f : F)
  (hf : Function.Injective ⇑f) (s t : Finset α),
  Finset.map { toFun := ⇑f, inj' := hf } (s ⊻ t) =
    Finset.map { toFun := ⇑f, inj' := hf } s ⊻ Finset.map { toFun := ⇑f, inj' := hf } t
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ℝ≥0∞`,
then the distance from `f 0` to the limit is bounded by `∑'_{k=0}^∞ d k`.  -/
edist_le_tsum_of_edist_le_of_tendsto₀ : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ ∑' (m : ℕ), d m
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_ext : ∀ {R S : CommSemiRingCat} {f g : R ⟶ S}, CommSemiRingCat.Hom.hom f = CommSemiRingCat.Hom.hom g → f = g
-- Mathlib.Topology.Order.LeftRightNhds
/-- **Alias** of `countable_setOfPred_isolated_right_within`.

---

The set of points in a set which are isolated on the right in this set is countable when the
space is second-countable.  -/
countable_setOf_isolated_right_within : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α}, {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable
-- Mathlib.CategoryTheory.Products.Basic
/-- `sectL C Z` is the functor `C ⥤ C × D` given by `X ↦ (X, Z)`.  -/
CategoryTheory.Prod.sectL : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → D → CategoryTheory.Functor C (C × D)
-- Mathlib.Topology.Basic
isClosed_compl_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed sᶜ ↔ IsOpen s
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.toZModPow.eq_1 : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (n : ℕ),
  PadicInt.toZModPow n = PadicInt.toZModHom (p ^ n) (fun x => x.appr n) ⋯ ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insertRatUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (f.insertRatUnits units).1.assignments.size = f.assignments.size
-- Lean.Parser.Term
Lean.Parser.Term.scientific : Lean.Parser.Parser
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.lintegral_prodMkRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : α × γ) (g : β → ENNReal),
  ∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.prodMkRight γ κ) ca = ∫⁻ (b : β), g b ∂κ ca.1
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The `u` coefficient of an admissible linear change of variables, which must be a unit.  -/
WeierstrassCurve.VariableChange.u : {R : Type u} → [inst : CommRing R] → WeierstrassCurve.VariableChange R → Rˣ
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setLIntegral_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {f : β × Ω → ENNReal},
  Measurable f →
    ∀ (a : α) {s : Set β},
      MeasurableSet s →
        ∀ {t : Set Ω},
          MeasurableSet t →
            ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
              ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂κ a
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- The `Derivation` associated with the ring.  -/
Differential.deriv : {R : Type u_1} → {inst : CommRing R} → [self : Differential R] → Derivation ℤ R R
-- Mathlib.MeasureTheory.Measure.Lebesgue.Complex
Complex.measurableEquivPi.eq_1 : Complex.measurableEquivPi = Complex.basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.text : Lean.Lsp.DocumentHighlightKind
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany?_eq_some : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {n : ℕ} {a : α},
  Std.PRange.succMany? n a = some (Std.PRange.succMany n a)
-- Mathlib.Combinatorics.Graph.Basic
Graph.mk : {α : Type u_3} →
  {β : Type u_4} →
    (vertexSet : Set α) →
      (IsLink : β → α → α → Prop) →
        (edgeSet : Set β) →
          (∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm (IsLink e)) →
            (∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w) →
              autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam →
                autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) Graph.left_mem_of_isLink._autoParam →
                  Graph α β
-- Mathlib.Topology.Homeomorph.Lemmas
/-- An embedding restricts to a homeomorphism between the preimage and any subset of its range.  -/
Topology.IsEmbedding.homeomorphOfSubsetRange : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f : X → Y} → Topology.IsEmbedding f → {s : Set Y} → s ⊆ Set.range f → ↑(f ⁻¹' s) ≃ₜ ↑s
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat'.eq_1 : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (aig : Std.Sat.AIG α),
  aig.relabelNat' =
    (Std.Sat.AIG.relabel
        (fun x =>
          match (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[x]? with
          | some var => var
          | none => 0)
        aig,
      Std.Sat.AIG.RelabelNat.State.ofAIG aig)
-- Mathlib.Probability.Moments.Variance
/-- **Alias** of `ProbabilityTheory.evariance_ne_top`. -/
MeasureTheory.MemLp.evariance_ne_top : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ → ProbabilityTheory.evariance X μ ≠ ⊤
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_iff_eq : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, y ∈ PiNat.cylinder x n ↔ PiNat.cylinder y n = PiNat.cylinder x n
-- Init.Notation
/-- `p,+` is shorthand for `sepBy1(p, ",")`. It parses 1 or more occurrences of
`p` separated by `,`, that is: `p | p,p | p,p,p | ...`.

It produces a `nullNode` containing a `SepArray` with the interleaved parser
results. It has arity 1, and auto-groups its component parser if needed.
 -/
«stx_,+» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.ChainOfDivisors
associatesEquivOfUniqueUnits.congr_simp : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : Subsingleton αˣ],
  associatesEquivOfUniqueUnits = associatesEquivOfUniqueUnits
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_comp_toAlgHom : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A),
  (MvPolynomial.aevalTower g y).comp (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g
-- Mathlib.Analysis.Normed.Group.Constructions
norm_fst_le : ∀ {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : Norm F] (x : E × F), ‖x.1‖ ≤ ‖x‖
-- Lean.Meta.Basic
/-- Number of times a TC instance is used.  -/
Lean.Meta.Diagnostics.instanceCounter : Lean.Meta.Diagnostics → Lean.PHashMap Lean.Name ℕ
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_comp_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.fst.comp AddMonoid.Coprod.inr = 0
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff space is second countable.  -/
GromovHausdorff.instSecondCountableTopologyGHSpace : SecondCountableTopology GromovHausdorff.GHSpace
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.div : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α} {a₁ a₂ : α},
  HasProd f a₁ L → HasProd g a₂ L → HasProd (fun b => f b / g b) (a₁ / a₂) L
-- Mathlib.RingTheory.Ideal.Operations
Submodule.comap_smul_top_of_surjective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (I : Ideal R) (f : M →ₗ[R] N),
  Function.Surjective ⇑f → Submodule.comap f (I • ⊤) = I • ⊤ ⊔ f.ker
-- Init.Data.Int.Lemmas
Int.add_left_inj : ∀ {i j : ℤ} (k : ℤ), i + k = j + k ↔ i = j
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instBEqRange : BEq Lean.Lsp.Range
-- Init.Data.BitVec.Lemmas
BitVec.sub_self : ∀ {n : ℕ} (x : BitVec n), x - x = 0#n
-- Mathlib.FieldTheory.Galois.Profinite
_private.Mathlib.FieldTheory.Galois.Profinite.0.InfiniteGalois.toAlgEquivAux.congr_simp : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g g_1 : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop),
  g = g_1 → ∀ (a a_1 : K), a = a_1 → InfiniteGalois.toAlgEquivAux✝ g a = InfiniteGalois.toAlgEquivAux✝ g_1 a_1
-- Init.Data.UInt.Bitwise
USize.xor_left_inj : ∀ {a b : USize} (c : USize), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.Analysis.Normed.Group.Basic
norm_sub_le_norm_sub_add_norm_sub : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b c : E), ‖a - c‖ ≤ ‖a - b‖ + ‖b - c‖
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_injective : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n], Function.Injective Matrix.circulant
-- Init.Data.UInt.Lemmas
UInt8.toUSize_mul : ∀ (a b : UInt8), (a * b).toUSize = a.toUSize * b.toUSize % 256
-- Init.Prelude
/-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code.

It may look strange to have an axiom that says "every proposition is true",
since this is obviously unsound, but the `unsafe` marker ensures that the
kernel will not let this through into regular proofs. The lower levels of the
code generator don't need proofs in terms, so this is used to stub the proofs
out.
 -/
lcProof : ∀ {α : Prop}, α
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.incl_apply_mem_ker : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L) (x : M), E.incl x ∈ E.proj.ker
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- Constructor for morphisms in `SemiSimplexCategory` which takes as an input
a monomorphism in `SimplexCategory`.  -/
SemiSimplexCategory.homOfMono : {n m : SemiSimplexCategory} →
  (f : SemiSimplexCategory.toSimplexCategory.obj n ⟶ SemiSimplexCategory.toSimplexCategory.obj m) →
    [CategoryTheory.Mono f] → n ⟶ m
-- Mathlib.Topology.Separation.GDelta
instPerfectlyNormalSpaceElem : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [PerfectlyNormalSpace X], PerfectlyNormalSpace ↑s
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.id.eq_1 : ∀ (M : Type u_10) [inst : MulOne M], MonoidHom.id M = { toFun := fun x => x, map_one' := ⋯, map_mul' := ⋯ }