mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Complex.Basic
Complex.conj_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (starRingEnd ℂ) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.isFractionRing_ofField : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K], IsFractionRing (↥(Localization.subalgebra.ofField K S hS)) K
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.abs_im_pow_eventuallyLE_exp_re : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → ∀ (n : ℕ), (fun z => |z.im| ^ n) ≤ᶠ[l] fun z => Real.exp z.re
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.code.injEq : ∀ (ctx : Lean.Elab.ContextInfo) (infos : Std.TreeMap ℕ Lean.Elab.Info compare) (ctx_1 : Lean.Elab.ContextInfo)
  (infos_1 : Std.TreeMap ℕ Lean.Elab.Info compare),
  (Lean.Widget.EmbedFmt.code✝ ctx infos = Lean.Widget.EmbedFmt.code✝ ctx_1 infos_1) = (ctx = ctx_1 ∧ infos = infos_1)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_self'' : ∀ {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 : ↥M}, IsLocalization.mk' S (↑x) x = 1
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_one_sub : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddGroup R] (f : ι → R),
  (Function.mulSupport fun x => 1 - f x) = Function.support f
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv)
      (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv
          (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)))
-- Std.Data.Internal.List.Associative
Std.Internal.List.List.getValue?_filter_containsKey_of_containsKey_eq_false_left : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₁ = false →
      Std.Internal.List.getValue? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = none
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.instInhabited : (α : Type u_2) → [inst : CompleteLattice α] → Inhabited (FrameHom α α)
-- Mathlib.Data.Set.Functor
/-- **Alias** of `Set.image_coe_eq_domRestrict_image`. -/
Set.image_coe_eq_restrict_image : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {δ : Type u_1} {f : α → δ},
  (f '' do
      let a ← γ
      pure ↑a) =
    β.domRestrict f '' γ
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getDₘ_eq_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} {fallback : β k},
  t.Ordered → Std.DTreeMap.Internal.Impl.getDₘ k t fallback = Std.Internal.List.getValueCastD k t.toListModel fallback
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_zero_le : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] (h0 : 0 < Ordinal.type r) (a : α),
  ¬r a ((Ordinal.enum r) ⟨0, h0⟩)
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instCompleteSemilatticeInf.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instCompleteSemilatticeInf =
    { toPartialOrder := inferInstance, toInfSet := inferInstance, isGLB_sInf := ⋯ }
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- **Alias** of `OrdinalApprox.gfpApprox_anti_right`. -/
OrdinalApprox.gfpApprox_antitone : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, Antitone (OrdinalApprox.gfpApprox f x)
-- Init.Data.Bool
Bool.cond_true_left : ∀ (c f : Bool), (bif c then true else f) = (c || f)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fromProd_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B),
  ((CategoryTheory.Comma.fromProd L R).obj X).right = X.2
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix.eq_1 : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : AddGroupWithOne R],
  SimpleGraph.lapMatrix R G = SimpleGraph.degMatrix R G - SimpleGraph.adjMatrix R G
-- Mathlib.MeasureTheory.OuterMeasure.AE
Set.mulIndicator_ae_eq_one : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {M : Type u_4} [inst_2 : One M] {f : α → M} {s : Set α},
  s.mulIndicator f =ᵐ[μ] 1 ↔ μ (s ∩ Function.mulSupport f) = 0
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.instIsClosedUnderSubobjectsIsNoetherianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.isNoetherianObject.IsClosedUnderSubobjects
-- Init.Data.Array.Int
Array.le_sum_div_length_of_min?_eq_some_int : ∀ {x : ℤ} {xs : Array ℤ}, xs.min? = some x → x ≤ xs.sum / ↑xs.size
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropEndWhile_iff_takeEndWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  (s.dropEndWhile pat).isEmpty = true ↔ s.takeEndWhile pat = s
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.of_isNoetherian_dom : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] [IsNoetherian K V] {f : V →ₗ[K] V₂}, f.HasNoetherianRange
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.forget_obj_of : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits F],
  (CategoryTheory.ExactFunctor.forget C D).obj (CategoryTheory.ExactFunctor.of F) = F
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_nndist_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (x y : WithLp ⊤ (α × β)),
  nndist x y = max (nndist x.fst y.fst) (nndist x.snd y.snd)
