mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx.induct_unfolding : ∀ {α : Type u} {β : Type v}
  (motive : (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → (n : ℕ) → n < t.size → α × β → Prop),
  (∀ (size : ℕ) (k : α) (v : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
      (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
      (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.lt),
      motive l' ⋯ n ⋯ (Std.DTreeMap.Internal.Impl.Const.entryAtIdx l' ⋯ n ⋯) →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h
          (Std.DTreeMap.Internal.Impl.Const.entryAtIdx l' ⋯ n ⋯)) →
    (∀ (size : ℕ) (k : α) (v : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
        (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
        (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size),
        compare n l'.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h (k, v)) →
      (∀ (size : ℕ) (k : α) (v : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
          (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
          (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) (h_1 : compare n l'.size = Ordering.gt),
          motive r' ⋯ (n - l'.size - 1) ⋯ (Std.DTreeMap.Internal.Impl.Const.entryAtIdx r' ⋯ (n - l'.size - 1) ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h
              (Std.DTreeMap.Internal.Impl.Const.entryAtIdx r' ⋯ (n - l'.size - 1) ⋯)) →
        ∀ (t : Std.DTreeMap.Internal.Impl α fun x => β) (hl : t.Balanced) (n : ℕ) (h : n < t.size),
          motive t hl n h (Std.DTreeMap.Internal.Impl.Const.entryAtIdx t hl n h)
-- Mathlib.ModelTheory.Definability
_private.Mathlib.ModelTheory.Definability.0.Set.DefinableFun.comp.match_1_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (j : Option α) → (Unit → motive none) → ((i : α) → motive (some i)) → motive j
-- Lean.Util.SCC
Lean.SCC.State.mk.injEq : ∀ {α : Type} [inst : BEq α] [inst_1 : Hashable α] (stack : List α) (nextIndex : ℕ) (data : Std.HashMap α Lean.SCC.Data)
  (sccs : List (List α)) (stack_1 : List α) (nextIndex_1 : ℕ) (data_1 : Std.HashMap α Lean.SCC.Data)
  (sccs_1 : List (List α)),
  ({ stack := stack, nextIndex := nextIndex, data := data, sccs := sccs } =
      { stack := stack_1, nextIndex := nextIndex_1, data := data_1, sccs := sccs_1 }) =
    (stack = stack_1 ∧ nextIndex = nextIndex_1 ∧ data = data_1 ∧ sccs = sccs_1)
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofSetoid_parts_val : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Setoid α) [inst_2 : DecidableRel ⇑s],
  (Finpartition.ofSetoid s).parts.val = (Multiset.map (fun a => {b | s a b}) Finset.univ.val).dedup
-- Mathlib.Analysis.Convex.Slope
ConvexOn.secant_mono_aux2 : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f → ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f x) / (z - x)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
IsLocalizedModule.toLocalizedQuotient' : ∀ {R : Type u_5} (S : Type u_6) {M : Type u_7} {N : Type u_8} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R) [inst_9 : IsLocalization p S] (f : M →ₗ[R] N)
  [inst_10 : IsLocalizedModule p f] (M' : Submodule R M), IsLocalizedModule p (Submodule.toLocalizedQuotient' S p f M')
-- Mathlib.Dynamics.Ergodic.Ergodic
QuasiErgodic.toQuasiMeasurePreserving : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) QuasiErgodic._auto_1},
  QuasiErgodic f μ → MeasureTheory.Measure.QuasiMeasurePreserving f μ μ
-- Mathlib.CategoryTheory.Localization.Predicate
/-- the induced functor from the constructed localized category is an equivalence  -/
CategoryTheory.Functor.IsLocalization.isEquivalence : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {L : CategoryTheory.Functor C D}
  {W : CategoryTheory.MorphismProperty C} [self : L.IsLocalization W],
  (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.comp : {B : Type u} →
  [inst : Quiver B] →
    {a b c : B} →
      CategoryTheory.FreeBicategory.Hom a b →
        CategoryTheory.FreeBicategory.Hom b c → CategoryTheory.FreeBicategory.Hom a c
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispan_map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (a : J.L),
  I.multispan.map (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) = I.fst a
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.liftExtend_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (φ : K.restriction e ⟶ L) (hφ : e.HasLift φ) {i' : ι'} {i : ι} (hi : e.f i = i'),
  (e.liftExtend φ hφ).f i' =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).inv
      (CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e hi).inv)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- `Equiv.Perm.toList (f : Perm α) (x : α)` generates the list `[x, f x, f (f x), ...]`
until looping. That means when `f x = x`, `toList f x = []`.
 -/
Equiv.Perm.toList : {α : Type u_1} → [Fintype α] → [DecidableEq α] → Equiv.Perm α → α → List α
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebraMap_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (r : R), (algebraMap R A) r ∈ S
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNatCast : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [NatCast Y] → NatCast (LocallyConstant X Y)
-- Lean.Linter.UnusedVariables
/-- Interpret an `IgnoreFunction` from the environment.  -/
Lean.Linter.mkIgnoreFnImpl : Lean.Name → Lean.ImportM Lean.Linter.IgnoreFunction
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.mk : (X : Type u) → TwoPointing X → TwoP
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
/-- A functor `F : C ⥤ H` has a left derived functor with respect to
`W : MorphismProperty C` if it has a right Kan extension along
`W.Q : C ⥤ W.Localization` (or any localization functor `L : C ⥤ D`
for `W`, see `hasLeftDerivedFunctor_iff`).  -/
CategoryTheory.Functor.HasLeftDerivedFunctor : {C : Type u_1} →
  {H : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_5, u_2} H] →
        CategoryTheory.Functor C H → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Analysis.Normed.Group.Pointwise
mul_ball_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E), s * Metric.ball 1 δ = Metric.thickening δ s
-- Std.Data.ExtTreeMap.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.ExtTreeMap.foldr : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → {δ : Type w} → [Std.TransCmp cmp] → (α → β → δ → δ) → δ → Std.ExtTreeMap α β cmp → δ
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.Compatible.of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (f : P ⟶ Q) [CategoryTheory.Mono f]
  {x : CategoryTheory.Presieve.FamilyOfElements P R}, (x.map f).Compatible → x.Compatible
-- Lean.Server.FileWorker.Utils
/-- Task reporting processing status back to client. We store it here for implementing
`waitForDiagnostics`.  -/
Lean.Server.FileWorker.EditableDocument.reporter : Lean.Server.FileWorker.EditableDocument → Lean.Server.ServerTask Unit
-- Mathlib.Algebra.Group.Hom.Basic
coe_invMonoidHom : ∀ {α : Type u_1} [inst : DivisionCommMonoid α], ⇑invMonoidHom = Inv.inv
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Differentiable.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.sin (f x)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_rio : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [inst_4 : Std.PRange.Least? α] [inst_5 : LT α] [inst_6 : DecidableLT α] [inst_7 : Std.PRange.UpwardEnumerable α]
  [inst_8 : Std.Rxo.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α]
  {xs : Std.Rio α} {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.Data.EReal.Operations
EReal.sub_neg : ∀ {x y : EReal}, x ≠ ⊤ ∨ y ≠ ⊤ → x ≠ ⊥ ∨ y ≠ ⊥ → (x - y < 0 ↔ x < y)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instLE.eq_1 : ∀ {M : Type u_1} [inst : Group M] [inst_1 : Lattice M],
  MulArchimedeanOrder.instLE = { le := fun a b => ∃ n, |MulArchimedeanOrder.val b|ₘ ≤ |MulArchimedeanOrder.val a|ₘ ^ n }
-- Mathlib.Geometry.Manifold.Instances.Quotient
AddAction.instChartedSpaceQuotient.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] {G : Type u_2} [inst_1 : AddGroup G] [inst_2 : AddAction G M]
  [inst_3 : ProperlyDiscontinuousVAdd G M] [inst_4 : ContinuousConstVAdd G M] [inst_5 : IsCancelVAdd G M]
  [inst_6 : T2Space M] [inst_7 : LocallyCompactSpace M] {H : Type u_3} [inst_8 : TopologicalSpace H]
  [inst_9 : ChartedSpace H M], AddAction.instChartedSpaceQuotient = ⋯.chartedSpace ⋯
-- Init.Data.UInt.Basic
instMaxUSize : Max USize
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.beqModel.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValueCast? x.fst l₂ == some x.snd
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.F : {α : Type u_1} → {f : Filter α} → (self : f.Realizer) → CFilter (Set α) self.σ
-- Mathlib.RingTheory.Polynomial.Wronskian
Polynomial.wronskian_neg_left : ∀ {R : Type u_1} [inst : CommRing R] (a b : Polynomial R), (-a).wronskian b = -a.wronskian b
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteLimits.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsFiniteLimits F] (J : Type)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), insert a s = {a} ∪ s
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.codRestrict_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₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c ∈ p} (x : M), ↑((LinearMap.codRestrict p f h) x) = f x
-- Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid
/-- `toNormalizedGCDMonoid` constructs a GCD monoid out of a normalization on a
unique factorization domain.  -/
UniqueFactorizationMonoid.toNormalizedGCDMonoid : (α : Type u_2) →
  [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → [NormalizationMonoid α] → NormalizedGCDMonoid α
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.lawfulMonad : LawfulMonad Stream'.Seq1
-- Mathlib.Data.Set.Card
Set.encard_sdiff_add_encard_of_subset : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → (t \ s).encard + s.encard = t.encard
-- Lean.Meta.LazyDiscrTree
/-- Constructs an initial entry from an expression and value.
 -/
Lean.Meta.LazyDiscrTree.InitEntry.fromExpr : {α : Type} → Lean.Expr → α → Lean.MetaM (Lean.Meta.LazyDiscrTree.InitEntry α)
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.hasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Over X)],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.MonoOver X)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.exists_measurableSet_of_ne : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α},
  x ≠ y → ∃ s, MeasurableSet s ∧ x ∈ s ∧ y ∉ s
