mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Range
Vector.count_range : ∀ {a n : ℕ}, Vector.count a (Vector.range n) = if a < n then 1 else 0
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_iSup : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Sort u_5} (f : M →ₙ* N) (s : ι → Subsemigroup M),
  Subsemigroup.map f (iSup s) = ⨆ i, Subsemigroup.map f (s i)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A cotrident `t` on the parallel family `f : J → (X ⟶ Y)` consists of two morphisms
`t.ι.app zero : X ⟶ t.X` and `t.ι.app one : Y ⟶ t.X`. Of these, only the second one is
interesting, and we give it the shorter name `Cotrident.π t`.  -/
CategoryTheory.Limits.Cotrident.π : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          (t : CategoryTheory.Limits.Cotrident f) →
            (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶
              ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj
                CategoryTheory.Limits.WalkingParallelFamily.one
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_zero : Polynomial.mahlerMeasure 0 = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.StructuralAtom → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
/-- The `Y`-coordinate of `-(x, y)` for a nonsingular affine point `(x, y)` on a Weierstrass curve
`W`.

This depends on `W`, and has argument order: `x`, `y`.  -/
WeierstrassCurve.Affine.negY : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → R → R → R
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  ((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom =
    CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_comp_const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {f : 𝕜 → 𝕜},
  ContDiff 𝕜 (↑n) f → ∀ (c : 𝕜), (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.lipschitz_compContinuous : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] (g : C(δ, α)), LipschitzWith 1 fun f => f.compContinuous g
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instInhabited.eq_1 : AddMonCat.instInhabited = { default := AddMonCat.of PUnit.{u_1 + 1} }
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.mem_rootsOfUnity : ∀ {M : Type u_1} [inst : CommMonoid M] {ζ : Mˣ} {n : ℕ}, IsPrimitiveRoot ζ n → ζ ∈ rootsOfUnity n M
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.forget_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X},
  ((CategoryTheory.MonoOver.forget X).obj f).left = f.obj.left
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false) {h' : k ∈ m₁.union! m₂},
  (m₁.union! m₂).get k h' = m₁.get k ⋯
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
Measurable.map_measurableSpace_eq_borel : ∀ {X : Type u_3} {Y : Type u_4} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : TopologicalSpace Y]
  [T0Space Y] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace Y] [SecondCountableTopology Y] {f : X → Y},
  Measurable f → Function.Surjective f → MeasurableSpace.map f inst = borel Y
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_self_le_one : ∀ {a : ENNReal}, a / a ≤ 1
-- Mathlib.Order.UpperLower.Closure
LowerSet.lowerClosure_sup_sdiff : ∀ {α : Type u_1} [inst : Preorder α] {s : LowerSet α} {t : Set α},
  t ⊆ ↑s → (∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) → lowerClosure t ⊔ s.sdiff t = s
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.CoverPreserving.of_comp_of_isCocontinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  {L : CategoryTheory.GrothendieckTopology E} {F : CategoryTheory.Functor C D} (G : CategoryTheory.Functor D E),
  CategoryTheory.CoverPreserving J L (F.comp G) →
    ∀ [G.IsCocontinuous K L] [G.Full] [G.Faithful], CategoryTheory.CoverPreserving J K F
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unop2_op2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (Bicategory.Opposite.op2 η).unop2 = η
-- Mathlib.Order.WithBot
WithTop.lt_iff_exists_coe_btwn : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] [NoMaxOrder α] {a b : WithTop α}, b < a ↔ ∃ x, b < ↑x ∧ ↑x < a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AntitoneOn.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulLeftMono α], AntitoneOn f s → ∀ (a : α), AntitoneOn (fun x => a * f x) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R)
  [inst_1 : W.IsElliptic], (C • W).Δ' = C.u⁻¹ ^ 12 * W.Δ'
