mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_6.congr_eq_1 : ∀ {n : ℕ} (motive : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → Sort u_1)
  (acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)) (h_1 : Unit → motive none)
  (h_2 : (map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool) → motive (some map)),
  acc = none →
    (match acc with
      | none => h_1 ()
      | some map => h_2 map) ≍
      h_1 ()
-- Mathlib.Algebra.Order.Interval.Basic
instNegNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α],
  instNegNonemptyInterval = { neg := fun s => { fst := -s.toProd.2, snd := -s.toProd.1, fst_le_snd := ⋯ } }
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.forget_obj : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) (P : CategoryTheory.MorphismProperty T)
  (Q : CategoryTheory.MorphismProperty A) (W : CategoryTheory.MorphismProperty B) [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  (CategoryTheory.MorphismProperty.Comma.forget L R P Q W).obj X = X.toComma
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_lt_prod' : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α]
  [MulLeftStrictMono α] {s : Multiset ι} {f g : ι → α},
  (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → (Multiset.map f s).prod < (Multiset.map g s).prod
-- Mathlib.Data.Set.Restrict
Set.domRestrict_def : ∀ {α : Type u_1} {π : α → Type u_6} (s : Set α), s.domRestrict = fun f x => f ↑x
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- `nthRoots n` as a `Finset` is equal to the union of `primitiveRoots i R` for `i ∣ n`.  -/
_private.Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots.0.IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots' : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] {n : ℕ} [NeZero n],
  Polynomial.nthRootsFinset n 1 = n.divisors.biUnion fun i => primitiveRoots i R
-- Mathlib.Analysis.Convex.Topology
Convex.sdiff_singleton_eventually_mem_nhds : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, Convex 𝕜 s → ∀ (a : 𝕜), ∀ᶠ (x : 𝕜) in nhdsWithin a (s \ {a}), s \ {a} ∈ nhds x
-- Mathlib.Topology.Compactification.StoneCech
/-- Basis for the topology on `Ultrafilter α`.  -/
ultrafilterBasis : (α : Type u) → Set (Set (Ultrafilter α))
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- Gluing `Iic a` and `Ioi a` into `ℕ`, version as a measurable equivalence
on dependent functions.  -/
MeasurableEquiv.IicProdIoi : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [DecidableLE ι] →
      {X : ι → Type u_2} →
        [inst_2 : LocallyFiniteOrderBot ι] →
          [inst_3 : (i : ι) → MeasurableSpace (X i)] →
            (a : ι) → ((i : ↥(Finset.Iic a)) → X ↑i) × ((i : ↑(Set.Ioi a)) → X ↑i) ≃ᵐ ((n : ι) → X n)
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
_private.Mathlib.Analysis.InnerProductSpace.Rayleigh.0.ContinuousLinearMap.rayleighQuotient_le_of_mem_resolventSet : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) (t : ℝ),
  0 < t →
    (algebraMap ℝ 𝕜) t ∈ resolventSet 𝕜 T → ∃ c > 0, ∀ (x : E), T.rayleighQuotient x ≤ (t ^ 2 + ‖T‖ ^ 2) / (2 * t) - c
-- Aesop.Rule
Aesop.NormSimpRule.name : Aesop.NormSimpRule → Aesop.RuleName
-- Mathlib.Topology.Order.CountableSeparating
HasCountableSeparatingOn.range_Iio : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : LinearOrder X] [OrderTopology X] [SecondCountableTopology X]
  {s : Set X}, HasCountableSeparatingOn X (fun x => x ∈ Set.range Set.Iio) s
-- Mathlib.Data.Finset.Fold
Finset.fold_hom : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {f : α → β} {b : β} {s : Finset α} {op' : γ → γ → γ} [inst : Std.Commutative op'] [inst_1 : Std.Associative op']
  {m : β → γ},
  (∀ (x y : β), m (op x y) = op' (m x) (m y)) → Finset.fold op' (m b) (fun x => m (f x)) s = m (Finset.fold op b f s)
-- Lean.Data.Position
/-- The last line should always be `positions.size - 1`.  -/
Lean.FileMap.getLastLine : Lean.FileMap → ℕ
-- Mathlib.Data.Int.Bitwise
Int.bit_val : ∀ (b : Bool) (n : ℤ), Int.bit b n = 2 * n + bif b then 1 else 0
-- Mathlib.Logic.Basic
forall_and_index : ∀ {p q : Prop} {r : p ∧ q → Prop}, (∀ (h : p ∧ q), r h) ↔ ∀ (hp : p) (hq : q), r ⋯
-- Init.Data.Vector.Attach
Vector.attach_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m},
  (xs ++ ys).attach =
    Vector.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      Vector.map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        ys.attach
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a right invariant measure under left multiplication is right invariant.  -/
MeasureTheory.isMulRightInvariant_map_mul_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G}
  [μ.IsMulRightInvariant] (g : G), (MeasureTheory.Measure.map (fun x => g * x) μ).IsMulRightInvariant
