mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_replicate : ∀ {M : Type u_3} [inst : CommMonoid M] (n : ℕ) (a : M), (Multiset.replicate n a).prod = a ^ n
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_self : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), ⁅g, g⁆ = 0
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.coeff.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (k : ℤ)
  (h_1 :
    (a : ℤ) →
      (y : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a y p))
  (h_2 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k)),
  (match Int.Internal.Linear.Poly.num k with
    | Int.Internal.Linear.Poly.add a y p => h_1 a y p
    | Int.Internal.Linear.Poly.num k => h_2 k) =
    h_2 k
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ones_and : ∀ {w : ℕ} (a : BitVec w), -1#w &&& a = a
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entry.mk : Lean.MessageData →
  Option ℕ → ℕ → Mathlib.Explode.Status → Lean.MessageData → List (Option ℕ) → Bool → Mathlib.Explode.Entry
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ},
  f ∈ 𝒜 m →
    0 < m →
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f))
-- Mathlib.GroupTheory.Coset.Defs
/-- Right cosets are in bijection with left cosets.  -/
QuotientAddGroup.quotientRightRelEquivQuotientLeftRel : {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → Quotient (QuotientAddGroup.rightRel s) ≃ α ⧸ s
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.size_toArray_eq_length : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toArray.size = it.length
-- Mathlib.Geometry.Manifold.Submersion
/-- Being a submersion at `x` w.r.t. `F` is stable under replacing `F` by an isomorphic copy.  -/
Manifold.IsSubmersionAtOfComplement.congr_F : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {F' : Type u_6} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] [inst_9 : TopologicalSpace H]
  [inst_10 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11}
  {N : Type u_13} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H M] [inst_13 : TopologicalSpace N]
  [inst_14 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M} (e : F ≃L[𝕜] F'),
  Manifold.IsSubmersionAtOfComplement F I J n f x ↔ Manifold.IsSubmersionAtOfComplement F' I J n f x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forM.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}) (x : RBTree.RBNode α),
  RBTree.RBNode.forM f x =
    match x with
    | RBTree.RBNode.nil => pure PUnit.unit
    | RBTree.RBNode.node c l v r => do
      RBTree.RBNode.forM f l
      f v
      RBTree.RBNode.forM f r
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.linear_decompAffineEquiv : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q],
  (ContinuousAffineMap.decompAffineEquiv R S V Q).linear = ContinuousAffineMap.decompLinearEquiv R S V W
-- Lean.Level
Lean.Level.depthEx : Lean.Level → UInt32
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_eq_inf_of_isCoprime : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → I * J = I ⊓ J
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kextract.match_3.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List (Sigma β) → Sort u_3) →
      (x : List (Sigma β)) → (Unit → motive []) → ((s : Sigma β) → (l : List (Sigma β)) → motive (s :: l)) → motive x
-- Init.MetaTypes
Lean.NameGenerator.mk : Lean.Name → ℕ → Lean.NameGenerator
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.casesOn.eq_1 : ∀ {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (xs : FreeMonoid α) (one : motive 1)
  (of_mul : (x : α) → (xs : FreeMonoid α) → motive (FreeMonoid.of x * xs)),
  FreeMonoid.casesOn xs one of_mul = List.casesOn xs one of_mul
-- Mathlib.Algebra.Group.Center
Set.addCenter_eq_univ : ∀ (M : Type u_1) [inst : AddCommSemigroup M], Set.addCenter M = Set.univ
-- Init.Data.Int.Order
Int.toNat_eq_max : ∀ (a : ℤ), ↑a.toNat = max a 0
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_antitone : ∀ {X : Type u_1} (T : X → X) (F : Set X), Antitone fun U => Dynamics.coverEntropyEntourage T F U
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- **Alias** of `HahnSeries.leadingCoeff_mul_of_ne_zero`. -/
HahnSeries.leadingCoeff_mul_of_nonzero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R},
  x.leadingCoeff * y.leadingCoeff ≠ 0 → (x * y).leadingCoeff = x.leadingCoeff * y.leadingCoeff
