mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Sym.Sym2
Sym2.pair_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (a b : α) (h : P a) (h' : P b),
  s(f a h, f b h') = Sym2.pmap f s(a, b) ⋯
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.get_eq_getₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α)
  (h : m.contains a = true), Std.DHashMap.Internal.Raw₀.Const.get m a h = Std.DHashMap.Internal.Raw₀.Const.getₘ m a h
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.mk.inj : ∀ {γ : Type} {builtinName name : Lean.Name} {descr : String} {valueTypeName : Lean.Name}
  {evalKey : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key}
  {onAdded : Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit} {builtinName_1 name_1 : Lean.Name}
  {descr_1 : String} {valueTypeName_1 : Lean.Name}
  {evalKey_1 : Bool → Lean.Syntax → Lean.AttrM Lean.KeyedDeclsAttribute.Key}
  {onAdded_1 : Bool → Lean.Name → Lean.KeyedDeclsAttribute.Key → Lean.AttrM Unit},
  { builtinName := builtinName, name := name, descr := descr, valueTypeName := valueTypeName, evalKey := evalKey,
        onAdded := onAdded } =
      { builtinName := builtinName_1, name := name_1, descr := descr_1, valueTypeName := valueTypeName_1,
        evalKey := evalKey_1, onAdded := onAdded_1 } →
    builtinName = builtinName_1 ∧
      name = name_1 ∧ descr = descr_1 ∧ valueTypeName = valueTypeName_1 ∧ evalKey = evalKey_1 ∧ onAdded = onAdded_1
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- The first leg of a pushout cocone is a regular epimorphism if the left component is too.

See also `Pushout.fstOfEpi` for the basic epimorphism version, and
`regularOfIsPushoutSndOfRegular` for the flipped version.
 -/
CategoryTheory.regularOfIsPushoutFstOfRegular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P Q R S : C} →
      {f : P ⟶ Q} →
        {g : P ⟶ R} →
          {h : Q ⟶ S} →
            {k : R ⟶ S} →
              CategoryTheory.RegularEpi f →
                (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h k comm) →
                    CategoryTheory.RegularEpi k
-- Mathlib.Topology.Connected.PathConnected
/-- The relation "being joined by a path". This is an equivalence relation.  -/
Joined : {X : Type u_1} → [TopologicalSpace X] → X → X → Prop
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.isLeftDerivedFunctor_of_inverts : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C)
  [inst_3 : L.IsLocalization W] (F' : CategoryTheory.Functor D H) (e : L.comp F' ≅ F), F'.IsLeftDerivedFunctor e.hom W
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} {p : α → β → Bool},
  m.WF → ((Std.DHashMap.Raw.Const.toList m).any fun x => p x.1 x.2) = m.any p
-- Mathlib.Algebra.Homology.Single
ChainComplex.toSingle₀Equiv.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V),
  C.toSingle₀Equiv X =
    { toFun := fun φ => ⟨φ.f 0, ⋯⟩, invFun := fun f => HomologicalComplex.mkHomToSingle ↑f ⋯, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.ext_iff : ∀ {X Y : FintypeCat.Skeleton}, X = Y ↔ X.len = Y.len
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.nonneg' : ∀ {p q r : ℝ}, p.HolderTriple q r → 0 ≤ r
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.del.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19} {fvarId_1 : Lean.FVarId}
  {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19},
  Lean.Compiler.LCNF.Code.del fvarId k h = Lean.Compiler.LCNF.Code.del fvarId_1 k_1 h_1 → fvarId = fvarId_1 ∧ k = k_1
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.instConcreteCategoryBialgHomX : {R : Type u} → [inst : CommRing R] → CategoryTheory.ConcreteCategory (CommHopfAlgCat R) fun x1 x2 => ↑x1 →ₐc[R] ↑x2
-- Mathlib.Data.Set.Function
Set.RightInvOn.mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.RightInvOn f' f t → Set.SurjOn f' t s → Set.MapsTo f s t
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_insertListConst : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  (Std.Internal.List.insertListConst l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)
-- Lean.Elab.Do.Basic
/-- Information about a success, `return`, `break` or `continue` continuation that will be filled in
after the code using it has been elaborated.
 -/