-- Mathlib.Data.Nat.Log
Nat.log.go_spec : ∀ {b n fuel : ℕ},
  1 < b →
    n ≠ 0 →
      n < b ^ fuel →
        (Nat.log.go n b fuel).1 = n / b ^ (Nat.log.go n b fuel).2 ∧
          b ^ (Nat.log.go n b fuel).2 ≤ n ∧ n < b ^ ((Nat.log.go n b fuel).2 + 1)
-- Mathlib.NumberTheory.Padics.PadicNorm
padicNorm.sum_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α},
  s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.transitionMap_comp_reduceModIdeal : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_3} [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) {m n : ℕ} (hmn : m ≤ n),
  AdicCompletion.transitionMap I N hmn ∘ₗ ↑R (LinearMap.reduceModIdeal (I ^ n) f) =
    ↑R (LinearMap.reduceModIdeal (I ^ m) f) ∘ₗ AdicCompletion.transitionMap I M hmn
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_iff_absorbing_le : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {S : Set E}, Bornology.IsVonNBounded 𝕜 S ↔ Filter.absorbing 𝕜 S ≤ nhds 0
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Natural isomorphisms between functors lift to additive monoid objects.  -/
CategoryTheory.Functor.mapAddMonNatIso : {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 F' : CategoryTheory.Functor C D} →
              [inst_4 : F.LaxMonoidal] →
                [inst_5 : F'.LaxMonoidal] →
                  (e : F ≅ F') → [CategoryTheory.NatTrans.IsMonoidal e.hom] → F.mapAddMon ≅ F'.mapAddMon
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.variance (X - Y) μ =
        ProbabilityTheory.variance X μ - 2 * ProbabilityTheory.covariance X Y μ + ProbabilityTheory.variance Y μ
-- Mathlib.Data.Finset.SymmDiff
Finset.image_symmDiff : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β} (s t : Finset α),
  Function.Injective f → Finset.image f (symmDiff s t) = symmDiff (Finset.image f s) (Finset.image f t)
-- Mathlib.Algebra.Order.Sub.Defs
antitone_const_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {c : α}
  [AddLeftMono α], Antitone fun x => c - x
-- Init.Data.UInt.Bitwise
UInt64.shiftLeft_and : ∀ {a b c : UInt64}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed-open intervals are equal if they agree on all
open-closed intervals.  -/
MeasureTheory.Measure.ext_of_Ioc : ∀ {α : Type u_5} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMinOrder α]
  (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ ⦃a b : α⦄, a < b → μ (Set.Ioc a b) = ν (Set.Ioc a b)) → μ = ν
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- Constructor `ℕ → SemiSimplexCategory`.  -/
SemiSimplexCategory.mk : ℕ → SemiSimplexCategory
-- Mathlib.Analysis.Normed.Module.TransferInstance
Equiv.seminormedAddCommGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddCommGroup β] (e : α ≃ β),
  e.seminormedAddCommGroup =
    { toNorm := (SeminormedAddCommGroup.induced α β e.addEquiv).toNorm,
      toAddCommGroup := (SeminormedAddCommGroup.induced α β e.addEquiv).toAddCommGroup,
      toPseudoMetricSpace := e.pseudometricSpace, dist_eq := ⋯ }
-- Lean.Elab.InfoTree.Basic
/-- Merges the `inner` partial context into the `outer` context s.t. fields of the `inner` context
overwrite fields of the `outer` context. Panics if the invariant described in the documentation
for `PartialContextInfo` is violated.

When traversing an `InfoTree`, this function should be used to combine the context of outer
nodes with the partial context of their subtrees. This ensures that the traversal has the context
from the inner node to the root node of the `InfoTree` available, with partial contexts of
inner nodes taking priority over contexts of outer nodes.
 -/
