mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Expr
/-- Similar for `setAppPPExplicit`, but only annotate children with `pp.explicit := false` if
`e` does not contain metavariables.
 -/
Lean.Expr.setAppPPExplicitForExposingMVars : Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteLimits.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam
      (∀ (J : Type) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
        CategoryTheory.Limits.ReflectsLimitsOfShape J F)
      CategoryTheory.Limits.ReflectsFiniteLimits.reflects._autoParam →
    CategoryTheory.Limits.ReflectsFiniteLimits F
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofBijective_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [inst_4 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_5 : RingHomInvPair σ₂₁ σ₁₂] {hf : Function.Bijective ⇑f} (x : M), (LinearEquiv.ofBijective f hf) x = f x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k},
  (t.insert k v).getD a fallback = if h : cmp k a = Ordering.eq then cast ⋯ v else t.getD a fallback
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_res_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U) {Z : C}
  (h : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map i.op) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) =
    CategoryTheory.CategoryStruct.comp (F.germ V x ⋯) h
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coePNat_injective : Function.Injective PrimeMultiset.toPNatMultiset
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_mks : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {f : A → B}
  (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := f, map_one' := h₁ }.toFun (x * y) =
        { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r)
  (h₆ :
    ∀ {i : ι} {x : A},
      x ∈ 𝒜 i →
        { toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom x ∈
          ℬ i),
  ⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_mem := h₆ } = f
-- Mathlib.Order.Sublattice
Sublattice.le_comap_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L M : Sublattice β) (f : LatticeHom α β),
  Sublattice.comap f L ⊔ Sublattice.comap f M ≤ Sublattice.comap f (L ⊔ M)
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.instIsTorsionFree : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  [Module.IsTorsionFree R M], Module.IsTorsionFree R ↥p
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mul_fin_two : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α),
  !![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup.  -/
Subsemiring.add_mem' : ∀ {R : Type u} [inst : NonAssocSemiring R] (self : Subsemiring R) {a b : R},
  a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.tendstoLocallyUniformly_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  [inst_2 : TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι),
  IsTopologicalGroup.rightUniformSpace G = u →
    (TendstoLocallyUniformly F f p ↔
      ∀ u_1 ∈ nhds 1, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1)
-- Init.Control.Basic
/-- Discards the value in a functor, retaining the functor's structure.

Discarding values is especially useful when using `Applicative` functors or `Monad`s to implement
effects, and some operation should be carried out only for its effects. In `do`-notation, statements
whose values are discarded must return `Unit`, and `discard` can be used to explicitly discard their
values.
 -/
Functor.discard : {f : Type u → Type v} → {α : Type u} → [Functor f] → f α → f PUnit.{u + 1}
-- Mathlib.Topology.Constructions.SumProd
continuous_swap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.swap
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_assoc : ∀ {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} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G) (j : J) {Z : C} (h : G.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j)
      (CategoryTheory.CategoryStruct.comp (w.hom.app j) h)
-- Mathlib.Data.Finset.NAry
Finset.image₂_union_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β}
  [inst_1 : DecidableEq β], Finset.image₂ f s (t ∪ t') = Finset.image₂ f s t ∪ Finset.image₂ f s t'
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.Hom.init : {J : Type w} → (j : J) → CategoryTheory.Limits.WidePushoutShape.Hom none (some j)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.compContinuousMap_apply : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g₀ g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (f : C(X, Y)) (x : ↑unitInterval × X),
  (G.compContinuousMap f) x = G (x.1, f x.2)
-- Lean.Server.InfoUtils
/-- Visit nodes, passing in a surrounding context (the innermost one combined with all outer ones) and
accumulating results on the way back up. If `preNode` returns `false`, the children of the current
node are skipped and `postNode` is invoked with an empty list of results.
 -/
Lean.Elab.InfoTree.visitM : {m : Type → Type u_1} →
  {α : Type} →
    [inst : Monad m] →
      (optParam (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool)
          fun x x_1 x_2 => pure true) →
        (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List (Option α) → m α) →
          optParam (Option Lean.Elab.ContextInfo) none → Lean.Elab.InfoTree → m (Option α)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.instConcreteCategoryAddHomCarrier.eq_1 : AddMagmaCat.instConcreteCategoryAddHomCarrier =
  { hom := fun {X Y} => AddMagmaCat.Hom.hom', ofHom := fun {X Y} => AddMagmaCat.Hom.mk✝,
    hom_ofHom := @AddMagmaCat.instConcreteCategoryAddHomCarrier._proof_1,
    ofHom_hom := @AddMagmaCat.instConcreteCategoryAddHomCarrier._proof_2,
    id_apply := @AddMagmaCat.instConcreteCategoryAddHomCarrier._proof_3,
    comp_apply := @AddMagmaCat.instConcreteCategoryAddHomCarrier._proof_4 }
-- Std.Data.ByteSlice
instSliceableByteSliceNat_6 : Std.Ric.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.Data.List.Chain
/-- If `l₁ l₂` and `l₃` are lists and `l₁ ++ l₂` and `l₂ ++ l₃` both satisfy
`IsChain R`, then so does `l₁ ++ l₂ ++ l₃` provided `l₂ ≠ []`  -/
List.IsChain.append_overlap : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ l₃ : List α},
  List.IsChain R (l₁ ++ l₂) → List.IsChain R (l₂ ++ l₃) → l₂ ≠ [] → List.IsChain R (l₁ ++ l₂ ++ l₃)
