mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.map_hasCompactSupport : ∀ {B : Type u_6} {E : outParam (Type u_7)} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E}
  {Ω : outParam (TopologicalSpace.Opens E)} {F : outParam (Type u_8)} {inst_2 : NormedAddCommGroup F}
  {inst_3 : NormedSpace ℝ F} {n : outParam ℕ∞} [self : TestFunctionClass B Ω F n] (f : B), HasCompactSupport ⇑f
-- Init.Control.Lawful.MonadAttach.Lemmas
LawfulMonadAttach.canReturn_map_imp' : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} {b : β} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m] {x : m α} {f : α → β},
  MonadAttach.CanReturn (f <$> x) b → ∃ a, MonadAttach.CanReturn x a ∧ f a = b
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_one : ∀ {α : Type u_2} [inst : One α] [inst_1 : DecidableEq α], Finset.image MulOpposite.op 1 = 1
-- Lean.Meta.DecLevel
Lean.Meta.getDecLevel? : Lean.Expr → Lean.MetaM (Option Lean.Level)
-- Mathlib.Algebra.Ring.Defs
boole_mul : ∀ {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst_1 : Decidable P] (a : α),
  (if P then 1 else 0) * a = if P then a else 0
-- Init.Data.Nat.Control
/-- Iterates the application of a monadic function `f` to a starting value `init`, `n` times. At each
step, `f` is applied to the current value and to the next natural number less than `n`, in
decreasing order.
 -/
Nat.foldRevM : {α : Type u} → {m : Type u → Type v} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → α → m α) → α → m α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?ₘ'_eq_minEntry?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : Std.DTreeMap.Internal.Impl α β}, l.minEntry?ₘ' = l.minEntry?ₘ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instFunLike : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → FunLike (MeasureTheory.FiniteMeasure Ω) (Set Ω) NNReal
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xNextIsoSelf.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι}
  (h : ¬c.Rel i (c.next i)), C.xNextIsoSelf h = C.xNextIsoSelf h
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Minute.Offset
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (r : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) →
          (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)) →
        ((a : RBTree.RBNode α) →
            (y : α) →
              (b : RBTree.RBNode α) →
                (z : α) →
                  (c : RBTree.RBNode α) →
                    motive
                      (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c)) →
          ((r : RBTree.RBNode α) →
              (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α),
                  r = RBTree.RBNode.node RBTree.RBColor.black a y b → False) →
                (∀ (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α) (c : RBTree.RBNode α),
                    r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c →
                      False) →
                  motive r) →
            motive r
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOp_right_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategory), X.rightOp.right.obj X_1 = Opposite.op (X.left.obj (Opposite.op X_1))
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.add : ∀ {M : Type u_1} [inst : AddMonoid M] {a b : M}, IsAddUnit a → IsAddUnit b → IsAddUnit (a + b)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_primeIdealOf : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  hU.fromSpec (hU.primeIdealOf x) = ↑x
-- Mathlib.LinearAlgebra.Goursat
Submodule.goursatSnd_toAddSubgroup : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Submodule R (M × N)},
  L.goursatSnd.toAddSubgroup = L.toAddSubgroup.goursatSnd
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insert k v).isEmpty = false
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- The proposition that two elements of a sesquilinear map space are orthogonal  -/
LinearMap.IsOrtho : {R : Type u_1} →
  {R₁ : Type u_2} →
    {R₂ : Type u_3} →
      {M : Type u_5} →
        {M₁ : Type u_6} →
          {M₂ : Type u_7} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring R₁] →
                [inst_2 : AddCommMonoid M₁] →
                  [inst_3 : Module R₁ M₁] →
                    [inst_4 : CommSemiring R₂] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R₂ M₂] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : Module R M] →
                              {I₁ : R₁ →+* R} → {I₂ : R₂ →+* R} → (M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) → M₁ → M₂ → Prop
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_pow : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (n : ℕ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom : {a a_1 : CategoryTheory.Limits.WalkingParallelPair} → DecidableEq (CategoryTheory.Limits.WalkingParallelPairHom a a_1)
-- Mathlib.NumberTheory.Dioph
Poly.mul_apply : ∀ {α : Type u_1} (f g : Poly α) (x : α → ℕ), (f * g) x = f x * g x
-- Mathlib.Algebra.Lie.TransferInstance
Equiv.lieEquiv_symm_apply : ∀ {R : Type u_1} {L' : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (e : L' ≃ L) (b : L), (Equiv.lieEquiv R e).symm b = e.symm b
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeTR.go.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys acc : List α)
  (h_1 : (l₂ acc : List α) → motive [] l₂ acc) (h_2 : (l₁ acc : List α) → motive l₁ [] acc)
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys acc : List α) → motive (x :: xs) (y :: ys) acc),
  (match x :: xs, y :: ys, acc with
    | [], l₂, acc => h_1 l₂ acc
    | l₁, [], acc => h_2 l₁ acc
    | x :: xs, y :: ys, acc => h_3 x xs y ys acc) =
    h_3 x xs y ys acc
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.flipLinear_apply_apply : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) (x : G)
  (m : (i : ι) → E i), (f.flipLinear x) m = (f m) x
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.projectionOntoL.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (p q : Submodule R M) (h : Submodule.IsTopCompl p q),
  p.projectionOntoL q h = { toLinearMap := p.projectionOnto q ⋯, cont := ⋯ }
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getElem_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getElem_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {h : k ∈ Std.TreeMap.filterMap f t},
  (Std.TreeMap.filterMap f t)[k] = (f k t[k]).get ⋯
