mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.multifork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (a : J.L),
  (CategoryTheory.Limits.Multiequalizer.multifork I).ι a = CategoryTheory.Limits.Multiequalizer.ι I a
-- Lean.DocString.Syntax
/-- Display-mode mathematical notation  -/
Lean.Doc.Syntax.display_math : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.epi_homMk : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X}
  {f : U.right ⟶ V.right} [CategoryTheory.Epi f] (w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom),
  CategoryTheory.Epi (CategoryTheory.Under.homMk f w)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.isPlausibleIndirectOutput_of_mem_toListRev : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {it : Std.Iter β} {b : β},
  b ∈ it.toListRev → it.IsPlausibleIndirectOutput b
-- Mathlib.Order.Filter.IsBounded
Antitone.isBoundedUnder_ge_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {u : γ → α}
  {v : α → β},
  Antitone v → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l (v ∘ u)
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprCertificateOracle.unsafe_impl_2 : Lean.Expr → Lean.MetaM Mathlib.Tactic.Linarith.CertificateOracle
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_union_left : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α]
  [inst_3 : DecidableEq α], a ∈ lowerClosure ↑s → a ∉ lowerClosure ↑t → (s ∪ t).truncatedSup a = s.truncatedSup a
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Sequential characterization of upper hemicontinuity**:
If `β` is a regular space and `f : α → Set β` is upper hemicontinuous at `x₀` and `f x₀` is
closed, then for any sequences `x` and `y` (in `α` and `β`, respectively) tending to `x₀` and `y₀`,
respectively, if `y n ∈ f (x n)` frequently, then `y₀ ∈ f x₀`.

This is a partial converse of `UpperHemicontinuousAt.of_sequences`.  -/
UpperHemicontinuousAt.mem_of_tendsto : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {ι : Type u_5}
  [RegularSpace β] {x₀ : α} {l : Filter ι},
  UpperHemicontinuousAt f x₀ →
    IsClosed (f x₀) →
      ∀ {x : ι → α},
        Filter.Tendsto x l (nhds x₀) →
          ∀ {y : ι → β}, (∃ᶠ (n : ι) in l, y n ∈ f (x n)) → ∀ {y₀ : β}, Filter.Tendsto y l (nhds y₀) → y₀ ∈ f x₀
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.alter.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (f : Option β → Option β)
  (hl_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.Const.alter k f Std.DTreeMap.Internal.Impl.leaf hl_2 =
    match f none with
    | none =>
      { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
    | some v =>
      { impl := Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf,
        balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative semiring.  -/
SemimoduleCat.instCommSemiringCarrierTensorUnit : {R : Type u} →
  [inst : CommSemiring R] → CommSemiring ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (SemimoduleCat R))
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiCompact_of_compactSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CompactSpace ↥X] [QuasiSeparatedSpace ↥Y],
  AlgebraicGeometry.QuasiCompact f
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- A partition of `Fin n` into finitely many nonempty subsets, given by the increasing
parameterization of these subsets. We order the subsets by increasing greatest element.
This definition is tailored-made for the Faa di Bruno formula, and probably not useful elsewhere,
because of the specific parameterization by `Fin n` and the peculiar ordering.  -/
OrderedFinpartition : ℕ → Type
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.End_equiv_aux : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2),
  (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f =
      IsScalarTower.toAlgHom R S
        ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal) ↔
    (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The expression for the structural 2-morphism `α`.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalExpr.nilM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
    Mathlib.Tactic.BicategoryLike.Structural → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Order.Filter.Prod
Filter.prod_top : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α}, f ×ˢ ⊤ = Filter.comap Prod.fst f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.deriv_sinh : deriv Real.sinh = Real.cosh
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → LowerSet α), ↑(⨅ i, f i) = ⋂ i, ↑(f i)
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- The essential image of `R`-algebras under `Spec` is precisely affine schemes over `Spec R`.  -/
AlgebraicGeometry.essImage_algSpec : ∀ {R : CommRingCat} {G : CategoryTheory.Over (AlgebraicGeometry.Spec R)},
  (AlgebraicGeometry.algSpec R).essImage G ↔ AlgebraicGeometry.IsAffine G.left