-- Lean.Util.ReplaceExpr
Lean.Expr.replaceImpl : (Lean.Expr → Option Lean.Expr) → Lean.Expr → Lean.Expr
-- Init.Data.String.Basic
String.Pos.cast_lt_cast_iff : ∀ {s t : String} {pos pos' : s.Pos} {h : s = t}, pos.cast h < pos'.cast h ↔ pos < pos'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.const : ∀ {α : Type u_1} {s : Stream'.Seq α}, Tactic.ComputeAsymptotics.Seq.FriendlyOperation fun x => s
-- Aesop.Builder.Cases
Aesop.CasesPattern.toIndexingMode : Aesop.CasesPattern → Lean.MetaM Aesop.IndexingMode
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_eraseₘaux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  Std.DHashMap.Internal.Raw.WFImp ↑m → m.containsₘ a = true → Std.DHashMap.Internal.Raw.WFImp ↑(m.eraseₘaux a)
-- Mathlib.Analysis.MellinTransform
MellinConvergent.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ},
  MellinConvergent f s →
    ∀ {𝕜 : Type u_2} [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E]
      [SMulCommClass ℂ 𝕜 E] (c : 𝕜), MellinConvergent (fun t => c • f t) s
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instInv.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ],
  MeasureTheory.AEEqFun.instInv = { inv := MeasureTheory.AEEqFun.comp Inv.inv ⋯ }
-- Mathlib.Topology.GDelta.Basic
/-- A set of second category (i.e. non-meagre) is nonempty.  -/
nonempty_of_not_isMeagre : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, ¬IsMeagre s → s.Nonempty
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddGroup : {α : Type u_1} → [AddGroup α] → AddGroup (Colex α)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
/-- The action of an elliptic orientation preserving matrix on `ℍ`
has a unique fixed point given by `fixedPt`.  -/
UpperHalfPlane.gl_smul_eq_self_iff_eq_fixedPt : ∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane},
  0 < (↑g).det → ∀ (hell : g.IsElliptic), g • z = z ↔ z = UpperHalfPlane.fixedPt g hell
-- Init.Data.List.Range
List.head?_range : ∀ {n : ℕ}, (List.range n).head? = if n = 0 then none else some 0
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.below.univ : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop},
  TopologicalSpace.GenerateOpen.below ⋯
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- **Alias** of the forward direction of `Bornology.isVonNBounded_neg`. -/
Bornology.IsVonNBounded.of_neg : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : TopologicalSpace E]
  [IsTopologicalAddGroup E] [inst_4 : DistribMulAction 𝕜 E] {s : Set E},
  Bornology.IsVonNBounded 𝕜 (-s) → Bornology.IsVonNBounded 𝕜 s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_insertC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.insertC k m p c) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denote ctx p
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_tmod_sub_self : ∀ {x m : ℤ}, m ∣ x.tmod m - x
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.State.simp : Lean.Meta.Grind.State → Lean.Meta.Simp.State
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.leftInverse_iff_rightInverse : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] [Module.Invertible R N] (f : M →ₗ[R] N)
  (g : N →ₗ[R] M), Function.LeftInverse ⇑f ⇑g ↔ Function.RightInverse ⇑f ⇑g
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.alter.match_1.eq_1 : ∀ {α : Type u_3} {β : α → Type u_1} (a : α) (motive : Option (β a) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (b : β a) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_not_bif : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w),
  ((bif d then a else b) == ~~~bif d then a else c) = bif d then a == ~~~a else b == ~~~c
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.lift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C}
  (f : X ⟶ Y), (P.lift F hF).map f = CategoryTheory.ObjectProperty.homMk (F.map f)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] (f : ι → β → α) [inst_1 : UniformSpace α],
  MultipliableUniformly f = Multipliable (⇑UniformFun.ofFun ∘ f)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_mul : ∀ (r s : ℝ), ↑(r * s) = ↑r * ↑s
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the signs of two oriented angles between nonzero vectors are negations of each other, the
oriented angles are negations of each other if and only if the unoriented angles are equal.  -/
Orientation.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {w x y z : V},
  w ≠ 0 →
    x ≠ 0 →
      y ≠ 0 →
        z ≠ 0 →
          (o.oangle w x).sign = -(o.oangle y z).sign →
            (InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = -o.oangle y z)
-- Mathlib.Algebra.Polynomial.Splits
/-- Pick a root of a polynomial that splits.  -/
Polynomial.rootOfSplits : {R : Type u_1} → [inst : CommRing R] → {f : Polynomial R} → f.Splits → f.degree ≠ 0 → R
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) `δ`-thickening `Metric.thickening δ E` of a subset `E` in a pseudo emetric space
consists of those points that are at distance less than `δ` from some point of `E`.  -/
Metric.thickening : {α : Type u} → [PseudoEMetricSpace α] → ℝ → Set α → Set α
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.w_obj : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) (a : 𝒳.obj), 𝒴.p.obj (F.obj a) = 𝒳.p.obj a
-- Lean.Parser.Basic
Lean.Parser.ParserState.keepLatest : Lean.Parser.ParserState → ℕ → Lean.Parser.ParserState
-- Std.Async.TCP
/-- Accepts an incoming connection.
 -/