-- Init.Ext
Unit.ext : ∀ (x y : Unit), x = y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_toList_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
IsAbsoluteValue.abv_sum : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  [IsOrderedRing S] (abv : R → S) [IsAbsoluteValue abv] (f : ι → R) (s : Finset ι),
  abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionCommMonoid α],
  OrderDual.instDivisionCommMonoid = { toDivisionMonoid := OrderDual.instDivisionMonoid, mul_comm := ⋯ }
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.instGroup : {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst_1 : Group H] → Group (Monoid.Coprod G H)
-- Init.Data.SInt.Lemmas
Int16.ofBitVec_inj : ∀ {a b : BitVec 16}, Int16.ofBitVec a = Int16.ofBitVec b ↔ a = b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Right map, from `J.R` to `C`  -/
CategoryTheory.Limits.MulticospanIndex.right : {J : CategoryTheory.Limits.MulticospanShape} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.MulticospanIndex J C → J.R → C
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_submonoid_closure : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R),
  Subsemiring.closure ↑(Submonoid.closure s) = Subsemiring.closure s
-- Lean.Meta.Basic
Lean.Meta.withTransparency : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Meta.TransparencyMode → n α → n α
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Stream.foldl.match_1.splitter : {σ : Sort u_3} →
  {α : Type u_1} →
    (motive : σ → RBTree.RBNode.Stream α → Sort u_2) →
      (x : σ) →
        (x_1 : RBTree.RBNode.Stream α) →
          ((b : σ) → motive b RBTree.RBNode.Stream.nil) →
            ((b : σ) →
                (v : α) →
                  (r : RBTree.RBNode α) →
                    (tail : RBTree.RBNode.Stream α) → motive b (RBTree.RBNode.Stream.cons v r tail)) →
              motive x x_1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p' p q : ℤ) (hpq : p + 0 = q),
  CategoryTheory.CategoryStruct.comp (F.d p' p) ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) =
    CategoryTheory.CategoryStruct.comp (F.d p' q) (ψ q)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  Std.DTreeMap.Raw.Const.insertMany t [] = t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, t[a]! = t[a]?.get!
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.id_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x x_1 : C),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Functor.id C) x x_1 =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj x x_1))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The cocone `Sigma.cocone X` is a colimit cocone.  -/
CategoryTheory.Limits.coproductIsCoproduct' : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Sigma.cocone X)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.eq_4 : ∀ (fuel_2 : ℕ) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁_2 : Lean.Grind.CommRing.Poly) (k₂ : ℤ),
  Lean.Grind.CommRing.Poly.combine.go fuel_2.succ (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2)
      (Lean.Grind.CommRing.Poly.num k₂) =
    (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_2).addConst k₂
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'_char : ∀ {α : Type u_1} (a : α), (RegularExpression.char a).matches' = {[a]}
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instForMSigmaOfTransCmpOfLawfulMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} →
        [Std.TransCmp cmp] → [inst : Monad m] → [LawfulMonad m] → ForM m (Std.ExtDTreeMap α β cmp) ((a : α) × β a)
