mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Simp.SimpM
_private.Lean.Meta.Sym.Simp.SimpM.0.Lean.Meta.Sym.Simp.MethodsRefPointed : NonemptyType
-- Init.Data.UInt.Lemmas
UInt16.le_of_eq : ∀ {a b : UInt16}, a = b → a ≤ b
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.quotientMap.eq_1 : ∀ {G : GrpCat} {P : ProfiniteGrp.{u}} (f : G ⟶ GrpCat.of ↑P.toProfinite.toTop)
  (H : OpenNormalSubgroup ↑P.toProfinite.toTop),
  ProfiniteGrp.ProfiniteCompletion.quotientMap f H =
    FiniteGrp.ofHom
      (QuotientGroup.map (ProfiniteGrp.ProfiniteCompletion.preimage f H).toSubgroup (↑H.toOpenSubgroup)
        (GrpCat.Hom.hom f) ⋯)
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond.eq_1 : Nat.stirlingSecond 0 0 = 1
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometric_radius_top_of_neg_nat₂ : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] (a c : 𝕂)
  {k : ℕ}, (ordinaryHypergeometricSeries 𝔸 a (-↑k) c).radius = ⊤
-- Lean.Meta.CoeAttr
/-- The coercion to a type, see `CoeSort.coe`  -/
Lean.Meta.CoeFnType.coeSort : Lean.Meta.CoeFnType
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.instInfSet : {M : Type u_1} → [inst : AddZeroClass M] → InfSet (AddSubmonoid M)
-- Batteries.Data.DList.Lemmas
Batteries.DList.empty.eq_1 : ∀ {α : Type u}, Batteries.DList.empty = { apply := id, invariant := ⋯ }
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (tree : Lean.Meta.LazyDiscrTree.PreDiscrTree α)
  (errors : Array Lean.Meta.LazyDiscrTree.ImportFailure),
  sizeOf { tree := tree, errors := errors } = 1 + sizeOf tree + sizeOf errors
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a * 0 = 0
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.CancelResult.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {mα : Q(Mul «$α»)} →
      {e v : Q(«$α»)} →
        (cancelled : Q(«$α»)) → Q(«$v» * «$e» = «$cancelled») → Mathlib.Tactic.CancelDenoms.CancelResult mα e v
-- Lean.Meta.DiscrTree.Util
/-- Apply a monadic function to the array of values at each node in a `DiscrTree`.  -/
Lean.Meta.DiscrTree.mapArraysM : {m : Type → Type} →
  [Monad m] → {α β : Type} → Lean.Meta.DiscrTree α → (Array α → m (Array β)) → m (Lean.Meta.DiscrTree β)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.equiv_iff_eq_of_Z_eq : ∀ {R : Type r} [inst : CommRing R] [NoZeroDivisors R] {P Q : Fin 3 → R}, P 2 = Q 2 → Q 2 ≠ 0 → (P ≈ Q ↔ P = Q)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Bisimulation principle using `map` and `Quot.mk` to match and relate children of two trees.  -/
MvQPF.Cofix.bisim_rel : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  (r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
  (∀ (x y : MvQPF.Cofix F α),
      r x y → MvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) →
    ∀ (x y : MvQPF.Cofix F α), r x y → x = y
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.of_gt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ t o₂ → Ordnode.nil.Bounded (↑x) o₂ → Ordnode.All (fun x_1 => x_1 > x) t → Ordnode.Valid' (↑x) t o₂
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isUniformEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding fun x => {x}
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_functor_obj_op_right : ∀ (C : Type u₁) {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (d : D),
  (CategoryTheory.Join.opEquiv C D).functor.obj (Opposite.op (CategoryTheory.Join.right d)) =
    CategoryTheory.Join.left (Opposite.op d)
-- Mathlib.Data.Set.Lattice
Set.biInter_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (t : α → Set β),
  ⋂ x ∈ ⋃ i, s i, t x = ⋂ i, ⋂ x ∈ s i, t x
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {P : HomotopicalAlgebra.Precylinder X} →
        {Y : C} →
          {f g : X ⟶ Y} →
            (h : P.I ⟶ Y) →
              autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h = f)
                  HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam →
                autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h = g)
                    HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam →
                  P.LeftHomotopy f g
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.rightUnitor_hom_hom : ∀ (X : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom = ProbabilityTheory.Kernel.id.map Prod.fst
-- Mathlib.Order.Height
Set.chainHeight_coe_univ_le : ∀ {α : Type u_1} (s : Set α) [inst : LE α],
  (Set.univ.chainHeight fun x1 x2 => x1 ≤ x2) = s.chainHeight fun x1 x2 => x1 ≤ x2
-- Mathlib.Tactic.Ring.Compare
/-- Prove goals of the form `A ≤ B` in an ordered commutative semiring, if the ring-normal forms of
`A` and `B` differ by a nonnegative (additive) constant.  -/
Mathlib.Tactic.Ring.proveLE : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Data.List.Defs
/-- Length of a list obtained using `mapAccumr₂`.  -/
List.length_mapAccumr₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : List α) (y : List β) (c : γ),
  (List.mapAccumr₂ f x y c).2.length = min x.length y.length
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- If `f` and `g` have the same constant term and derivative, then they are equal.  -/
PowerSeries.derivative.ext : ∀ {R : Type u_1} [inst : CommRing R] [IsAddTorsionFree R] {f g : PowerSeries R},
  (PowerSeries.derivative R) f = (PowerSeries.derivative R) g →
    PowerSeries.constantCoeff f = PowerSeries.constantCoeff g → f = g
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Decompose a bounded continuous function to its positive and negative parts.  -/
BoundedContinuousFunction.self_eq_nnrealPart_sub_nnrealPart_neg : ∀ {α : Type u} [inst : TopologicalSpace α] (f : BoundedContinuousFunction α ℝ),
  ⇑f = NNReal.toReal ∘ ⇑f.nnrealPart - NNReal.toReal ∘ ⇑(-f).nnrealPart