-- Mathlib.Topology.Algebra.OpenSubgroup
IsTopologicalAddGroup.addNegClosureNhd.neg : ∀ {G : Type u_1} [inst : TopologicalSpace G] {T W : Set G} [inst_1 : AddGroup G],
  IsTopologicalAddGroup.addNegClosureNhd T W → -T = T
-- Init.Data.SInt.Lemmas
ISize.toInt16_sub : ∀ (a b : ISize), (a - b).toInt16 = a.toInt16 - b.toInt16
-- Aesop.Search.SearchM
Aesop.NormSimpContext.enabled : Aesop.NormSimpContext → Bool
-- Lean.Elab.Tactic.FalseOrByContra
/-- Changes the goal to `False`, retaining as much information as possible:

* If the goal is `False`, do nothing.
* If the goal is an implication or a function type, introduce the argument and restart.
  (In particular, if the goal is `x ≠ y`, introduce `x = y`.)
* Otherwise, for a propositional goal `P`, replace it with `¬ ¬ P`
  (attempting to find a `Decidable` instance, but otherwise falling back to working classically)
  and introduce `¬ P`.
* For a non-propositional goal use `False.elim`.
 -/
Lean.MVarId.falseOrByContra : Lean.MVarId → optParam (Option Bool) none → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates finite colimits, then `F.rightOp : C ⥤ Dᵒᵖ` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteLimits F.rightOp
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.trichotomous : ∀ {x : ZFSet.{u}}, x.IsOrdinal → Std.Trichotomous (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.Computability.RecursiveIn
RecursiveIn.oracle : ∀ {O : Set (ℕ →. ℕ)}, ∀ g ∈ O, RecursiveIn O g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.add_def : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] (P Q : W.Point),
  P + Q = P.add Q
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.State.mk.injEq : ∀ (cache cache_1 : Lean.PersistentExprMap Mathlib.Tactic.BicategoryLike.Mor₁),
  ({ cache := cache } = { cache := cache_1 }) = (cache = cache_1)
-- Mathlib.Data.Set.Card
Set.exists_ne_of_one_lt_encard : ∀ {α : Type u_1} {s : Set α}, 1 < s.encard → ∀ (a : α), ∃ b ∈ s, b ≠ a
-- Mathlib.Data.Quot
Trunc.instInhabited : {α : Sort u_1} → [Inhabited α] → Inhabited (Trunc α)
-- Mathlib.Order.SuccPred.CompleteLinearOrder
Order.IsSuccPrelimit.sSup_Iio : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {x : α}, Order.IsSuccPrelimit x → sSup (Set.Iio x) = x
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_4 : ∀ (a a_1 : SimplexCategory) (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star)
  (f₂_2 : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1),
  AugmentedSimplexCategory.tensorHom x f₂_2 = f₂_2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.getKey? a).isSome = true ↔ a ∈ t
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.derivedSeries_eq_top : ∀ (G : Type u_1) [inst : Group G] [Group.IsPerfect G] (n : ℕ), derivedSeries G n = ⊤
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- Isomorphic monoids have isomorphic monoid algebras.  -/
AddMonoidAlgebra.domCongrBialgEquiv : (R : Type u_1) →
  (A : Type u_3) →
    {M : Type u_8} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Bialgebra R A] →
              [inst_3 : AddMonoid M] →
                [inst_4 : AddMonoid N] → M ≃+ N → AddMonoidAlgebra A M ≃ₐc[R] AddMonoidAlgebra A N
