mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- The bijection between `rootSet p p.SplittingField` and `rootSet p E`.  -/
Polynomial.Gal.rootsEquivRoots : {F : Type u_1} →
  [inst : Field F] →
    (p : Polynomial F) →
      (E : Type u_2) →
        [inst_1 : Field E] →
          [inst_2 : Algebra F E] →
            [Fact (Polynomial.map (algebraMap F E) p).Splits] → ↑(p.rootSet p.SplittingField) ≃ ↑(p.rootSet E)
-- Lean.Meta.Basic
Lean.Meta.MetaM.toIO : {α : Type} →
  Lean.MetaM α →
    Lean.Core.Context →
      Lean.Core.State →
        optParam Lean.Meta.Context { } → optParam Lean.Meta.State { } → IO (α × Lean.Core.State × Lean.Meta.State)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algEquivOfTranscendental.eq_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f),
  RatFunc.algEquivOfTranscendental f h = IsFractionRing.algEquivOfAlgEquiv (Polynomial.algEquivOfTranscendental K f h)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.isOpen_iff_generate_Ici_compl : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {s : Set α},
  IsOpen s ↔ TopologicalSpace.GenerateOpen {t | ∃ a, (Set.Ici a)ᶜ = t} s
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.nth_mul_coeff' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (k : Type u_1) [inst : CommRing k] [CharP k p] (n : ℕ),
  ∃ f,
    ∀ (x y : WittVector p k),
      f (WittVector.truncateFun (n + 1) x) (WittVector.truncateFun (n + 1) y) =
        (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
-- Mathlib.Order.RelSeries
/-- Given a series `a₀ -r→ a₁ -r→ ... -r→ aₙ` and an `a` such that `a₀ -r→ a` holds, there is
a series of length `n+1`: `a -r→ a₀ -r→ a₁ -r→ ... -r→ aₙ`.
 -/
RelSeries.cons : {α : Type u_1} → {r : SetRel α α} → (p : RelSeries r) → (newHead : α) → (newHead, p.head) ∈ r → RelSeries r
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.mulOppositeEquiv.eq_1 : ∀ {M : Type u_2} [inst : Monoid M],
  MulActionHom.End.mulOppositeEquiv =
    { toFun := fun f => f 1, invFun := fun m => { toFun := fun x => m * x, map_smul' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Lean.Util.SCC
Lean.SCC.State.mk.inj : ∀ {α : Type} {inst : BEq α} {inst_1 : Hashable α} {stack : List α} {nextIndex : ℕ} {data : Std.HashMap α Lean.SCC.Data}
  {sccs : List (List α)} {stack_1 : List α} {nextIndex_1 : ℕ} {data_1 : Std.HashMap α Lean.SCC.Data}
  {sccs_1 : List (List α)},
  { stack := stack, nextIndex := nextIndex, data := data, sccs := sccs } =
      { stack := stack_1, nextIndex := nextIndex_1, data := data_1, sccs := sccs_1 } →
    stack = stack_1 ∧ nextIndex = nextIndex_1 ∧ data = data_1 ∧ sccs = sccs_1
-- Mathlib.Algebra.Polynomial.Degree.Domain
Polynomial.eq_zero_of_dvd_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p q : Polynomial R}, p ∣ q → q.natDegree < p.natDegree → q = 0
-- Mathlib.Order.KrullDimension
Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top : ∀ {α : Type u_1} [inst : Preorder α], FiniteDimensionalOrder α ↔ Order.krullDim α ≠ ⊥ ∧ Order.krullDim α ≠ ⊤
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a `CommGroup` is a `CommGroup`.  -/
Subgroup.toCommGroup : {G : Type u_3} → [inst : CommGroup G] → (H : Subgroup G) → CommGroup ↥H
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (i j : n), A.adjugate i j = (A.updateRow j (Pi.single i 1)).det
-- Std.Do.WP.SimpLemmas
Std.Do.WP.ExceptT_run : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond (Except ε α) ps}
  [inst : Std.Do.WP m ps] (x : ExceptT ε m α),
  (Std.Do.wp x.run).apply Q = (Std.Do.wp x).apply (fun a => Q.1 (Except.ok a), fun e => Q.1 (Except.error e), Q.2)
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.liftSemilatticeInf.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : SemilatticeInf α]
  (gi : GaloisCoinsertion u l),
  gi.liftSemilatticeInf =
    { toPartialOrder := inst, inf := fun a b => l (u a ⊓ u b), inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Init.Data.Vector.Find
Vector.find?_flatten_eq_none_iff : ∀ {α : Type} {m n : ℕ} {xs : Vector (Vector α m) n} {p : α → Bool},
  Vector.find? p xs.flatten = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, (!p x) = true
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_apply : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : Module.Dual R M) (m : M) (n : N),
  ((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m • n
-- Plausible.Gen
Plausible.instMonoBindExceptGenError : Lean.Order.MonoBind (Except Plausible.GenError)
-- Mathlib.Algebra.Order.Field.GeomSum
geom_sum_of_lt_one : ∀ {K : Type u_1} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [CanonicallyOrderedAdd K]
  [inst_4 : Sub K] [OrderedSub K] {x : K}, x < 1 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_one : ∀ (a : Ordinal.{u_4}), a % 1 = 0
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Header.targetType : Lean.Elab.Deriving.Header → Lean.Term
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
_private.Mathlib.Algebra.Category.HopfAlgCat.Basic.0.HopfAlgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (carrier : Type v) [instRing : Ring carrier]
  [instHopfAlgebra : HopfAlgebra R carrier] (carrier_1 : Type v) (instRing_1 : Ring carrier_1)
  (instHopfAlgebra_1 : HopfAlgebra R carrier_1),
  ({ carrier := carrier, instRing := instRing, instHopfAlgebra := instHopfAlgebra } =
      { carrier := carrier_1, instRing := instRing_1, instHopfAlgebra := instHopfAlgebra_1 }) =
    (carrier = carrier_1 ∧ instRing ≍ instRing_1 ∧ instHopfAlgebra ≍ instHopfAlgebra_1)
-- Mathlib.Order.WellFoundedSet
Set.isPWO_iff_exists_monotone_subseq : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, Monotone (f ∘ ⇑g)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData.mk : {α : Type u} →
  [inst : Ord α] → (Std.DTreeMap.Internal.Impl α fun x => Unit) → Std.Rcc α → Std.DTreeMap.Internal.Unit.RccSliceData α
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.Measure.condKernel.instIsCondKernel : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (ρ : MeasureTheory.Measure (α × Ω)) [inst_2 : MeasureTheory.IsFiniteMeasure ρ],
  ρ.IsCondKernel ρ.condKernel
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.inter : ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
  DirSupClosedOn D s → DirSupClosedOn D t → DirSupClosedOn D (s ∩ t)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).isEmpty = true
-- Lean.Meta.InferType
/-- `isProp e` returns `true` if `e` is a proposition.

If `e` contains metavariables, it may not be possible to decide whether it is a proposition or not.
We return `false` in this case. We considered using `LBool` and returning `LBool.undef`, but we
have no applications for it.
 -/
Lean.Meta.isProp : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Real.Basic
Real.cauchy_mul : ∀ (a b : ℝ), (a * b).cauchy = a.cauchy * b.cauchy
-- Mathlib.Analysis.Quaternion
Quaternion.linearIsometryEquivTuple_symm_apply : ∀ (a : EuclideanSpace ℝ (Fin 4)),
  Quaternion.linearIsometryEquivTuple.symm a = { re := a.ofLp 0, imI := a.ofLp 1, imJ := a.ofLp 2, imK := a.ofLp 3 }
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The relationship between the counit and hom set equivalence of an adjunction  -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (self : CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G) {X : C} {Y : D} {g : X ⟶ G.obj Y},
  (self.homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (self.counit.app Y)
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Polynomial.aeval_mem_adjoin_singleton : ∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {p : Polynomial R}
  (x : A), (Polynomial.aeval x) p ∈ R[x]
-- Aesop.Tree.Data
Aesop.Goal.priority : Aesop.Goal → Aesop.Percent
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOpId_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Functor.rightOpId C).inv.app X = CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.op X))
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- Given an adjunction `F ⊣ G` and a `CommShift` structure on `G`, this constructs
the unique compatible `CommShift` structure on `F`.
 -/