-- Mathlib.Topology.Order
clusterPt_of_indiscreteTopology : ∀ {α : Type u} [inst : TopologicalSpace α] [IndiscreteTopology α] {x : α} {f : Filter α} [f.NeBot], ClusterPt x f
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.prevn.eq_1 : ∀ (x : Substring.Raw) (x_1 : String.Pos.Raw), x.prevn 0 x_1 = x_1
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_inj : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {p q : PMF α},
  p.toMeasure = q.toMeasure ↔ p = q
-- Mathlib.Control.Fix
/-- The least fixed point of `f`.

If `f` is a continuous function (according to complete partial orders),
it satisfies the equations:

  1. `fix f = f (fix f)`          (is a fixed point)
  2. `∀ X, f X ≤ X → fix f ≤ X`   (least fixed point)
 -/
Part.fix : {α : Type u_1} → {β : α → Type u_2} → (((a : α) → Part (β a)) → (a : α) → Part (β a)) → (x : α) → Part (β x)
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- A scheme isomorphism viewed as a partial isomorphism defined on all of `X` and `Y`.  -/
AlgebraicGeometry.Scheme.PartialIso.ofIso : {X Y : AlgebraicGeometry.Scheme} → (X ≅ Y) → X.PartialIso Y
-- Std.Http.Server.Connection
/-- All mutable state carried through the connection processing loop.
Bundled into a struct so it can be passed to and returned from helper functions.
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState : Type → Type
-- Mathlib.Algebra.Ring.Ext
NonAssocSemiring.toNonUnitalNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonAssocSemiring.toNonUnitalNonAssocSemiring R)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapId_hom_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T) (X : CategoryTheory.Over Y),
  ((CategoryTheory.Over.mapId Y).hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instMul : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [∀ (i : ι), IsScalarTower R (A i) (A i)] → Mul (PiTensorProduct R fun i => A i)
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
CategoryTheory.SingleFunctors.instAdditiveFunctorLift : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{u_5, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_6, u_2} D] [inst_2 : CategoryTheory.Category.{u_7, u_3} E] {A : Type u_4}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C E A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] [inst_7 : G.Full]
  [inst_8 : G.Faithful] (Φ : A → CategoryTheory.Functor C D) (hΦ : (a : A) → (Φ a).comp G ≅ F.functor a)
  [inst_9 : CategoryTheory.Preadditive C] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : CategoryTheory.Preadditive E] [G.Additive] (a : A) [(F.functor a).Additive],
  ((F.lift G Φ hΦ).functor a).Additive
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_le_infEDist_add_edist`.

---

The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
the edist from `x` to `y`  -/
EMetric.infEdist_le_infEdist_add_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α},
  Metric.infEDist x s ≤ Metric.infEDist y s + edist x y
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine.go.match_1.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (p₁ p₂ : Lean.Grind.CommRing.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁_1 : Lean.Grind.CommRing.Poly) (k₂ : ℤ),
  p₁ = Lean.Grind.CommRing.Poly.add k₁ m₁ p₁_1 →
    p₂ = Lean.Grind.CommRing.Poly.num k₂ →
      (match p₁, p₂ with
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
        | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
        | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) ≍
        h_3 k₁ m₁ p₁_1 k₂
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.mk.inj : ∀ {K : Type u} {inst : DivisionRing K} {toSubring : Subring K}
  {inv_mem' : ∀ x ∈ toSubring.carrier, x⁻¹ ∈ toSubring.carrier} {toSubring_1 : Subring K}
  {inv_mem'_1 : ∀ x ∈ toSubring_1.carrier, x⁻¹ ∈ toSubring_1.carrier},
  { toSubring := toSubring, inv_mem' := inv_mem' } = { toSubring := toSubring_1, inv_mem' := inv_mem'_1 } →
    toSubring = toSubring_1
-- Mathlib.Topology.Compactness.Compact
isCompact_generateFrom' : ∀ {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)},
  T = TopologicalSpace.generateFrom S →
    ∀ {s : Set X}, (∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)) → IsCompact s
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_basisDivisor_left_of_ne : ∀ {F : Type u_1} [inst : Field F] {x y : F}, x ≠ y → Polynomial.eval x (Lagrange.basisDivisor x y) = 1
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.unitsComplexConj_eq_self_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (u : (NumberField.RingOfIntegers K)ˣ),
  (NumberField.IsCMField.unitsComplexConj K) u = u ↔ u ∈ NumberField.IsCMField.realUnits K
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on augmented cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Augmented.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u') →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.Functor (CategoryTheory.Functor C D)
          (CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Augmented C)
            (CategoryTheory.CosimplicialObject.Augmented D))
-- Mathlib.ModelTheory.ElementarySubstructures
/-- A set meets definable sets if it meets every nonempty definable subset.  -/
FirstOrder.Language.MeetsDefinable : {L : FirstOrder.Language} → {M : Type u_1} → [L.Structure M] → Set M → Prop
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below.refl : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} (x : M),
  ConGen.Rel.below ⋯
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
/-- The sum defining the Eisenstein series (of weight `k` and level `Γ(N)` with congruence
condition `a : Fin 2 → ZMod N`) converges locally uniformly on `ℍ`.  -/
EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly : ∀ {k : ℤ},
  3 ≤ k →
    ∀ {N : ℕ} (a : Fin 2 → ZMod N),
      TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, EisensteinSeries.eisSummand k (↑x_1) x)
        (fun x => eisensteinSeries a k x) Filter.atTop
-- Mathlib.Topology.UnitInterval
/-- `unitInterval.symm` as a `Homeomorph`.  -/
unitInterval.symmHomeomorph : ↑unitInterval ≃ₜ ↑unitInterval
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_toMeasurable_add_inter_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → (μ + ν) t ≠ ⊤ → μ (MeasureTheory.toMeasurable (μ + ν) t ∩ s) = μ (t ∩ s)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.of_integral_ne_zero : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0 → μ.Integrable f
-- Lean.Elab.Command
/-- Cancellation token forwarded to `Core.cancelTk?`.  -/
Lean.Elab.Command.Context.cancelTk? : Lean.Elab.Command.Context → Option IO.CancelToken
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.gen.eq_1 : ∀ (α : Type u_1) (β : Type u_2) (V : Set (β × β)),
  UniformFun.gen α β V = {uv | ∀ (x : α), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V}
-- Mathlib.Data.Nat.Init
Nat.leRec_trans : ∀ {n m k : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (hnm : n ≤ m) (hmk : m ≤ k),
  Nat.leRec refl le_succ_of_le ⋯ =
    Nat.leRec (Nat.leRec refl (fun x h => le_succ_of_le h) hnm) (fun x h => le_succ_of_le ⋯) hmk
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- To construct an isomorphism between coforks,
it suffices to give an isomorphism between the cocone points
and check that it commutes with the `π` morphisms.
 -/
CategoryTheory.Limits.Cofork.ext : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s t : CategoryTheory.Limits.Cofork f g} →
          (i : s.pt ≅ t.pt) →
            autoParam (CategoryTheory.CategoryStruct.comp s.π i.hom = t.π) CategoryTheory.Limits.Cofork.ext._auto_1 →
              (s ≅ t)
-- Lean.Compiler.IR.CompilerM
Lean.IR.findLocalDecl : Lean.Name → Lean.IR.CompilerM (Option Lean.IR.Decl)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_limit : ∀ (o : ONote) {f : ℕ → ONote}, o.fundamentalSequence = Sum.inr f → o.fastGrowing = fun i => (f i).fastGrowing i
-- Mathlib.Topology.Closure
forall_isOpen_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Set X → Prop},
  (∀ (t : Set X), IsOpen t → p t) ↔ ∀ (t : Set X), p (interior t)
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.val_list_prod : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (l : List ↥H), ↑l.prod = (List.map Subtype.val l).prod
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_zero_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S 0 f = 0
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.root.eq_def : ∀ (self : Batteries.UnionFind) (x : Fin self.size),
  self.root x =
    let y := self.arr[↑x].parent;
    if h : y = ↑x then x
    else
      have this := ⋯;
      self.root ⟨y, ⋯⟩
-- Mathlib.Topology.Separation.Basic
/-- See also `continuousWithinAt_sdiff_self` for the case `y = x` but not requiring `T1Space`.  -/
continuousWithinAt_sdiff_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x y : X}
  {s : Set X} {f : X → Y}, ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x
-- Init.Data.Ord.Basic
/-- Checks whether the ordering is `lt` or `eq`.
 -/
Ordering.isLE : Ordering → Bool
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.mulHead_head : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j)
  (x : M i) (hnotone : x * w.head ≠ 1), (w.mulHead x hnotone).head = x * w.head
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_snd : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)),
  (CategoryTheory.Limits.pullback.snd f g) (AlgebraicGeometry.Scheme.Pullback.carrierEquiv.symm ⟨T, p⟩) = T.y
-- Mathlib.Algebra.Order.Group.PosPart
one_lt_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], a < 1 → 1 < a⁻ᵐ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgEquiv.eq_1 : ∀ (σ : Type u_1) (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R] (hn : Fintype.card σ = n),
  MvPolynomial.esymmAlgEquiv σ R hn = AlgEquiv.ofBijective (MvPolynomial.esymmAlgHom σ R n) ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
/-- Let `𝒜` be a graded ring generated over `𝒜₀` by finitely many homogeneous elements.
Suppose we have the following diagram for some homogeneous `x`
with `O` a valuation ring and `K = Frac(O)`.
```
    φ
