mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.DocString.Markdown
/-- Finds a docstring without performing any alias resolution or enrichment with extra metadata. The
result is rendered as Markdown.

Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
 -/
Lean.findSimpleDocString? : Lean.Environment →
  Lean.Name →
    optParam Bool true →
      optParam Lean.Options ∅ →
        optParam Lean.Name Lean.Name.anonymous →
          optParam (List Lean.OpenDecl) [] → optParam (Option IO.CancelToken) none → IO (Option String)
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.image_toSnowflaking_closedEBall`. -/
Metric.Snowflaking.image_toSnowflaking_emetricClosedBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking '' Metric.closedEBall x r =
    Metric.closedEBall (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Lean.Meta.Tactic.Util
/-- Get the type of the given metavariable.  -/
Lean.MVarId.getType : Lean.MVarId → Lean.MetaM Lean.Expr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.size.eq_1 : ∀ {α : Type u} [inst : Std.Rxc.HasSize α] (r : Std.Rcc α), r.size = Std.Rxc.HasSize.size r.lower r.upper
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegrable_congr_uIoo : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {g : ℝ → ε},
  Set.EqOn f g (Set.uIoo a b) → (IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b)
-- Mathlib.Tactic.NormNum.NatSqrt
/-- Evaluates the `Nat.sqrt` function.  -/
Mathlib.Meta.NormNum.evalNatSqrt : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.orderBot : {α : Type u_1} → [inst : Preorder α] → {a : α} → OrderBot { x // a ≤ x }
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.seq.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A), H.seq f 0 = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_sInf : ∀ {α : Type u_1} {ms : Set (MeasurableSpace α)} {s : Set α}, MeasurableSet s ↔ ∀ m ∈ ms, MeasurableSet s
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain K F m),
  α = α_1 →
    ∀ (β β_1 : CochainComplex.HomComplex.Cochain K G n),
      β = β_1 →
        ∀ (h : n + 1 = m) (T : CochainComplex.HomComplex.Triplet n),
          CochainComplex.mappingCone.liftCochain φ α β h T = CochainComplex.mappingCone.liftCochain φ α_1 β_1 h T
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H1CoresCoinf_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal],
  (groupHomology.H1CoresCoinf A S).g = groupHomology.map (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S) 1
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- **Alias** of `MeasureTheory.sdiff_ae_eq_self`. -/
MeasureTheory.diff_ae_eq_self : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s \ t =ᵐ[μ] s ↔ μ (s ∩ t) = 0
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
/-- The entropy of `φ '' F` is at most the entropy of `F` if `φ` is uniformly continuous. This
version uses a `liminf`.  -/
Dynamics.coverEntropyInf_image_le_of_uniformContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    UniformContinuous φ → ∀ (F : Set X), Dynamics.coverEntropyInf T (φ '' F) ≤ Dynamics.coverEntropyInf S F
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.of_smul_isIntegral : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {z : A} {y : R},
  ¬IsNilpotent y → IsIntegral R (y • z) → IsAlgebraic R z
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_def : ∀ {α : Type u_1} (s : Set α), sᶜ = {x | x ∉ s}
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Given isomorphisms `f : G ≃g G'` and `g : H ≃g H'`, returns an isomorphism from `G ⊕g H` to
`G' ⊕g H'` that applies `f` to the left component and `g` to the right component.  -/
SimpleGraph.Iso.sumCongr : {V : Type u_3} →
  {V' : Type u_4} →
    {W : Type u_5} →
      {W' : Type u_6} →
        {G : SimpleGraph V} →
          {H : SimpleGraph W} → {G' : SimpleGraph V'} → {H' : SimpleGraph W'} → G ≃g G' → H ≃g H' → G ⊕g H ≃g G' ⊕g H'
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.comap_equiv_eq_map_symm : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R ≃+* S)
  (K : NonUnitalSubring S), NonUnitalSubring.comap (↑f) K = NonUnitalSubring.map f.symm K
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A trivial vector bundle, in which the model fiber has an inner product,
is a Riemannian bundle.  -/
instIsContinuousRiemannianBundleTrivial : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_4} [inst_1 : NormedAddCommGroup F₁]
  [inst_2 : InnerProductSpace ℝ F₁], IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.primaryComponent.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G] (p : ℕ),
  AddCommGroup.primaryComponent G p = { toAddSubmonoid := AddCommMonoid.primaryComponent G p, neg_mem' := ⋯ }
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_succ' : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M) (n : ℕ) (x : α),
  birkhoffSum f g (n + 1) x = g x + birkhoffSum f g n (f x)
-- Mathlib.Tactic.FBinop
/-- Leaf of the tree. Stores the generated `InfoTree` from elaborating `val`.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.term : Lean.Syntax → Lean.PersistentArray Lean.Elab.InfoTree → Lean.Expr → FBinopElab.Tree✝
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.toEquiv_comp : ∀ {X Y Z : Type u} (f : X ≅ Y) (g : Y ≅ Z), (f ≪≫ g).toEquiv = f.toEquiv.trans g.toEquiv
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augmentOfIsTerminal_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T), (X.augmentOfIsTerminal hT).right = T
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Minute.Offset n
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.forall_apply_eq_apply_iff : ∀ (G : Type u_1) {M : Type u_2} [inst : CommGroup G] [Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] {g g' : G}, (∀ (φ : G →* Mˣ), φ g = φ g') ↔ g = g'
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.reindex.eq_1 : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11}
  (l : Combinatorics.Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι'),
  l.reindex eη eα eι = { idxFun := fun i => Sum.map (⇑eα) (⇑eη) (l.idxFun (eι.symm i)), proper := ⋯ }
-- Aesop.Forward.Match.Types
Aesop.instInhabitedCompleteMatch : Inhabited Aesop.CompleteMatch
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃), LinearMap.snd R M₂ M₃ ∘ₗ f.prod g = g
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateR.eq_2 : ∀ {α : Type u_1} (x : α) (x_1 : Ordnode α), Ordnode.nil.rotateR x x_1 = Ordnode.nil.node' x x_1
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestSimpTrace : Lean.Elab.Tactic.Try.TryTactic
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] (k : α) (f : β → β) (l : List ((_ : α) × β)),
  (Std.Internal.List.Const.modifyKey k f l).isEmpty = l.isEmpty
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- Isomorphic algebras have isomorphic localizations.

See `localAlgEquiv` for a variant where the base ring is not localized.  -/
Localization.localAlgEquiv' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              (I : Ideal R) →
                [hI : I.IsPrime] →
                  [inst_4 : Algebra R P] →
                    (J : Ideal S) →
                      (K : Ideal P) →
                        [inst_5 : J.IsPrime] →
                          [inst_6 : K.IsPrime] →
                            [inst_7 : J.LiesOver I] →
                              [inst_8 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] →
                                [Localization.AtPrime.IsLiesOverAlgebra I J] →
                                  [inst_10 : K.LiesOver I] →
                                    [inst_11 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)] →
                                      [Localization.AtPrime.IsLiesOverAlgebra I K] →
                                        (f : S ≃ₐ[R] P) →
                                          J = Ideal.comap f K →
                                            Localization.AtPrime J ≃ₐ[Localization.AtPrime I] Localization.AtPrime K
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.toExpr : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Expr
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sdiff_eq_sum_sdiff_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M},
  ∑ i ∈ s \ t, f i = ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i = ∑ i ∈ t, f i
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Also see `LinearIndependent.pair_iff'` for a simpler version over fields.  -/
LinearIndependent.pair_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bindOnSupport_apply : ∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (b : β),
  (p.bindOnSupport f) b = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x : E}, 0 ≤ RCLike.re (inner 𝕜 x x)
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturalityᵣ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n n' : M}
  (g : n ⟶ n') (X : C) [inst_3 : F.OplaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      ((F.map g).app ((F.obj m).obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m g)).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.δ F m n').app X)