-- Lean.Environment
/-- Creates fallback info to be used in case promises are dropped unfulfilled.  -/
_private.Lean.Environment.0.Lean.Environment.mkFallbackConstInfo : Lean.Name → Lean.ConstantKind → Lean.ConstantInfo
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Bound.one_lt_mul : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a b : M₀} [ZeroLEOneClass M₀] [PosMulMono M₀]
  [MulPosMono M₀], 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- Let `S` be a closed subalgebra of a Banach algebra `A`. If `a : S` is invertible in `A`,
and for all `x : S` sufficiently close to `a` within some filter `l`, `x` is invertible in `S`,
then `a` is invertible in `S` as well.  -/
Subalgebra.isUnit_of_isUnit_val_of_eventually : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] {l : Filter ↥S} {a : ↥S},
  IsUnit ↑a → l ≤ nhds a → (∀ᶠ (x : ↥S) in l, IsUnit x) → l.NeBot → IsUnit a
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.subtheoryModel_Carrier : ∀ {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T), ↑(M.subtheoryModel h) = ↑M
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_left_neg : ∀ {n : ℕ} {G : Type u_3} [inst : AddGroup G] (f : Fin (n + 1) → G),
  (f 0 +ᵥ Fin.partialSum fun i => -f i.castSucc + f i.succ) = f
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a signed measure `s` and a positive measurable set `i`, `toMeasureOfZeroLE`
provides the measure, mapping measurable sets `j` to `s (i ∩ j)`.  -/
MeasureTheory.SignedMeasure.toMeasureOfZeroLE : {α : Type u_1} →
  {m : MeasurableSpace α} →
    (s : MeasureTheory.SignedMeasure α) →
      (i : Set α) →
        MeasurableSet i →
          MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i → MeasureTheory.Measure α
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift.eq_1 : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M)
  (HN : N ≤ φ.ker), QuotientGroup.lift N φ HN = (QuotientGroup.con N).lift φ ⋯
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.homotopyEquiv_homotopyInvHomId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  (HomologicalComplex.pathObject.homotopyEquiv K hc).homotopyInvHomId =
    HomologicalComplex.pathObject.π₀CompιHomotopy K hc
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.instAddCommMonoid : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : TopologicalSpace R] → AddCommMonoid (StieltjesFunction R)
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.equiv_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (R' : Type u_6)
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [h : Algebra.IsPushout R S R' S'] (a : S) (b : R'),
  (Algebra.IsPushout.equiv R S R' S') (a ⊗ₜ[R] b) = (algebraMap S S') a * (algebraMap R' S') b
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- A version of `linearIndependent_iff` where the linear combination is a `Finset` sum
of a function with support contained in the `Finset`.  -/
linearIndependent_iff'' : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {v : ι → M},
  LinearIndependent R v ↔ ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_comp_eq_pullbackSymmetry : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j k : D.J),
  CategoryTheory.CategoryStruct.comp (D.t' j k i) (D.t' k i j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (D.f j k) (D.f j i)).hom
      (CategoryTheory.CategoryStruct.comp (D.t' j i k) (CategoryTheory.Limits.pullbackSymmetry (D.f i k) (D.f i j)).hom)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanLocationLink.toJson : Lean.Lsp.LeanLocationLink → Lean.Json
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- The infimum of an intersection of two sets is bounded below by the maximum of the
infima of each set, if all sets are bounded below and nonempty.  -/
le_csInf_inter : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s t : Set α},
  BddBelow s → BddBelow t → (s ∩ t).Nonempty → sInf s ⊔ sInf t ≤ sInf (s ∩ t)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.mk : Std.HashMap Lean.MVarId Lean.MVarId →
  Std.HashMap Lean.LMVarId Lean.LMVarId →
    Std.HashMap Lean.MVarId Lean.Expr → Std.HashMap Lean.MVarId Lean.Expr → Aesop.EqualUpToIdsM.State
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- Variant version of `IsCusp.of_isFiniteRelIndex`.  -/
IsCusp.of_isFiniteRelIndex_conj : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ} [𝒢.IsFiniteRelIndex ℋ],
  IsCusp c ℋ → ∀ {h : GL (Fin 2) ℝ}, h ∈ ℋ → IsCusp c (ConjAct.toConjAct h • 𝒢)
-- Mathlib.Combinatorics.Additive.FreimanHom
isAddFreimanIso_id : ∀ {α : Type u_2} [inst : AddCommMonoid α] {A : Set α} {n : ℕ}, IsAddFreimanIso n A A id
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.localInstances₁ : Aesop.EqualUpToIds.GoalContext → Lean.LocalInstances
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_apply_snd_fst : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (f : CategoryTheory.Arrow T),
  ((CategoryTheory.Arrow.equivSigma T) f).snd.fst = f.right
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The alternating face map complex, on morphisms  -/
AlgebraicTopology.AlternatingFaceMapComplex.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : CategoryTheory.SimplicialObject C} →
        (X ⟶ Y) →
          (AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ AlgebraicTopology.AlternatingFaceMapComplex.obj Y)
-- Std.Do.Triple.SpecLemmas
/-- Helper definition for specifying loop invariants for loops with early return.

`for ... in ...` loops with early return of type `γ` elaborate to a call like this:
```lean
forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody
```
Note that the first component of the `MProd` state tuple is the optional early return value.
It is `none` as long as there was no early return and `some r` if the loop returned early with `r`.

This function allows to specify different invariants for the loop body depending on whether the loop
terminated early or not. When there was an early return, the loop has effectively finished, which is
encoded by the additional `⌜pos = s.endPos⌝` assertion in the invariant. This assertion is vital for
successfully proving the induction step, as it contradicts with the assumption that
`pos ≠ s.endPos` of the inductive hypothesis at the start of the loop body, meaning that users
won't need to prove anything about the bogus case where the loop has returned early yet takes
another iteration of the loop body.
 -/
Std.Do.StringSliceInvariant.withEarlyReturn : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {γ : Type (max u₁ u₂)} →
      {s : String.Slice} →
        (s.Pos → β → Std.Do.Assertion ps) →
          (γ → β → Std.Do.Assertion ps) →
            optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false →
              Std.Do.StringSliceInvariant s (MProd (Option γ) β) ps
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.subgraphOfAdj_adj_self : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), (G.subgraphOfAdj h).Adj u v
-- Mathlib.Data.Set.Card
Set.toENat_cardinalMk_subtype : ∀ {α : Type u_1} (P : α → Prop), Cardinal.toENat (Cardinal.mk { x // P x }) = {x | P x}.encard
-- Mathlib.Tactic.Linter.TextBased
/-- The bare string "Adaptation note" (or variants thereof):
instead, the `#adaptation_note` command should be used.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.adaptationNote : Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_pi : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {ι : Type u_3}
  (f : ι → R → R) (a : A) (ha : autoParam (p a) cfcₙ_apply_pi._auto_1)
  (hf : autoParam (∀ (i : ι), ContinuousOn (f i) (quasispectrum R a)) cfcₙ_apply_pi._auto_3)
  (hf0 : autoParam (∀ (i : ι), f i 0 = 0) cfcₙ_apply_pi._auto_5),
  (fun i => cfcₙ (f i) a) = fun i =>
    (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }
-- Batteries.Data.List.Pairwise
List.pwFilter.congr_simp : ∀ {α : Type u_1} (R R_1 : α → α → Prop),
  R = R_1 →
    ∀ {inst : DecidableRel R} [inst_1 : DecidableRel R_1] (l l_1 : List α),
      l = l_1 → List.pwFilter R l = List.pwFilter R_1 l_1
-- Init.Data.Iterators.PostconditionMonad
/-- A predicate that holds for the return value(s) of the `m`-monadic operation.
 -/
Std.Iterators.PostconditionT.Property : {m : Type w → Type w'} → {α : Type w} → Std.Iterators.PostconditionT m α → α → Prop
-- Lean.Data.Json.Printer
/-- This table contains for each UTF-8 byte whether we need to escape a string that contains it.
 -/
_private.Lean.Data.Json.Printer.0.Lean.Json.escapeTable : { xs // xs.size = 256 }
-- Lean.Elab.Open
Lean.Elab.OpenDecl.elabOpenDecl : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadExceptOf Lean.Exception m] →
        [Lean.MonadRef m] →
          [Lean.AddMessageContext m] →
            [MonadLiftT (ST IO.RealWorld) m] →
              [Lean.MonadLog m] →
                [Lean.MonadOptions m] →
                  [Lean.MonadResolveName m] →
                    [Lean.Elab.MonadInfoTree m] → Lean.TSyntax `Lean.Parser.Command.openDecl → m (List Lean.OpenDecl)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {f : ℤ → M},
  (Multipliable fun n => f ↑n) → (Multipliable fun n => f (-(↑n + 1))) → Multipliable f
-- Init.Data.Range.Polymorphic.Iterators
Std.Rco.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId : {α : Type u} →
  {m : Type u → Type u_1} →
    [inst : Std.PRange.UpwardEnumerable α] →
      [inst_1 : LE α] →
        [inst_2 : LT α] →
          [inst_3 : DecidableLT α] →
            [Std.PRange.LawfulUpwardEnumerable α] →
              [Std.PRange.LawfulUpwardEnumerableLE α] →
                [Std.PRange.LawfulUpwardEnumerableLT α] →
                  [Monad m] → [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] → ForIn' m (Std.Rco α) α inferInstance
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G),
  (P.coconePointsIsoOfNatIso Q w).hom = P.map t w.hom
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.mk.injEq : ∀ (toGrp : GrpCat) [isFinite : Finite ↑toGrp] (toGrp_1 : GrpCat) (isFinite_1 : Finite ↑toGrp_1),
  ({ toGrp := toGrp, isFinite := isFinite } = { toGrp := toGrp_1, isFinite := isFinite_1 }) = (toGrp = toGrp_1)
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.mk : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1},
  autoParam (AEMeasurable X P) ProbabilityTheory.HasLaw.aemeasurable._autoParam →
    MeasureTheory.Measure.map X P = μ → ProbabilityTheory.HasLaw X μ P
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_mapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) (hf : Function.Injective f)
  (l : α →₀ M), Finsupp.comapDomain f (Finsupp.mapDomain f l) ⋯ = l
-- Mathlib.Logic.Relation
Relation.EqvGen.eqvGen_transGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.EqvGen (Relation.TransGen r) = Relation.EqvGen r
-- Mathlib.Order.Closure
/-- The set of closed elements has a Galois insertion to the underlying type.  -/
ClosureOperator.gi : {α : Type u_1} → [inst : PartialOrder α] → (c : ClosureOperator α) → GaloisInsertion c.toCloseds Subtype.val
-- Init.Data.Vector.Lemmas
Vector.size_eq_one : ∀ {α : Type u_1} {xs : Vector α 1}, ∃ a, xs = #v[a]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
StarAlgebra.elemental.continuous_characterSpaceToSpectrum : ∀ {A : Type u_1} [inst : CStarAlgebra A] (x : A), Continuous (StarAlgebra.elemental.characterSpaceToSpectrum x)
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
_private.Mathlib.Combinatorics.SetFamily.KruskalKatona.0.Finset.UV.familyMeasure.eq_1 : ∀ {n : ℕ} (𝒜 : Finset (Finset (Fin n))), Finset.UV.familyMeasure✝ 𝒜 = ∑ A ∈ 𝒜, ∑ a ∈ A, 2 ^ ↑a
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
MeasureTheory.VectorMeasure.enorm_apply_le_semivariation : ∀ {X : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mX : MeasurableSpace X}
  {μ : MeasureTheory.VectorMeasure X E} {s : Set X}, ‖μ s‖ₑ ≤ μ.semivariation s