mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.beckFork_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  (CategoryTheory.Comonad.beckFork X).ι = X.a
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃), (-a).re = -a.re
-- Mathlib.Topology.Sober
/-- The set of generic points of irreducible components.  -/
genericPoints : (α : Type u_1) → [TopologicalSpace α] → Set α
-- Mathlib.FieldTheory.CardinalEmb
/-- If `i` is a limit, the type of embeddings of `E⟮<i⟯` into `Ē` is
the limit of the types of embeddings of `E⟮<j⟯` for `j < i`.  -/
Field.Emb.Cardinal.equivLim : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] →
            [inst_3 : Algebra.IsAlgebraic F E] →
              {i : WithTop (Module.rank F E).ord.ToType} →
                Order.IsSuccPrelimit i →
                  (↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E) ≃
                    ↑(InverseSystem.limit (Field.Emb.Cardinal.embFunctor F E) i)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.coe_eq_zero_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : ↥s}, ↑x = 0 ↔ x = 0
-- Init.Data.SInt.Lemmas
BitVec.ofInt_int16ToInt : ∀ (x : Int16), BitVec.ofInt 16 x.toInt = x.toBitVec
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.collectType : Lean.Expr → Lean.FVarIdHashSet → Lean.FVarIdHashSet
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.smul_def : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {S : Subgroup G} (g : ↥S) (m : α),
  g • m = ↑g • m
-- Mathlib.Lean.Meta.Basic
/-- Checks that `e` is a type (i.e. that its type is a `Sort` after `instantiateMVars` and
`whnf`). If not, coerces `e` to a Sort or fails with a descriptive error.  -/
Lean.Meta.ensureIsSort : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.div₀_def : ∀ {ι : 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 : Nonempty ι]
  [inst_5 : (i : ι) → GroupWithZero (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)]
  (i : ι) (x y : G i), ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = ⟦⟨i, x / y⟩⟧
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.instPartialOrderCarrier : (X : FinPartOrd) → PartialOrder ↑X.toPartOrd
-- Init.Data.Array.Sort.Lemmas
/-- The result of `Array.mergeSort` is sorted,
as long as the comparison function is transitive (`le a b → le b c → le a c`)
and total in the sense that `le a b || le b a`.

The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
 -/
Array.pairwise_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ {xs : Array α}, List.Pairwise (fun x1 x2 => le x1 x2 = true) (xs.mergeSort le).toList
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.sum_toPartitionOfUnity_eq : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s) (x : X),
  ∑ᶠ (i : ι), (f.toPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - (f i) x)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_ofClass : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} {F : Type u_10} [inst_4 : FunLike F A B]
  [inst_5 : GradedFunLike F 𝒜 ℬ] [inst_6 : RingHomClass F A B] (f : F), ⇑↑f = ⇑f
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from variables to their denotations.
Remark each variable can be in only one ring.
 -/
Lean.Meta.Grind.Arith.CommRing.Ring.vars : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.PArray Lean.Expr
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_idem : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : Zero R], a.im.im = a.im
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.exists_of_trans_eq_trans : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j k : 𝒰.I₀} (fi : i ⟶ k) (fj : j ⟶ k)
  (xi : ↥(𝒰.X i)) (xj : ↥(𝒰.X j)),
  (𝒰.trans fi) xi = (𝒰.trans fj) xj → ∃ l fli flj x, (𝒰.trans fli) x = xi ∧ (𝒰.trans flj) x = xj
