mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Subtracting two `affineCombination`s.  -/
Finset.affineCombination_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ w₂ : ι → k) (p : ι → P),
  (Finset.affineCombination k s p) w₁ -ᵥ (Finset.affineCombination k s p) w₂ = (s.weightedVSub p) (w₁ - w₂)
-- Mathlib.Topology.Algebra.Module.LocallyConvex
locallyConvexSpace_iff : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E],
  LocallyConvexSpace 𝕜 E ↔ ∀ (x : E), (nhds x).HasBasis (fun s => s ∈ nhds x ∧ Convex 𝕜 s) id
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.IsNontrivial.eq_1 : ∀ {R : Type u_5} [inst : Semiring R] {S : Type u_6} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (v : AbsoluteValue R S), v.IsNontrivial = ∃ x, x ≠ 0 ∧ v x ≠ 1
-- Mathlib.InformationTheory.Hamming
hammingNorm_comp : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {γ : ι → Type u_4}
  [inst_2 : (i : ι) → DecidableEq (γ i)] [inst_3 : (i : ι) → Zero (β i)] [inst_4 : (i : ι) → Zero (γ i)]
  (f : (i : ι) → γ i → β i) {x : (i : ι) → γ i},
  (∀ (i : ι), Function.Injective (f i)) → (∀ (i : ι), f i 0 = 0) → (hammingNorm fun i => f i (x i)) = hammingNorm x
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_C_X : ∀ {R : Type u_1} [inst : CommSemiring R],
  (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C Polynomial.X) = MvPolynomial.X 0
-- Batteries.Lean.Meta.DiscrTree
/-- Compare two `Key`s. The ordering is total but otherwise arbitrary. (It uses
`Name.quickCmp` internally.)
 -/
Lean.Meta.DiscrTree.Key.cmp : Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → Ordering
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.map_id_equiv : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp},
  (Std.TreeMap.map (fun x v => v) t).Equiv t
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
IsCyclotomicExtension.Rat.isTotallyComplex : ∀ {n : ℕ} [NeZero n] (K : Type u) [inst : Field K] [inst_1 : CharZero K] [IsCyclotomicExtension {n} ℚ K],
  2 < n → NumberField.IsTotallyComplex K
-- Lean.Meta.Eqns
/-- Environment extension that stores the values of `eqnAffectingOptions` at definition time,
keyed by declaration name. Only populated when at least one option has a non-default value.
Stores an association list of (option name, value) pairs for options that differ from defaults.  -/
Lean.Meta.eqnOptionsExt : Lean.MapDeclarationExtension (Array (Lean.Name × Lean.DataValue))
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- the canonical element `⟨0, 1⟩` in a quadratic algebra `QuadraticAlgebra R a b`.  -/
QuadraticAlgebra.termω : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_lt_of_one_lt' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, b < c → 1 < a → b < c * a
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to a `Minute.Offset`.
 -/
Std.Time.Nanosecond.Offset.toMinutes : Std.Time.Nanosecond.Offset → Std.Time.Minute.Offset
-- Mathlib.Tactic.Simps.Basic
/-- Auxiliary function for `getRawProjections`.
Find custom projections, automatically found by simps.
These come from `DFunLike` and `SetLike` instances.  -/
Simps.findAutomaticProjections : Lean.Name → Array Simps.ParsedProjectionData → Lean.CoreM (Array Simps.ParsedProjectionData)
-- Batteries.Data.List.Perm
List.Perm.idxBij_surjective : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys), Function.Surjective h.idxBij
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_add_single_eq_single_add_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {k l m n : ι} {u v : M},
  u ≠ 0 →
    v ≠ 0 →
      ((((fun₀ | k => u) + fun₀ | l => v) = (fun₀ | m => u) + fun₀ | n => v) ↔
        k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.id_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.ContainsIdentities]
  (X : C), W (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
additive subgroups of `G`.  -/
AddSubgroupClass : (S : Type u_3) → (G : outParam (Type u_4)) → [SubNegMonoid G] → [SetLike S G] → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} (f : G → G'),
  SkewMonoidAlgebra.mapDomain f =
    { toFun := fun v => v.sum fun a => SkewMonoidAlgebra.single (f a), map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RepresentationTheory.Coinvariants
Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G) [inst_2 : S.Normal]
  {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
  (Rep.Hom.hom ((Rep.quotientToCoinvariantsFunctor k S).map f)).toLinearMap =
    Representation.Coinvariants.map (MonoidHom.comp X.ρ S.subtype) (MonoidHom.comp Y.ρ S.subtype)
      (Rep.Hom.hom (Rep.resMap S.subtype f))
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A convex combination of a single point is that point.  -/
Convexity.ConvexSpace.sConvexComb_single : ∀ {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R}
  [self : Convexity.ConvexSpace R M] (x : M), Convexity.sConvexComb (Convexity.StdSimplex.single x) = x
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Applying a continuous linear map commutes with taking an (infinite) sum.  -/
ContinuousLinearEquiv.hasSum' : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂} {σ' : R₂ →+* R}
  [inst_8 : RingHomInvPair σ σ'] [inst_9 : RingHomInvPair σ' σ] {L : SummationFilter ι} {f : ι → M} (e : M ≃SL[σ] M₂)
  {x : M}, HasSum (fun b => e (f b)) (e x) L ↔ HasSum f x L
-- Mathlib.Algebra.Ring.Pi
/-- `Function.const` as a `NonUnitalRingHom`.  -/
Pi.constNonUnitalRingHom : (α : Type u_1) → (β : Type u_2) → [inst : NonUnitalNonAssocSemiring β] → β →ₙ+* α → β
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.linear_injective_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2),
  Function.Injective ⇑f.linear ↔ Function.Injective ⇑f
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.run : {α : Type} → Lean.Meta.Simp.Arith.Int.ToLinear.M α → Lean.MetaM (α × Array Lean.Expr)
-- Batteries.Data.MLList.Heartbeats
/-- Take an initial segment of a monadic lazy list,
stopping when there is less than `percent` of the remaining allowed heartbeats.