-- Lean.Meta.Transform
Lean.instInhabitedTransformStep.default : Lean.TransformStep
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.subsingleton_quotient_top : ∀ {G : Type u} [inst : Group G], Subsingleton (G ⧸ ⊤)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Normed group structure constructed from an `InnerProductSpace.Core` structure  -/
InnerProductSpace.Core.toNormedAddCommGroup : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [cd : InnerProductSpace.Core 𝕜 F] → NormedAddCommGroup F
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.abs_ceil_sub_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] {a : R},
  0 ≤ a → |↑⌈a⌉₊ - a| ≤ 1
-- Mathlib.Algebra.Polynomial.RuleOfSigns
/-- If P's coefficients start with signs `[+, -, ...]`, then multiplying by a binomial `X - η`
commutes with `eraseLead` in the number of sign changes. This is because the product of
`P` and `X - η` has the pattern `[+, -, ...]` as well, so then `P.eraseLead` starts with
`[-,...]`, and multiplying by `X - η` gives `[-, ...]` too.  -/
Polynomial.signVariations_eraseLead_mul_X_sub_C : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {P : Polynomial R} {η : R},
  0 < η →
    0 < P.leadingCoeff →
      P.nextCoeff < 0 →
        ((Polynomial.X - Polynomial.C η) * P).eraseLead.signVariations =
          ((Polynomial.X - Polynomial.C η) * P.eraseLead).signVariations