-- Init.Data.String.Basic
String.Pos.Raw.utf8PrevAux.eq_2 : ∀ (x x_1 : String.Pos.Raw) (c : Char) (cs : List Char),
  String.Pos.Raw.utf8PrevAux (c :: cs) x x_1 = if x_1 ≤ x + c then x else String.Pos.Raw.utf8PrevAux cs (x + c) x_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M` and a localization map
`g : M →* P` for the same submonoid, the homomorphism induced from
`N` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : M, y ∈ S`.  -/
Submonoid.LocalizationMap.lift_localizationMap_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) (x : M) (y : ↥S),
  (f.lift ⋯) (f.mk' x y) = g.mk' x y
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), h.adjoinRootAlgEquiv.symm h.root = AdjoinRoot.root f
-- Mathlib.Data.Matrix.Basic
Equiv.mapMatrix_symm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} (f : α ≃ β), f.mapMatrix.symm = f.symm.mapMatrix
-- Plausible.Functions
Plausible.TotalFunction.inhabited : {α : Type u} → {β : Type v} → [Inhabited β] → Inhabited (Plausible.TotalFunction α β)
-- Mathlib.Tactic.Translate.GuessName
/-- The data that is required to guess the name of a translation.  -/
Mathlib.Tactic.GuessName.GuessNameData : Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false} {fallback : α},
  Std.Internal.List.maxKey l he = Std.Internal.List.maxKeyD l fallback
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_add_right_deg : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n k : ℕ),
  g.natDegree ≤ n → f.resultant g m (n + k) = f.coeff m ^ k * f.resultant g m n
-- Mathlib.GroupTheory.ResiduallyFinite
Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup : ∀ {G : Type u_1} [inst : Group G],
  Group.ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.hom_hom_id : ∀ (R : Type u) [inst : Ring R] (A : FGModuleCat R),
  ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id A).hom = LinearMap.id
-- Mathlib.Algebra.Group.Action.Hom
addMonoidHomEquivAddActionVAddAssocClass.eq_1 : ∀ (M : Type u_4) (N : Type u_5) [inst : AddMonoid M] [inst_1 : AddMonoid N],
  addMonoidHomEquivAddActionVAddAssocClass M N =
    { toFun := fun f => ⟨AddAction.compHom N f, ⋯⟩,
      invFun := fun x =>
        match x with
        | ⟨val, property⟩ => AddMonoidHom.vaddZeroHom,
      left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst_1 : Inhabited α] {k k' : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).getKey! k' =
    if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsFiltered.sequentialFunctor_map : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsFiltered J],
  Monotone (CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J)
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_3 : HAdd Std.Time.Duration Std.Time.Minute.Offset Std.Time.Duration
-- Lean.Elab.App
/-- Add a new argument to the result. That is, `f := f arg`, update `fType`.
This method assumes `fType` is a function type.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.addNewArg : Lean.Name → Lean.Expr → Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.CategoryTheory.Limits.Presentation
/-- Map a colimit presentation under an isomorphism.  -/
CategoryTheory.Limits.ColimitPresentation.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} →
          CategoryTheory.Limits.ColimitPresentation J X →
            {Y : C} → (X ≅ Y) → CategoryTheory.Limits.ColimitPresentation J Y
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toIsLinearOrder : ∀ {α : Type u} [self : Std.LinearOrderPackage α], Std.IsLinearOrder α
-- Mathlib.Tactic.CongrExclamation
/-- This is like `Lean.MVarId.hcongr?` but (1) looks at both sides when generating the congruence lemma
and (2) inserts additional hypotheses from equalities from previous arguments.

It uses `Lean.Meta.mkRichHCongr` to generate the congruence lemmas.

If the goal is an `Eq`, it uses `eq_of_heq` first.

As a backup strategy, it uses the LHS/RHS method like in `Lean.MVarId.congrSimp?`
(where `Congr!.Config.preferLHS` determines which side to try first). This uses a particular side
of the target, generates the congruence lemma, then tries applying it. This can make progress
with higher transparency settings. To help the unifier, in this mode it assumes both sides have the
exact same function.
 -/