If `getMaxHeartbeats` returns `0`, then this passes through the original list unmodified.

The `initial` heartbeat counter is recorded when the first element of the list is requested.
Then each time an element is requested from the wrapped list the heartbeat counter is checked, and
if `current * 100 / initial < percent` then that element is returned,
but no further elements.
 -/
MLList.whileAtLeastHeartbeatsPercent : {m : Type → Type} → {α : Type} → [Monad m] → [MonadLiftT Lean.CoreM m] → MLList m α → optParam ℕ 10 → MLList m α
-- Init.Control.Basic
/-- Lifts a monadic action that returns a state and a value in the inner monad to an action in the
outer monad. The extra state information is used to restore the results of effects from the
reverse lift passed to `liftWith`'s parameter.
 -/
MonadControlT.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControlT m n] → {α : Type u} → stM m n α → n α
-- Batteries.Data.Stream
Std.Stream.fst_takeTR : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (n : ℕ),
  (Std.Stream.takeTR s n).1 = (Std.Stream.take s n).1
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The constant factor occurring in the conclusion of `eLpNorm_le_eLpNorm_fderiv_of_eq_inner`.
It only depends on `E`, `μ` and `p`.  -/
MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst : {E : Type u_4} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] →
        [BorelSpace E] → [FiniteDimensional ℝ E] → (μ : MeasureTheory.Measure E) → [μ.IsAddHaarMeasure] → ℝ → NNReal
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.comm : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}, m₁.Equiv m₂ ↔ m₂.Equiv m₁
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality_obj_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.Cocone.functoriality F G).obj A).pt = G.obj A.pt
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {km : α} {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to left-scalar-multiply it by a constant (scalar).
If relevant, also take into account the degree of positivity which can be proved of the constant:
strict or non-strict.  -/
Mathlib.Ineq.smulRelConstData : Mathlib.Ineq.WithStrictness → Lean.Name
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.insert c =
    match c.isUnit with
    | none =>
      { clauses := clauses.push (some c), rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }
    | some (l, true) =>
      { clauses := clauses.push (some c), rupUnits := rupUnits, ratUnits := ratUnits,
        assignments := assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
    | some (l, false) =>
      { clauses := clauses.push (some c), rupUnits := rupUnits, ratUnits := ratUnits,
        assignments := assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }
-- Mathlib.Data.Set.Lattice
Set.iUnion_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {s : ι → Set α} {t : ι₂ → Set α},
  (∀ (i : ι), ∃ j, s i ⊆ t j) → ⋃ i, s i ⊆ ⋃ i, t i
-- Init.Core
Subtype.instLawfulBEq : ∀ {α : Type u} {p : α → Prop} [inst : BEq α] [LawfulBEq α], LawfulBEq { x // p x }
-- Mathlib.Data.PNat.Notation
instDecidableEqPNat : DecidableEq ℕ+
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ) (i : σ),
  (MvPolynomial.expand p) (MvPolynomial.X i) = MvPolynomial.X i ^ p
-- Mathlib.Algebra.Ring.Opposite
NonUnitalRingHom.op_symm_apply_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) (a : R), (NonUnitalRingHom.op.symm f) a = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y : C}
  (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).snd =
    (CategoryTheory.ConcreteCategory.hom
        (F.map
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp p.fst f).op
            (CategoryTheory.eqToHom ⋯))))
      p.snd