-- Mathlib.Tactic.Widget.Conv
Mathlib.Tactic.Conv.Path.arg.inj : ∀ {arg : ℕ} {all : Bool} {next : Mathlib.Tactic.Conv.Path} {arg_1 : ℕ} {all_1 : Bool}
  {next_1 : Mathlib.Tactic.Conv.Path},
  Mathlib.Tactic.Conv.Path.arg arg all next = Mathlib.Tactic.Conv.Path.arg arg_1 all_1 next_1 →
    arg = arg_1 ∧ all = all_1 ∧ next = next_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.zero_rpow_le_one : ∀ (x : ℝ), 0 ^ x ≤ 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.inv_base_hom_base_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) {Z : TopCat} (h : ↑Y.toPresheafedSpace ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.base (CategoryTheory.CategoryStruct.comp e.hom.base h) = h
-- Mathlib.Algebra.BigOperators.Finprod
finprod_of_isEmpty : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] [IsEmpty α] (f : α → M), ∏ᶠ (i : α), f i = 1
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
CompactlyGeneratedSpace.isClosed_iff_of_t2 : ∀ {X : Type u} [inst : TopologicalSpace X] [T2Space X] [CompactlyGeneratedSpace X] (s : Set X),
  IsClosed s ↔ ∀ ⦃K : Set X⦄, IsCompact K → IsClosed (s ∩ K)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.copy_eq : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S), S.copy s hs = S
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.instLEValueGroupWithZero : {R : Type u_1} → [inst : Semiring R] → [inst_1 : ValuativeRel R] → LE (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackComp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.ChosenPullbacksAlong.pullbackComp f g =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).rightAdjointUniq
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- **Alias** of `SemiconjBy.isTrans`.

---

The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup
is transitive.  -/
SemiconjBy.transitive : ∀ {S : Type u_1} [inst : Semigroup S], IsTrans S fun a b => ∃ c, SemiconjBy c a b
-- Mathlib.Order.Bounds.Image
mem_upperBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → a ∈ upperBounds s → b ∈ upperBounds t → f a b ∈ upperBounds (Set.image2 f s t)
-- Lean.Elab.ConfigEval.Commands
/-- `omit f1, f2, f3` disables generating setters for fields `f1`, `f2`, and `f3`
of the structure.  -/
Lean.Elab.ConfigEval.configEntryOmit : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
/-- Negating a bitvector created from a natural number equals
creating a bitvector from the negative of that number.
 -/
BitVec.neg_ofNat_eq_ofInt_neg : ∀ {w x : ℕ}, -BitVec.ofNat w x = BitVec.ofInt w (-↑x)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true` if pattern `p` contains a child `c` such that
1- `p` and `c` have the same new pattern variables. We say a pattern variable is new if it is not in `alreadyFound`.
2- `c` is not a support argument. See `NormalizePattern.getPatternSupportMask` for definition.
3- `c` is not an offset pattern.
4- `c` is not a bound variable.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.OldCollector.hasChildWithSameNewBVars : Lean.Expr → Array Lean.Meta.Grind.NormalizePattern.PatternArgKind → Std.HashSet ℕ → Lean.CoreM Bool
-- Init.Data.Option.Monadic
Option.forIn_join : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  (o : Option (Option α)) (f : α → β → m (ForInStep β)),
  forIn o.join init f = forIn o init fun o' b => ForInStep.yield <$> forIn o' b f
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.i_w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.i) (CategoryTheory.CategoryStruct.comp g h_1) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right h.i) h_1)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Iio : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] {l : ℝ},
  Filter.Tendsto (↑f) Filter.atBot (nhds l) →
    ∀ (x : R), f.measure (Set.Iio x) = ENNReal.ofReal (Function.leftLim (↑f) x - l)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `f.val x` has a non-zero coefficient at the position of the Archimedean class of `x`.  -/
HahnEmbedding.Partial.coeff_ne_zero : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [IsOrderedAddMonoid R] [Archimedean R] {x : ↥(↑f).domain} (hx0 : ↑x ≠ 0),
  (ofLex (↑↑f x)).coeff (FiniteArchimedeanClass.mk (↑x) hx0) ≠ 0
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.takeWhile.go.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α) (i : ℕ) (acc : Array α),
  Array.takeWhile.go✝ p as i acc =
    if h : i < as.size then
      have a := as[i];
      if p a = true then Array.takeWhile.go✝ p as (i + 1) (acc.push a) else acc
    else acc
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_top : ∀ {V : Type u} {G : SimpleGraph V} (v : V), ⊤.neighborSet v = G.neighborSet v
-- Mathlib.Algebra.Ring.Equiv
RingHomClass.toRingHom.congr_simp : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] {x : NonAssocSemiring α}
  {x_1 : NonAssocSemiring β} [inst_1 : RingHomClass F α β] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.mono : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f g : ι → α},
  s.PairwiseDisjoint f → g ≤ f → s.PairwiseDisjoint g
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.leadingCoeff_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] {x : HahnSeries Γ R},
  (-x).leadingCoeff = -x.leadingCoeff
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_limZero_left : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f : CauSeq β abv} (g : CauSeq β abv),
  f.LimZero → (f * g).LimZero
-- Lean.Meta.Match.MatcherInfo
/-- `some h` if the discriminant is annotated with `h:`  -/
Lean.Meta.Match.DiscrInfo.hName? : Lean.Meta.Match.DiscrInfo → Option Lean.Name
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.ne'`. -/
HasSSubset.SSubset.ne' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → a ≠ b
-- Mathlib.Computability.TuringMachine.Tape
Turing.instInhabitedDir.default : Turing.Dir
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformly.multipliableUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], MultipliableUniformly f → MultipliableUniformlyOn f s
-- Mathlib.Topology.Semicontinuity.Basic
continuous_iff_lower_upperSemicontinuous : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [OrderTopology γ] {f : α → γ}, Continuous f ↔ LowerSemicontinuous f ∧ UpperSemicontinuous f
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ D` preserves limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.rightOp : C ⥤ Dᵒᵖ` preserves
colimits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesColimit_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.PreservesLimit K.op F],
  CategoryTheory.Limits.PreservesColimit K F.rightOp
-- Mathlib.Analysis.Meromorphic.Order
/-- If two meromorphic functions have unequal orders, then the order of their sum is
exactly the minimum of the orders of the summands.
 -/
meromorphicOrderAt_add_of_ne : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x →
        meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.write.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : List Bool) (x_1 : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ),
  Turing.TM1to1.write x x_1 =
    match x, x_1 with
    | [], q => q
    | a :: l, q =>
      Turing.TM1.Stmt.write (fun x x_2 => a) (Turing.TM1.Stmt.move Turing.Dir.right (Turing.TM1to1.write l q))
-- Mathlib.Algebra.Homology.Single
ChainComplex.toSingle₀Equiv_apply_coe : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] (C : ChainComplex V ℕ) (X : V)
  (φ : C ⟶ (ChainComplex.single₀ V).obj X), ↑((C.toSingle₀Equiv X) φ) = φ.f 0
-- Mathlib.Order.Monotone.Monovary
Antitone.antivary : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  [inst_2 : LinearOrder ι], Antitone f → Monotone g → Antivary f g
-- Lean.DocString.Syntax
/-- Items from both ordered and unordered lists  -/
Lean.Parser.Category.list_item : Lean.Parser.Category
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppScalarLeft_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_4} [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {ι : Type u_5}
  [inst_3 : DecidableEq ι] (pn : TensorProduct R (ι →₀ R) N) (i : ι),
  ((TensorProduct.finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (Finsupp.lapply i)) pn)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpiCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.IsRegularEpi f) →
    CategoryTheory.IsRegularEpiCategory C
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul_monic : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).leadingCoeff = p.leadingCoeff
-- Mathlib.RingTheory.Polynomial.Vieta
/-- Vieta's formula for the coefficients and the roots of a polynomial over an integral domain
with as many roots as its degree.  -/
Polynomial.coeff_eq_esymm_roots_of_card : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R},
  p.roots.card = p.natDegree →
    ∀ {k : ℕ}, k ≤ p.natDegree → p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_concat : ∀ {w : ℕ} (x : BitVec w) (b : Bool), (x.concat b).toFin = ⟨x.toNat * 2 + b.toNat, ⋯⟩
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_neg : ∀ {R : Type u_1} [inst : Ring R] {S : Type u_2} [inst_1 : Ring S] (p : SkewPolynomial R) (f : ℕ → R → S),
  (p.sum fun n x => -f n x) = -p.sum f