CategoryTheory.Adjunction.leftAdjointCommShift : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              (A : Type u_3) →
                [inst_2 : AddGroup A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] → [G.CommShift A] → F.CommShift A
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_ofAddUnits_iff : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) (x : M), x ∈ S.ofAddUnits ↔ ∃ y ∈ S, ↑y = x
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_zsmul' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocDiv hp (a + m • p) b = toIocDiv hp a b - m
-- Std.Internal.Do.PredTrans
/-- Lift a predicate transformer to one with a state argument (pointwise).  -/
Std.Internal.Do.instMonadLiftPredTransForall : {σ : Type u} →
  {Pred : Type v} →
    {EPred : Type w} → MonadLift (Std.Internal.Do.PredTrans Pred EPred) (Std.Internal.Do.PredTrans (σ → Pred) EPred)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.πE_EToCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_EToCycles._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_EToCycles._auto_3) {Z : C}
  (h : X.cycles f₁ f₂₃ n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.EToCycles f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂) h) =
    CategoryTheory.CategoryStruct.comp
      (X.cyclesMap f₁ f₂ f₁ f₂₃ (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) h
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
/-- If `d : MulticospanIndex J C`, `c : Multifork d` and `F : C ⥤ D`,
the cone `F.mapCone c` is limiting iff the multifork `c.map F` is.  -/
CategoryTheory.Limits.Multifork.isLimitMapEquiv : {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] →
        {J : CategoryTheory.Limits.MulticospanShape} →
          {d : CategoryTheory.Limits.MulticospanIndex J C} →
            (c : CategoryTheory.Limits.Multifork d) →
              (F : CategoryTheory.Functor C D) →
                CategoryTheory.Limits.IsLimit (F.mapCone c) ≃ CategoryTheory.Limits.IsLimit (c.map F)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.topEquiv_toAddHom : ∀ {M : Type u_1} [inst : Add M], ↑AddSubsemigroup.topEquiv = AddMemClass.subtype ⊤
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k) κ μ
-- Mathlib.Combinatorics.Graph.Simple
Graph.IsLink.eq : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} [G.Simple], G.IsLink e u v → G.IsLink f u v → e = f
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IsPreorder` instance if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.isPreorderInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_eq_nilradical : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, 1 < p → pNilradical R p = nilradical R
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.values_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.values = t₂.values
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.mem_even : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → x ∈ CliffordAlgebra.even Q
-- Lean.Meta.Tactic.Util
_private.Lean.Meta.Tactic.Util.0.Lean.Meta.saturate.go : (Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) →
  Lean.MVarId → StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
-- Mathlib.Logic.Equiv.Set
/-- If `s : Set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`.

See also `Equiv.sumCompl`.  -/
Equiv.Set.sumCompl : {α : Type u_3} → (s : Set α) → [DecidablePred fun x => x ∈ s] → ↑s ⊕ ↑sᶜ ≃ α
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.map.eq_1 : ∀ (p : ENNReal) {V : Type u_4} {V' : Type u_5} (f : V → V') (x : WithLp p V),
  WithLp.map p f x = WithLp.toLp p (f x.ofLp)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE?_eq_getEntryLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α},
  Std.DTreeMap.Internal.Impl.getKeyLE? k t = Option.map (fun x => x.fst) (Std.DTreeMap.Internal.Impl.getEntryLE? k t)
-- Init.Data.List.Find
List.findIdx?_eq_some_iff_getElem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ},
  List.findIdx? p xs = some i ↔ ∃ (h : i < xs.length), p xs[i] = true ∧ ∀ (j : ℕ) (hji : j < i), ¬p xs[j] = true
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_mul : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  (f g : AddMonoidAlgebra M ι), (f * g).toDirectSum = f.toDirectSum * g.toDirectSum
-- Lean.Parser.Term
Lean.Parser.Term.defaultOrOfNonempty.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Message
Lean.MessageData.hasSyntheticSorry : Lean.MessageData → Bool
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.exists_app_map_eq_zero_of_isLimit : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {i : I} {U : (D.obj i).Opens},
  IsCompact ↑U →
    ∀ (s : ↑((D.obj i).presheaf.obj (Opposite.op U))),
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (c.π.app i) U)) s = 0 →
        ∃ j f, (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (D.map f) U)) s = 0
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.zero : Nat.Primrec fun x => 0
-- Init.Data.Fin.Basic
/-- Division of bounded numbers, usually invoked via the `/` operator.

The resulting value is that computed by the `/` operator on `Nat`. In particular, the result of
division by `0` is `0`.

Examples:
 * `(5 : Fin 10) / (2 : Fin 10) = (2 : Fin 10)`
 * `(5 : Fin 10) / (0 : Fin 10) = (0 : Fin 10)`
 * `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
 -/