Lean.MVarId.smartHCongr? : Congr!.Config → Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Algebra.Lie.Basic
LieEquiv.ext : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂] {f g : L₁ ≃ₗ⁅R⁆ L₂}, (∀ (x : L₁), f x = g x) → f = g
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
ContinuousSup.measurableSup₂ : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] {mγ : MeasurableSpace γ} [BorelSpace γ] [SecondCountableTopology γ]
  [inst_3 : Max γ] [ContinuousSup γ], MeasurableSup₂ γ
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.isoOfLE_inv_ι : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hUV : U ≤ V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Opens.isoOfLE hUV).inv
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map V.ι.base).obj U).ι V.ι) =
    U.ι
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.inclusionPathAux.eq_1 : ∀ {B : Type u} [inst : Quiver B] {a : B},
  CategoryTheory.FreeBicategory.inclusionPathAux Quiver.Path.nil = CategoryTheory.FreeBicategory.Hom.id a
-- Mathlib.Order.Interval.Finset.Defs
WithTop.Icc_coe_top : ∀ (α : Type u_1) [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : LocallyFiniteOrder α] (a : α),
  Finset.Icc ↑a ⊤ = Finset.insertNone (Finset.Ici a)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mkOfOplax'_mapComp_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) [inst_2 : ∀ (a : B), CategoryTheory.IsIso (F.mapId a)]
  [inst_3 : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfOplax' F).mapComp f g).inv = CategoryTheory.inv (F.mapComp f g)
-- Std.Http.Data.Status
Std.Http.Status.payloadTooLarge.sizeOf_spec : sizeOf Std.Http.Status.payloadTooLarge = 1
-- Mathlib.GroupTheory.QuotientGroup.Finite
AddGroup.fintypeOfKerOfCodom.eq_1 : ∀ {G : Type u_2} {H : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup H] [inst_2 : Fintype H] (g : G →+ H)
  [inst_3 : Fintype ↥g.ker],
  AddGroup.fintypeOfKerOfCodom g =
    AddGroup.fintypeOfKerLeRange (AddSubgroup.topEquiv.toAddMonoidHom.comp (AddSubgroup.inclusion ⋯)) g ⋯
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : MeasurableSpace α} {inst_1 : MeasurableSpace β} {toEquiv : α ≃ β}
  {measurable_toFun : autoParam (Measurable ⇑toEquiv) MeasurableEquiv.measurable_toFun._autoParam}
  {measurable_invFun : autoParam (Measurable ⇑toEquiv.symm) MeasurableEquiv.measurable_invFun._autoParam}
  {toEquiv_1 : α ≃ β}
  {measurable_toFun_1 : autoParam (Measurable ⇑toEquiv_1) MeasurableEquiv.measurable_toFun._autoParam}
  {measurable_invFun_1 : autoParam (Measurable ⇑toEquiv_1.symm) MeasurableEquiv.measurable_invFun._autoParam},
  { toEquiv := toEquiv, measurable_toFun := measurable_toFun, measurable_invFun := measurable_invFun } =
      { toEquiv := toEquiv_1, measurable_toFun := measurable_toFun_1, measurable_invFun := measurable_invFun_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.dart_fst_fiber : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V] (v : V),
  {d | d.toProd.1 = v} = Finset.image (G.dartOfNeighborSet v) Finset.univ
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The equivalence between `NormedAddGroupHom M N` vanishing on the inseparable setoid and
`NormedAddGroupHom (SeparationQuotient M) N`.  -/
SeparationQuotient.liftNormedAddGroupHomEquiv : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {N : Type u_3} →
      [inst_1 : SeminormedAddCommGroup N] →
        { f // ∀ (x : M), ‖x‖ = 0 → f x = 0 } ≃ NormedAddGroupHom (SeparationQuotient M) N
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.ofStateSearchJson? : Lean.Json → Option LeanSearchClient.SearchResult
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.neg_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.neg P 2 = P 2
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Given a bifunctor `G : C₁ ⥤ C₂ ⥤ C`, diagrams `K₁ : J₁ ⥤ C₁` and `K₂ : J₂ ⥤ C₂`, and cones
over these diagrams, `G.mapCone₂ c₁ c₂` is the cone over the diagram `J₁ × J₂ ⥤ C` obtained
by applying `G` to both `c₁` and `c₂`.  -/
CategoryTheory.Functor.mapCone₂ : {J₁ : Type u_1} →
  {J₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] →
        {C₁ : Type u_3} →
          {C₂ : Type u_4} →
            {C : Type u_5} →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] →
                    (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                      {K₁ : CategoryTheory.Functor J₁ C₁} →
                        {K₂ : CategoryTheory.Functor J₂ C₂} →
                          CategoryTheory.Limits.Cone K₁ →
                            CategoryTheory.Limits.Cone K₂ →
                              CategoryTheory.Limits.Cone
                                (CategoryTheory.Functor.uncurry.obj
                                  ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceLocation : Lean.Lsp.FileSource Lean.Lsp.Location
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.isEqv.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → (α → α → Bool) → Sort u_2) →
    (x x_1 : List α) →
      (x_2 : α → α → Bool) →
        ((x : α → α → Bool) → motive [] [] x) →
          ((a : α) → (as : List α) → (b : α) → (bs : List α) → (eqv : α → α → Bool) → motive (a :: as) (b :: bs) eqv) →
            ((x x_3 : List α) →
                (x_4 : α → α → Bool) →
                  (x = [] → x_3 = [] → False) →
                    (∀ (a : α) (as : List α) (b : α) (bs : List α), x = a :: as → x_3 = b :: bs → False) →
                      motive x x_3 x_4) →
              motive x x_1 x_2
-- Mathlib.Data.Vector3
Vector3.insert.eq_1 : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) (i j : Fin2 (n + 1)),
  Vector3.insert a v i j = Vector3.cons a v (i.insertPerm j)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.quotientEquivOfIsCompl_apply_mk_right`. -/
Submodule.quotientEquivOfIsCompl_apply_mk_coe : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) (x : ↥q), (p.quotientEquivOfIsCompl q h) (Submodule.Quotient.mk ↑x) = x
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.lift_step_bind_congr : ∀ {m : Type w → Type u_1} {n : Type w → Type u_2} {β γ α₁ α₂ : Type w} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_6 : Std.Iterator α₁ m β]
  [inst_7 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb →
    ∀ {f : Std.Shrink ita.Step → n γ} {g : Std.Shrink itb.Step → n γ},
      (∀ (s₁ : Std.Shrink ita.Step) (s₂ : Std.Shrink itb.Step),
          (↑s₁.inflate).bundledQuotient = (↑s₂.inflate).bundledQuotient → f s₁ = g s₂) →
        liftM ita.step >>= f = liftM itb.step >>= g
-- Std.Http.Internal.Char
/-- field-content character class:
field-vchar / SP / HTAB
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.fieldContent : Char → Bool
-- Lean.Meta.Basic
/-- Execute `x`, and apply `f` to the produced error message  -/
Lean.Meta.mapError : {m : Type → Type u_1} →
  {α : Type} → [MonadControlT Lean.MetaM m] → [Monad m] → m α → (Lean.MessageData → Lean.MessageData) → m α
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprRecurringRule.repr : Std.Time.TimeZone.RecurringRule → ℕ → Std.Format
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformlyOn.mul` -/
TendstoLocallyUniformlyOn.fun_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      TendstoLocallyUniformlyOn (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l s
-- Mathlib.Order.Lattice
Pairwise.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop), Pairwise r = ∀ ⦃i j : α⦄, i ≠ j → r i j
-- Mathlib.NumberTheory.Divisors
Nat.sum_properDivisors_dvd : ∀ {n : ℕ}, ∑ x ∈ n.properDivisors, x ∣ n → ∑ x ∈ n.properDivisors, x = 1 ∨ ∑ x ∈ n.properDivisors, x = n
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
NNRealRMK.rieszMeasure.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X] [inst_3 : MeasurableSpace X] [inst_4 : BorelSpace X],
  NNRealRMK.rieszMeasure Λ = (rieszContent Λ).measure