-- Lean.DocString.Markdown
/-- The internal rendering state for `MarkdownM`.
 -/
Lean.Doc.MarkdownM.State : Type
-- Init.Control.Basic
/-- Runs the monadic action `f` on each element of the collection `coll`.
 -/
ForM.forM : {m : Type u → Type v} →
  {γ : Type w₁} → {α : outParam (Type w₂)} → [self : ForM m γ α] → γ → (α → m PUnit.{u + 1}) → m PUnit.{u + 1}
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
      (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.imp : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ₁ φ₂ : L.BoundedFormula α n}, φ₁.IsQF → φ₂.IsQF → (φ₁.imp φ₂).IsQF
-- Mathlib.Data.Matrix.Basic
Subsemiring.coe_matrix : ∀ {n : Type u_3} {R : Type u_14} [inst : NonAssocSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (S : Subsemiring R), ↑S.matrix = S.toAddSubmonoid.matrix.carrier
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofBdd_indep : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug : ∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E) (h_bdd : ∃ n, ∀ (I : Set α), Indep I → I.encard ≤ ↑n),
  (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).Indep = Indep
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.trim : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (hm : m ≤ mΩ),
  Measurable X → ProbabilityTheory.HasSubgaussianMGF X c μ → ProbabilityTheory.HasSubgaussianMGF X c (μ.trim hm)
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsLocallyNoetherianPullbackSchemeOfLocallyOfFiniteType : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsLocallyNoetherian Y]
  [AlgebraicGeometry.LocallyOfFiniteType f], AlgebraicGeometry.IsLocallyNoetherian (CategoryTheory.Limits.pullback f g)
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.Direction.sending.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Direction.sending = 1
-- Mathlib.Order.Atoms
CompleteAtomicBooleanAlgebra.eq_setOfPred_le_sSup_and_isAtom : ∀ {α : Type u_4} [inst : CompleteAtomicBooleanAlgebra α] {S : Set α},
  (∀ a ∈ S, IsAtom a) → S = {a | a ≤ sSup S ∧ IsAtom a}
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instIsPartialOrderDvd : IsPartialOrder Ordinal.{u_4} fun x1 x2 => x1 ∣ x2
-- Lean.Server.FileWorker.InlayHints
Lean.Elab.InlayHintKind.toLspInlayHintKind : Lean.Elab.InlayHintKind → Lean.Lsp.InlayHintKind
-- Mathlib.Algebra.Group.Irreducible.Lemmas
addIrreducible_add_iff : ∀ {M : Type u_2} [inst : AddMonoid M] {x y : M},
  AddIrreducible (x + y) ↔ AddIrreducible x ∧ IsAddUnit y ∨ AddIrreducible y ∧ IsAddUnit x
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.exists_distinct_prev_or : ∀ {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] (j : ι), (∃ k, c.Rel j k ∧ j ≠ k) ∨ ∀ (k : ι), ¬c.Rel j k
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.comp_homologySequenceδ_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A} (h_1 : (F.shift n₁).obj T.obj₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂)
          (CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Algebra.Order.Ring.Canonical
mul_tsub_one : ∀ {R : Type u} [inst : NonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b : R), a * (b - 1) = a * b - a
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.JD.congr_simp : ∀ (l : Type u_4) (R : Type u₂) {inst : DecidableEq l} [inst_1 : DecidableEq l] [inst_2 : CommRing R] (a a_1 : l ⊕ l),
  a = a_1 → ∀ (a_2 a_3 : l ⊕ l), a_2 = a_3 → LieAlgebra.Orthogonal.JD l R a a_2 = LieAlgebra.Orthogonal.JD l R a_1 a_3
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filter_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).isEmpty = false ↔
      ∃ k,
        ∃ (h : Std.Internal.List.containsKey k l = true),
          f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h) = true)
-- Init.Data.List.Lemmas
List.getLast?_eq_some_iff : ∀ {α : Type u_1} {xs : List α} {a : α}, xs.getLast? = some a ↔ ∃ ys, xs = ys ++ [a]