Std.Async.TCP.Socket.Server.accept : Std.Async.TCP.Socket.Server → Std.Async.Async Std.Async.TCP.Socket.Client
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.add.inj : ∀ {k : ℤ} {v : Lean.Grind.Linarith.Var} {p : Lean.Grind.Linarith.Poly} {k_1 : ℤ} {v_1 : Lean.Grind.Linarith.Var}
  {p_1 : Lean.Grind.Linarith.Poly},
  Lean.Grind.Linarith.Poly.add k v p = Lean.Grind.Linarith.Poly.add k_1 v_1 p_1 → k = k_1 ∧ v = v_1 ∧ p = p_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.sign.eq_2 : ∀ (hd : ℝ) (tl : List ℝ),
  Tactic.ComputeAsymptotics.UnitMonomial.sign (hd :: tl) =
    if 0 < hd then Tactic.ComputeAsymptotics.UnitMonomial.Sign.pos
    else
      if hd < 0 then Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg else Tactic.ComputeAsymptotics.UnitMonomial.sign tl
-- Mathlib.Analysis.Complex.Conformal
/-- A real differentiable function of the complex plane into some complex normed space `E` is
conformal at a point `z` if it is holomorphic at that point with a nonvanishing differential.
This is a version of the Cauchy-Riemann equations.  -/
DifferentiableAt.conformalAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {z : ℂ} {f : ℂ → E},
  DifferentiableAt ℂ f z → deriv f z ≠ 0 → ConformalAt f z
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_mor₂ : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  (X.triangle f g).mor₂ =
    X.ω₁.map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g (CategoryTheory.CategoryStruct.comp f g) ⋯)
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.multisetProd : ∀ {α : Type u_1} {ι : Type u_2} {β : Type u_3} [inst : NormedField β] {l : Filter α} {s : Multiset ι} {f g : ι → α → β},
  (∀ i ∈ s, Asymptotics.IsEquivalent l (f i) (g i)) →
    Asymptotics.IsEquivalent l (fun x => (Multiset.map (fun x_1 => f x_1 x) s).prod) fun x =>
      (Multiset.map (fun x_1 => g x_1 x) s).prod
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_left_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∩ (s ∩ t) = s ∩ t
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_le_max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} {he : t ≠ ∅},
  (cmp (t.max he) ((t.insert k).max ⋯)).isLE = true
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM : Type → Type
-- Init.Data.UInt.Lemmas
UInt16.le_iff_toNat_le : ∀ {a b : UInt16}, a ≤ b ↔ a.toNat ≤ b.toNat
-- Mathlib.Topology.NhdsKer
nhdsKer_inter_subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey : Type
-- Mathlib.LinearAlgebra.Projection
/-- If `q` is a complement of `p`, then `p × q` is isomorphic to `E`.  -/
Submodule.prodEquivOfIsCompl : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → (p q : Submodule R E) → IsCompl p q → (↥p × ↥q) ≃ₗ[R] E
-- Mathlib.Order.WithBot
WithTop.decidableLE : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → DecidableLE (WithTop α)
-- Mathlib.Topology.Sets.OpenCover
/-- Pullback of a covering of `Y` by a continuous map `X → Y`, giving a covering of `X` with the
same index type.  -/
TopologicalSpace.IsOpenCover.comap : ∀ {κ : Type u_2} {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {v : κ → TopologicalSpace.Opens Y},
  TopologicalSpace.IsOpenCover v →
    ∀ (f : C(X, Y)), TopologicalSpace.IsOpenCover fun k => (TopologicalSpace.Opens.comap f) (v k)
-- Aesop.Forward.State
Aesop.Hyp.instBEq : BEq Aesop.Hyp
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso_inv_app_app_τ₃ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) (X_1 : J),
  (((CategoryTheory.ShortComplex.FunctorEquivalence.counitIso J C).inv.app X).app X_1).τ₃ =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X₃
-- Mathlib.Topology.Connected.PathConnected
/-- If `x₁` is joined to `x₂` within `s` and `y₁` to `y₂` within `t`, then `(x₁, y₁)` is joined
to `(x₂, y₂)` within `s ×ˢ t`.  -/
JoinedIn.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y}
  {x₁ x₂ : X} {y₁ y₂ : Y}, JoinedIn s x₁ x₂ → JoinedIn t y₁ y₂ → JoinedIn (s ×ˢ t) (x₁, y₁) (x₂, y₂)
