mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Do.Basic
Lean.Elab.Do.getContinueCont : Lean.Elab.Do.DoElabM (Option (Lean.Elab.Do.DoElabM Lean.Expr))
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instCoeStringSuggestionText : Coe String Lean.Meta.Tactic.TryThis.SuggestionText
-- Mathlib.NumberTheory.ModularForms.NormTrace
/-- The norm of a slash-invariant form, as a slash-invariant form.  -/
SlashInvariantForm.norm : {𝒢 : Subgroup (GL (Fin 2) ℝ)} →
  (ℋ : Subgroup (GL (Fin 2) ℝ)) →
    {F : Type u_1} →
      F →
        [inst : FunLike F UpperHalfPlane ℂ] →
          {k : ℤ} →
            [SlashInvariantFormClass F 𝒢 k] →
              [𝒢.IsFiniteRelIndex ℋ] →
                [ℋ.HasDetPlusMinusOne] → SlashInvariantForm ℋ (k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)))
-- Lean.Meta.Tactic.Grind.Theorems
/-- Returns `true` if the theorem has been marked as erased.  -/
Lean.Meta.Grind.Theorems.isErased : {α : Type} → Lean.Meta.Grind.Theorems α → Lean.Meta.Grind.Origin → Bool
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and insert all of its elements into `t` if they are new.  -/
Std.DTreeMap.Internal.Impl.insertManyIfNew : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} →
        [ForIn Id ρ ((a : α) × β a)] →
          (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.Balanced → t.IteratedNewInsertionInto
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] {A : Type u_2} [inst_2 : NonUnitalRing A]
  [inst_3 : StarRing A] [inst_4 : Module ℝ A] [inst_5 : TopologicalSpace A] [IsSemitopologicalRing A]
  (φ : ContinuousMapZero X NNReal →⋆ₙₐ[NNReal] A), Continuous ⇑φ → Continuous ⇑φ.realContinuousMapZeroOfNNReal
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_pairwise_pi_lex : ∀ (k n : ℕ), List.Pairwise (Pi.Lex (fun x1 x2 => x1 < x2) fun x x1 x2 => x1 < x2) (List.Nat.antidiagonalTuple k n)
-- Mathlib.RingTheory.DedekindDomain.PID
/-- Let `p` be a prime in the Dedekind domain `R` and `S` be an integral extension of `R`,
then the localization `Sₚ` of `S` at `p` is a PID.  -/
IsDedekindDomain.isPrincipalIdealRing_localization_over_prime : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (S : Type u_2) [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [Module.IsTorsionFree R S] [Module.Finite R S] (p : Ideal R),
  p ≠ ⊥ →
    ∀ [inst_6 : p.IsPrime] {Sₚ : Type u_3} [inst_7 : CommRing Sₚ] [inst_8 : Algebra S Sₚ]
      [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [inst_10 : Algebra R Sₚ] [IsScalarTower R S Sₚ]
      [IsDedekindDomain Sₚ] [IsDomain S], IsPrincipalIdealRing Sₚ
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.length_cycle_cons : ∀ (n : ℕ) (m : Fin (n + 3)), (SimpleGraph.cycleGraph.cycleCons✝ n m).length = ↑m
-- Mathlib.CategoryTheory.EpiMono
/-- `section_` composed with `f` is the identity  -/
CategoryTheory.SplitEpi.id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.SplitEpi f),
  CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y
-- Init.Data.Range.Polymorphic.Map
Std.Rxi.IsAlwaysFinite.ofMap : ∀ {α : Type u_2} {β : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [Std.Rxi.IsAlwaysFinite β] (f : Std.PRange.UpwardEnumerable.Map α β), Std.Rxi.IsAlwaysFinite α
-- Mathlib.Topology.Maps.Proper.Basic
/-- A map is proper if and only if it is closed and its fibers are compact.  -/
isProperMap_iff_isClosedMap_and_compact_fibers : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkXorCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkXorCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Std.Http.Data.URI.Basic
/-- Creates an empty query string.
 -/
Std.Http.URI.Query.empty : Std.Http.URI.Query
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.isoMk.congr_simp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X}
  (hr hr_1 : f.right ≅ g.right) (e_hr : hr = hr_1) (hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom),
  CategoryTheory.Under.isoMk hr hw = CategoryTheory.Under.isoMk hr_1 ⋯
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_inv₀ : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → GroupWithZero (G i)] [inst_7 : GroupWithZero C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  [∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h x⁻¹ = (DirectLimit.lift f (fun x => ⇑(g x)) h x)⁻¹
-- Mathlib.Algebra.Homology.Homotopy
/-- An additive functor preserves homotopy equivalences.  -/
CategoryTheory.Functor.mapHomotopyEquiv : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {W : Type u_2} →
              [inst_2 : CategoryTheory.Category.{v_1, u_2} W] →
                [inst_3 : CategoryTheory.Preadditive W] →
                  (F : CategoryTheory.Functor V W) →
                    [inst_4 : F.Additive] →
                      HomotopyEquiv C D →
                        HomotopyEquiv ((F.mapHomologicalComplex c).obj C) ((F.mapHomologicalComplex c).obj D)
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrLeft.eq_1 : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] [inst_1 : Semiring 𝕜]
  {ι' : Type u_5} [inst_2 : Fintype ι'] (E : Type u_6) [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E]
  (e : ι ≃ ι'),
  LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e =
    {
      toLinearEquiv :=
        WithLp.linearEquiv p 𝕜 (ι → E) ≪≫ₗ
          (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e ≪≫ₗ (WithLp.linearEquiv p 𝕜 (ι' → E)).symm),
      norm_map' := ⋯ }
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
SpectrumRestricts.mul_comm_iff : ∀ {R : Type u_6} {S : Type u_7} {A : Type u_8} [inst : Semifield R] [inst_1 : Field S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] {a b : A} {f : S → R},
  SpectrumRestricts (a * b) f ↔ SpectrumRestricts (b * a) f
-- Init.Data.Dyadic.Basic
Dyadic.toRat_le_toRat_iff : ∀ {x y : Dyadic}, x.toRat ≤ y.toRat ↔ x ≤ y
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Additive.ofMul_lt`. -/
Additive.ofMul_strictMono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a < b → Additive.ofMul a < Additive.ofMul b
-- Mathlib.GroupTheory.Divisible
/-- If for all `n ≠ 0 ∈ ℤ`, `n • A = A`, then `A` is divisible.
 -/
AddCommGroup.divisibleByIntOfSMulTopEqTop : (A : Type u_1) → [inst : AddCommGroup A] → (∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤) → DivisibleBy A ℤ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → t.maxKey? = none
-- Mathlib.AlgebraicGeometry.Normalization
/-- The morphism from the relative normalization to itself. This map is integral.  -/
AlgebraicGeometry.Scheme.Hom.fromNormalization : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] → AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Y
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Determinant of a transvection.

It is not necessary to assume that the module is finite and free
because `LinearMap.det` is identically 1 otherwise.  -/
LinearEquiv.transvection.det_eq_one : ∀ {R : Type u_3} {V : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  {f : Module.Dual R V} {v : V} (hfv : f v = 0), LinearEquiv.det (LinearEquiv.transvection hfv) = 1
-- Mathlib.GroupTheory.IsSubnormal
AddSubgroup.IsSubnormal.iff_eq_top_or_exists : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.IsSubnormal ↔ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.addSubgroupOf K).Normal
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The trivial `k`-linear `G`-representation on a `k`-module `V.`  -/
Rep.trivial : (k : Type u) →
  (G : Type v) →
    [inst : Semiring k] →
      [inst_1 : Monoid G] → (V : Type w) → [inst_2 : AddCommGroup V] → [Module k V] → Rep.{w, u, v} k G
-- Mathlib.Topology.ClusterPt
AccPt.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X) (F : Filter X), AccPt x F = (nhdsWithin x {x}ᶜ ⊓ F).NeBot
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.IsCorepresentable.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)},
  (∃ X, Nonempty (F.CorepresentableBy X)) → F.IsCorepresentable
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpLeftOpIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) (X : Cᵒᵖ),
  F.rightOpLeftOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.elabChoiceAux : Array Lean.Syntax → ℕ → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toListRev_toIter : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter.toListRev = xs.toList.reverse
-- Mathlib.RingTheory.Idempotents
eq_of_isNilpotent_sub_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {e₁ e₂ : R},
  IsIdempotentElem e₁ → IsIdempotentElem e₂ → IsNilpotent (e₁ - e₂) → e₁ = e₂
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.StandardOneDimIsocrystal.frobenius_apply : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k] [inst_2 : IsDomain k] [inst_3 : CharP k p]
  [inst_4 : PerfectRing k p] (m : ℤ) (x : WittVector.StandardOneDimIsocrystal p k m),
  (WittVector.Isocrystal.frobenius p k) x = ↑p ^ m • (WittVector.FractionRing.frobeniusRingHom p k) x
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.moduleDoc.injEq : ∀ (n n_1 : ℕ), (Lean.Doc.DeferredCheckSite.moduleDoc n = Lean.Doc.DeferredCheckSite.moduleDoc n_1) = (n = n_1)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- Auxiliary definition for `Homotopy.extend`.  -/
Homotopy.extend.hom : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Preadditive C] →
                {K L : HomologicalComplex C c} →
                  (e : c.Embedding c') →
                    ((i j : ι) → K.X i ⟶ L.X j) → (i' j' : ι') → (K.extend e).X i' ⟶ (L.extend e).X j'
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.isPosSemidef_diagonalStrongDualPi : ∀ {ι : Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace ℝ (E i)]
  {L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ},
  (∀ (i : ι), (L i).toBilinForm.IsPosSemidef) → (ContinuousLinearMap.diagonalStrongDualPi✝ L).toBilinForm.IsPosSemidef
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `g'`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commg' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp self.φQ h₂.g' = CategoryTheory.CategoryStruct.comp h₁.g' φ.τ₃
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring with finite quotients is noetherian.  -/
Ring.HasFiniteQuotients.instIsNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R], IsNoetherianRing R
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAdd : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → Add (G i)] →
                  [∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] → Add (DirectLimit G f)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.of : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    {F : CategoryTheory.Functor J MonCat} → (j : J) → ↑(F.obj j) → MonCat.Colimits.Prequotient F
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.final_of_isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsRightAdjoint], F.Final
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableDiv : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Div (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableDiv (α i)], MeasurableDiv ((i : ι) → α i)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.copyIndep_E : ∀ {α : Type u_1} (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E)
  (h : ∀ (I : Set α), Indep I ↔ M.Indep I), (M.copyIndep E Indep hE h).E = E
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.of_hasKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {Y Z : C} (g : Y ⟶ Z) (X : C) [CategoryTheory.Limits.HasKernel g],
  { X₁ := X, X₂ := Y, X₃ := Z, f := 0, g := g, zero := ⋯ }.HasRightHomology
-- Mathlib.Computability.TuringDegree
TuringEquivalent.trans : ∀ (f g h : ℕ →. ℕ), TuringEquivalent f g → TuringEquivalent g h → TuringEquivalent f h
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_commute : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M} [inst_1 : Add M],
  (∀ (m' : M), AddCommute m m') →
    (∀ (r' : R), Commute r r') → ∀ (x : AddMonoidAlgebra R M), Commute (AddMonoidAlgebra.single m r) x
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : RBTree.RBNode.Path α),
  RBTree.RBNode.Path.Ordered cmp x =
    match x with
    | RBTree.RBNode.Path.root => True
    | RBTree.RBNode.Path.left c parent x b =>
      RBTree.RBNode.Path.Ordered cmp parent ∧
        RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x x_1) b ∧
          RBTree.RBNode.Path.RootOrdered cmp parent x ∧
            RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp parent) b ∧ RBTree.RBNode.Ordered cmp b
    | RBTree.RBNode.Path.right c a x parent =>
      RBTree.RBNode.Path.Ordered cmp parent ∧
        RBTree.RBNode.All (fun x_1 => RBTree.RBNode.cmpLT cmp x_1 x) a ∧
          RBTree.RBNode.Path.RootOrdered cmp parent x ∧
            RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp parent) a ∧ RBTree.RBNode.Ordered cmp a
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.HasDimensionLT.degenerate_eq_top : ∀ {X : SSet} {d : ℕ} [self : X.HasDimensionLT d] (n : ℕ), d ≤ n → X.degenerate n = ⊤
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {a : α} {fallback : β a},
  ∅.getD a fallback = fallback
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_mapWithPostcondition : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Std.Iterators.PostconditionT n γ}
  {g : δ → γ → δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← (f b).run
          pure (g d c))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.mapWithPostcondition f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_unitIso_inv_app_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 : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- Exponentiation is eventually larger than linear growth.  -/