-- Mathlib.Data.Set.Function
/-- This lemma exists for use by `grind`/`aesop` as a forward rule.  -/
Set.EqOn.eq_of_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} {a : α}, Set.EqOn f₁ f₂ s → a ∈ s → f₁ a = f₂ a
-- Mathlib.Analysis.Complex.Angle
Complex.angle_one_left : ∀ {y : ℂ}, y ≠ 0 → InnerProductGeometry.angle 1 y = |y.arg|
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The underlying function.

Do NOT use directly. Use the coercion instead.  -/
ContinuousLinearMap.NonlinearRightInverse.toFun : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] → {f : E →SL[σ] F} → f.NonlinearRightInverse → F → E
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
KummerDedekind.quotMapEquivQuotQuotMap.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤)
  (hx' : IsIntegral R x), KummerDedekind.quotMapEquivQuotQuotMap hx hx' = KummerDedekind.quotMapEquivQuotQuotMap hx hx'
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- This is `PartialEquiv.single` as an open partial homeomorphism: a constant map,
whose source and target are necessarily singleton sets.
 -/
OpenPartialHomeomorph.const : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {a : X} → {b : Y} → IsOpen {a} → IsOpen {b} → OpenPartialHomeomorph X Y
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.tsub_encard_le_encard_sdiff`. -/
Set.tsub_encard_le_encard_diff : ∀ {α : Type u_1} (s t : Set α), s.encard - t.encard ≤ (s \ t).encard
-- Init.Data.Format.Basic
Std.Format.FlattenAllowability.allow.sizeOf_spec : ∀ (fits : Bool), sizeOf (Std.Format.FlattenAllowability.allow fits) = 1 + sizeOf fits
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` is the field of `p`-adic complex numbers, that is, the completion of `PadicAlgCl p` with
respect to the `p`-adic norm.  -/
PadicComplex : (p : ℕ) → [hp : Fact (Nat.Prime p)] → Type
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
/-- When two morphisms `X ⟶ Y` with `X` cofibrant and `Y` fibrant are related
by a left homotopy, this is a choice of a left homotopy relative
to any good cylinder object for `X`.  -/
HomotopicalAlgebra.LeftHomotopyRel.leftHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          [HomotopicalAlgebra.IsCofibrant X] →
            [HomotopicalAlgebra.IsFibrant Y] →
              HomotopicalAlgebra.LeftHomotopyRel f g →
                (Q : HomotopicalAlgebra.Cylinder X) → [Q.IsGood] → Q.LeftHomotopy f g
-- Lean.Meta.Basic
Lean.Meta.SavedState.mk.sizeOf_spec : ∀ (core : Lean.Core.SavedState) («meta» : Lean.Meta.State),
  sizeOf { core := core, «meta» := «meta» } = 1 + sizeOf core + sizeOf «meta»
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.instNonsingularObjSimplexCategoryStdSimplex : ∀ (n : SimplexCategory), (SSet.stdSimplex.obj n).Nonsingular
-- Init.Data.Vector.Lemmas
Vector.all_cast : ∀ {α : Type u_1} {n a : ℕ} {h : n = a} {f : α → Bool} {xs : Vector α n}, (Vector.cast h xs).all f = xs.all f
-- Mathlib.Probability.Independence.InfinitePi
/-- Random variables are independent iff their joint distribution is the product measure. This is
an `AEMeasurable` version of `iIndepFun_iff_map_fun_eq_infinitePi_map`, which is why it requires
`ι` to be countable.  -/
ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀' : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [MeasureTheory.IsProbabilityMeasure P] [Countable ι],
  (∀ (i : ι), AEMeasurable (X i) P) →
    (ProbabilityTheory.iIndepFun X P ↔
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P)
-- Mathlib.Data.Finset.Basic
Finset.choose_mem : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a),
  Finset.choose p l hp ∈ l
