mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) (j : J) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.ι.app j)
      (CategoryTheory.CategoryStruct.comp (P.coconePointUniqueUpToIso Q).hom h) =
    CategoryTheory.CategoryStruct.comp (t.ι.app j) h
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.inv : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Inv β]
  [ContinuousInv β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable f⁻¹
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtHashMap.unitOfList l).getKey? k' = some k
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instAddCommGroup : {A : Type u_1} →
  {G : Type u_2} →
    [inst : Semiring A] →
      [inst_1 : Monoid G] →
        {V : Type u_6} →
          {W : Type u_7} →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommGroup W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → AddCommGroup (ρ.IntertwiningMap σ)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.le_of_inf_neBot' : ∀ {α : Type u} (f : Ultrafilter α) {g : Filter α}, (g ⊓ ↑f).NeBot → ↑f ≤ g
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreservingₗ_apply : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  (𝕜 : Type u_8) [inst_2 : NormedRing 𝕜] [inst_3 : Module 𝕜 E] [inst_4 : IsBoundedSMul 𝕜 E] (f : α → β)
  (hf : MeasureTheory.MeasurePreserving f μ μb) (a : ↥(MeasureTheory.Lp E p μb)),
  (MeasureTheory.Lp.compMeasurePreservingₗ 𝕜 f hf) a = (↑(MeasureTheory.Lp.compMeasurePreserving f hf)).toFun a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback b : β a}, (t.insert a b).getD a fallback = b
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_sq_mul_cos_sq : ∀ {a b : ℝ},
  ∫ (x : ℝ) in a..b, Real.sin x ^ 2 * Real.cos x ^ 2 = (b - a) / 8 - (Real.sin (4 * b) - Real.sin (4 * a)) / 32
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.instMulOfIsOrderedMonoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : CommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedMonoid β],
  OrderMonoidHom.instMulOfIsOrderedMonoid =
    {
      mul := fun f g =>
        let __src := ↑f * ↑g;
        { toMonoidHom := __src, monotone' := ⋯ } }
-- Mathlib.Order.Bounds.Basic
/-- The least upper bound of a set is also the least upper bound of any cofinal subset.  -/
IsLUB.of_isCofinalFor : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {s t : Set α}, IsLUB s a → t ⊆ s → IsCofinalFor s t → IsLUB t a
-- Mathlib.Computability.Encoding
/-- An arbitrary section of the natural inclusion of `Bool` in `Γ'`.  -/
Computability.sectionΓ'Bool : Computability.Γ' → Bool
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit : ∀ {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] {F : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : D),
  CategoryTheory.CategoryStruct.comp (F.map ((adj1.rightAdjointUniq adj2).hom.app x)) (adj2.counit.app x) =
    adj1.counit.app x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.k : Lean.Grind.CommRing.Power → ℕ
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.instNonUnitalRing : {α : Type u₁} → {β : Type u₂} → [inst : NonUnitalRing β] → NonUnitalRing (α →₀ β)
-- Lean.Level
Lean.Level.param.inj : ∀ {a a_1 : Lean.Name}, Lean.Level.param a = Lean.Level.param a_1 → a = a_1
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalCommRing : {R : Type u_1} → {M : Type u_4} → [inst : CommRing R] → [CommSemigroup M] → NonUnitalCommRing (MonoidAlgebra R M)
-- Lean.Meta.Tactic.SplitIf
Lean.Meta.SplitIf.splitIfAt? : Lean.MVarId → Lean.Expr → Option Lean.Name → Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))
-- Mathlib.CategoryTheory.Yoneda
/-- A functor `F : Cᵒᵖ ⥤ Type v` is representable if there is an object `Y` with a structure
`F.RepresentableBy Y`, i.e. there is a natural bijection `(X ⟶ Y) ≃ F.obj (op X)`,
which may also be rephrased as a natural isomorphism `yoneda.obj X ≅ F` when `Category.{v} C`.  -/
CategoryTheory.Functor.IsRepresentable : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᵒᵖ (Type v) → Prop
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isLeftInversion_inv_iff : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w t : W},
  cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- Given a column partitioned matrix extract the first column  -/