-- Init.Data.Sum.Lemmas
Sum.inl_ne_inr : ∀ {α : Type u_1} {a : α} {β : Type u_2} {b : β}, Sum.inl a ≠ Sum.inr b
-- Mathlib.RingTheory.Polynomial.Pochhammer
descPochhammer_eval_eq_ascPochhammer : ∀ (R : Type u) [inst : Ring R] (r : R) (n : ℕ),
  Polynomial.eval r (descPochhammer R n) = Polynomial.eval (r - ↑n + 1) (ascPochhammer R n)
-- Lean.Message
/-- An exception was thrown during the traced action (💥️, `bombEmoji`).  -/
Lean.TraceResult.error : Lean.TraceResult
-- Mathlib.RingTheory.Valuation.ExtendToLocalization
/-- We can extend a valuation `v` on a ring to a localization at a submonoid of
the complement of `v.supp`.  -/
Valuation.extendToLocalization : {A : Type u_1} →
  [inst : CommRing A] →
    {Γ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ] →
        (v : Valuation A Γ) →
          {S : Submonoid A} →
            S ≤ v.supp.primeCompl →
              (B : Type u_3) → [inst_2 : CommRing B] → [inst_3 : Algebra A B] → [IsLocalization S B] → Valuation B Γ
-- Mathlib.Algebra.Quaternion
Quaternion.imK_intCast : ∀ {R : Type u_3} [inst : CommRing R] (z : ℤ), (↑z).imK = 0
-- Mathlib.CategoryTheory.Linear.Yoneda
/-- The Yoneda embedding for `R`-linear categories `C`,
sending an object `Y : Cᵒᵖ` to the `ModuleCat R`-valued copresheaf on `C`,
with value on `X : C` given by `ModuleCat.of R (unop Y ⟶ X)`.  -/
CategoryTheory.linearCoyoneda : (R : Type w) →
  [inst : Ring R] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [CategoryTheory.Linear R C] → CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (ModuleCat R))
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.branch : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} → (Γ → σ → Bool) → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Γ Λ σ → Turing.TM1.Stmt Γ Λ σ
-- Mathlib.Algebra.Ring.Associated
Associated.neg_right : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : HasDistribNeg M] {a b : M}, Associated a b → Associated a (-b)
-- Init.Data.UInt.IntToBitVec
UInt32.toBitVec32_toUSize : ∀ (n : UInt32) (h : System.Platform.numBits = 32), n.toUSize.toBitVec32 h = n.toBitVec
-- Mathlib.Data.Set.SymmDiff
Set.symmDiff_def : ∀ {α : Type u} (s t : Set α), symmDiff s t = s \ t ∪ t \ s
-- Mathlib.Order.Ideal
Order.Cofinal.le_above : ∀ {P : Type u_1} [inst : Preorder P] (D : Order.Cofinal P) (x : P), x ≤ D.above x
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `f` is a polynomial over `A`, `g` and `h` are power series over `A`,
then `PowerSeries.IsWeierstrassFactorizationAt g f h I` is a `Prop` which asserts that `f` is
distinguished at `I`, `h` is a unit, such that `g = f * h`.  -/
PowerSeries.IsWeierstrassFactorizationAt : {A : Type u_1} → [inst : CommRing A] → PowerSeries A → Polynomial A → PowerSeries A → Ideal A → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.toArrow_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C),
  (CategoryTheory.SimplicialObject.Augmented.toArrow.obj X).hom = X.hom.app (Opposite.op { len := 0 })
-- Lean.SubExpr
/-- A location within a goal.  -/
Lean.SubExpr.GoalLocation : Type
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.instAddCommMonoid : {α : Type u_1} → {f : α → α} → AddCommMonoid (IterateAddAct f)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_eq_zero_iff : ∀ {R : Type u_1} {a b : R} [inst : Zero R] {r : R}, QuadraticAlgebra.C r = 0 ↔ r = 0
-- Lean.Meta.Basic
Lean.Meta.instInhabitedProjReductionKind : Inhabited Lean.Meta.ProjReductionKind
-- Mathlib.Analysis.Analytic.ConvergenceRadius
constFormalMultilinearSeries.eq_2 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type u_2) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : ContinuousConstSMul 𝕜 E] [inst_4 : IsTopologicalAddGroup E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : ContinuousConstSMul 𝕜 F] (c : F) (x : ℕ), (x = 0 → False) → constFormalMultilinearSeries 𝕜 E c x = 0
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.Finsupp.sampleableExt : {α : Type u} →
  {β : Type v} →
    [DecidableEq α] →
      [inst : Zero β] →
        [DecidableEq β] →
          [Plausible.SampleableExt α] → [Plausible.SampleableExt β] → [Repr α] → Plausible.SampleableExt (α →₀ β)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- Let `s : Set 𝕜` be a compact set and consider pairs `(f, a) : (𝕜 → 𝕜) × A` where `f` is
continuous on `s` and `spectrum 𝕜 a ⊆ s` and `a` satisfies the predicate `p a` for the continuous
functional calculus.

Then `cfc` is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on `s`.  -/
continuousOn_cfc_setProd : ∀ {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜},
  IsCompact s →
    ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
      ({f | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a | p a ∧ spectrum 𝕜 a ⊆ s})
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.instFaithfulSMul : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p], FaithfulSMul (A ⧸ p) (B ⧸ P)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instPartialOrder : {k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → PartialOrder (FiniteGaloisIntermediateField k K)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_append_toArray_roc : ∀ {l m n : ℤ}, l ≤ m → m ≤ n → (l<...=m).toArray ++ (m<...=n).toArray = (l<...=n).toArray
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The `edgeSet` of the graph as a `Finset`.  -/
SimpleGraph.edgeFinset : {V : Type u_1} → (G : SimpleGraph V) → [Fintype ↑G.edgeSet] → Finset (Sym2 V)
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Logic.Encodable.Basic
Encodable.encodeSigma.eq_1 : ∀ {α : Type u_1} {γ : α → Type u_3} [inst : Encodable α] [inst_1 : (a : α) → Encodable (γ a)] (a : α) (b : γ a),
  Encodable.encodeSigma ⟨a, b⟩ = Nat.pair (Encodable.encode a) (Encodable.encode b)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- For any `n ≠ 0`, we have the identity
`(stirlingSeq n)^4 / (stirlingSeq (2*n))^2 * (n / (2 * n + 1)) = W n`, where `W n` is the
`n`-th partial product of Wallis' formula for `π / 2`.  -/
Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq : ∀ (n : ℕ), n ≠ 0 → Stirling.stirlingSeq n ^ 4 / Stirling.stirlingSeq (2 * n) ^ 2 * (↑n / (2 * ↑n + 1)) = Real.Wallis.W n
-- Mathlib.Order.ScottContinuity
ScottContinuous.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], ScottContinuous Prod.snd
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_faithful : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.Faithful
-- Mathlib.RingTheory.Artinian.Defs
/-- `IsArtinian R M` is the proposition that `M` is an Artinian `R`-module,
implemented as the well-foundedness of submodule inclusion.  -/
IsArtinian : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.IsLimit.mk_lift : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (t : CategoryTheory.Limits.Fan f)
  (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j)
      CategoryTheory.Limits.Fan.IsLimit.mk._auto_1)
  (uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt),
        (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s)
      CategoryTheory.Limits.Fan.IsLimit.mk._auto_3)
  (s : CategoryTheory.Limits.Fan f), (CategoryTheory.Limits.Fan.IsLimit.mk t lift fac uniq).lift s = lift s
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨯ Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ X'))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g)
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g'))
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g g') h
-- Mathlib.Algebra.Quaternion
Cardinal.mk_univ_quaternion_of_infinite : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] [Infinite R], Cardinal.mk ↑Set.univ = Cardinal.mk R
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.proj.eq_1 : ∀ {P : ProfiniteAddGrp.{u}} (U : OpenNormalAddSubgroup ↑P.toProfinite.toTop),
  ProfiniteAddGrp.proj U =
    ProfiniteAddGrp.ofHom { toFun := QuotientAddGroup.mk, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.Order.Filter.Defs
Filter.instBind : Bind Filter
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R),
  f.Splits = (f ∈ Submonoid.closure ({x | ∃ a, Polynomial.C a = x} ∪ {x | ∃ a, Polynomial.X + Polynomial.C a = x}))
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biprod.lift_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {T : C} {f : T ⟶ X} {g : T ⟶ Y},
  CategoryTheory.Limits.biprod.lift f g =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl +
      CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr
-- Mathlib.GroupTheory.GroupAction.Pointwise
image_vadd_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β]
  [inst_2 : FunLike F α β] [AddActionHomClass F M α β] (f : F) (c : M) (s : Set α), ⇑f '' (c +ᵥ s) = c +ᵥ ⇑f '' s
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.run_bind.match_1.eq_1 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (x : α) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok x with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_1 x