-- Mathlib.Algebra.DirectSum.Idempotents
/-- The decomposition of `(1 : R)` where `1 = e₁ + e₂ + ⋯ + eₙ` which is induced by
the decomposition of the semiring `R = V1 ⊕ V2 ⊕ ⋯ ⊕ Vn`.  -/
DirectSum.idempotent : {R : Type u_1} →
  {I : Type u_2} →
    [inst : Semiring R] → [inst_1 : DecidableEq I] → (V : I → Ideal R) → [DirectSum.Decomposition V] → I → R
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.EStateM.adaptExcept.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s))
  (h_2 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.error e s => h_1 e s
    | EStateM.Result.ok a s => h_2 a s) =
    h_1 e s
-- Qq.MetaM
/-- A version of `Lean.Meta.isDefEq` which returns a strongly-typed witness rather than a bool.  -/
Qq.isDefEqQ : {u : Lean.Level} →
  {α :
      have u := u;
      Q(Sort u)} →
    (a b : Q(«$α»)) → Lean.MetaM (Qq.MaybeDefEq a b)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_zero : ∀ {G : Type u_1} [inst : AddGroup G] (S : AddSubgroup G), S.lowerCentralSeries 0 = S
-- Aesop.Tree.Data
Aesop.MVarClusterRef : Type
-- Plausible.DeriveShrinkable
/-- For constructor `C x₁ ... xₙ` of inductive type `T`, builds the `List T` expression:
- subterm shrinks: each `xᵢ : T` is yielded directly
- argument shrinks: for each `xᵢ`, shrink it and reconstruct `C` with the shrunk value
For recursive fields (type = T), uses `auxFn` for the recursive call instead of
`Shrinkable.shrink`, since the instance doesn't exist yet during derivation.  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkCtorShrinkExpr : Lean.Name → Lean.Ident → Array Lean.Ident → Array Lean.Expr → Lean.Ident → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.rangeRestrict_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  Function.Surjective ⇑f.rangeRestrict
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `avgRisk_const_left` for a similar result with integrals swapped.  -/
ProbabilityTheory.avgRisk_const_left' : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
      [ProbabilityTheory.IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ) [MeasureTheory.SFinite π],
      ProbabilityTheory.avgRisk ℓ (ProbabilityTheory.Kernel.const Θ μ) κ π = ∫⁻ (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y ∂π ∂μ.bind ⇑κ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapIso_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y),
  (CategoryTheory.Under.mapIso f).inverse = CategoryTheory.Under.map f.inv
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.dropWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  s.dropWhile pat = s.sliceFrom (s.skipPrefixWhile pat)
-- Mathlib.Tactic.FunProp.Types
/-- discrimination tree keys used to index this theorem  -/
Mathlib.Meta.FunProp.GeneralTheorem.keys : Mathlib.Meta.FunProp.GeneralTheorem → List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)
-- Init.Prelude
/-- Exception handlers in `EStateM` save some part of the state, determined by `δ`, and restore it if an
exception is caught. By default, `δ` is `Unit`, and no information is saved.
 -/
EStateM.Backtrackable : outParam (Type u) → Type u → Type u
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.instIsMulCommutative_adjoin : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : Type u_5} [inst_6 : SetLike S A]
  [inst_7 : MulMemClass S A] [StarMemClass S A] (s : S) [IsMulCommutative ↥s],
  IsMulCommutative ↥(StarAlgebra.adjoin R ↑s)
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isCompactlyGenerated_of_wellFoundedGT : ∀ {α : Type u_2} [inst : CompleteLattice α] [h : WellFoundedGT α], IsCompactlyGenerated α
-- Mathlib.Topology.Algebra.Module.TransferInstance
Shrink.continuousLinearEquiv_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : AddCommMonoid α] [inst_2 : TopologicalSpace α]
  [inst_3 : Semiring R] [inst_4 : Module R α] (a : Shrink.{v, u_2} α),
  (Shrink.continuousLinearEquiv R α) a = (equivShrink α).symm a
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Day` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.day : Std.Time.PlainDateTime → Std.Time.Day.Ordinal
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.instProp : Topology.IsUpperSet Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.kernelBiproductπIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) (i : J)
  [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)],
  (CategoryTheory.Limits.kernelBiproductπIso f i).inv =
    CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.π f i) 0)
      (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biproduct.fromSubtype f fun j => ¬j = i) ⋯)