Lean.Elab.Do.ContInfo : Type
-- Mathlib.Topology.Closure
/-- The frontier of a closed set has no interior point.  -/
interior_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → interior (frontier s) = ∅
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → ¬cmp k t.maxKey! = Ordering.eq → (t.erase k).maxKey! = t.maxKey!
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X],
  (Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).target = Set.range f
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.EStateM.instWP.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s' : σ) → motive (EStateM.Result.ok a s')) →
        ((e : ε) → (s' : σ) → motive (EStateM.Result.error e s')) → motive x
-- Mathlib.Order.Interval.Finset.Defs
instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder : {α : Type u_1} →
  [inst : Preorder α] → {y : α} → [DecidableLE α] → [LocallyFiniteOrder α] → LocallyFiniteOrderBot { x // y ≤ x }
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.isUnit_iff_range_eq_top : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] (f : V →ₗ[K] V), IsUnit f ↔ f.range = ⊤
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized₀_iSup : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] {ι : Type u_5} (g : ι → Submodule R M),
  Submodule.localized₀ p f (⨆ i, g i) = ⨆ i, Submodule.localized₀ p f (g i)
-- Mathlib.Topology.Order.IsLUB
exists_seq_tendsto_sSup : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [FirstCountableTopology α] {S : Set α},
  S.Nonempty → BddAbove S → ∃ u, Monotone u ∧ Filter.Tendsto u Filter.atTop (nhds (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toLinearMap_ofAlgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A ≃ₐ[R] B)
  (counit_comp : (Bialgebra.counitAlgHom R B).comp ↑f = Bialgebra.counitAlgHom R A)
  (map_comp_comul :
    (Algebra.TensorProduct.map ↑f ↑f).comp (Bialgebra.comulAlgHom R A) = (Bialgebra.comulAlgHom R B).comp ↑f),
  ↑↑(BialgEquiv.ofAlgEquiv f counit_comp map_comp_comul).toAlgEquiv = ↑↑f
-- Qq.ForLean.ToExpr
instToExprMVarId_qq : Lean.ToExpr Lean.MVarId
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesColimitsOfShape.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D},
  autoParam (∀ {K : CategoryTheory.Functor J C}, CategoryTheory.Limits.PreservesColimit K F)
      CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit._autoParam →
    CategoryTheory.Limits.PreservesColimitsOfShape J F
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The constant relative morphism when the given subcomplex of the target
is generated by a `0`-simplex.  -/
SSet.RelativeMorphism.const : {X Y : SSet} →
  {A : X.Subcomplex} →
    {y : Y.obj (Opposite.op { len := 0 })} →
      {φ : A.toSSet ⟶ (SSet.Subcomplex.ofSimplex y).toSSet} → SSet.RelativeMorphism A (SSet.Subcomplex.ofSimplex y) φ
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.R.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p p_1 : Besicovitch.TauPackage β α),
  p = p_1 → ∀ (i i_1 : Ordinal.{u}), i = i_1 → p.R i = p_1.R i_1
-- Mathlib.Topology.MetricSpace.Bounded
/-- If a function is continuous on a neighborhood of a compact set `k`, then it is bounded on
some open neighborhood of `k`.  -/
Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {k s : Set β} {f : β → α},
  IsCompact k → IsOpen s → k ⊆ s → ContinuousOn f s → ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)
-- Mathlib.CategoryTheory.Limits.Elements
/-- (implementation) A system `(Fi, fi)_i` of elements induces an element in `lim_i A(Fi)`.  -/
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [inst_2 : Small.{w, u₁} I] →
            (F : CategoryTheory.Functor I A.Elements) →
              CategoryTheory.Limits.limit ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A)
-- Init.Data.List.Control
List.findSomeM?_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → Option β}
  {as : List α}, List.findSomeM? (fun x => pure (f x)) as = pure (List.findSome? f as)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- For each type `α` in `toIntInfos`, the mapping `toIntVarMap` contains a mapping