-- Mathlib.Order.Lattice
/-- A subtype forms a `⊓`-semilattice if `⊓` preserves the property.
See note [reducible non-instances].  -/
Subtype.semilatticeInf : {α : Type u} →
  [inst : SemilatticeInf α] → {P : α → Prop} → (∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) → SemilatticeInf { x // P x }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.appTop.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.appTop f = AlgebraicGeometry.Scheme.Hom.app f ⊤
-- Std.Async.Process
/-- Number of IPC messages received
 -/
Std.IO.Process.ResourceUsageStats.messagesReceived : Std.IO.Process.ResourceUsageStats → UInt64
-- Init.Data.Float.Model.Unpacked.Sign
Float.Model.UnpackedFloat.instReprSign.repr : Float.Model.UnpackedFloat.Sign → ℕ → Std.Format
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.range_extendLeft_zero : ∀ {n : ℕ} (c : OrderedFinpartition n), Set.range (c.extendLeft.emb 0) = {0}
-- Mathlib.Data.PFun
PFun.inhabited : {α : Type u_1} → {β : Type u_2} → Inhabited (α →. β)
-- Std.Internal.Do.Order.Basic
/-- Indexed infimum  -/
Lean.Order.iInf : {α : Type u} → [Lean.Order.CompleteLattice α] → {ι : Type v} → (ι → α) → α
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.instAddGroupSubtypeMemAddSubmonoid : {M : Type u_1} → [inst : AddMonoid M] → AddGroup ↥(IsAddUnit.addSubmonoid M)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratHintsExhaustive.eq_1 : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)),
  f.ratHintsExhaustive pivot ratHints =
    decide
      (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.getRatClauseIndices f.clauses pivot =
        Array.map (fun x => x.1) ratHints)
-- Batteries.Data.List.Lemmas
List.disjoint_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₁ → a ∉ l₂
-- Mathlib.RingTheory.WittVector.InitTail
/-- `WittVector.tail n x` is the Witt vector of which the first `n` coefficients are `0`
and all other coefficients are those from `x`.
See `WittVector.init` for the complementary part.  -/
WittVector.tail : {p : ℕ} → {R : Type u_1} → [CommRing R] → ℕ → WittVector p R → WittVector p R
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.instToMessageDataRecursionContext : Lean.ToMessageData Lean.Meta.IndPredBelow.RecursionContext
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (F : CategoryTheory.Functor C₂ H) [Φ.IsRightDerivabilityStructure]
  (X : C₁),
  (Φ.functor.comp F).HasPointwiseRightDerivedFunctorAt W₁ X ↔ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X)
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.tendsto_mul_zero_of_left : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [IsLinearTopology Rᵐᵒᵖ R] {ι : Type u_2} {f : Filter ι}
  (a b : ι → R), Filter.Tendsto a f (nhds 0) → Filter.Tendsto (a * b) f (nhds 0)
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.ideal_comp : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} (self : hI.DPMorphism hJ), Ideal.map self.toRingHom I ≤ J
-- Mathlib.Analysis.Analytic.Binomial
binomialSeries_radius_ge_one : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {𝔸 : Type u_2} [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] {a : 𝕂},
  1 ≤ (binomialSeries 𝔸 a).radius
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.mul_comm'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj M] {Z : C}
  (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ M M).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- There is always a satellite configuration with a single point.  -/