Matrix.toCols₁ : {R : Type u_1} → {m : Type u_2} → {n₁ : Type u_6} → {n₂ : Type u_7} → Matrix m (n₁ ⊕ n₂) R → Matrix m n₁ R
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- If `G : C ⥤ D` is a dense subsite and `F` a sheaf on `C`, this is the morphism
`F.val.obj (op Y) ⟶ F.val.obj (op X)` induced by a morphism
`G.obj X ⟶ G.obj Y` in the category `D`.  -/
CategoryTheory.Functor.IsDenseSubsite.mapPreimage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (K : CategoryTheory.GrothendieckTopology D) →
            (G : CategoryTheory.Functor C D) →
              {A : Type u_4} →
                [inst_2 : CategoryTheory.Category.{v_4, u_4} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J K G] →
                    (F : CategoryTheory.Sheaf J A) →
                      {X Y : C} → (G.obj X ⟶ G.obj Y) → (F.obj.obj (Opposite.op Y) ⟶ F.obj.obj (Opposite.op X))
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.isChain_of_isChain_cons`. -/
List.IsChain.of_cons : ∀ {α : Type u_1} {R : α → α → Prop} {b : α} {l : List α}, List.IsChain R (b :: l) → List.IsChain R l
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basis
/-- A basis on `M` can be lifted to a basis on `SymmetricAlgebra R M`.  -/
Module.Basis.symmetricAlgebra : {κ : Type uκ} →
  {R : Type uR} →
    {M : Type uM} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.Basis κ R M → Module.Basis (κ →₀ ℕ) R (SymmetricAlgebra R M)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Raw.Const.insertMany t l).getKey? k = t.getKey? k
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- Construct an ultrafilter extending a given filter.
The ultrafilter lemma is the assertion that such a filter exists;
we use the axiom of choice to pick one.  -/
Ultrafilter.of : {α : Type u} → (f : Filter α) → [f.NeBot] → Ultrafilter α
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k : α} (mem : k ∈ m) {h : k ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l).getKey k h = m.getKey k mem
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprTZifV2 : Repr Std.Time.TimeZone.TZif.TZifV2
-- Mathlib.Data.Rat.Cast.Order
NNRat.preimage_cast_Icc : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0),
  NNRat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
-- Mathlib.Logic.Relation
Relation.TransGen.head_induction_on : ∀ {α : Type u_1} {r : α → α → Prop} {b : α} {motive : (a : α) → Relation.TransGen r a b → Prop} {a : α}
  (h : Relation.TransGen r a b),
  (∀ {a : α} (h : r a b), motive a ⋯) →
    (∀ {a c : α} (h' : r a c) (h : Relation.TransGen r c b), motive c h → motive a ⋯) → motive a h
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instSemigroupQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : Semigroup R] → (c : RingCon R) → Semigroup c.Quotient
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι d.functor i) d.toBase =
    CategoryTheory.CategoryStruct.comp (d.natTrans.app i) (𝒰.f i)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprLambdaTheoremArgs : Repr Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.Data.Set.Sigma
biSup_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [inst : CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i))
  (f : Sigma α → β), ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
-- Aesop.Forward.State
Aesop.VariableMap.mk.injEq : ∀ (map map_1 : Lean.PHashMap Aesop.PremiseIndex Aesop.InstMap), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.Dynamics.BirkhoffSum.Basic
birkhoffSum_zero' : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : α → α) (g : α → M), birkhoffSum f g 0 = 0
-- Mathlib.Algebra.Group.Pi.Basic
Function.extend_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Sub γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ),
  Function.extend f (g₁ - g₂) (e₁ - e₂) = Function.extend f g₁ e₁ - Function.extend f g₂ e₂
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_unique : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [inst_1 : Unique ι] {s : ι → α},
  ⨅ i, s i = s default
-- Mathlib.Analysis.Complex.Liouville
/-- An auxiliary lemma for Liouville's theorem `Differentiable.apply_eq_apply_of_bounded`.  -/
Complex.liouville_theorem_aux : ∀ {F : Type v} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F},
  Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∀ (z w : ℂ), f z = f w
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.symm_neg : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (LinearEquiv.neg R).symm = LinearEquiv.neg R
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertListIfNewUnit_of_contains : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.getKey? k (Std.Internal.List.insertListIfNewUnit l toInsert) = Std.Internal.List.getKey? k l
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit.congr_simp : ∀ {α : Type u} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (l l_1 : ρ),
  l = l_1 →
    ∀ (h : t.Balanced),
      Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l h =
        Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l_1 h
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₂ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_dist_aux : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (n k : ℕ),
  ‖newton_seq_gen✝ hnorm (n + k) - newton_seq_gen✝ hnorm n‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen✝ p F a ^ 2 ^ n
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNatClamp_of_le : ∀ {n : ℕ}, UInt8.size ≤ n → (UInt8.ofNatClamp n).toNat = UInt8.size - 1
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.eq_tsub_iff_add_eq_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable c → c ≤ b → (a = b - c ↔ a + c = b)
-- Lean.Parser.Types
Lean.Parser.minPrec : ℕ
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getPatternVarsEx : Lean.Term → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.differentiableWithinAt_Ioi_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ}, ConvexOn ℝ S f → x ∈ interior S → DifferentiableWithinAt ℝ f (Set.Ioi x) x
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUInt64HOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instLargeCategory : CategoryTheory.LargeCategory SemiNormedGrp₁
-- Batteries.Data.List.Scan
List.getElem_partialProds : ∀ {α : Type u_1} {i : ℕ} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {l : List α} (h : i < l.partialProds.length),
  l.partialProds[i] = (List.take i l).prod
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α]
  {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.mk.inj : ∀ {catName : Lean.Name} {first leftRec : Bool} {behavior : Lean.Parser.LeadingIdentBehavior} {catName_1 : Lean.Name}
  {first_1 leftRec_1 : Bool} {behavior_1 : Lean.Parser.LeadingIdentBehavior},
  { catName := catName, first := first, leftRec := leftRec, behavior := behavior } =
      { catName := catName_1, first := first_1, leftRec := leftRec_1, behavior := behavior_1 } →
    catName = catName_1 ∧ first = first_1 ∧ leftRec = leftRec_1 ∧ behavior = behavior_1
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.of_isLocalization : ∀ {R : Type u_2} {Rₘ : Type u_4} [inst : CommRing R] [inst_1 : CommRing Rₘ] (M : Submonoid R) [inst_2 : Algebra R Rₘ]
  [IsLocalization M Rₘ], Algebra.FormallyEtale R Rₘ
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Descr.addEntry : {α β σ : Type} → Lean.ScopedEnvExtension.Descr α β σ → σ → β → σ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.place_conjugate : ∀ {K : Type u_1} [inst : Field K] (φ : K →+* ℂ),
  NumberField.place (NumberField.ComplexEmbedding.conjugate φ) = NumberField.place φ
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.impTo.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- This is the same as `ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀`,
where `embed` is upgraded to `orderMonoidIso`.  -/
ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀ : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible] (x : R),
  (ValuativeRel.ValueGroupWithZero.orderMonoidIso v) ((ValuativeRel.valuation R) x) =
    (MonoidWithZeroHom.ValueGroup₀.restrict₀ (MonoidWithZeroHom.ofClass v)) x
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.invFun.eq_1 : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (M : Matrix n n A),
  MatrixEquivTensor.invFun n R A M = ∑ p, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
mulRothNumber_map_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : CancelCommMonoid α] (s : Finset α) (a : α),
  mulRothNumber (Finset.map (mulLeftEmbedding a) s) = mulRothNumber s
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_ne_top_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.eRk X ≠ ⊤ ↔ M.IsRkFinite X
-- Mathlib.RingTheory.PicardGroup
/-- The group homomorphism from the invertible submodules in a faithful algebra over `R` to
the Picard group of `R`. See Lemma 2.2 in [RobertsSingh1993].  -/
Submodule.unitsToPic : (R : Type u) →
  (A : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [FaithfulSMul R A] → (Submodule R A)ˣ →* CommRing.Pic R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {hc : t.minKey he ∈ t}, t.getKey (t.minKey he) hc = t.minKey he
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Modular forms of weight 2 for `𝒮ℒ` are zero.  -/
ModularForm.levelOne_weight_two_rank_zero : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2) = 0
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.associator_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  (H : CategoryTheory.Functor E E') (x : C),
  (F.associator G H).hom.app x = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x)
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.Measure.MeasureDense.nonempty' : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 → {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}.Nonempty
-- Mathlib.Algebra.Lie.TraceForm
/-- Given a representation `M` of a Lie algebra `L`, the action of any `x : L` is skew-adjoint
w.r.t. the trace form.  -/
LieModule.traceForm_apply_lie_apply' : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y z : L),
  ((LieModule.traceForm R L M) ⁅x, y⁆) z = -((LieModule.traceForm R L M) y) ⁅x, z⁆
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.SimpleFunc.exists_lt_lintegral_simpleFunc_of_lt_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f : MeasureTheory.SimpleFunc α NNReal} {L : ENNReal},
  L < ∫⁻ (x : α), ↑(f x) ∂μ → ∃ g, (∀ (x : α), g x ≤ f x) ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(g x) ∂μ
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.toNat_natCast`. -/
ENat.toNat_coe : ∀ (n : ℕ), (↑n).toNat = n
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.bicategory_leftUnitor_hom_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} (f : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor f).hom.unop2 = (CategoryTheory.Bicategory.rightUnitor f.unop).hom
-- Mathlib.Algebra.GroupWithZero.Units.Basic
pow_sub₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {m n : ℕ} (a : G₀), a ≠ 0 → n ≤ m → a ^ (m - n) = a ^ m * (a ^ n)⁻¹
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node4L : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α}
  {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) m ↑y →
      Ordnode.Valid' (↑y) r o₂ →
        0 < m.size →
          l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
              0 < l.size ∧
                Ordnode.ratio * r.size ≤ m.size ∧
                  Ordnode.delta * l.size ≤ m.size + r.size ∧
                    3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ Ordnode.delta * r.size →
            Ordnode.Valid' o₁ (l.node4L x m y r) o₂