Real.exists_natCast_add_one_lt_pow_of_one_lt : ∀ {a : ℝ}, 1 < a → ∃ m, ↑m + 1 < a ^ m
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_fst_v_assoc : ∀ {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 φ] (i j k : ℤ)
  (hij : i + 1 = j) (hjk : j + 1 = k) {Z : C} (h : F.X k ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
      (CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v j k hjk) h) =
    CategoryTheory.CategoryStruct.comp
      (-CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (F.d j k)) h
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_inf_mul_relIndex : ∀ {G : Type u_1} [inst : AddGroup G] (H K L : AddSubgroup G), H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- Applying a functor which preserves pullbacks and effective epimorphisms to a regular epi diagram
of the form `X ×_Y X ⇉ X → Y` gives a regular epi diagram.
 -/
CategoryTheory.Functor.regularEpiOfPreserves : {C : Type u_3} →
  {D : Type u_4} →
    [inst : CategoryTheory.Category.{v_3, u_3} C] →
      [inst_1 : CategoryTheory.Category.{v_4, u_4} D] →
        {X Y : C} →
          (f : X ⟶ Y) →
            [CategoryTheory.EffectiveEpi f] →
              (F : CategoryTheory.Functor C D) →
                [F.PreservesEffectiveEpis] →
                  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F] →
                    (c : CategoryTheory.Limits.PullbackCone f f) →
                      CategoryTheory.Limits.IsLimit c → CategoryTheory.RegularEpi (F.map f)
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_m_density : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ (a : α) [ProbabilityTheory.IsFiniteKernel ν] {s : Set β},
      MeasurableSet s →
        ∀ᵐ (x : γ) ∂ν a, Filter.Tendsto (fun n => κ.densityProcess ν n a x s) Filter.atTop (nhds (κ.density ν a x s))
