mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightMopIso_hom_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  (X_1 : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X).hom.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X_1.unmop)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderOutput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.Analysis.Analytic.Constructions
one_le_formalMultilinearSeries_geometric_radius : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A],
  1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius
-- Lean.Parser.Extra
Lean.Parser.ppIndent.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Image
Set.range_eval : ∀ {ι : Sort u_4} {α : ι → Type u_5} [∀ (i : ι), Nonempty (α i)] (i : ι), Set.range (Function.eval i) = Set.univ
-- Aesop.Builder.Apply
Aesop.RuleBuilderOptions.applyIndexTransparency : Aesop.RuleBuilderOptions → Lean.Meta.TransparencyMode
-- Mathlib.Algebra.Lie.Prod
LieHom.fst_comp_inl : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], (LieHom.fst R L₁ L₂).comp (LieHom.inl R L₁ L₂) = LieHom.id
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeCommandParsedSnapshot.go : Lean.Language.Lean.CommandParsedSnapshot → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.associativity_counitIso : ∀ (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],
  (CategoryTheory.prod.associativity C D E).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.prod.inverseAssociator C D E).comp (CategoryTheory.prod.associator C D E))
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `x` is a fixed point of `f` and `g` is a left inverse of `f`, then `x` is a fixed
point of `g`.  -/
Function.IsFixedPt.to_leftInverse : ∀ {α : Type u_1} {f g : α → α} {x : α}, Function.IsFixedPt f x → Function.LeftInverse g f → Function.IsFixedPt g x
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- A strong epimorphism `f` is an epimorphism which has the left lifting property
with respect to monomorphisms.  -/
CategoryTheory.StrongEpi : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {P Q : C} → (P ⟶ Q) → Prop
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_sub_intCast : ∀ {x : ℝ} (m : ℤ), Irrational (x - ↑m) → Irrational x
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapSnd_hom_app : ∀ {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] {B' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B'] {A' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} A']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {R : CategoryTheory.Functor B T}
  {L : CategoryTheory.Functor A T} {R' : CategoryTheory.Functor B' T'} {L' : CategoryTheory.Functor A' T'}
  {F₂ : CategoryTheory.Functor B B'} {F₁ : CategoryTheory.Functor A A'} {F : CategoryTheory.Functor T T'}
  (β : F₁.comp L' ⟶ L.comp F) (α : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.mapSnd β α).hom.app X = CategoryTheory.CategoryStruct.id (F₂.obj X.right)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₀₁_ker_eq_invariants : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  (ModuleCat.Hom.hom (groupCohomology.d₀₁ A)).ker = A.ρ.invariants
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {c : NNReal}
  {μ : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasSubgaussianMGF._auto_1},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ (t : ℝ), MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {k : ℕ}
  [inst_4 : Finite σ],
  (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
    (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
      (MvPowerSeries.truncTotal k)
        (MvPowerSeries.subst (fun i => ↑((MvPowerSeries.truncTotal k) (a i))) ↑((MvPowerSeries.truncTotal k) f))
-- Mathlib.RingTheory.Filtration
/-- Also see `Ideal.isIdempotentElem_iff_eq_bot_or_top` for integral domains.  -/
Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing : ∀ {R : Type u_3} [inst : CommRing R] [IsNoetherianRing R] [IsLocalRing R] (I : Ideal R),
  IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.Birational.refl : ∀ (X : AlgebraicGeometry.Scheme), X.Birational X
-- Mathlib.Order.Filter.Finite
Filter.iInf_principal_finite : ∀ {α : Type u} {ι : Type w} {s : Set ι},
  s.Finite → ∀ (f : ι → Set α), ⨅ i ∈ s, Filter.principal (f i) = Filter.principal (⋂ i ∈ s, f i)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instNonUnitalNonAssocRingQuotient : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (c : RingCon R) → NonUnitalNonAssocRing c.Quotient
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.add : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f g : α → β} [inst_1 : AddZeroClass β] [ContinuousAdd β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    MeasureTheory.AEFinStronglyMeasurable g μ → MeasureTheory.AEFinStronglyMeasurable (f + g) μ
-- Mathlib.Data.Finset.Basic
Finset.subset_insert_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Finset α}, s ⊆ insert a t ↔ s.erase a ⊆ t
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
/-- Let `u : E → F` be a continuous linear map, and `A` a *complemented* finite dimensional
subspace of `F`. Then `u` is strict with closed range if and only if the induced map `E → F ⧸ A`
is strict with closed range.

This is [N. Bourbaki, *Théories Spectrales*, Chapitre III, § 3, n° 1, Cor. 2][bourbaki2023].  -/
ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 F)
  [FiniteDimensional 𝕜 ↥A],
  A.ClosedComplemented →
    (Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔
      Topology.IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed ↑(↑(A.mkQL ∘SL u)).range)
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.DHashMap.Const.get? : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → α → Option β
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, k ∈ m → (f m[k]?).isSome = true → (m.alter k f).size = m.size
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.responseError.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID) (code : Lean.JsonRpc.ErrorCode) (message : String) (data? : Option Lean.Json),
  sizeOf (Lean.JsonRpc.MessageMetaData.responseError id code message data?) =
    1 + sizeOf id + sizeOf code + sizeOf message + sizeOf data?
-- Batteries.Data.BinomialHeap.Basic
/-- The minimum element.  -/
Batteries.BinomialHeap.Imp.FindMin.val : {α : Type u_1} → Batteries.BinomialHeap.Imp.FindMin α → α
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.pow.eq_1 : ∀ (k : ℕ), ArithmeticFunction.pow k = ArithmeticFunction.id.ppow k
-- Mathlib.Data.Nat.Factorial.Basic
Nat.ascFactorialBinary.match_1.congr_eq_3 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ) (n : ℕ),
  k = n.succ.succ →
    (match k with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k@h:n.succ.succ => h_3 k n h) ≍
      h_3 (n + 2) n ⋯