-- Init.Data.UInt.Lemmas
UInt8.zero_le : ∀ {a : UInt8}, 0 ≤ a
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.trailingCoeff_mul : ∀ {R : Type u_2} [inst : Semiring R] [NoZeroDivisors R] (p q : Polynomial R),
  (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- The preimage of a finitely generated normal subgroup by a surjective additive
homomorphism with a finitely generated kernel is finitely generated.  -/
AddSubgroup.IsFinitelyNormallyGenerated.comap : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {N : AddSubgroup H},
  N.IsFinitelyNormallyGenerated →
    ∀ {f : G →+ H},
      Function.Surjective ⇑f → f.ker.IsFinitelyNormallyGenerated → (AddSubgroup.comap f N).IsFinitelyNormallyGenerated
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_c₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {A : Type v} [inst_1 : CommRing A] (f : R →+* A),
  (W.map f).c₆ = f W.c₆
-- Mathlib.Topology.Bornology.Constructions
instBornologyMultiplicative : {α : Type u_1} → [Bornology α] → Bornology (Multiplicative α)
-- Mathlib.Algebra.Algebra.Defs
/-- The canonical ring homomorphism `algebraMap R A : R →+* A` for any `R`-algebra `A`,
packaged as an `R`-linear map.
 -/
RingTheory.LinearMap.«termη[_]» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isOpen_range : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f], IsOpen (Set.range ⇑f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β}
  {hc : k ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKey k hc = k
-- Mathlib.Order.Part
Antitone.partSeq : ∀ {α : Type u_1} [inst : Preorder α] {β γ : Type u_4} {f : α → Part (β → γ)} {g : α → Part β},
  Antitone f → Antitone g → Antitone fun x => f x <*> g x
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.target : Aesop.IndexMatchLocation
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₂_X_right : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S) (i : σ), (MvPolynomial.bind₂ f) (MvPolynomial.X i) = MvPolynomial.X i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_eq_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {he : t ≠ ∅}, t.maxKey he = t.maxKey!
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
/-- The fiber of multiplication at `x`: all pairs `(a, b)` with `a * b = x`.  -/
DiscreteConvolution.mulFiber : {M : Type u_1} → [Monoid M] → M → Set (M × M)
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.downMulHom.eq_1 : ∀ (G : Type u) [inst : Mul G], downMulHom✝ G = { toFun := ULift.down, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.prodMk_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {f : α × β → X},
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    ∀ᵐ (y : β) ∂ν, MeasureTheory.AEStronglyMeasurable (fun x => f (x, y)) μ
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isBounded_iff_subset_smul_ball : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instMonoidHomClassMulHom_1 : ∀ {M : Type u_10} {N : Type u_11} [inst : Monoid M] [inst_1 : RightCancelMonoid N], MonoidHomClass (M →ₙ* N) M N
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.invertible_mk'_one : {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] → (s : ↥M) → Invertible (IsLocalization.mk' S 1 s)
-- Mathlib.Data.List.Enum
/-- Variant of `forall_mem_zipIdx` with the `zipIdx` argument specialized to `0`.  -/
List.forall_mem_zipIdx' : ∀ {α : Type u_1} {l : List α} {p : α × ℕ → Prop}, (∀ x ∈ l.zipIdx, p x) ↔ ∀ (i : ℕ) (x : i < l.length), p (l[i], i)
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.sum_incMatrix_apply : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : NonAssocSemiring R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a : α} [inst_3 : Fintype (Sym2 α)] [inst_4 : Fintype ↑(G.neighborSet a)],
  ∑ e, SimpleGraph.incMatrix R G a e = ↑(G.degree a)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if a set `s` is closed when `f ⁻¹' s` is