-- Lean.Level
Lean.instEmptyCollectionLMVarIdSet : EmptyCollection Lean.LMVarIdSet
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.whiskerLeft : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g h : b ⟶ c) →
          [CategoryTheory.BicategoricalCoherence g h] →
            CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f g)
              (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Order.Interval.Basic
Interval.coe_zero : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α], ↑0 = 0
-- Init.Data.UInt.Lemmas
UInt64.lt_ofNat_iff : ∀ {n : UInt64} {m : ℕ}, m < UInt64.size → (n < UInt64.ofNat m ↔ n.toNat < m)
-- Init.Grind.AC
Lean.Grind.AC.Seq.erase0.eq_def : ∀ (s : Lean.Grind.AC.Seq),
  s.erase0 =
    match s with
    | Lean.Grind.AC.Seq.var x => Lean.Grind.AC.Seq.var x
    | Lean.Grind.AC.Seq.cons x s =>
      have s' := s.erase0;
      if (x == 0) = true then s'
      else if (s' == Lean.Grind.AC.Seq.var 0) = true then Lean.Grind.AC.Seq.var x else Lean.Grind.AC.Seq.cons x s'
-- Mathlib.Analysis.Convex.Mul
ConvexOn.pow : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f : G → E},
  ConvexOn 𝕜 s f → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → ∀ (n : ℕ), ConvexOn 𝕜 s (f ^ n)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.mulVec_injective_iff_isUnit : ∀ {m : Type u} [inst : DecidableEq m] {K : Type u_3} [inst_1 : Field K] [inst_2 : Fintype m] {A : Matrix m m K},
  Function.Injective A.mulVec ↔ IsUnit A