-- Batteries.Data.Array.Match
/-- Prefix table for the pattern  -/
Array.Matcher.table : {α : Type u_1} → Array.Matcher α → Array.PrefixTable α
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraRing.ι_eq_zero : ∀ {R : Type u_1} [inst : CommRing R], CliffordAlgebra.ι 0 = 0
-- Mathlib.Analysis.Complex.Exponential
Real.exp_le_exp : ∀ {x y : ℝ}, Real.exp x ≤ Real.exp y ↔ x ≤ y
-- Mathlib.Computability.RegularExpressions
RegularExpression.char : {α : Type u} → α → RegularExpression α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_compl : ∀ {α : Type u_1} [inst : LE α] (s : UpperSet α), ↑s.compl = (↑s)ᶜ
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_strict_mono : ∀ {n : ℕ} (c : Composition n) {i : ℕ}, i < c.length → c.sizeUpTo i < c.sizeUpTo (i + 1)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_map_left : ∀ {α : Type u} {β : Type v} {α' : Type u'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : α → α'),
  (Stream'.Seq.map f s₁).zip s₂ = Stream'.Seq.map (Prod.map f id) (s₁.zip s₂)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_indep_iff : ∀ {α : Type u_1} {E I : Set α}, (Matroid.freeOn E).Indep I ↔ I ⊆ E
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mdifferentiablefWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → (MDiffAt[s] f₁ x ↔ MDiffAt[s] f x)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.minpoly_mk : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : L),
  (ConjRootClass.mk K x).minpoly = minpoly K x
-- Aesop.Rule
Aesop.instLTNormRuleInfo : LT Aesop.NormRuleInfo
-- Init.Data.UInt.Basic
/-- The power operation, raising a 32-bit unsigned integer to a natural number power,
wrapping around on overflow. Usually accessed via the `^` operator.

This function is currently *not* overridden at runtime with an efficient implementation,
and should be used with caution. See https://github.com/leanprover/lean4/issues/7887.
 -/
UInt32.pow : UInt32 → ℕ → UInt32
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousOn.fun_neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn (fun i => -f i) s
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.comp.eq_1 : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Monoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (g : B →ₜ* C) (f : A →ₜ* B),
  g.comp f = { toMonoidHom := g.comp f.toMonoidHom, continuous_toFun := ⋯ }
-- Mathlib.Topology.NhdsKer
nhdsKer_univ : ∀ {X : Type u_2} [inst : TopologicalSpace X], nhdsKer Set.univ = Set.univ
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- A subquiver which by construction is an arborescence.  -/
Quiver.geodesicSubtree : {V : Type u} → [inst : Quiver V] → (r : V) → [Quiver.RootedConnected r] → WideSubquiver V
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {m : α → β} {f : Filter α},
  Filter.Tendsto m f Filter.atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
-- Mathlib.Order.Filter.Lift
Filter.map_lift'_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : β → γ},
  Monotone h → Filter.map m (f.lift' h) = f.lift' (Set.image m ∘ h)
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_withReader_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [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] {ρ α : Type u}
  {post : α → ρ → Pred} {epost : EPred} (f : ρ → ρ) (x : ReaderT ρ m α),
  Std.Internal.Do.wp (MonadWithReaderOf.withReader f x) post epost = fun r =>
    Std.Internal.Do.wp x (fun a x => post a r) epost (f r)
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_not : ∀ (a : UInt8), (~~~a).toUInt32 = ~~~a.toUInt32 % 256
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
OnePoint.equivProjectivization.eq_1 : ∀ (K : Type u_1) [inst : DivisionRing K] [inst_1 : DecidableEq K],
  OnePoint.equivProjectivization K =
    { toFun := fun p => p.elim (Projectivization.mk K ![1, 0] ⋯) fun t => Projectivization.mk K ![t, 1] ⋯,
      invFun := fun p => Projectivization.lift (fun u => if ↑u 1 = 0 then OnePoint.infty else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p,
      left_inv := ⋯, right_inv := ⋯ }
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.wordDiff : String → String → Array (Lean.Diff.Action × String)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_hom_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
            (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom.app
      X =
    X.iso.hom
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqCtorInfo.beq : Lean.Compiler.LCNF.CtorInfo → Lean.Compiler.LCNF.CtorInfo → Bool
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray.congr_simp : ∀ {α : Type u} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] (r r_1 : Std.Ric α), r = r_1 → r.toArray = r_1.toArray
-- Mathlib.NumberTheory.Bernoulli
bernoulli'PowerSeries.eq_1 : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Algebra ℚ A],
  bernoulli'PowerSeries A = PowerSeries.mk fun n => (algebraMap ℚ A) (bernoulli' n / ↑n.factorial)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.mapNatIso_hom : ∀ {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.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  (τ : F ≅ G), (S.mapNatIso τ).hom = S.mapNatTrans τ.hom
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homAddEquiv_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.AddMonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful) (a : X ⟶ M),
  (CategoryTheory.Functor.FullyFaithful.homAddEquiv F hF) a = F.map a
-- Std.Data.TreeMap.Raw.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.TreeMap.Raw.erase : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Std.TreeMap.Raw α β cmp
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_isNonloop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {C : Set α}, (M.contract C).IsNonloop e ↔ e ∈ M.E \ M.closure C
-- Mathlib.Data.Nat.Cast.Defs
/-- `AddMonoidWithOne` implementation using unary recursion.  -/
AddMonoidWithOne.unary : {R : Type u_1} → [AddMonoid R] → [One R] → AddMonoidWithOne R
-- Mathlib.RingTheory.Ideal.IsPrimary
Ideal.IsPrimary.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R), I.IsPrimary = Submodule.IsPrimary I
-- Mathlib.CategoryTheory.Elements
/-- If `F` is represented by `X`, `X` with its universal element is the initial object of
`F.Elements.`  -/
CategoryTheory.Functor.Elements.isInitialOfRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} →
      {X : C} →
        (h : F.RepresentableBy X) →
          CategoryTheory.Limits.IsInitial (CategoryTheory.Functor.Elements.initialOfRepresentableBy h)