-- Mathlib.Order.InitialSeg
InitialSeg.strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α ≤i β), StrictMono ⇑f
-- Mathlib.Topology.Separation.Basic
isClosed_singleton_inter : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {A : Set X} {a : X}, IsClosed ({a} ∩ A)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_alter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : Option (β a) → Option (β a)}
  (htb : t.Balanced),
  t.Ordered →
    (Std.DTreeMap.Internal.Impl.alter a f t htb).impl.toListModel.Perm (Std.Internal.List.alterKey a f t.toListModel)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → (∀ y ∈ s, g y = f y) → g x = f x → ContinuousWithinAt g s x
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isInt_ratNum : ∀ {q : ℚ} {n : ℤ} {n' d : ℕ},
  Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsInt q.num n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y}
  (R : CategoryTheory.Sieve Z),
  CategoryTheory.Sieve.pushforward (CategoryTheory.CategoryStruct.comp g f) R =
    CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pushforward g R)
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiable_fun_neg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  (Differentiable 𝕜 fun y => -f y) ↔ Differentiable 𝕜 f
-- Mathlib.Topology.Compactness.Lindelof
instHereditarilyLindelofSpaceSubtype : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] (p : X → Prop),
  HereditarilyLindelofSpace { x // p x }
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_zero : ∀ {α : Type u} [inst : Preorder α] [h : IsEmpty α], Order.cof α = 0
-- Aesop.Tree.Data
Aesop.NormalizationState : Type
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct.match_1.splitter : {basis_tl : Tactic.ComputeAsymptotics.Basis} →
  (motive : Stream'.Seq1 (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) → Sort u_1) →
    (x : Stream'.Seq1 (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)) →
      ((exp : ℝ) →
          (coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl) →
            (tl : Stream'.Seq (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)) →
              motive ((exp, coef), tl)) →
        motive x
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.seminormedCommGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {s : Subgroup E},
  Subgroup.seminormedCommGroup =
    { toNorm := Subgroup.seminormedGroup.toNorm, toCommGroup := s.toCommGroup,
      toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ}, forIn t init f = forIn t.toArray init f
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_3.eq_2 : ∀ (motive : ONote → ONote → Sort u_1) (o : ONote) (h_1 : (x : ONote) → motive ONote.zero x)
  (h_2 : (o : ONote) → motive o ONote.zero)
  (h_3 :
    (o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          o₁ = e₁.oadd n₁ a₁ → (e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (o = ONote.zero → False) →
    (match o, ONote.zero with
      | ONote.zero, x => h_1 x
      | o, ONote.zero => h_2 o
      | o₁@h:(e₁.oadd n₁ a₁), e₂.oadd n₂ a₂ => h_3 o₁ e₁ n₁ a₁ h e₂ n₂ a₂) =
      h_2 o
-- Mathlib.Topology.EMetricSpace.Defs
instEDistOrderDual : {X : Type u_1} → [EDist X] → EDist Xᵒᵈ
-- Mathlib.Algebra.Star.SelfAdjoint
/-- Self-adjoint elements commute if and only if their product is self-adjoint.  -/
IsSelfAdjoint.commute_iff : ∀ {R : Type u_3} [inst : Mul R] [inst_1 : StarMul R] {x y : R},
  IsSelfAdjoint x → IsSelfAdjoint y → (Commute x y ↔ IsSelfAdjoint (x * y))
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instGroup.eq_1 : ∀ {α : Type u_1} [inst : Group α],
  OrderDual.instGroup = { toDivInvMonoid := OrderDual.instDivInvMonoid, inv_mul_cancel := ⋯ }
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat_primes : ∀ {p q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)], p ≠ q → padicValNat p q = 0
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction of an `𝒪ₓ`-module along an open immersion.
This is isomorphic to the pullback functor (see `restrictFunctorIsoPullback`)
but has better defeqs.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctor : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) → [AlgebraicGeometry.IsOpenImmersion f] → CategoryTheory.Functor Y.Modules X.Modules
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} [inst_2 : Inhabited (β a)] {v : β k},
  (t.insert k v).get! a = if h : cmp k a = Ordering.eq then cast ⋯ v else t.get! a
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_iterated_deriv : ∀ {𝕜 : Type u_3} {E : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    ∀ {k n : ℕ} [CharZero 𝕜], ↑n = analyticOrderAt f z₀ → n ≠ 0 → k ≤ n → analyticOrderAt (deriv^[k] f) z₀ = ↑(n - k)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.mkBneNat : Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.Bool
Bool.lt_trans : ∀ {x y z : Bool}, x < y → y < z → x < z
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_nnreal_eq : ∀ (r : NNReal), ↑r = ENNReal.ofReal ↑r
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
/-- The commutation with the shift isomorphism for the functor on cochain complexes
induced by an additive functor between preadditive categories.  -/
CategoryTheory.Functor.mapCochainComplexShiftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          [inst_3 : CategoryTheory.Preadditive D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.Additive] →
                (n : ℤ) →
                  (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).comp
                      (F.mapHomologicalComplex (ComplexShape.up ℤ)) ≅
                    (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp
                      (CategoryTheory.shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n)
-- Batteries.Data.Array.Scan
Subarray.scanl_eq_scanl_extract : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : Subarray α},
  Subarray.scanl f init as = Array.scanl f init (as.array.extract as.start as.stop)
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.IsNilpotent.nilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  [LieModule.IsNilpotent L M], ∃ k, LieModule.lowerCentralSeries R L M k = ⊥
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.dpow_mem_span_of_mem_span : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (hI : DividedPowers I) {S : Set A},
  S ⊆ ↑I →
    ∀ {k : ℕ},
      k ≠ 0 →
        ∀ {z : A},
          z ∈ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} →
            hI.dpow k z ∈ Ideal.span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
-- Std.Time.DateTime
/-- Creates a `DateTime` from a local date given as a `Day.Offset` relative to 1970-01-01, a
`PlainTime`, and `ZoneRules`. The day offset is interpreted as a local (civil) date, not UTC.
 -/
Std.Time.DateTime.ofEpochDay : Std.Time.Day.Offset → Std.Time.PlainTime → Std.Time.TimeZone.ZoneRules → Std.Time.DateTime
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_eq_const : ∀ {α : Type u_1} {a b : α} [inst : Mul α], a = b → ∀ (c : α), a * c = b * c
-- Mathlib.Algebra.Category.Grp.Biproducts
AddCommGrpCat.binaryProductLimitCone_cone_π_app_right : ∀ (G H : AddCommGrpCat),
  (G.binaryProductLimitCone H).cone.π.app { as := CategoryTheory.Limits.WalkingPair.right } =
    AddCommGrpCat.ofHom (AddMonoidHom.snd ↑G ↑H)
-- Lean.Util.Trace
/-- Should return the value of `inheritedTraceOptions.get`, which does not change after
initialization. As `IO.Ref.get` may be too expensive on frequent and multi-threaded access, the
value may want to be cached, which is done in the stdlib in `CoreM`.
 -/
Lean.MonadTrace.getInheritedTraceOptions : {m : Type → Type} → [self : Lean.MonadTrace m] → m (Std.HashSet Lean.Name)
-- Mathlib.Tactic.CongrExclamation
_private.Mathlib.Tactic.CongrExclamation.0.eq_imp_of_iff_imp : ∀ {x y : Prop} {p : x = y → Prop}, (∀ (he : x ↔ y), p ⋯) → ∀ (he : x = y), p he
-- Mathlib.Algebra.Order.Group.Abs
eq_of_abs_sub_nonpos : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, |a - b| ≤ 0 → a = b
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₂_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₂.obj T = T.obj₂
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.kstar_mul_le_kstar : ∀ {α : Type u_5} [self : KleeneAlgebra α] (a : α), KStar.kstar a * a ≤ KStar.kstar a
-- Mathlib.Data.List.Sigma
List.keys_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
  (List.kerase a l).keys = l.keys.erase a
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mrange_inl_sup_mrange_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange AddMonoid.Coprod.inl ⊔ AddMonoidHom.mrange AddMonoid.Coprod.inr = ⊤