-- Mathlib.ModelTheory.Order
/-- Joins two terms `t₁, t₂` in a formula representing `t₁ < t₂`.  -/
FirstOrder.Language.Term.lt : {L : FirstOrder.Language} →
  {α : Type w} → {n : ℕ} → [L.IsOrdered] → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, m.isEmpty = true → m.getD a fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v},
  p.IsPath → w ∉ p.support → ∀ (h : G.Adj v w), (p.concat h).IsPath
-- Lean.Data.NameMap.Basic
Lean.NameMap.insert : {α : Type} → Lean.NameMap α → Lean.Name → α → Std.TreeMap Lean.Name α Lean.Name.quickCmp
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.degree_smul_of_smul_regular : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] {k : S} (p : Polynomial R),
  IsSMulRegular R k → (k • p).degree = p.degree
-- Mathlib.Topology.Separation.Basic
/-- In an R₀ space, relatively compact sets form a bornology.
Its cobounded filter is `Filter.coclosedCompact`.
See also `Bornology.inCompact` the bornology of sets contained in a compact set.  -/
Bornology.relativelyCompact : (X : Type u_1) → [inst : TopologicalSpace X] → [R0Space X] → Bornology X
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.forget_reflects_isos : (CategoryTheory.forget MonCat).ReflectsIsomorphisms
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_localization : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  IsLocalization.AtPrime (↥(A.ofPrime P)) P
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.coconeOfDiagramTerminal_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {X : J} (tX : CategoryTheory.Limits.IsTerminal X) (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.coconeOfDiagramTerminal tX F).pt = F.obj X
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain : ∀ {G : Type u_6} {α : Type u_7} {inst : One G} {inst_1 : SMul G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasFundamentalDomain._auto_1}
  [self : MeasureTheory.HasFundamentalDomain G α ν], ∃ s, MeasureTheory.IsFundamentalDomain G s ν
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_add_im_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K),
  (algebraMap ℝ K) (RCLike.re z) + (algebraMap ℝ K) (RCLike.im z) * RCLike.I = z
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_bot : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] [inst_4 : T1Space M], ↑⊥ = {0}
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.Sat.eq_1 : ∀ {α : Type} (a : α → Bool) (x : Std.Tactic.BVDecide.BoolExpr α),
  Std.Tactic.BVDecide.BoolExpr.Sat a x = (Std.Tactic.BVDecide.BoolExpr.eval a x = true)
-- Mathlib.Order.Category.Semilat
SemilatSupCat.isOrderBot : (self : SemilatSupCat) → OrderBot self.X
-- Mathlib.Algebra.Star.Basic
/-- `star` commutes with addition  -/
StarRing.star_add : ∀ {R : Type u} {inst : NonUnitalNonAssocSemiring R} [self : StarRing R] (r s : R), star (r + s) = star r + star s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instPow.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : Pow G M],
  Filter.Germ.instPow = { pow := fun f n => Filter.Germ.map (fun x => x ^ n) f }
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.of_isIntegrallyClosed_of_isIntegrallyClosedIn : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain S]
  [FaithfulSMul R S] [IsIntegrallyClosed S] [IsIntegrallyClosedIn R S], IsIntegrallyClosed R
-- Mathlib.Data.DFinsupp.Defs
/-- Replace the value of a `Π₀ i, β i` at a given point `i : ι` by a given value `b : β i`.
If `b = 0`, this amounts to removing `i` from the support.
Otherwise, `i` is added to it.

This is the (dependent) finitely-supported version of `Function.update`.  -/
DFinsupp.update : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → [DecidableEq ι] → (Π₀ (i : ι), β i) → (i : ι) → β i → Π₀ (i : ι), β i
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isSup.sizeOf_spec : ∀ (lhs rhs res : ℕ),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.isSup lhs rhs res) = 1 + sizeOf lhs + sizeOf rhs + sizeOf res
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.leftToRight.congr_simp : ∀ {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}
  {H : CategoryTheory.Functor C D} (t t_1 : CategoryTheory.Adjunction.Triple F G H),
  t = t_1 → ∀ [inst_2 : F.Full] [inst_3 : F.Faithful], t.leftToRight = t_1.leftToRight