-- Mathlib.Data.List.TFAE
List.tfae_of_forall : ∀ (b : Prop) (l : List Prop), (∀ a ∈ l, a ↔ b) → l.TFAE
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE.eq_1 : ∀ (n : ℕ), n.primesLE = (n + 1).primesBelow
-- Std.Http.Data.Method
Std.Http.Method.orderpatch.sizeOf_spec : sizeOf Std.Http.Method.orderpatch = 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α), Std.DTreeMap.Internal.Impl.leaf.getKey? k = none
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_sub_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R (n - 1) = Polynomial.X * Polynomial.Chebyshev.S R n - Polynomial.Chebyshev.S R (n + 1)
-- Mathlib.CategoryTheory.EffectiveEpi.Coproduct
/-- If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of
the coproduct is effective epimorphic whenever `Sigma.desc` induces an effective epimorphism from
the coproduct itself.
 -/
CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        (X : α → C) →
          (π : (a : α) → X a ⟶ B) →
            [inst_1 : CategoryTheory.Limits.HasCoproduct X] →
              [CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)] →
                [inst_3 :
                    ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α),
                      CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] →
                  [inst_4 :
                      ∀ {Z : C} (g : Z ⟶ ∐ X),
                        CategoryTheory.Limits.HasCoproduct fun a =>
                          CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] →
                    [∀ {Z : C} (g : Z ⟶ ∐ X),
                          CategoryTheory.Epi
                            (CategoryTheory.Limits.Sigma.desc fun a =>
                              CategoryTheory.Limits.pullback.fst g (CategoryTheory.Limits.Sigma.ι X a))] →
                      CategoryTheory.EffectiveEpiFamilyStruct X π
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.toList_iter_eq_toList : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α}, r.iter.toList = r.toList
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, (t.insertMany l).contains k = (t.contains k || l.contains k)
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Given functions `f`, `g` and a real number `R`, the following convenience structure packs the
information relevant in the extended canonical decomposition.
 -/