-- Mathlib.Data.Set.Image
Set.preimage_congr : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Set β}, (∀ (x : α), f x = g x) → f ⁻¹' s = g ⁻¹' s
-- Lean.Elab.Syntax
Lean.Elab.Command.resolveSyntaxKind : Lean.Name → Lean.Elab.Command.CommandElabM Lean.Name
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Scalar matrix as an element of `GL n R`.  -/
Matrix.GeneralLinearGroup.scalar : (n : Type u) → [inst : DecidableEq n] → [inst_1 : Fintype n] → {R : Type v} → [inst_2 : Semiring R] → Rˣ →* GL n R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_eq_isSome_get? : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, Std.DTreeMap.Internal.Impl.contains a t = (Std.DTreeMap.Internal.Impl.Const.get? t a).isSome
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
map_ne_zero_of_mem_nonZeroDivisors : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F M₀ M₀'] [Nontrivial M₀] [ZeroHomClass F M₀ M₀'] (g : F),
  Function.Injective ⇑g → ∀ {x : M₀}, x ∈ nonZeroDivisors M₀ → g x ≠ 0
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Subgroup.isCyclic_of_le : ∀ {G : Type u_2} [inst : Group G] {H H' : Subgroup G}, H ≤ H' → ∀ [IsCyclic ↥H'], IsCyclic ↥H
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c) = 1 + sizeOf c
-- Mathlib.Probability.CentralLimitTheorem
/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
independent, identically distributed with mean `μ` and non-zero variance `v`, and a random variable
`Y : Ω' → ℝ` following `gaussianReal 0 1`, the sequence
`n ↦ (√(n * v)⁻¹ * (∑ k ∈ Finset.range n, X k ω - n * μ)` converges to `Y` in distribution.  -/
_private.Mathlib.Probability.CentralLimitTheorem.0.ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω}
  {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [inst : MeasureTheory.IsProbabilityMeasure P]
  [inst_1 : MeasureTheory.IsProbabilityMeasure P'],
  ProbabilityTheory.HasLaw Y (ProbabilityTheory.gaussianReal 0 1) P' →
    ProbabilityTheory.variance (X 0) P ≠ 0 →
      ProbabilityTheory.iIndepFun X P →
        (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) →
          MeasureTheory.TendstoInDistribution
            (fun n ω =>
              (√(↑n * ProbabilityTheory.variance (X 0) P))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P))
            Filter.atTop Y (fun x => P) P'
-- Mathlib.Tactic.FunProp.Decl
Mathlib.Meta.FunProp.instBEqFunPropDecl.beq : Mathlib.Meta.FunProp.FunPropDecl → Mathlib.Meta.FunProp.FunPropDecl → Bool
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_eq_pullback : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_6} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {V : E' → E'},
  VectorField.mpullback (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V = VectorField.pullback 𝕜 f V
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.List.of_findIdx?_eq_some.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_atBot_atBot : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ioc Filter.atBot Filter.atBot