from a α-term `e` to the pair `(toInt e, α)`.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.toIntTermMap : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.unitOfTensorIsoUnit_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  [inst_3 : F.Monoidal] (X : C),
  (CategoryTheory.unitOfTensorIsoUnit F m n h).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map h.hom).app X) ((CategoryTheory.Functor.OplaxMonoidal.η F).app X))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α}, k ∉ t₂ → Std.ExtDTreeMap.Const.get! (t₁ ∩ t₂) k = default
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.functorPushforward_over_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : CategoryTheory.Over X)
  (S : CategoryTheory.Sieve Z.left),
  CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map f) ((CategoryTheory.Sieve.overEquiv Z).symm S) =
    (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.map f).obj Z)).symm S
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulStrictMono α β] [SMulPosStrictMono α β],
  a₁ < a₂ → b₁ < b₂ → 0 < a₁ → 0 < b₂ → a₁ • b₁ < a₂ • b₂
-- Std.Data.TreeMap.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.TreeMap.keys : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → List α
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.Basis.sumQuot_inl : ∀ {R : Type u_2} {V : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {W : Submodule R V}
  {m : Type u_4} {n : Type u_5} (bW : Module.Basis m R ↥W) (bQ : Module.Basis n R (V ⧸ W)) (i : m),
  (bW.sumQuot bQ) (Sum.inl i) = ↑(bW i)
-- Mathlib.RingTheory.Ideal.Nonunits
mul_mem_nonunits_right : ∀ {α : Type u_2} {a b : α} [inst : CommMonoid α], b ∈ nonunits α → a * b ∈ nonunits α
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.rayleighQuotient.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (x : E), T.rayleighQuotient x = T.reApplyInnerSelf x / ‖x‖ ^ 2
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instSFiniteVolume : MeasureTheory.SFinite MeasureTheory.volume
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tprod_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] [Nonempty ι] {f : ι → M} {C : ℝ},
  (∀ (i : ι), ‖f i‖ ≤ C) → ‖∏' (i : ι), f i‖ ≤ C
-- Init.Data.Int.DivMod.Lemmas
Int.emod.eq_1 : ∀ (x : ℤ) (m : ℕ), (Int.ofNat m).emod x = Int.ofNat (m % x.natAbs)
-- Mathlib.Data.Quot
Trunc.instMonad : Monad Trunc
-- Init.Data.Int.Pow
Int.pow_mul : ∀ {a : ℤ} {n m : ℕ}, a ^ (n * m) = (a ^ n) ^ m
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.subset_sub_left : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s t : Set α}, 0 ∈ t → s ⊆ s - t
-- Mathlib.Order.Bounds.Basic
isGLB_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → IsGLB (Set.Ico b a) b
-- Mathlib.CategoryTheory.Action.Concrete
TypeCat.instCoeFunEndForall : (X : Type u) → CoeFun (CategoryTheory.End X) fun x => X → X
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.coe_toContinuousMap : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : CocompactMap α β},
  ⇑f.toContinuousMap = ⇑f