Besicovitch.SatelliteConfig.instInhabited : {α : Type u_1} → {τ : ℝ} → [Inhabited α] → [inst : MetricSpace α] → Inhabited (Besicovitch.SatelliteConfig α 0 τ)
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is cofiltered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be final. The converse is also true, see `initial_iff_of_isCofiltered`.  -/
CategoryTheory.Functor.initial_of_exists_of_isCofiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C],
  (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) →
    (∀ {d : D} {c : C} (s s' : F.obj c ⟶ d),
        ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') →
      F.Initial
-- Mathlib.RingTheory.FinitePresentation
/-- If `f : A →ₐ[R] B` is a surjection between finitely-presented `R`-algebras, then the kernel of
`f` is finitely generated.  -/
Algebra.FinitePresentation.ker_fG_of_surjective : ∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Surjective ⇑f →
    ∀ [Algebra.FinitePresentation R A] [Algebra.FinitePresentation R B], (RingHom.ker f.toRingHom).FG
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.mul_inverse_cancel_left : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] (x y : M₀), IsUnit x → x * (Ring.inverse x * y) = y
-- Mathlib.Algebra.GroupWithZero.Associated
Prime.dvd_prime_iff_associated : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q : M},
  Prime p → Prime q → (p ∣ q ↔ Associated p q)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β k}, k ∉ t₁ → (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentCoordChange_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {x y z : M},
  tangentCoordChange I x y z =
    fderivWithin 𝕜 (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preRight_obj_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (F : CategoryTheory.Functor C B)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L (F.comp R)),
  ((CategoryTheory.Comma.preRight L F R).obj X).left = X.left
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sumSet_range : ∀ {α : Type u_1} {s t : Set α} (h : Disjoint s t), Set.range ⇑(Function.Embedding.sumSet h) = s ∪ t
-- Mathlib.Order.Filter.Cofinite
Nat.frequently_atTop_iff_infinite : ∀ {p : ℕ → Prop}, (∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ {n | p n}.Infinite
-- Mathlib.Order.Hom.Bounded
BotHom.coe_id : ∀ (α : Type u_2) [inst : Bot α], ⇑(BotHom.id α) = id
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
_private.Mathlib.Order.CompleteLattice.MulticoequalizerDiagram.0.CompleteLattice.MulticoequalizerDiagram.multispanIndex.match_1.splitter : {ι : Type u_1} →
  (motive : (CategoryTheory.Limits.MultispanShape.prod ι).L → Sort u_2) →
    (x : (CategoryTheory.Limits.MultispanShape.prod ι).L) → ((i j : ι) → motive (i, j)) → motive x
-- Lean.Elab.InfoTree.Main
/-- Embeds a `CoreM` action in `IO` by supplying the information stored in `info`.  -/
Lean.Elab.ContextInfo.runCoreM : {α : Type} → Lean.Elab.ContextInfo → Lean.CoreM α → IO α
-- Mathlib.CategoryTheory.Category.PartialFun
/-- The functor which maps undefined values to a new point. This makes the maps total and creates
pointed types. This is the noncomputable part of the equivalence `PartialFunEquivPointed`. It can't
be computable because `= Option.none` is decidable while the domain of a general `Part` isn't.  -/
partialFunToPointed : CategoryTheory.Functor PartialFun Pointed
-- Mathlib.Data.Erased
Erased.mk_out : ∀ {α : Sort u_1} (a : Erased α), Erased.mk a.out = a
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The left unitor as a bimodule isomorphism.  -/
Bimod.leftUnitorBimod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {X Y : CategoryTheory.Mon C} → (M : Bimod X Y) → (Bimod.regular X).tensorBimod M ≅ M
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_erase_self : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.erase k).get? k = none
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
/-- A one-element family `x` is algebraically independent if and only if
its element is transcendental.  -/
algebraicIndependent_unique_type_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] [inst_3 : Unique ι], AlgebraicIndependent R x ↔ Transcendental R (x default)