mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.Internal.AssocList.iter.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : Std.DHashMap.Internal.AssocList α β), l.iter = { internalState := { l := l } }
-- Mathlib.Algebra.PEmptyInstances
AddSemigroupPEmpty.eq_1 : AddSemigroupPEmpty = { add := fun x x_1 => PEmpty.casesOn (fun t => x = t → PEmpty.{u + 1}) x ⋯, add_assoc := ⋯ }
-- Init.Data.List.Lemmas
List.prod_append : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1]
  [Std.Associative fun x1 x2 => x1 * x2] {l₁ l₂ : List α}, (l₁ ++ l₂).prod = l₁.prod * l₂.prod
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.conj_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E},
  T.IsPositive → ∀ (S : E →ₗ[𝕜] F), (S ∘ₗ T ∘ₗ LinearMap.adjoint S).IsPositive
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.toIsPreimmersion : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsPreimmersion f
-- Mathlib.NumberTheory.ZetaValues
/-- Recurrence relation (in `k`) for the `n`-th Fourier coefficient of `Bₖ`.  -/
bernoulliFourierCoeff_recurrence : ∀ (k : ℕ) {n : ℤ},
  n ≠ 0 →
    bernoulliFourierCoeff k n =
      1 / (-2 * ↑Real.pi * Complex.I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.parts_partition : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α},
  σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The affine coordinate ring `R[W] := R[X, Y] / ⟨W(X, Y)⟩` of a Weierstrass curve `W`.  -/
WeierstrassCurve.Affine.CoordinateRing : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → Type r
-- Mathlib.Topology.Instances.ENNReal.Lemmas
nhds_eq_nhds_emetric_ball : ∀ {β : Type u_2} [inst : EMetricSpace β] (a x : β) (r : ENNReal) (h : x ∈ Metric.eball a r),
  nhds x = Filter.map Subtype.val (nhds ⟨x, h⟩)
-- Mathlib.Topology.Algebra.Module.Basic
/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.

In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well.  -/
Submodule.closure_coe_iSup_map_single : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : (i : ι) → TopologicalSpace (M i)] [inst_4 : DecidableEq ι]
  (s : (i : ι) → Submodule R (M i)),
  closure ↑(⨆ i, Submodule.map (LinearMap.single R M i) (s i)) = Set.univ.pi fun i => closure ↑(s i)
-- Lean.Environment
/-- Commits the full constant info as well as the current environment extension state and set of nested
asynchronous constants to the main environment branch. If `info?` is `none`, it is taken from the
given environment. The declaration name and kind must match the original values given to
`addConstAsync`. The signature must match the previous `commitSignature` call, if any.
 -/
Lean.Environment.AddConstAsyncResult.commitConst : Lean.Environment.AddConstAsyncResult →
  Lean.Environment → optParam (Option Lean.ConstantInfo) none → optParam (Option Lean.ConstantInfo) none → IO Unit
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying modification of oplax transformations.  -/
CategoryTheory.Oplax.OplaxTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.OplaxTrans.Hom η θ → CategoryTheory.Oplax.OplaxTrans.Modification η θ
-- Mathlib.Algebra.Quandle
/-- The canonical homomorphism from a rack to its enveloping group.
Satisfies universal properties given by `toEnvelGroup.map` and `toEnvelGroup.univ`.
 -/