Lean.Elab.PartialContextInfo.mergeIntoOuter? : Lean.Elab.PartialContextInfo → Option Lean.Elab.ContextInfo → Option Lean.Elab.ContextInfo
-- Mathlib.Data.Sym.Basic
Sym.equivCongr_apply : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : Sym α n), (Sym.equivCongr e) x = Sym.map (⇑e) x
-- Aesop.Index.RulePattern
/-- Merge two rule pattern indices. Patterns that appear in both indices appear
twice in the result.  -/
Aesop.RulePatternIndex.merge : Aesop.RulePatternIndex → Aesop.RulePatternIndex → Aesop.RulePatternIndex
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Functor AugmentedSimplexCategory C),
  AugmentedSimplexCategory.equivAugmentedCosimplicialObjectFunctorCompPointIso.hom.app X =
    CategoryTheory.CategoryStruct.id (X.obj CategoryTheory.WithInitial.star)
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.Event.endHeaders.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (head head_1 : Std.Http.Protocol.H1.Message.Head dir),
  (Std.Http.Protocol.H1.Event.endHeaders head = Std.Http.Protocol.H1.Event.endHeaders head_1) = (head = head_1)
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- In a space with an inner regular measure for finite measure sets, the everywhere positive subset
of a measurable set of finite measure is itself everywhere positive. This is not obvious as
`μ.everywherePosSubset s` is defined as the points whose neighborhoods intersect `s` along positive
measure subsets, but this does not say they also intersect `μ.everywherePosSubset s` along positive
measure subsets.  -/
MeasureTheory.Measure.isEverywherePos_everywherePosSubset_of_measure_ne_top : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α}
  [OpensMeasurableSpace α] [μ.InnerRegularCompactLTTop],
  MeasurableSet s → μ s ≠ ⊤ → μ.IsEverywherePos (μ.everywherePosSubset s)
-- Mathlib.Tactic.Bound.Attribute
/-- Map a type to a score  -/
Mathlib.Tactic.Bound.typePriority : Lean.Name → Lean.Expr → Lean.MetaM ℕ
-- Mathlib.RingTheory.Morita.Matrix
fromModuleCatToModuleCatLinearEquiv_symm_apply_coe : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (M : Type u_1)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (i : ι) (x : M) (j : ι),
  ↑((fromModuleCatToModuleCatLinearEquiv R M i).symm x) j = Pi.single i x j
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `neg_add_le_iff_le_add`. -/
neg_add_le_of_le_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a ≤ b + c → -b + a ≤ c
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.colimitFiberwiseColimitIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)],
  CategoryTheory.Limits.colimitFiberwiseColimitIso G =
    (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.fiberwiseColimit G)).coconePointUniqueUpToIso
      (CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone (CategoryTheory.Limits.colimit.isColimit G))
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.sum_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R),
  ∑ i ∈ Finset.range (φ.totalDegree + 1), (MvPolynomial.homogeneousComponent i) φ = φ
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.bsize : ∀ {l m r : List Char} {s : Substring.Raw}, Substring.Raw.ValidFor l m r s → s.bsize = String.utf8Len m
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_eq_top : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ → ¬MeasureTheory.MemLp X 2 μ → ProbabilityTheory.evariance X μ = ⊤
-- Mathlib.RingTheory.Flat.TorsionFree
/-- If `R` is a Dedekind domain then an `R`-module is flat iff it has no torsion.  -/
IsDedekindDomain.flat_iff_torsion_eq_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsDedekindDomain R], Module.Flat R M ↔ Submodule.torsion R M = ⊥
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A skeleton and an open cell of a higher dimension are disjoint.  -/
Topology.RelCWComplex.disjoint_skeleton_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] {n : ℕ∞}
  {m : ℕ} {j : Topology.RelCWComplex.cell C m},
  n < ↑m → Disjoint (↑(Topology.RelCWComplex.skeleton C n)) (Topology.RelCWComplex.openCell m j)
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.baseChange_apply_coe : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [inst_5 : Module.Free R V] [inst_6 : Module.Finite R V]
  (g : SpecialLinearGroup R V), ↑(SpecialLinearGroup.baseChange g) = LinearEquiv.baseChange R S V V ↑g
-- Mathlib.Data.Multiset.Sections
Multiset.coe_sections : ∀ {α : Type u_1} (l : List (List α)), (↑(List.map (fun l => ↑l) l)).Sections = ↑(List.map (fun l => ↑l) l.sections)
-- Init.Data.Iterators.Basic
/-- `Finite α m` asserts that `IterM (α := α) m` terminates after finitely many steps. Technically,
this means that the relation of plausible successors is well-founded.
Given this typeclass, termination proofs for well-founded recursion over an iterator `it` can use
`it.finitelyManySteps` as a termination measure.
 -/