Complex.ECanonicalDecomp : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → (ℂ → E) → ℝ → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_modify_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Mathlib.CategoryTheory.EpiMono
/-- Every split epi is an epi.  -/
CategoryTheory.IsSplitEpi.epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f],
  CategoryTheory.Epi f
-- Mathlib.Algebra.Order.Module.Defs
le_of_smul_le_smul_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosReflectLE α β], a₁ • b ≤ a₂ • b → 0 < b → a₁ ≤ a₂
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Composition on the left by a (lipschitz-continuous) homomorphism of topological `AddMonoid`s,
as a `AddMonoidHom`. Similar to `AddMonoidHom.compLeftContinuous`.  -/
AddMonoidHom.compLeftContinuousBounded : {β : Type v} →
  {γ : Type w} →
    (α : Type u_3) →
      [inst : TopologicalSpace α] →
        [inst_1 : PseudoMetricSpace β] →
          [inst_2 : AddMonoid β] →
            [inst_3 : BoundedAdd β] →
              [inst_4 : ContinuousAdd β] →
                [inst_5 : PseudoMetricSpace γ] →
                  [inst_6 : AddMonoid γ] →
                    [inst_7 : BoundedAdd γ] →
                      [inst_8 : ContinuousAdd γ] →
                        (g : β →+ γ) →
                          {C : NNReal} →
                            LipschitzWith C ⇑g → BoundedContinuousFunction α β →+ BoundedContinuousFunction α γ
-- Mathlib.Order.Bounds.Basic
bddAbove_iff_subset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s ↔ ∃ a, s ⊆ Set.Iic a
-- Mathlib.Order.UpperLower.Closure
UpperSet.le_sdiff_left : ∀ {α : Type u_1} [inst : Preorder α] {s : UpperSet α} {t : Set α}, s ≤ s.sdiff t
-- Mathlib.Algebra.Lie.Weights.IsSimple
/-- The intersection of a Lie ideal and a Cartan subalgebra is the span of the coroots whose roots
have root spaces in the ideal.  -/
LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [CharZero K]
  [LieAlgebra.IsKilling K L] [LieModule.IsTriangularizable K (↥H) L] (I : LieIdeal K L),
  LieSubmodule.restr I H ⊓ H.toLieSubmodule = ⨆ α ∈ I.rootSet, LieAlgebra.IsKilling.corootSubmodule ↑α
-- Init.System.IO
/-- Marks given value and its object graph closure as multi-threaded if currently
marked single-threaded. This will make reference counter updates atomic and
thus more costly. It can still be useful to do eagerly when the value will be
shared between threads later anyway and there is available time budget to mark
it now.  -/
Runtime.markMultiThreaded : {α : Type} → α → BaseIO α
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_fst : ∀ {ι : Type u_3} (V : ι → Type u_4) (f : (i : ι) → V i) (i : ι),
  ((SimpleGraph.completeMultipartiteGraph.topEmbedding V f) i).fst = i