Fin.div : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.Analysis.Normed.Group.Indicator
indicator_norm_le_norm_self : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α),
  s.indicator (fun a => ‖f a‖) a ≤ ‖f a‖
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.length_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id], (it.attachWith P hP).length = it.length
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapAlgEquiv_refl : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] {A₁ : Type u_2} [inst_1 : CommSemiring A₁]
  [inst_2 : Algebra R A₁], MvPolynomial.mapAlgEquiv σ AlgEquiv.refl = AlgEquiv.refl
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_join : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)), f.join.weights = f.weights.sum fun d r => r • d.weights
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.Λ'.write.injEq : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ) (a_1 : Turing.TM1.Stmt Γ Λ σ) (a_2 : Γ)
  (a_3 : Turing.TM1.Stmt Γ Λ σ), (Turing.TM1to1.Λ'.write a a_1 = Turing.TM1to1.Λ'.write a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Data.Set.Image
Set.instNonemptyRange : ∀ {α : Type u_1} {ι : Sort u_4} [Nonempty ι] (f : ι → α), Nonempty ↑(Set.range f)
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Localizing w.r.t. `M ⊆ R` and then w.r.t. `N ⊆ S = M⁻¹R` is equal to the localization of `R`
w.r.t. this submonoid. See `localization_localization_isLocalization`.
 -/
IsLocalization.localizationLocalizationSubmodule : {R : Type u_1} →
  [inst : CommSemiring R] →
    Submonoid R → {S : Type u_2} → [inst_1 : CommSemiring S] → [Algebra R S] → Submonoid S → Submonoid R
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the unit of an adjunction is an isomorphism, then its inverse on the image of L is given
by L whiskered with the counit.  -/
CategoryTheory.Adjunction.inv_map_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X : C}
  [inst_2 : CategoryTheory.IsIso (h.unit.app X)], CategoryTheory.inv (L.map (h.unit.app X)) = h.counit.app (L.obj X)