-- Std.Data.DTreeMap.Raw.DecidableEquiv
Std.DTreeMap.Raw.instDecidableEquiv : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          [inst : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] → {t₁ t₂ : Std.DTreeMap.Raw α β cmp} → t₁.WF → t₂.WF → Decidable (t₁.Equiv t₂)
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.neg : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : SubtractionMonoid β] [ContinuousNeg β]
  {l : Filter α} {f : α → β}, l.ZeroAtFilter f → l.ZeroAtFilter (-f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- The square
```
  X --inl--> X ⊞ Y
  |            |
  0           snd
  |            |
  v            v
  0 ---0-----> Y
```
is a pushout square.
 -/
CategoryTheory.IsPushout.inl_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
-- Init.Data.Rat.Lemmas
Rat.le_iff_lt_or_eq : ∀ {a b : ℚ}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
derivWithin_arctan : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * derivWithin f s x
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.cons : Mathlib.Deriving.Encodable.S✝ → Mathlib.Deriving.Encodable.S✝ → Mathlib.Deriving.Encodable.S✝
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_sub : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x y : WithLp p V), (x - y).ofLp = x.ofLp - y.ofLp
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.mk.injEq : ∀ (sysname release version machine sysname_1 release_1 version_1 machine_1 : String),
  ({ sysname := sysname, release := release, version := version, machine := machine } =
      { sysname := sysname_1, release := release_1, version := version_1, machine := machine_1 }) =
    (sysname = sysname_1 ∧ release = release_1 ∧ version = version_1 ∧ machine = machine_1)
-- Init.Data.Array.Lemmas
Array.map_eq_flatMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, Array.map f xs = Array.flatMap (fun x => #[f x]) xs
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.isOrdered.eq_2 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (l r : Option α),
  (∀ (l_1 r_1 : α), l = some l_1 → r = some r_1 → False) → RBTree.RBNode.isOrdered cmp RBTree.RBNode.nil l r = true
-- Mathlib.Algebra.Module.ZLattice.Covolume
/-- A version of `ZLattice.covolume.tendsto_card_le_div` for the `InnerProductSpace` case;
see the `Naming convention` section in the introduction.  -/
ZLattice.covolume.tendsto_card_le_div' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L]
  [IsZLattice ℝ L] [Nontrivial E] {X : Set E} {F : E → ℝ},
  (∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) →
    (∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Module.finrank ℝ E * F x) →
      Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1} →
        MeasurableSet {x | x ∈ X ∧ F x ≤ 1} →
          MeasureTheory.volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0 →
            Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop
              (nhds (MeasureTheory.volume.real {x | x ∈ X ∧ F x ≤ 1} / ZLattice.covolume L MeasureTheory.volume))
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mkConeMorphism_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t)
  (uniq : ∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.IsLimit.mkConeMorphism lift uniq).lift s = (lift s).hom
-- Std.Sync.Broadcast
Std.Broadcast.instHashableError : Hashable Std.Broadcast.Error
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.distribMulActionHom_ext : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : DistribMulAction R M] [inst_4 : DistribMulAction R N] {α : Type u_6} {f g : SkewMonoidAlgebra M α →+[R] N},
  (∀ (a : α) (m : M), f (SkewMonoidAlgebra.single a m) = g (SkewMonoidAlgebra.single a m)) → f = g
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instRightIdentityMeetTop : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l],
  Std.RightIdentity (fun x1 x2 => Lean.Order.meet x1 x2) Lean.Order.top
-- Mathlib.Topology.Inseparable
GeneralizingMap.stableUnderGeneralization_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  GeneralizingMap f → StableUnderGeneralization (Set.range f)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- A set is analytic if and only if it is the continuous image of some Polish space.  -/
MeasureTheory.analyticSet_iff_exists_polishSpace_range : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α},
  MeasureTheory.AnalyticSet s ↔ ∃ β h, ∃ (_ : PolishSpace β), ∃ f, Continuous f ∧ Set.range f = s
-- Std.Internal.UV.TCP
/-- Creates a new TCP socket.
 -/