-- Mathlib.Algebra.Regular.Basic
/-- An element is right-regular if and only if multiplying it on the right with a right-regular
element is right-regular.  -/
mul_isRightRegular_iff : ∀ {R : Type u_1} [inst : Semigroup R] {a : R} (b : R), IsRightRegular a → (IsRightRegular (b * a) ↔ IsRightRegular b)
-- Mathlib.Data.List.Infix
List.IsPrefix.drop : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ → ∀ (n : ℕ), List.drop n l₁ <+: List.drop n l₂
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pullbackArrows.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X}
  [inst_1 : R.HasPullbacks f] (Z : C) (h : Z ⟶ X) (hRh : R h),
  CategoryTheory.Presieve.pullbackArrows f R (CategoryTheory.Limits.pullback.snd h f)
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ico_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Ico a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioc (OrderDual.ofDual b) (OrderDual.ofDual a))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.toContinuousAddMonoidHom.eq_1 : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : AddMonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑f = { toAddMonoidHom := ↑f, continuous_toFun := ⋯ }
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The ordinal-indexed supremum of `lfpApprox` equals `nextFixed`: the least fixed point
greater than or equal to `x`.  -/
OrdinalApprox.nextFixed_eq_iSup_lfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x),
  ↑(f.nextFixed x hx) = ⨆ a, OrdinalApprox.lfpApprox f x a
-- Aesop.Util.Basic
Aesop.isDefEqReducibleRigid : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_zero_eq_singleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.closedCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive commutative groups to additive groups preserves all
limits. (That is, the underlying group could have been computed instead as limits in the
category of additive groups.)  -/
AddCommGrpCat.forget₂AddGroup_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ AddCommGrpCat AddGrpCat)
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
IsBoundedBilinearMap.hasFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {b : E × F → G} {u : Set (E × F)}
  (h : IsBoundedBilinearMap 𝕜 b) (p : E × F), HasFDerivWithinAt b (h.deriv p) u p