K ←--- 𝒜_{(x)}
↑       ↑
|       |
|       |
O ←---- 𝒜₀
    φ₀
```
Then there exists a lift `φₗ : 𝒜_{(x₀)} →+* O` for some `x₀`
such that these two diagrams exist and commute.
```
    φ'                      φ'
K ←--- 𝒜_{(x x₀)}       K ←--- 𝒜_{(x x₀)}
↑       ↑                 ↖       ↑
|       |                 φ ⟍     |
|       |                     ⟍   |
O ←---- 𝒜_{(x₀)}                𝒜_{(x)}
    φₗ
```
This is the underlying algebraic statement of the valuative criterion for `Proj 𝒜`.
 -/
AlgebraicGeometry.Proj.valuativeCriterion_existence_aux : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {O : Type u_3} [inst_4 : CommRing O] [inst_5 : IsDomain O] [ValuationRing O] {K : Type u_4}
  [inst_7 : Field K] [inst_8 : Algebra O K] [IsFractionRing O K] (φ₀ : ↥(𝒜 0) →+* O) (ι : Type u_5) [Finite ι]
  (x : ι → A),
  Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤ →
    ∀ (j : ι) (φ : HomogeneousLocalization.Away 𝒜 (x j) →+* K),
      (algebraMap O K).comp φ₀ = φ.comp (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers (x j))) →
        ∀ (d : ι → ℕ),
          (∀ (i : ι), 0 < d i) →
            ∀ (hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)),
              ∃ j₀ φ',
                φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯) = φ ∧
                  (φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
-- Std.Data.HashSet.Lemmas
Std.HashSet.distinct_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  List.Pairwise (fun a b => (a == b) = false) m.toList
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
PrimeSpectrum.sigmaToPi_apply : ∀ {ι : Type u_3} (R : ι → Type u_2) [inst : (i : ι) → CommSemiring (R i)] (i : ι) (p : PrimeSpectrum (R i)),
  PrimeSpectrum.sigmaToPi R ⟨i, p⟩ = PrimeSpectrum.comap (Pi.evalRingHom R i) p
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimitNegAux_eq_of_rel : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)),
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget AddGrpCat)) x y →
    AddGrpCat.FilteredColimits.colimitNegAux F x = AddGrpCat.FilteredColimits.colimitNegAux F y
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstHSubInt : Lean.Expr → Lean.MetaM Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.Equiv t₂ → t₁.getKeyLED k fallback = t₂.getKeyLED k fallback
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iio_subset_Iic_self : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] {a : α}, Finset.Iio a ⊆ Finset.Iic a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `S`.  -/
CategoryTheory.Limits.ChosenPullback₃.p : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (self : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → self.chosenPullback.pullback ⟶ S
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.joinedIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F → ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Multiset α}, Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
-- Mathlib.Analysis.Convex.Topology
segment_subset_closure_openSegment : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DenselyOrdered 𝕜]
  [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] [inst_6 : AddCommGroup E] [inst_7 : TopologicalSpace E]
  [ContinuousAdd E] [inst_9 : Module 𝕜 E] [ContinuousSMul 𝕜 E] {x y : E}, segment 𝕜 x y ⊆ closure (openSegment 𝕜 x y)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_eq_get : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  Std.PRange.succ a = (Std.PRange.succ? a).get ⋯
-- Mathlib.Topology.Instances.ENat
ENat.mem_nhds_natCast_iff : ∀ (n : ℕ) {s : Set ℕ∞}, s ∈ nhds ↑n ↔ ↑n ∈ s