-- Init.Data.List.Impl
/-- Applies a function that returns an `Option` to each element of a list, collecting the non-`none`
values.

`O(|l|)`. This is a tail-recursive version of `List.filterMap`, used at runtime.

Example:
```lean example
#eval [1, 2, 5, 2, 7, 7].filterMapTR fun x =>
  if x > 2 then some (2 * x) else none
```
```output
[10, 14, 14]
```
 -/
List.filterMapTR : {α : Type u_1} → {β : Type u_2} → (α → Option β) → List α → List β
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub_nsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + ↑m
-- Mathlib.Order.Preorder.Chain
IsChain.mono : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, s ⊆ t → IsChain r t → IsChain r s
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKeyD_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.ready.sizeOf_spec : sizeOf Lean.Meta.Grind.ActivateNextGuardResult.ready = 1
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_pos_iff_nonempty : ∀ (α : Type u_3), 0 < ENat.card α ↔ Nonempty α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.iSup_coe_lt_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α},
  ⨆ x, ↑(f x) < ⊤ ↔ BddAbove (Set.range f)
-- Mathlib.Algebra.Order.Ring.Basic
Odd.pow_le_pow : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [ExistsAddOfLE R] {n : ℕ},
  Odd n → ∀ {a b : R}, a ^ n ≤ b ^ n ↔ a ≤ b
-- Mathlib.Computability.MyhillNerode
Language.mem_leftQuotient : ∀ {α : Type u} {L : Language α} (x y : List α), y ∈ L.leftQuotient x ↔ x ++ y ∈ L
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mul_nc_go : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ acc) =
    Lean.Grind.CommRing.Poly.denote ctx acc +
      Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.Simp.Config
-- Mathlib.Order.UpperLower.Prod
UpperSet.sup_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : UpperSet α) (t : UpperSet β),
  (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
-- Mathlib.Data.Matrix.Basic
Matrix.vecMul_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] (x : n → α) (s : Finset ι) (y : ι → Matrix n m α),
  Matrix.vecMul x (∑ i ∈ s, y i) = ∑ i ∈ s, Matrix.vecMul x (y i)