closed for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
uCompactlyGeneratedSpace_of_isClosed : ∀ {X : Type w} [tX : TopologicalSpace X],
  (∀ (s : Set X), (∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)) → IsClosed s) →
    UCompactlyGeneratedSpace X
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.insertIdxTR.go.eq_def : ∀ {α : Type u_1} (a : α) (a_1 : ℕ) (a_2 : List α) (a_3 : Array α),
  List.insertIdxTR.go✝ a a_1 a_2 a_3 =
    match a_1, a_2, a_3 with
    | 0, l, acc => acc.toListAppend (a :: l)
    | x, [], acc => acc.toList
    | n.succ, a_4 :: l, acc => List.insertIdxTR.go✝ a n l (acc.push a_4)
-- Init.Data.Vector.Zip
Vector.zipWith_map : ∀ {γ : Type u_1} {δ : Type u_2} {α : Type u_3} {β : Type u_4} {n : ℕ} {μ : Type u_5} {f : γ → δ → μ} {g : α → γ}
  {h : β → δ} {as : Vector α n} {bs : Vector β n},
  Vector.zipWith f (Vector.map g as) (Vector.map h bs) = Vector.zipWith (fun a b => f (g a) (h b)) as bs
-- Mathlib.Data.NNRat.Lemmas
Rat.toNNRat_inv : ∀ (q : ℚ), q⁻¹.toNNRat = q.toNNRat⁻¹
-- Mathlib.Topology.Algebra.Monoid
AddSubmonoid.top_closure_add_self_eq : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [SeparatelyContinuousAdd M] (s : AddSubmonoid M),
  closure ↑s + closure ↑s = closure ↑s
-- Mathlib.LinearAlgebra.Basis.SMul
/-- Given a basis `v` and a map `w` such that for all `i`, `w i` are elements of a group,
`groupSMul` provides the basis corresponding to `w • v`.  -/
Module.Basis.groupSMul : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {G : Type u_5} →
              [inst_3 : Group G] →
                [inst_4 : DistribMulAction G R] →
                  [inst_5 : DistribMulAction G M] →
                    [IsScalarTower G R M] → [SMulCommClass G R M] → Module.Basis ι R M → (ι → G) → Module.Basis ι R M
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- If a measure `μ` on a quotient satisfies `QuotientMeasureEqMeasurePreimage` with respect to a
sigma-finite measure `ν`, then it is itself `SigmaFinite`.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  [i : MeasureTheory.SigmaFinite ν] [i' : MeasureTheory.HasFundamentalDomain G α ν]
  (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ],
  MeasureTheory.SigmaFinite μ
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- Construct a term of `SimpleGraph.Coloring` using a function that
assigns vertices to colors and a proof that it is as proper coloring.

(Note: this is a definitionally the constructor for `SimpleGraph.Hom`,
but with a syntactically better proper coloring hypothesis.)
 -/
SimpleGraph.Coloring.mk : {V : Type u} →
  {G : SimpleGraph V} → {α : Type u_2} → (color : V → α) → (∀ {v w : V}, G.Adj v w → color v ≠ color w) → G.Coloring α
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.uppcRec.match_1.eq_2 : ∀ {w : ℕ} (motive : (s : ℕ) → s < w → Sort u_1) (i : ℕ) (hs : i + 1 < w) (h_1 : (hs : 0 < w) → motive 0 hs)
  (h_2 : (i : ℕ) → (hs : i + 1 < w) → motive i.succ hs),
  (match i.succ, hs with
    | 0, hs => h_1 hs
    | i.succ, hs => h_2 i hs) =
    h_2 i hs
-- Std.Data.TreeMap.Raw.Iterator
Std.TreeMap.Raw.toList_iter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Std.TreeMap.Raw α β cmp), m.iter.toList = m.toList
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_anti : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s t : Set M}, t ⊆ s → PointedCone.dual p s ≤ PointedCone.dual p t
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_union_closure_right_eq : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α), M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.inv_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal],
  CategoryTheory.inv (CategoryTheory.Functor.LaxMonoidal.ε F) = CategoryTheory.Functor.OplaxMonoidal.η F
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.co : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound →
  Lean.Meta.Grind.Arith.Cutsat.SymbolicBound → Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_tryCatch_ReaderT_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u_3} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {ρ α : Type u} {post : α → ρ → Pred}
  {epost : EPred} (x : ReaderT ρ m α) (h : ε → ReaderT ρ m α),
  Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) post epost = fun r =>
    Std.Internal.Do.wp (MonadExceptOf.tryCatch (x.run r) fun e => (h e).run r) (fun a => post a r) epost
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheaf_isSheaf : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C],
  (skyscraperPresheaf p₀ A).IsSheaf