Std.Internal.UV.TCP.Socket.new : IO Std.Internal.UV.TCP.Socket
-- Lean.Expr
Lean.Expr.fvar.sizeOf_spec : ∀ (fvarId : Lean.FVarId), sizeOf (Lean.Expr.fvar fvarId) = 1 + sizeOf fvarId
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.and_contra : ∀ {w : ℕ} (a : BitVec w), a &&& ~~~a = 0#w
-- Mathlib.RingTheory.Artinian.Ring
/-- Localizing an Artinian ring can only reduce the amount of elements.  -/
IsArtinianRing.localization_surjective : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [inst_2 : CommSemiring L]
  [inst_3 : Algebra R L] [IsLocalization S L], Function.Surjective ⇑(algebraMap R L)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.posRootForm_posForm_anisotropic : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [inst_8 : IsStrictOrderedRing S] [IsDomain R]
  [inst_10 : Algebra S R] [inst_11 : FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [inst_13 : Module S M]
  [inst_14 : IsScalarTower S R M] [inst_15 : Module S N] [IsScalarTower S R N],
  (LinearMap.BilinMap.toQuadraticMap (P.posRootForm S).posForm).Anisotropic
-- Lean.Message
Lean.MessageLog.reportedPlusUnreported : Lean.MessageLog → Lean.PersistentArray Lean.Message
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.ZeroAtFilter.boundedAtFilter : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddGroup β] {l : Filter α} {f : α → β},
  l.ZeroAtFilter f → l.BoundedAtFilter f
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- the factorisation through a mono has the universal property of the image.  -/
CategoryTheory.Limits.Types.isImage : {α β : Type u} → (f : α ⟶ β) → CategoryTheory.Limits.IsImage (CategoryTheory.Limits.Types.monoFactorisation f)
-- Mathlib.Condensed.Discrete.Module
CompHausLike.LocallyConstantModule.functor_obj_obj_map_hom_apply_apply : ∀ {P : TopCat → Prop} (R : Type (max u w)) [inst : Ring R] [inst_1 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_2 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : ModuleCat R) {X_1 Y : (CompHausLike P)ᵒᵖ} (f : X_1 ⟶ Y) (g : LocallyConstant ↑(Opposite.unop X_1).toTop ↑X)
  (a : ↑(Opposite.unop Y).toTop),
  ((ModuleCat.Hom.hom (((CompHausLike.LocallyConstantModule.functor R hs).obj X).obj.map f)) g) a =
    g ((TopCat.Hom.hom f.unop.hom) a)
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway`
if whenever `P` holds for `f` it also holds for the composition with
localization maps on the left and on the right.  -/
RingHom.StableUnderCompositionWithLocalizationAway : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_of_fintype : ∀ (R M : Type u) [inst : Semiring R] [inst_1 : Fintype M],
  Cardinal.mk (MonoidAlgebra R M) = Cardinal.mk R ^ Fintype.card M
-- Mathlib.Data.Multiset.Fold
Multiset.coe_fold_r : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α) (l : List α),
  Multiset.fold op b ↑l = List.foldr op b l
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
swap_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α], Function.swap dist = dist
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.bayesRisk.eq_1 : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  [inst : MeasurableSpace 𝓨] (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.bayesRisk ℓ P π = ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ProbabilityTheory.avgRisk ℓ P κ π
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N O : CategoryTheory.Mon C} (f : M.Hom N) (g : N.Hom O),
  CategoryTheory.Mon.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isMonHom_hom := ⋯ }
-- Init.Data.String.Decode
Char.utf8Size_eq : ∀ (c : Char), c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instDecidableEqOffset : DecidableEq Std.Time.Hour.Offset
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ : ∀ {p t x : ℝ}, 0 ≤ x → 0 < t → p.rpowIntegrand₁₂ t x = x * (p - 1).rpowIntegrand₀₁ t x
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` has open lower sections if, for every `b`, the set `{x | b ∈ f x}`
is open. Equivalently, whenever `b ∈ f x`, then `b ∈ f x'` for all `x'` sufficiently close to
`x`.  -/
HasOpenLowerSections : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → (α → Set β) → Prop
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfcHomSuperset_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : spectrum R a ⊆ s), (cfcHomSuperset ha hs) (ContinuousMap.restrict s (ContinuousMap.id R)) = a
-- Mathlib.LinearAlgebra.Dual.BaseChange
_private.Mathlib.LinearAlgebra.Dual.BaseChange.0.IsBaseChange.toDualBaseChangeAux_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] {A : Type u_4} [inst_5 : CommSemiring A] [inst_6 : Algebra R A]
  [inst_7 : Module A W] [inst_8 : IsScalarTower R A W] {j : V →ₗ[R] W} (ibc : IsBaseChange A j) (a : A)
  (f : Module.Dual R V) (v : V),
  ((IsBaseChange.toDualBaseChangeAux✝ ibc) (a ⊗ₜ[R] f)) (j v) = a * (algebraMap R A) (f v)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivAt.unique : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f₀' f₁' : F}
  {x v : E}, HasLineDerivAt 𝕜 f f₀' x v → HasLineDerivAt 𝕜 f f₁' x v → f₀' = f₁'
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
/-- The bijection `A.N ≃ B.N` on nondegenerate simplices not belonging
to a certain subcomplex that is induced by an isomorphism `X ≅ Y` of
simplicial sets which maps `A : X.Subcomplex` to `B : Y.Subcomplex`.  -/
SSet.Subcomplex.N.orderIsoOfIso : {X : SSet} → {A : X.Subcomplex} → {Y : SSet} → {B : Y.Subcomplex} → (e : X ≅ Y) → B.preimage e.hom = A → A.N ≃o B.N
-- Mathlib.Order.SuccPred.Archimedean
antitoneOn_of_succ_le : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → Order.succ a ∈ s → f (Order.succ a) ≤ f a) → AntitoneOn f s