Rack.toEnvelGroup : (R : Type u_1) → [inst : Rack R] → ShelfHom R (Quandle.Conj (Rack.EnvelGroup R))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtTreeMap α β cmp}, (∀ (k : α), t₁[k]? = t₂[k]?) → t₁ = t₂
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivRight_symm_apply : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R] (a : MvPolynomial S₁ (Polynomial R)),
  (MvPolynomial.optionEquivRight R S₁).symm a =
    (MvPolynomial.aevalTower (Polynomial.aeval (MvPolynomial.X none)) fun i => MvPolynomial.X (some i)) a
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.rightHomologyMap_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (a : R) [inst_4 : S₁.HasRightHomology] [inst_5 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.rightHomologyMap φ
-- Mathlib.Topology.Convenient.Category
/-- The underlying type of an object in `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.carrier : {ι : Type t} → {X : ι → Type u} → [inst : (i : ι) → TopologicalSpace (X i)] → ContinuousGeneratedByCat X → Type v
-- Lean.Server.CodeActions.Basic
/-- A code action provider is a function for providing LSP code actions for an editor.
You can register them with the `@[code_action_provider]` attribute.

This is a low-level interface for making LSP code actions.
This interface can be used to implement the following applications:
- refactoring code: adding underscores to unused variables,
- suggesting imports
- document-level refactoring: removing unused imports, sorting imports, formatting.
- Helper suggestions for working with type holes (`_`)
- Helper suggestions for tactics.

When implementing your own `CodeActionProvider`, we assume that no long-running computations are allowed.
If you need to create a code-action with a long-running computation, you can use the `lazy?` field on `LazyCodeAction`
to perform the computation after the user has clicked on the code action in their editor.
 -/
Lean.Server.CodeActionProvider : Type
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.one_comp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.comp 1 p = 1
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.norm_mem_relNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] [Module.Free R S]
  (I : Ideal S) {x : S}, x ∈ I → (Algebra.norm R) x ∈ (Ideal.relNorm R) I
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_eq_top : ∀ {M : Type u_2} [inst : Mul M] {S : Subsemigroup Mᵐᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.kernelFork.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst fst_1 : X₁ ⟶ X₂} (e_fst : fst = fst_1)
  {snd snd_1 : X₁ ⟶ X₃} (e_snd : snd = snd_1) {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq fst snd f g),
  sq.kernelFork = ⋯.kernelFork
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.Nondegenerate.congr : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  B.Nondegenerate → ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).Nondegenerate
-- Mathlib.Order.UpperLower.Closure
upperClosure_univ : ∀ {α : Type u_1} [inst : Preorder α], upperClosure Set.univ = ⊥
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.brecOn.eq : ∀ {motive : Mathlib.Tactic.ITauto.IProp → Sort u} (t : Mathlib.Tactic.ITauto.IProp)
  (F_1 : (t : Mathlib.Tactic.ITauto.IProp) → Mathlib.Tactic.ITauto.IProp.below t → motive t),
  Mathlib.Tactic.ITauto.IProp.brecOn t F_1 = F_1 t (Mathlib.Tactic.ITauto.IProp.brecOn.go t F_1).2
-- Init.Data.List.Monadic
List.zipWithM'.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x : List α)
  (x_1 : List β),
  (∀ (x_2 : α) (xs : List α) (y : β) (ys : List β), x = x_2 :: xs → x_1 = y :: ys → False) →
    List.zipWithM' f x x_1 = pure []
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVar.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : L.Term α) → (↥x.varFinset → β) → Sort u_4) (a : α) (f : ↥(FirstOrder.Language.var a).varFinset → β)
  (h_1 : (a : α) → (f : ↥(FirstOrder.Language.var a).varFinset → β) → motive (FirstOrder.Language.var a) f)
  (h_2 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term α) →
          (f : ↥(FirstOrder.Language.func F ts).varFinset → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.var a, f with
    | FirstOrder.Language.var a, f => h_1 a f
    | FirstOrder.Language.func F ts, f => h_2 l F ts f) =
    h_1 a f
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationLeftAdjoint_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (d : D) {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.evaluationLeftAdjoint D c).obj d).map f =
    CategoryTheory.Limits.Sigma.desc fun g =>
      CategoryTheory.Limits.Sigma.ι (fun x => d) (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Order.Filter.Ker
Filter.ker_mono : ∀ {α : Type u_2}, Monotone Filter.ker
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.SeparatingLeft.toLinearMap₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  M.SeparatingLeft → ((Matrix.toLinearMap₂' R) M).SeparatingLeft
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.mk.injEq : ∀ (var : ℕ) (irrelevant : List Lean.Elab.Tactic.Omega.Fact)
  (lowerBounds upperBounds : List (Lean.Elab.Tactic.Omega.Fact × ℤ)) (lowerExact upperExact : Bool) (var_1 : ℕ)
  (irrelevant_1 : List Lean.Elab.Tactic.Omega.Fact)
  (lowerBounds_1 upperBounds_1 : List (Lean.Elab.Tactic.Omega.Fact × ℤ)) (lowerExact_1 upperExact_1 : Bool),
  ({ var := var, irrelevant := irrelevant, lowerBounds := lowerBounds, upperBounds := upperBounds,
        lowerExact := lowerExact, upperExact := upperExact } =
      { var := var_1, irrelevant := irrelevant_1, lowerBounds := lowerBounds_1, upperBounds := upperBounds_1,
        lowerExact := lowerExact_1, upperExact := upperExact_1 }) =
    (var = var_1 ∧
      irrelevant = irrelevant_1 ∧
        lowerBounds = lowerBounds_1 ∧
          upperBounds = upperBounds_1 ∧ lowerExact = lowerExact_1 ∧ upperExact = upperExact_1)
-- Mathlib.Data.Finset.NoncommProd
/-- The non-commutative version of `Finset.prod_union`  -/
Finset.noncommProd_union_of_disjoint : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] [inst_1 : DecidableEq α] {s t : Finset α},
  Disjoint s t →
    ∀ (f : α → β) (comm : (↑(s ∪ t)).Pairwise (Function.onFun Commute f)),
      (s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯
-- Mathlib.Logic.Equiv.Fin.Rotate
finRotate_apply_zero : ∀ {n : ℕ}, (finRotate n.succ) 0 = 1
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd_ac_fst : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ),
  (ρ.IicSnd r).AbsolutelyContinuous ρ.fst
-- Init.Data.UInt.Bitwise
UInt8.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt8}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.mk.inj : ∀ {α : Type} {smap : Lean.PHashMap Lean.Name (List α)} {origins erased : Lean.PHashSet Lean.Meta.Grind.Origin}
  {omap : Lean.PHashMap Lean.Meta.Grind.Origin (List α)} {smap_1 : Lean.PHashMap Lean.Name (List α)}
  {origins_1 erased_1 : Lean.PHashSet Lean.Meta.Grind.Origin} {omap_1 : Lean.PHashMap Lean.Meta.Grind.Origin (List α)},
  { smap := smap, origins := origins, erased := erased, omap := omap } =
      { smap := smap_1, origins := origins_1, erased := erased_1, omap := omap_1 } →
    smap = smap_1 ∧ origins = origins_1 ∧ erased = erased_1 ∧ omap = omap_1
-- Init.Prelude
/-- `a >> b` executes `a`, ignores the result, and then executes `b`.
If `a` fails then `b` is not executed. Because `b` is not always executed, it
is passed as a thunk so it can be forced only when needed.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `>>` in identifiers is `andThen`. -/
HAndThen.hAndThen : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAndThen α β γ] → α → (Unit → β) → γ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toENNRealVectorMeasure_zero : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasureTheory.Measure.toENNRealVectorMeasure 0 = 0
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willChange.sizeOf_spec : sizeOf Lean.Widget.DiffTag.willChange = 1
-- Init.Data.String.Lemmas.StringOrder
String.ne_of_lt : ∀ {a b : String}, a < b → a ≠ b
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.eval.eq_6 : ∀ (f g : Turing.ToPartrec.Code),
  (f.case g).eval = fun v => Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
_private.Mathlib.Topology.Algebra.Valued.ValuativeRel.0.IsValuativeTopology.termV_1 : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage : AlgebraicGeometry.Scheme.jointlySurjectivePrecoverage.IsStableUnderBaseChange
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Transfer the arguments to a map along an equivalence between argument indices.

The naming is derived from `Finsupp.domCongr`, noting that here the permutation applies to the
domain of the domain.  -/
MultilinearMap.domDomCongr : {R : Type uR} →
  {M₂ : Type v₂} →
    {M₃ : Type v₃} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M₃] →
            [inst_3 : Module R M₂] →
              [inst_4 : Module R M₃] →
                {ι₁ : Type u_1} →
                  {ι₂ : Type u_2} → ι₁ ≃ ι₂ → MultilinearMap R (fun x => M₂) M₃ → MultilinearMap R (fun x => M₂) M₃
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaPDF_of_pos_lt_one : ∀ {α β x : ℝ},
  0 < x →
    x < 1 →
      ProbabilityTheory.betaPDF α β x =
        ENNReal.ofReal (1 / ProbabilityTheory.beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
-- Init.Data.Rat.Lemmas
Rat.le_of_lt : ∀ {a b : ℚ}, a < b → a ≤ b
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.mk.inj : ∀ {R : Type u_1} {S : Type u_2} {inst : Semiring R} {inst_1 : Semiring S} {σ : R →+* S} {σ' : S →+* R}
  {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ} {M : Type u_3} {inst_4 : TopologicalSpace M}
  {inst_5 : AddCommMonoid M} {M₂ : Type u_4} {inst_6 : TopologicalSpace M₂} {inst_7 : AddCommMonoid M₂}
  {inst_8 : Module R M} {inst_9 : Module S M₂} {toLinearEquiv : M ≃ₛₗ[σ] M₂}
  {continuous_toFun : autoParam (Continuous (↑toLinearEquiv).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toLinearEquiv.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam}
  {toLinearEquiv_1 : M ≃ₛₗ[σ] M₂}
  {continuous_toFun_1 :
    autoParam (Continuous (↑toLinearEquiv_1).toFun) ContinuousLinearEquiv.continuous_toFun._autoParam}
  {continuous_invFun_1 :
    autoParam (Continuous toLinearEquiv_1.invFun) ContinuousLinearEquiv.continuous_invFun._autoParam},
  { toLinearEquiv := toLinearEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toLinearEquiv := toLinearEquiv_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 } →
    toLinearEquiv = toLinearEquiv_1
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.Pos.find?_char_eq_none_iff : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  pos.find? c = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), pos'.get h ≠ c
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- The class of weak equivalences in a category with weak equivalences.  -/
HomotopicalAlgebra.weakEquivalences : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → CategoryTheory.MorphismProperty C
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.trivialFibrations_sub_weakEquivalences : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialFibrations C ≤ HomotopicalAlgebra.weakEquivalences C
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.wr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g)
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (self.a i) (F.p₂ (self.H i)) = g.h₀ i
-- Mathlib.AlgebraicGeometry.Sites.Small
/-- The presieve defined by a `P`-cover of `S`-schemes.  -/
AlgebraicGeometry.Scheme.Cover.toPresieveOver : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : P.IsStableUnderBaseChange] →
      {X : CategoryTheory.Over S} →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X.left) →
          [AlgebraicGeometry.Scheme.Cover.Over S 𝒰] → CategoryTheory.Presieve X
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_add_ofNat_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIocMod hp a (b + OfNat.ofNat m * p) = toIocMod hp a b
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.mapCotangent_toCotangent : ∀ {R : Type u} [inst : CommRing R] {A : Type u_1} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B)
  (h : I₁ ≤ Ideal.comap f I₂) (x : ↥I₁), (I₁.mapCotangent I₂ f h) (I₁.toCotangent x) = I₂.toCotangent ⟨f ↑x, ⋯⟩
-- Lean.Environment
/-- Creates an async context for the given declaration name, normalizing it for use as a prefix.  -/
_private.Lean.Environment.0.Lean.Environment.enterAsync : Lean.Name → Lean.Environment → Lean.Environment
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- The **valuative criterion** for separated morphisms.  -/
AlgebraicGeometry.IsSeparated.eq_valuativeCriterion : @AlgebraicGeometry.IsSeparated = AlgebraicGeometry.ValuativeCriterion.Uniqueness ⊓ @AlgebraicGeometry.QuasiSeparated
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.leadingCoeff_preHilbertPoly : ∀ (F : Type u_1) [inst : Field F] [CharZero F] (d k : ℕ),
  (Polynomial.preHilbertPoly F d k).leadingCoeff = (↑d.factorial)⁻¹
-- Mathlib.Topology.SmallInductiveDimension
HasSmallInductiveDimensionLT.hasSmallInductiveDimensionLE : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ},
  HasSmallInductiveDimensionLT X n → HasSmallInductiveDimensionLE X n
-- Mathlib.GroupTheory.CoprodI
/-- See note [partially-applied ext lemmas].  -/
Monoid.CoprodI.ext_hom : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N]
  (f g : Monoid.CoprodI M →* N), (∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of) → f = g
-- Lean.Structure
_private.Lean.Structure.0.Lean.StructureState.mk.sizeOf_spec : ∀ (map : Lean.PersistentHashMap Lean.Name Lean.StructureInfo), sizeOf { map := map } = 1 + sizeOf map
-- Init.Data.Array.Basic
/-- Returns `true` if no two elements of `as` are equal according to the `==` operator.

Examples:
* `#["red", "green", "blue"].allDiff = true`
* `#["red", "green", "red"].allDiff = false`
* `(#[] : Array Nat).allDiff = true`
 -/
Array.allDiff : {α : Type u} → [BEq α] → Array α → Bool
-- Batteries.Tactic.GeneralizeProofs
/-- Core loop for `withGeneralizedProofs`, adds generalizations one at a time.  -/
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.withGeneralizedProofs.go : {α : Type} →
  (Array Lean.Expr → Array Lean.Expr → Lean.Expr → Batteries.Tactic.GeneralizeProofs.MGen α) →
    Lean.Expr →
      Array (Lean.Expr × Lean.Expr) →
        [Nonempty α] →
          ℕ →
            Array Lean.Expr →
              Array Lean.Expr →
                Lean.ExprMap Lean.Expr → Lean.ExprMap Lean.Expr → Batteries.Tactic.GeneralizeProofs.MGen α
-- Mathlib.Logic.Function.Basic
Function.bijective_of_subsingleton : ∀ {α : Sort u_1} [Subsingleton α] (f : α → α), Function.Bijective f
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.coe_range : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), ↑f.range = Set.range ⇑f
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.pi : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_6} {M : ι → Type u_7} [Finite ι]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] [h : ∀ (i : ι), Module.Finite R (M i)],
  Module.Finite R ((i : ι) → M i)
-- Mathlib.Algebra.Module.LinearMap.End
DistribMulAction.toModuleEnd_apply : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : S),
  (DistribMulAction.toModuleEnd R M) s = DistribSMul.toLinearMap R M s
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeOpEquiv_inverse : ∀ (J : Type w), (CategoryTheory.Limits.widePullbackShapeOpEquiv J).inverse = CategoryTheory.Limits.widePushoutShapeOp J
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- The map `R[X] → S[X]` as an algebra homomorphism.  -/
Polynomial.mapAlg : (R : Type u) →
  [inst : CommSemiring R] →
    (S : Type v) → [inst_1 : Semiring S] → [inst_2 : Algebra R S] → Polynomial R →ₐ[R] Polynomial S
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidLe.eq_2 : ∀ (p : Int.Internal.Linear.Poly), (∀ (k : ℤ), p = Int.Internal.Linear.Poly.num k → False) → p.isValidLe = false
-- Mathlib.Data.EReal.Basic
EReal.toReal_nonneg : ∀ {x : EReal}, 0 ≤ x → 0 ≤ x.toReal