-- Mathlib.Topology.Algebra.Group.Extension
/-- Construct a short exact sequence of topological groups from a
closed normal subgroup.  -/
TopologicalAddGroup.IsSES.ofClosedAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (H : AddSubgroup G)
  [inst_3 : H.Normal], IsClosed ↑H → TopologicalAddGroup.IsSES H.subtype (QuotientAddGroup.mk' H)
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans'_target : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z)
  (h : e.target = e'.source), (e.trans' e' h).target = e'.target
-- Init.Data.UInt.Bitwise
USize.toUInt32_not : ∀ (a : USize), (~~~a).toUInt32 = ~~~a.toUInt32
-- Init.Prelude
Nat.ble_self_eq_true : ∀ (n : ℕ), n.ble n = true
-- Lean.Environment
/-- Branch specification for asynchronous environment extension access.

Note: For declarations not created via `addConstAsync`, including those created via `realizeConst`,
the two specifiers are equivalent.
 -/
Lean.AsyncBranch : Type
-- Lean.Parser.Command
/-- An internal bootstrapping command that reinterprets a Markdown docstring as Verso.
 -/
Lean.Parser.Command.docs_to_verso : Lean.Parser.Parser
-- Mathlib.Computability.RecursiveIn
RecursiveIn.none : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {O : Set (ℕ →. ℕ)},
  RecursiveIn O fun x => Part.none
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.div_logb : ∀ {a b c : ℝ}, c ≠ 0 → c ≠ 1 → c ≠ -1 → Real.logb a c / Real.logb b c = Real.logb a b
-- Lean.Meta.Iterator
/-- Return the first value returned by the iterator that `f` succeeds on.
 -/
Lean.Meta.Iterator.firstM : {α β : Type} → Lean.Meta.Iterator α → (α → Lean.MetaM (Option β)) → Lean.MetaM β
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : α → β → m (ForInStep β)} {inv : Std.Do.PostCond β ps},
  (∀ (hd : α) (b : β),
      ⦃inv.1 b⦄
        f hd b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 b'
          | ForInStep.done b' => inv.1 b',
          inv.2)⦄) →
    ⦃inv.1 init⦄ forIn xs init f ⦃inv⦄
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofBitVec : ∀ {b : BitVec 32}, { toBitVec := b }.toFin = b.toFin
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerLeft_naturality_comp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.OplaxTrans G H) {a b c : B} {a' : C}
  (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)))
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h)))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g) (H.map h)))
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)))))
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.epi_desc_of_epi_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc f g)
-- Init.Data.SInt.Lemmas
Int16.toUInt16_add : ∀ (a b : Int16), (a + b).toUInt16 = a.toUInt16 + b.toUInt16
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.neg_apply : ∀ {M : Type u_2} {G : Type u_5} [inst : AddZeroClass M] [inst_1 : AddCommGroup G] (f : M →+ G) (x : M), (-f) x = -f x
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
closedBall_prod_same : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (x : α) (y : β) (r : ℝ),
  Metric.closedBall x r ×ˢ Metric.closedBall y r = Metric.closedBall (x, y) r
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.LinearM.Context.mk.inj : ∀ {structId structId_1 : ℕ}, { structId := structId } = { structId := structId_1 } → structId = structId_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).get!
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.coe_factorₐ : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (hIJ : I ≤ J),
  ↑(Ideal.Quotient.factorₐ R₁ hIJ) = Ideal.Quotient.factor hIJ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.isEmpty = true → m.contains a = false
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_singleton_le : ∀ {α : Type u_1} (M : Matroid α) (e : α), M.eRk {e} ≤ 1
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.toUniformSpace_eq : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_u : UniformSpace R] [IsUniformAddGroup R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible],
  _u = IsTopologicalAddGroup.rightUniformSpace R
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.termW_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The coequalizer projection for `(f, f)` is an isomorphism.  -/
CategoryTheory.Limits.coequalizer.π_of_self : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  CategoryTheory.IsIso (CategoryTheory.Limits.coequalizer.π f f)
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- The `(m * n)`-th Chebyshev `C` polynomial is the composition of the `m`-th and `n`-th.  -/
Polynomial.Chebyshev.C_mul : ∀ (R : Type u_1) [inst : CommRing R] (m n : ℤ),
  Polynomial.Chebyshev.C R (m * n) = (Polynomial.Chebyshev.C R m).comp (Polynomial.Chebyshev.C R n)
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_zero : ∀ {X : Type u_1}, FreeAbelianGroup.support 0 = ∅
-- Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Ideal.pi_mkQ_rTensor : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (I : ι → Ideal R) [inst_3 : Fintype ι] [inst_4 : DecidableEq ι],
  LinearMap.rTensor M (LinearMap.pi fun i => Submodule.mkQ (I i)) =
    ↑(TensorProduct.piLeft R M fun i => R ⧸ I i).symm ∘ₗ
      (LinearMap.pi fun i => (TensorProduct.mk R (R ⧸ I i) M) 1) ∘ₗ ↑(TensorProduct.lid R M)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_sub_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s - t) → s.Nonempty → Bornology.IsVonNBounded 𝕜 t
-- Init.Data.BitVec.Lemmas
/-- Moves one-sided right toNat equality to BitVec equality.  -/
BitVec.nat_eq_toNat : ∀ {w : ℕ} {x : BitVec w} {y : ℕ}, y = x.toNat ↔ y < 2 ^ w ∧ x = BitVec.ofNat w y
-- Mathlib.Algebra.Category.BoolRing
BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier : ∀ (X : BoolAlg), ↑(CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolRing ↑X
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_functor_obj_coe : ∀ (X : AddMonCat), ↑(AddMonCat.equivalence.functor.obj X) = Multiplicative ↑X
-- Mathlib.Data.Finset.Image
Equiv.finsetSubtypeComm_symm_apply : ∀ {α : Type u_1} (p : α → Prop) (s : { s // ∀ a ∈ s, p a }),
  (Equiv.finsetSubtypeComm p).symm s = Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach