mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.diagramObj.eq_1 : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : SemilatticeInf α] (a : ι),
  CategoryTheory.Pairwise.diagramObj U (CategoryTheory.Pairwise.single a) = U a
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, `M'` and `N'` are submodules of `M` and `N`,
respectively, such that `M` and `N'` are flat, then `M'` and `N'` are also linearly disjoint.  -/
Submodule.LinearDisjoint.of_le_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ {M' N' : Submodule R S}, M' ≤ M → N' ≤ N → ∀ [Module.Flat R ↥M] [Module.Flat R ↥N'], M'.LinearDisjoint N'
-- Mathlib.Dynamics.PeriodicPts.Defs
/-- The definition of a periodic orbit, in terms of `Cycle.map`.  -/
Function.periodicOrbit_eq_cycle_map : ∀ {α : Type u_1} (f : α → α) (x : α),
  Function.periodicOrbit f x = Cycle.map (fun n => f^[n] x) ↑(List.range (Function.minimalPeriod f x))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_expandIfNecessary : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  (Std.DHashMap.Internal.toListModel (↑m.expandIfNecessary).buckets).Perm
    (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.RingTheory.Localization.Defs
/-- Given `z : S`, `IsLocalization.sec M z` is defined to be a pair `(x, y) : R × M` such
that `z * f y = f x` (so this lemma is true by definition).  -/
IsLocalization.sec_spec : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (z : S),
  z * (algebraMap R S) ↑(IsLocalization.sec M z).2 = (algebraMap R S) (IsLocalization.sec M z).1
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.response.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β] (x : Except IO.Error (Std.Http.Response β)),
  sizeOf (Std.Http.Server.Connection.Recv.response✝ x) = 1 + sizeOf x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between the negation of a nonzero vector and that vector is `π`.  -/
Orientation.oangle_neg_self_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → o.oangle (-x) x = ↑Real.pi
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R), ↑s.toSubsemigroup = ↑s
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ComonToMonOpOp_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Comon C} (f : X ⟶ Y),
  (CategoryTheory.Comon.ComonToMonOpOp C).map f = Opposite.op { hom := f.hom.op, isMonHom_hom := ⋯ }
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.w : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (φ : f ⟶ g),
  CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.Under.Hom.right φ) = g.hom
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_erase : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF → ∀ {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Mathlib.RingTheory.ClassGroup.Basic
coe_toPrincipalIdeal : ∀ {R : Type u_1} {K : Type u_2} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] (x : Kˣ),
  ↑((toPrincipalIdeal R K) x) = FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `lt_of_tsub_lt_tsub_left_of_le` for a weaker statement in a partial order.  -/
lt_of_tsub_lt_tsub_left : ∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α]
  [AddLeftMono α], a - b < a - c → c < b
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.ι_colimitConstInitial_hom_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasInitial C] {j : J} {Z : C}
  (h : ⊥_ C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.colimitConstInitial.hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.initial.to (⊥_ C)) h
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  (f : PowerSeries A) (k : ℕ) {i : ℕ},
  i ≥ ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → (PowerSeries.coeff i) (f - g * H.seq f k) ∈ I ^ k
-- Mathlib.Algebra.Divisibility.Units
/-- In a monoid, an element `a` divides an element `b` iff all associates of `a` divide `b`.  -/
Units.mul_right_dvd : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {u : αˣ}, a * ↑u ∣ b ↔ a ∣ b
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_iff_prime_squarefree : ∀ {n : ℕ}, Squarefree n ↔ ∀ (x : ℕ), Nat.Prime x → ¬x * x ∣ n
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.pre : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.sInf_le : ∀ {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α}, t ∈ tt → sInf tt ≤ t
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_eq_zero : ∀ {n : ℕ}, Nat.fib n = 0 ↔ n = 0
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_empty' : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (f : α → M), ∅.mulIndicator f = 1
-- Lean.Meta.Tactic.Grind.Proj
/-- If `parent` is a projection-application `proj_i c`,
check whether the root of the equivalence class containing `c` is a constructor-application `ctor ... a_i ...`.
If so, internalize the term `proj_i (ctor ... a_i ...)` and add the equality `proj_i (ctor ... a_i ...) = a_i`.
 -/
Lean.Meta.Grind.propagateProjEq : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The universal property of a limit cone: a map `W ⟶ X` is the same as
a cone on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsLimit.homIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t →
              (W : C) → ULift.{u₁, v₃} (W ⟶ t.pt) ≅ (CategoryTheory.Functor.const J).obj W ⟶ F
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.id_mapId : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  (CategoryTheory.Pseudofunctor.id B).mapId a = CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Data.Finset.SDiff
Finset.insert_sdiff_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) {t : Finset α} {x : α}, x ∉ t → insert x s \ t = insert x (s \ t)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.tracedForM : {α : Type u_1} →
  Array α →
    (α → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit) →
      StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.Data.Fintype.EquivFin
Fintype.exists_pair_of_one_lt_card : ∀ {α : Type u_1} [inst : Fintype α], 1 < Fintype.card α → ∃ a b, a ≠ b
-- Mathlib.RingTheory.Algebraic.Basic
/-- Given a transcendental element `s : S` over `R`, the `R`-algebra equivalence
between `R[X]` and `R[s]` given by sending `X` to `s`.  -/
Polynomial.algEquivOfTranscendental : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → [inst_2 : Algebra R S] → (s : S) → Transcendental R s → Polynomial R ≃ₐ[R] ↥R[s]
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.equivSMul_apply_coe : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Group α] [inst_2 : MulDistribMulAction α G] (a : α)
  (H : Subgroup G) (x : ↑↑H.toSubmonoid), ↑((Subgroup.equivSMul a H) x) = a • ↑x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ ∩ m₂)[k]? = if k ∈ m₂ then m₁[k]? else none
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.instDecidableEqDyadic.decEq.match_1.eq_2 : ∀ (motive : Dyadic → Dyadic → Sort u_1) (n k : ℤ) (hn : n % 2 = 1) (h_1 : Unit → motive Dyadic.zero Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive Dyadic.zero (Dyadic.ofOdd n k hn))
  (h_3 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn) Dyadic.zero)
  (h_4 :
    (a a_1 : ℤ) →
      (a_2 : a % 2 = 1) → (b b_1 : ℤ) → (b_2 : b % 2 = 1) → motive (Dyadic.ofOdd a a_1 a_2) (Dyadic.ofOdd b b_1 b_2)),
  (match Dyadic.zero, Dyadic.ofOdd n k hn with
    | Dyadic.zero, Dyadic.zero => h_1 ()
    | Dyadic.zero, Dyadic.ofOdd n k hn => h_2 n k hn
    | Dyadic.ofOdd n k hn, Dyadic.zero => h_3 n k hn
    | Dyadic.ofOdd a a_1 a_2, Dyadic.ofOdd b b_1 b_2 => h_4 a a_1 a_2 b b_1 b_2) =
    h_2 n k hn
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_id_map : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → ProbabilityTheory.mgf id (MeasureTheory.Measure.map X μ) = ProbabilityTheory.mgf X μ
-- Mathlib.Order.ModularLattice
/-- A modular lattice is one with a limited associativity between `⊓` and `⊔`.  -/
IsModularLattice : (α : Type u_2) → [Lattice α] → Prop
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe : ∀ (s : (n : ℕ) × Finset (Fin n)),
  ↑(FormalMultilinearSeries.changeOriginIndexEquiv.symm s).snd.snd = Finset.map (finCongr ⋯).toEmbedding s.snd
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.nondegenerate_iff_separatingLeft : ∀ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] {B : M →ₗ[R] M →ₗ[R] M₁},
  B.IsRefl → (B.Nondegenerate ↔ B.SeparatingLeft)
-- Mathlib.RingTheory.Localization.Ideal
/-- If `R` is a ring, then prime ideals in the localization at `M`
correspond to prime ideals in the original ring `R` that are disjoint from `M`.
This lemma gives the particular case for an ideal and its comap,
see `le_rel_iso_of_prime` for the more general relation isomorphism  -/
IsLocalization.isPrime_iff_isPrime_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (J : Ideal S),
  J.IsPrime ↔ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)
-- Lean.Meta.Sym.SymM
/-- State for registered `SymExtension`s, indexed by extension id.  -/
Lean.Meta.Sym.State.extensions : Lean.Meta.Sym.State → Array Lean.Meta.Sym.SymExtensionState
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomain_single_map : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f) (m : M)
  (r : R), AddMonoidAlgebra.comapDomain f hf (AddMonoidAlgebra.single (f m) r) = AddMonoidAlgebra.single m r
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.left_lt_opow : ∀ {a b : Ordinal.{u_1}}, 1 < a → 1 < b → a < a ^ b
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_startPos : ∀ {s : String} {pos : s.Pos}, String.Pos.ofSliceFrom (s.sliceFrom pos).startPos = pos
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The functor defined by the under categories  -/
CategoryTheory.Under.mapFunctor : (T : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} T] → CategoryTheory.Functor Tᵒᵖ CategoryTheory.Cat
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given a surjective addition-preserving function `f` whose kernel is contained in
an additive congruence relation `c`, the additive congruence relation on `f`'s codomain defined
by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` by `c`.'  -/
AddCon.mapOfSurjective : {M : Type u_1} →
  {N : Type u_2} →
    {F : Type u_4} →
      [inst : Add M] →
        [inst_1 : Add N] →
          [inst_2 : FunLike F M N] →
            [inst_3 : AddHomClass F M N] →
              {c : AddCon M} → (f : F) → AddCon.ker f ≤ c → Function.Surjective ⇑f → AddCon N
-- Mathlib.Topology.Sheaves.Skyscraper
/-- The cocone at `A` for the stalk functor of `skyscraperPresheaf p₀ A` when `y ∈ closure {p₀}` is a
colimit
 -/
skyscraperPresheafCoconeIsColimitOfSpecializes : {X : TopCat} →
  (p₀ : ↑X) →
    [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] →
      {C : Type v} →
        [inst_1 : CategoryTheory.Category.{u, v} C] →
          (A : C) →
            [inst_2 : CategoryTheory.Limits.HasTerminal C] →
              {y : ↑X} → (h : p₀ ⤳ y) → CategoryTheory.Limits.IsColimit (skyscraperPresheafCoconeOfSpecializes p₀ A h)
-- Mathlib.Analysis.Calculus.Gradient.Basic
DifferentiableOn.hasGradientAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {s : Set F},
  DifferentiableOn 𝕜 f s → s ∈ nhds x → HasGradientAt f (gradient f x) x
-- Mathlib.Order.SymmDiff
Disjoint.symmDiff_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b c : α},
  Disjoint a b → Disjoint a c → Disjoint a (symmDiff b c)
-- Mathlib.Data.Finmap
Finmap.lookup_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), Finmap.lookup a ∅ = none
-- Aesop.Builder.Cases
Aesop.RuleBuilder.getCasesIndexingMode : Lean.Name → Lean.Meta.TransparencyMode → Array Aesop.CasesPattern → Lean.MetaM Aesop.IndexingMode
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks.0.CategoryTheory.Limits.WidePushoutShape.mkCocone.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePushoutShape J → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (j : J) → motive (some j)),
  (match none with
    | none => h_1 ()
    | some j => h_2 j) =
    h_1 ()
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
_private.Mathlib.CategoryTheory.Functor.KanExtension.Pointwise.0.CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_natIso_left : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} (F : CategoryTheory.Functor C H) {L' : CategoryTheory.Functor C D} (e : L ≅ L')
  (Y : D), L.HasPointwiseRightKanExtensionAt F Y ↔ L'.HasPointwiseRightKanExtensionAt F Y
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `b` is a binary bicone such that `b.fst` is a cokernel of `b.inr`, then `b` is a bilimit
bicone.  -/
CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        (b : CategoryTheory.Limits.BinaryBicone X Y) → CategoryTheory.Limits.IsColimit b.inrCokernelCofork → b.IsBilimit
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_apply_coe : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (z : S) (i : Fin f.natDegree), h.coeff z ↑i = (h.basis.repr z) i
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.sub_toProd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A]
  (a b : DoubleCentralizer 𝕜 A), (a - b).toProd = a.toProd - b.toProd
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : t.alter k f ≠ ∅},
  (t.alter k f).minKey he = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  (p : ℕ), p + 1 = n → (R.extMk f m hm hf = 0 ↔ ∃ g, CategoryTheory.CategoryStruct.comp g (R.cocomplex.d p n) = f)
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.below : {α : Type u_3} →
  {s : Set (Set α)} →
    {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop} →
      {a : Set α} → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop
-- Mathlib.Combinatorics.Quiver.Covering
/-- A prefunctor induces a map of path stars.  -/
Prefunctor.pathStar : {U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → (φ : U ⥤q V) → (u : U) → Quiver.PathStar u → Quiver.PathStar (φ.obj u)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_of_measurable_nnreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ENNReal → α}, (Measurable fun p => f ↑p) → Measurable f
-- Mathlib.Control.Fix
Part.hasFix : {α : Type u_1} → Fix (Part α)
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_eq_ofNat : ∀ {r : ℝ} {n : ℕ} [inst : n.AtLeastTwo], ENNReal.ofReal r = OfNat.ofNat n ↔ r = OfNat.ofNat n
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_X_le_single : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {s : σ},
  m.toSyn (m.degree (MvPolynomial.X s)) ≤ m.toSyn fun₀ | s => 1
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_iff_pred_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [inst_2 : SuccOrder α] {a b : α},
  b ≤ Order.succ a ↔ Order.pred b ≤ a
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_zero_iff : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {r : ℝ}, a ∈ Metric.ball 0 r ↔ ‖a‖ < r
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_sum : ∀ {ι : Type u_1} {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (s : Finset ι)
  (ψ : ι → AddChar A M), ⇑(∑ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- If equivalences `E : C ≌ D` and `E' : D ≌ F` are triangulated, so is `E.trans E'`.
 -/
CategoryTheory.Equivalence.IsTriangulated.trans : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] (E : C ≌ D) [inst_12 : E.functor.CommShift ℤ]
  [inst_13 : E.inverse.CommShift ℤ] [E.CommShift ℤ] {D' : Type u_3} [inst_15 : CategoryTheory.Category.{v_3, u_3} D']
  [inst_16 : CategoryTheory.Limits.HasZeroObject D'] [inst_17 : CategoryTheory.Preadditive D']
  [inst_18 : CategoryTheory.HasShift D' ℤ] [inst_19 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D' n).Additive]
  [inst_20 : CategoryTheory.Pretriangulated D'] {E' : D ≌ D'} [inst_21 : E'.functor.CommShift ℤ]
  [inst_22 : E'.inverse.CommShift ℤ] [E'.CommShift ℤ] [E.IsTriangulated] [E'.IsTriangulated],
  (E.trans E').IsTriangulated
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- If `f : G → H` is a multiplicative homomorphism between two additive monoids, then
`AddMonoidAlgebra.mapDomain f` is a ring homomorphism between their additive monoid algebras.  -/
AddMonoidAlgebra.mapDomainRingHom : (R : Type u_3) →
  {M : Type u_6} →
    {N : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddMonoid M] → [inst_2 : AddMonoid N] → (M →+ N) → AddMonoidAlgebra R M →+* AddMonoidAlgebra R N
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.mk : String →
  Option Lean.Lsp.InlayHintTooltip → Option Lean.Lsp.Location → Option Lean.Lsp.Command → Lean.Lsp.InlayHintLabelPart
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → M.Indep I
-- Mathlib.Algebra.GradedMonoid
/-- A version of `GradedMonoid.ghas_one` for internally graded objects.  -/
SetLike.GradedMul : {ι : Type u_1} → {R : Type u_2} → {S : Type u_3} → [SetLike S R] → [Mul R] → [Add ι] → (ι → S) → Prop
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.interSmaller : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Raw α β → Std.DHashMap.Internal.Raw₀ α β
-- Init.Prelude
/-- Adds an element to the end of an array. The resulting array's size is one greater than the input
array. If there are no other references to the array, then it is modified in-place.

This takes amortized `O(1)` time because `ByteArray` is represented by a dynamic array.
 -/
ByteArray.push : ByteArray → UInt8 → ByteArray
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  [inst_8 : DecidableEq ι] (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F),
  ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f.fderivCompContinuousLinearMap g =
    (f.fderivCompContinuousLinearMap fun x => g) ∘SL
      ContinuousLinearMap.pi fun x => ContinuousLinearMap.id 𝕜 (E →L[𝕜] F)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.TreeSet.Raw.ofList l cmp).get! k = default
-- Init.Data.Vector.Lemmas
Vector.foldr_map : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {n : ℕ} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Vector α₁ n} {init : β},
  Vector.foldr g init (Vector.map f xs) = Vector.foldr (fun x y => g (f x) y) init xs
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.toLinearMap'_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [inst : CommRing R]
  [inst_1 : CommRing A₁] [inst_2 : LieRing L₁] [inst_3 : Module A₁ L₁] [inst_4 : LieRingModule L₁ A₁]
  [inst_5 : CommRing A₂] [inst_6 : LieRing L₂] [inst_7 : Module A₂ L₂] [inst_8 : LieRingModule L₂ A₂]
  [inst_9 : Algebra R A₁] [inst_10 : LieAlgebra R L₁] [inst_11 : Algebra R A₂] [inst_12 : LieAlgebra R L₂]
  {σ₁₂ : A₁ →ₐ[R] A₂} (f : LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) (x : L₁), f.toLinearMap' x = f.toLieHom x
-- Lean.Compiler.InitAttr
_private.Lean.Compiler.InitAttr.0.Lean.registerInitAttrInner : Lean.Name → Bool → Lean.Name → IO (Lean.ParametricAttribute Lean.Name)
-- Init.Data.List.Lemmas
List.length_le_length_insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, l.length ≤ (List.insert a l).length