-- Lean.DocString.Parser
/-- Parses a footnote.  -/
Lean.Doc.Parser.footnote : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_one : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K], ArchimedeanClass.stdPart 1 = 1
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.instCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.Category.{v, max (v + 1) u} (CommBialgCat R)
-- Std.Data.TreeMap.Raw.Iterator
_private.Std.Data.TreeMap.Raw.Iterator.0.Std.TreeMap.Raw.iter.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Std.TreeMap.Raw α β cmp),
  m.iter = Std.Iter.map (fun e => (e.fst, e.snd)) m.inner.iter
-- Lean.Parser.Command
Lean.Parser.Command.deprecatedSyntax.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_smul_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.BalancedAtRoot.erase_right : ∀ {l r r' : ℕ},
  Std.DTreeMap.Internal.Impl.BalancedAtRoot l r →
    r - 1 ≤ r' → r' ≤ r → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l r'
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.assoc_inv_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (h : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) {Z : C} (h_1 : (h.F (m₁ + m₂ + m₃)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((h.F m₃).map ((h.add m₁ m₂).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((h.add (m₁ + m₂) m₃).inv.app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((h.add m₂ m₃).inv.app ((h.F m₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((h.add m₁ (m₂ + m₃)).inv.app X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} {inv : Bool} (aig : Std.Sat.AIG α)
  (curr : ℕ) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO_def : ∀ {α : Type u_18} {E : Type u_19} {F : Type u_20} [inst : Norm E] [inst_1 : Norm F] (l : Filter α) (f : α → E)
  (g : α → F), f =o[l] g = ∀ ⦃c : ℝ⦄, 0 < c → Asymptotics.IsBigOWith c l f g
-- Lean.Meta.Tactic.Grind.Attr
_private.Lean.Meta.Tactic.Grind.Attr.0.Lean.Meta.Grind.Extension.eraseEMatchAttr : Lean.Meta.Grind.Extension → Lean.Name → Lean.MetaM Unit
-- Mathlib.GroupTheory.Index
AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {X : Type u_3} [inst_1 : AddAction G X]
  [AddAction.IsPretransitive G X], H.index ≠ 0 → Finite (AddAction.orbitRel.Quotient (↥H) X)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ⟶ b` and `ψ : b ⟶ c` lift `𝟙 R`, then so does `φ ≫ ψ`  -/
CategoryTheory.IsHomLift.comp_of_lift_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) (R : 𝒮) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c)
  [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ] [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ],
  p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_sum : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {X : Type u_2} (s : Finset X) (f : X → MvPolynomial σ R)
  (m : σ →₀ ℕ), MvPolynomial.coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, MvPolynomial.coeff m (f x)
-- Mathlib.Analysis.Normed.Module.Ball.Action
isScalarTower_sphere_sphere_ball : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜']
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜' E] {r : ℝ}
  [inst_5 : NormedAlgebra 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E],
  IsScalarTower ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- If a Riemannian bundle structure is defined using `g.toRiemannianMetric` where `g` is
a `ContinuousRiemannianMetric`, then we make sure typeclass inference can infer automatically
that the bundle is a continuous Riemannian bundle.  -/
Bundle.instIsContinuousRiemannianBundle : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)]
  [inst_7 : ∀ (b : B), IsTopologicalAddGroup (E b)] [inst_8 : ∀ (b : B), ContinuousConstSMul ℝ (E b)]
  [inst_9 : FiberBundle F E] [inst_10 : VectorBundle ℝ F E] (g : Bundle.ContinuousRiemannianMetric F E),
  IsContinuousRiemannianBundle F E
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_bot_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  ⊥.relfinrank A = Module.finrank F ↥A
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.localInstances₂ : Aesop.EqualUpToIds.GoalContext → Lean.LocalInstances
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitInv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f)) (e.unitInv.app X) =
    CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) f
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.lsingle.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Module R S] (a : M),
  MonoidAlgebra.lsingle a = ↑(MonoidAlgebra.coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle a
-- Mathlib.Order.Monotone.Basic
StrictAnti.maximal_of_minimal_image : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ {a : α}, (∀ (p : β), f a ≤ p) → ∀ (x : α), x ≤ a
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.one_def : ∀ {n : ℕ}, 1 = QuaternionGroup.a 0
-- Std.Data.HashMap.Basic
/-- Groups the elements of an array `xs` according to the function `key`, returning a hash map in which
each group is associated with its key. Groups preserve the relative order of elements in `xs`.

Example:
```lean example
#eval #[0, 1, 2, 3, 4, 5, 6].groupByKey (· % 2)
```
```output
Std.HashMap.ofList [(0, #[0, 2, 4, 6]), (1, #[1, 3, 5])]
```
 -/
Array.groupByKey : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (β → α) → Array β → Std.HashMap α (Array β)
-- Mathlib.RingTheory.PowerSeries.Order
/-- If `n` is strictly smaller than the order of `ψ`, then the `n`th coefficient of its product
with any other power series is `0`.  -/
PowerSeries.coeff_mul_of_lt_order : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : PowerSeries R} {n : ℕ}, ↑n < ψ.order → (PowerSeries.coeff n) (φ * ψ) = 0
-- Aesop.Rule
Aesop.defaultSuccessProbability : Aesop.Percent
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.isBasis_of_subset_of_subset_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.Indep I → I ⊆ X → X ⊆ M.closure I → M.IsBasis I X
-- Batteries.Tactic.PrintPrefix
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.lexNameLt : Lean.Name → Lean.Name → Bool
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.comap_comp : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} {N : Type u_3} [inst_1 : Group H] [inst_2 : Group N] (f : G →* H)
  (g : H →* N) (K : FiniteIndexNormalSubgroup N),
  FiniteIndexNormalSubgroup.comap (g.comp f) K = FiniteIndexNormalSubgroup.comap f (FiniteIndexNormalSubgroup.comap g K)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.continuous : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂), Continuous ⇑f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.refl_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), ((Path.refl x₀).trans p).Homotopic p