Std.Iterators.Finite : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → Prop
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.instTensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.IsCommMonObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.AliasInfo.reverse.sizeOf_spec : ∀ (n : Lean.Name), sizeOf (Batteries.Tactic.Alias.AliasInfo.reverse n) = 1 + sizeOf n
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₁) (CategoryTheory.CategoryStruct.id l₁) =
    CategoryTheory.CategoryStruct.id r₁
-- Mathlib.Tactic.Translate.Core
/-- An attribute that tells that certain arguments of this definition are not
involved when translating.
This helps the translation heuristic by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments.  -/
Mathlib.Tactic.Translate.TranslateData.ignoreArgsAttr : Mathlib.Tactic.Translate.TranslateData → Lean.NameMapExtension (List ℕ)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- The constructed `sheafHom α` is equal to `α` when restricted onto `C`.  -/
CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq : ∀ {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] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj), G.op.whiskerLeft (CategoryTheory.Functor.IsCoverDense.sheafHom α) = α
-- Mathlib.RingTheory.AdjoinRoot
PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (pb : PowerBasis R S)
  (I : Ideal R) (g : Polynomial R),
  (pb.quotientEquivQuotientMinpolyMap I).symm
      ((Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)}))
        (Polynomial.map (Ideal.Quotient.mk I) g)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((Polynomial.aeval pb.gen) g)
-- Mathlib.Algebra.Module.Defs
/-- Pullback a `Module` structure along an injective additive monoid homomorphism.
See note [reducible non-instances].  -/
Function.Injective.module : (R : Type u_1) →
  {M : Type u_3} →
    {M₂ : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid M₂] →
              [inst_4 : SMul R M₂] →
                (f : M₂ →+ M) → Function.Injective ⇑f → (∀ (c : R) (x : M₂), f (c • x) = c • f x) → Module R M₂
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.re_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ℂ),
  MeasureTheory.ComplexMeasure.re v = v.mapRange Complex.reLm.toAddMonoidHom Complex.continuous_re
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.isClosed : {α : Type} → Std.CloseableChannel.Zero✝ α → BaseIO Bool
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.isPredictable_predictablePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [SecondCountableTopology E]
  [inst_3 : MeasurableSpace E] [BorelSpace E],
  MeasureTheory.IsStronglyPredictable ℱ (MeasureTheory.predictablePart f ℱ μ)
-- Mathlib.Topology.MetricSpace.ProperSpace
instProperSpaceReal : ProperSpace ℝ
-- Mathlib.Order.Height
Set.exists_isChain_of_le_chainHeight : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} (n : ℕ), ↑n ≤ s.chainHeight r → ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An action is `2`-pretransitive iff
it can move any two distinct elements to any two distinct elements.  -/
MulAction.is_two_pretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2nd differential in the complex of inhomogeneous chains of `A : Rep k G`, as a
`k`-linear map `(G³ →₀ A) → (G² →₀ A)`. It is defined by
`a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂)`.  -/
groupHomology.d₃₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k (G × G × G →₀ ↑A) ⟶ ModuleCat.of k (G × G →₀ ↑A)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.topEquiv_apply : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (x : ↥⊤), NonUnitalSubsemiring.topEquiv x = ↑x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.restrict_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  {M₂ : Type u_5} {M₃ : Type u_6} [inst_4 : TopologicalSpace M₁] [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁]
  [inst_7 : TopologicalSpace M₂] [inst_8 : AddCommMonoid M₂] [inst_9 : Module R₂ M₂] [inst_10 : TopologicalSpace M₃]
  [inst_11 : AddCommMonoid M₃] [inst_12 : Module R₃ M₃] {p : Submodule R₁ M₁} {p₂ : Submodule R₂ M₂}
  {p₃ : Submodule R₃ M₃} {f : M₁ →SL[σ₁₂] M₂} {g : M₂ →SL[σ₂₃] M₃} (hf : Set.MapsTo ⇑f ↑p ↑p₂)
  (hg : Set.MapsTo ⇑g ↑p₂ ↑p₃) (hfg : optParam (Set.MapsTo ⇑(g ∘SL f) ↑p ↑p₃) ⋯),
  (g ∘SL f).restrict hfg = g.restrict hg ∘SL f.restrict hf
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x