-- Mathlib.Data.QPF.Multivariate.Constructions.Comp
MvQPF.Comp.mk_get : ∀ {n m : ℕ} {F : TypeVec.{u} n → Type u_1} {G : Fin2 n → TypeVec.{u} m → Type u} {α : TypeVec.{u} m}
  (x : MvQPF.Comp F G α), MvQPF.Comp.mk x.get = x
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- Given a diagram `{ Dᵢ }_{i ∈ I}` of schemes and an open `U ⊆ Dᵢ`,
the preimage of `U ⊆ Dᵢ` under the map `lim Dᵢ ⟶ Dᵢ` is the limit of `{ Dⱼᵢ⁻¹ U }_{j ≤ i}`.  -/
AlgebraicGeometry.isLimitOpensCone : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
      (c : CategoryTheory.Limits.Cone D) →
        CategoryTheory.Limits.IsLimit c →
          [CategoryTheory.IsCofiltered I] →
            (i : I) → (U : (D.obj i).Opens) → CategoryTheory.Limits.IsLimit (AlgebraicGeometry.opensCone D c i U)
-- Lean.Data.PersistentArray
Lean.PersistentArray.set : {α : Type u} → Lean.PersistentArray α → ℕ → α → Lean.PersistentArray α
-- Mathlib.Order.Partition.Equipartition
Nat.divModEquiv.congr_simp : ∀ (n : ℕ) [inst : NeZero n], n.divModEquiv = n.divModEquiv
-- Init.Data.SInt.Lemmas
ISize.toInt_neg_ofNat_of_le : ∀ {n : ℕ}, n ≤ 2 ^ 31 → (-ISize.ofNat n).toInt = -↑n
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasStrictFDerivAt_iff_isLittleO`. -/
HasStrictFDerivAt.of_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  ((fun p => f p.1 - f p.2 - f' (p.1 - p.2)) =o[nhds (x, x)] fun p => p.1 - p.2) → HasStrictFDerivAt f f' x
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.coverMincard_image_le : ∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) (V : SetRel Y Y) (n : ℕ),
      Dynamics.coverMincard T (φ '' F) V n ≤ Dynamics.coverMincard S F (Prod.map φ φ ⁻¹' V) n
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.IsRoot.map : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] {f : R →+* S} {x : R} {p : Polynomial R},
  p.IsRoot x → (Polynomial.map f p).IsRoot (f x)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.const_smul : ∀ {𝕜 : 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'] {s : Set M} {z : M} {f : M → E'}, MDiffAt[s] f z → ∀ (a : 𝕜), MDiffAt[s] (a • f) z
-- Batteries.Recycling.MonadSatisfying.Array
Array.size_modifyM : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (as : Array α) (i : ℕ) (f : α → m α),
  SatisfiesM (fun x => x.size = as.size) (as.modifyM i f)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- A class of morphisms `W : MorphismProperty C` is stable under transfinite composition
if it is multiplicative and stable under transfinite composition of any shape
(in a certain universe).  -/
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Also see `LinearIndependent.pair_iff` for the version over arbitrary rings.  -/
LinearIndependent.pair_iff' : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x y : V},
  x ≠ 0 → (LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_trans_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Semiring C]
  [inst_6 : TopologicalSpace C] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra R C] (e₁ : B ≃A[R] A)
  (e₂ : C ≃A[R] B) (a : A), (e₂.trans e₁).symm a = e₂.symm (e₁.symm a)
-- Init.Data.Ord.Basic
/-- Version of `Ordering.then'` for proof by reflection.  -/
Ordering.then' : Ordering → Ordering → Ordering
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.uniqueFromBot : {X : Type u} → [inst : Preorder X] → [inst_1 : OrderBot X] → {x : X} → Unique (⊥ ⟶ x)
-- Mathlib.Order.Basic
/-- **Alias** of `ge_trans`. -/
le_trans' : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, b ≤ a → c ≤ b → c ≤ a