mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Bitwise
Int32.not_inj : ∀ {a b : Int32}, ~~~a = ~~~b ↔ a = b
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ico_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Ico a b = Set.Ioc (b / c) (a / c)
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- If a point `p` is equidistant to two different lines `p₁ p₂` and `p₁ p₃`, the oriented angles
at `p₁` are equal modulo `π`.  -/
EuclideanGeometry.two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  AffineIndependent ℝ ![p₁, p₂, p₃] →
    dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₂]) p) =
        dist p ↑((EuclideanGeometry.orthogonalProjection line[ℝ, p₁, p₃]) p) →
      2 • EuclideanGeometry.oangle p₂ p₁ p = 2 • EuclideanGeometry.oangle p p₁ p₃
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_mul_X_iff : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R}, IsNilpotent (P * Polynomial.X) ↔ IsNilpotent P
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.instToStringExprDiffTag : ToString Lean.Widget.ExprDiffTag✝
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.DTreeMap.Const.insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.comp_autMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C] {A B : C}
  [inst_2 : CategoryTheory.PreGaloisCategory.IsConnected A] [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois B]
  (f : A ⟶ B) (σ : CategoryTheory.Aut A),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.PreGaloisCategory.autMap f σ).hom =
    CategoryTheory.CategoryStruct.comp σ.hom f
-- Mathlib.RingTheory.WittVector.StructurePolynomial
eq_wittStructureInt : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (φ : ℕ → MvPolynomial (idx × ℕ) ℤ),
  (∀ (n : ℕ),
      (MvPolynomial.bind₁ φ) (wittPolynomial p ℤ n) =
        (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (wittPolynomial p ℤ n)) Φ) →
    φ = wittStructureInt p Φ
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- The `n`th exterior power of a finite module is a finite module.  -/
exteriorPower.instFinite : ∀ {R : Type u_1} {M : Type u_3} {n : ℕ} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Finite R M], Module.Finite R ↥(⋀[R]^n M)
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), B.polar ∅ = Set.univ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofIntLE : ∀ {n : ℤ} (h₁ : Int16.minValue.toInt ≤ n) (h₂ : n ≤ Int16.maxValue.toInt), (Int16.ofIntLE n h₁ h₂).toInt8 = Int8.ofInt n
-- Mathlib.Topology.ContinuousMap.Ideals
WeakDual.CharacterSpace.continuousMapEval_apply_apply : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : CommRing 𝕜] [inst_2 : TopologicalSpace 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] [inst_4 : Nontrivial 𝕜] [inst_5 : NoZeroDivisors 𝕜] (x : X) (f : C(X, 𝕜)),
  ((WeakDual.CharacterSpace.continuousMapEval X 𝕜) x) f = f x
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.Hom.hom.eq_1 : ∀ {X Y : Semigrp} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Init.Data.Bool
Bool.le_true : ∀ (x : Bool), x ≤ true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_mem_prefix : ∀ {w : ℕ} {inv : Bool} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign.toAIGAssignment,
      { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign.toAIGAssignment, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.homotopyFrom_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p q : ↑(GenLoop N X x)} (H : Path.Homotopy (GenLoop.toLoop i p) (GenLoop.toLoop i q))
  (a : ↑unitInterval × (N → ↑unitInterval)),
  (GenLoop.homotopyFrom i H) a =
    Function.uncurry (fun x_1 y => Function.uncurry (fun x_2 y => (H (x_1, x_2)) y) y)
      (Prod.map id (⇑(Cube.splitAt i)) a)
-- Mathlib.Algebra.Order.Ring.WithTop
_private.Mathlib.Algebra.Order.Ring.WithTop.0.WithTop.instMonoidWithZero.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (a : α) (n : ℕ) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match some a, n with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_1 a n
-- Mathlib.CategoryTheory.IsConnected
/-- Lifting the universe level of morphisms and objects preserves connectedness.  -/
CategoryTheory.instIsConnectedULiftHomULift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [hc : CategoryTheory.IsConnected J],
  CategoryTheory.IsConnected (CategoryTheory.ULiftHom (ULift.{u₂, u₁} J))
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toArray_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β},
  (array.iterM m).toArray = pure array
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_iff_of_isColimit_cofan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  {f : β → C} {c : CategoryTheory.Limits.Cofan f} (hc : CategoryTheory.Limits.IsColimit c),
  CategoryTheory.IsSeparator c.pt ↔ (CategoryTheory.ObjectProperty.ofObj f).IsSeparating
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_eq_nnnorm_vsub' : ∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y : P), nndist x y = ‖y -ᵥ x‖₊
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roo_eq_none_iff : ∀ {m n i : ℕ}, (m<...n).toArray[i]? = none ↔ n ≤ i + (m + 1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_dblU : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R F]
  [inst_6 : Algebra S F] [IsScalarTower R S F] [inst_8 : Algebra R K] [inst_9 : Algebra S K] [IsScalarTower R S K]
  (f : F →ₐ[S] K) (P : Fin 3 → F), (W'.baseChange K).dblU (⇑f ∘ P) = f ((W'.baseChange F).dblU P)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The notation for the submonoid of non-zero smul-divisors.  -/
nonZeroSMulDivisors.«term_⁰[_]» : Lean.TrailingParserDescr
-- Std.Data.Iterators.Lemmas.Consumers.Set
Std.Iter.toExtTreeSet_eq_ofList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {cmp : β → β → Ordering} [inst_4 : Std.TransCmp cmp],
  it.toExtTreeSet cmp = Std.ExtTreeSet.ofList it.toList cmp
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.comp_zero : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ), g.comp 0 = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_mono : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A), f ∣ g → AlgebraicGeometry.Proj.basicOpen 𝒜 g ≤ AlgebraicGeometry.Proj.basicOpen 𝒜 f
-- Lean.Elab.Command
Lean.Elab.Command.Linter.mk.sizeOf_spec : ∀ (run : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name : autoParam Lean.Name Lean.Elab.Command.Linter.name._autoParam),
  sizeOf { run := run, name := name } = 1 + sizeOf name
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.Iterators.Types.Zip.instIterator.match_5.eq_1 : ∀ {m : Type u_1 → Type u_2} {α₁ β₁ : Type u_1} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) (h_1 : none = none → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → none = some out₁ → motive (some out₁)),
  (match hm : none with
    | none => h_1 hm
    | some out₁ => h_2 out₁ hm) =
    h_1 ⋯
-- Mathlib.Data.Set.Card
Set.ncard_insert_le : ∀ {α : Type u_1} (a : α) (s : Set α), (insert a s).ncard ≤ s.ncard + 1
-- Mathlib.Algebra.Algebra.Bilinear
/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`.  -/
RingTheory.LinearMap.«termμ[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Module.Defs
Prod.instPosSMulMono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Preorder γ] [inst_4 : SMul α β] [inst_5 : SMul α γ] [PosSMulMono α β] [PosSMulMono α γ],
  PosSMulMono α (β × γ)
-- Mathlib.GroupTheory.GroupAction.Transitive
/-- An action of a group is pretransitive iff the orbit of every given element is full  -/
AddAction.isPretransitive_iff_orbit_eq_univ : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] (a : X),
  AddAction.IsPretransitive G X ↔ AddAction.orbit G a = Set.univ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
the right, namely `a₁ * b < a₂ * b → a₁ < a₂` if `0 ≤ b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsStrictOrderedRing`.  -/
MulPosReflectLT : (α : Type u_1) → [Mul α] → [Zero α] → [Preorder α] → Prop
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instToStringPosition : ToString Lean.Lsp.Position
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.nnnorm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), ‖f x‖₊ = ‖x‖₊
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditive_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : Additive α →+ Additive β) (a : α),
  (MonoidHom.toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord_mul_of_isUnit_right : ∀ {R : Type u_1} [inst : CommRing R] {a : R}, IsUnit a → ∀ (x : R), Ring.ord R (x * a) = Ring.ord R x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.instFullOverToOver : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T) [F.Full], (CategoryTheory.CostructuredArrow.toOver F X).Full
-- Mathlib.Probability.Kernel.Category.Stoch
instDeterministicStochCounit : ∀ {X : Stoch}, CategoryTheory.Deterministic CategoryTheory.ComonObj.counit
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.substAssignedMVarsAndNormalize : Lean.Level → Lean.MetaM Lean.Level
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq l] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : l) (r : m → α) (B : Matrix m n α),
  A.updateRow i r * B = (A * B).updateRow i (Matrix.vecMul r B)
-- Mathlib.Geometry.Group.Growth.QuotientInter
Finset.card_pow_quotient_mul_pow_inter_subgroup_le : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {H : Subgroup G} [inst_2 : DecidablePred fun x => x ∈ H]
  [inst_3 : H.Normal] {A : Finset G} {m n : ℕ},
  (Finset.image (⇑(QuotientGroup.mk' H)) (A ^ m)).card * {x ∈ A ^ n | x ∈ H}.card ≤ (A ^ (m + n)).card
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.coe_natAbs_nonneg : ∀ (a : ℤ), ↑a.natAbs ≥ 0
-- Std.Async.TCP
/-- Represents a TCP server socket, managing incoming client connections.
 -/
Std.Async.TCP.Socket.Server : Type
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Subsemiring.homogeneousCore_mono : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜],
  Monotone (Subsemiring.homogeneousCore 𝒜)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.eq_1 : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  (f : α → ε) (s : Set α) (μ : MeasureTheory.Measure α),
  MeasureTheory.IntegrableOn f s μ = MeasureTheory.Integrable f (μ.restrict s)
-- Mathlib.Tactic.NormNum.Basic
_private.Mathlib.Tactic.NormNum.Basic.0.Mathlib.Meta.NormNum.Result.add.nnratArm : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : Q(Add «$α»)) → Q(DivisionSemiring «$α») → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» + «$b»))
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The 1-dimensional generalized loops based at `x` are in bijection with loops at `x`.  -/
genLoopEquivOfUnique : {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → (N : Type u_3) → [Unique N] → ↑(GenLoop N X x) ≃ LoopSpace X x
-- Batteries.Data.Array.Scan
Array.scanrM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : ℕ) (h_start : start ≤ as.size) (acc : Array β),
  Array.scanrM.loop f init as start stop h_start acc =
    if h_gt : stop < start then
      let i := start - 1;
      do
      let next ← f as[i] init
      Array.scanrM.loop f next as i stop ⋯ (acc.push init)
    else pure (acc.push init).reverse
-- Mathlib.NumberTheory.NumberField.CMField
/-- The index of the subgroup of `(𝓞 K)ˣ` generated by the real units and the roots of unity is equal
to `2` iff there exists a unit whose image by `unitsMulComplexConjInv` generates the torsion
subgroup of `K`.
 -/
NumberField.IsCMField.indexRealUnits_eq_two_iff : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K],
  NumberField.IsCMField.indexRealUnits K = 2 ↔
    ∃ u, Subgroup.zpowers ((NumberField.IsCMField.unitsMulComplexConjInv K) u) = ⊤
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_eq_span_left_iff_dvd : ∀ {α : Type u} [inst : CommSemiring α] {x y : α}, Ideal.span {x, y} = Ideal.span {x} ↔ x ∣ y
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- The integral of the conditional expectation `condExpL1CLM` over an `m`-measurable set is equal
to the integral of `f` on that set. See also `setIntegral_condExp`, the similar statement for
`condExp`.  -/
MeasureTheory.setIntegral_condExpL1CLM : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α}
  [inst_3 : CompleteSpace F'] (f : ↥(MeasureTheory.Lp F' 1 μ)),
  MeasurableSet s → ∫ (x : α) in s, ↑↑((MeasureTheory.condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instInhabited : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] → {I₀ : WithTop (BoxIntegral.Box ι)} → Inhabited (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Init.Data.BitVec.Bootstrap
BitVec.getElem_cons : ∀ {b : Bool} {n : ℕ} {x : BitVec n} {i : ℕ} (h : i < n + 1), (BitVec.cons b x)[i] = if h : i = n then b else x[i]
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSets.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (π : ι → Set (Set Ω)) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndepSets m' hm' π μ =
    ProbabilityTheory.Kernel.iIndepSets π (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_diff_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Lean.Util.InstantiateLevelParams
/-- Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two arrays have different length, the smallest one is used.
 -/
Lean.Expr.instantiateLevelParamsArray : Lean.Expr → Array Lean.Name → Array Lean.Level → Lean.Expr
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.normedAddCommGroup : {α : Type u_3} →
  {E : α → Type u_4} →
    {p : ENNReal} → [inst : (i : α) → NormedAddCommGroup (E i)] → [hp : Fact (1 ≤ p)] → NormedAddCommGroup ↥(lp E p)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.ite_sdiff_self`. -/
Set.ite_diff_self : ∀ {α : Type u_1} (t s s' : Set α), t.ite s s' \ t = s' \ t
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.keys_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ}, (Std.ExtTreeMap.map f t).keys = t.keys
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isConnected_setOfPred_wSameSide`. -/
AffineSubspace.isConnected_setOf_wSameSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} (x : P),
  (↑s).Nonempty → IsConnected {y | s.WSameSide x y}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.ExtDTreeMap.filterMap f t}, (Std.ExtDTreeMap.filterMap f t).get k h' = (f k (t.get k ⋯)).get ⋯
-- Mathlib.GroupTheory.SemidirectProduct
/-- The homomorphism from a semidirect product of subgroups to the ambient group.  -/
SemidirectProduct.monoidHomSubgroup : {G : Type u_2} →
  [inst : Group G] →
    {H K : Subgroup G} →
      (h : K ≤ Subgroup.normalizer ↑H) → ↥H ⋊[H.normalizerMonoidHom.comp (Subgroup.inclusion h)] ↥K →* G
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- Sum of elements in an `AddSubgroup` of an `AddCommGroup` indexed by a `Finset`
is in the `AddSubgroup`.  -/
AddSubgroup.sum_mem : ∀ {G : Type u_3} [inst : AddCommGroup G] (K : AddSubgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G},
  (∀ c ∈ t, f c ∈ K) → ∑ c ∈ t, f c ∈ K
-- Lean.Meta.Match.Basic
Lean.Meta.Match.instInhabitedPattern.default : Lean.Meta.Match.Pattern
-- Mathlib.RepresentationTheory.Rep.Res
Rep.liftHomOfSurj_toLinearMap : ∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G)
  {X Y : Rep.{u_1, u, v1} k G} (hf : Function.Surjective ⇑f) (f' : Rep.res f X ⟶ Rep.res f Y),
  (Rep.Hom.hom (Rep.liftHomOfSurj f hf f')).toLinearMap = (Rep.Hom.hom f').toLinearMap
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.support_comap : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : γ ↪ β), (L.comap f).support = ⇑f ⁻¹' L.support
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.instHasIdealSupportOfHasMemOrNegMem : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [HasMemOrNegMem P], P.HasIdealSupport
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- Multiplicativity of leading coefficients  -/
MonomialOrder.leadingCoeff_mul_of_isRegular_right : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  IsRegular (m.leadingCoeff g) → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.CategoryTheory.Adjunction.Opposites
/-- If `F.rightOp` is adjoint to `G` then `G.rightOp` is adjoint to `F`.  -/
CategoryTheory.Adjunction.rightOp : {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} → (F.rightOp ⊣ G) → (G.rightOp ⊣ F)
-- Mathlib.Topology.QuasiSeparated
QuasiSeparatedSpace.isCompact_sInter : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] [CompactSpace α] {s : Set (Set α)},
  s.Finite → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → IsCompact (⋂₀ s)
-- Lean.Util.Trace
Lean.trace.profiler.useHeartbeats : Lean.Option Bool
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_iInf : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {ι : Type u_2} {I : ι → TwoSidedIdeal R} {x : R},
  x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.MonoidalClosedFunctor.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} D]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.MonoidalClosed D]
  [inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  (∀ (A : C), CategoryTheory.IsIso (CategoryTheory.expComparison F A).natTrans) → CategoryTheory.MonoidalClosedFunctor F
-- Mathlib.Algebra.CharP.Lemmas
Commute.add_pow_prime_eq' : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p →
    ∀ {x y : R},
      Commute x y → (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
-- Mathlib.Tactic.Widget.SelectPanelUtils
/-- Locations currently selected in the goal state.  -/
SelectInsertParams.selectedLocations : SelectInsertParams → Array Lean.SubExpr.GoalsLocation
-- Lean.Util.ReplaceLevel
_private.Lean.Util.ReplaceLevel.0.Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit : (Lean.Level → Option Lean.Level) → USize → Lean.Expr → Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counit_pow : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a : A) (n : ℕ),
  CoalgebraStruct.counit (a ^ n) = CoalgebraStruct.counit a ^ n
-- Mathlib.Data.Finset.Prod
Finset.singleton_product : ∀ {α : Type u_1} {β : Type u_2} {t : Finset β} {a : α}, {a} ×ˢ t = Finset.map { toFun := Prod.mk a, inj' := ⋯ } t
-- Init.Data.UInt.Lemmas
UInt8.toUSize_lt : ∀ {a b : UInt8}, a.toUSize < b.toUSize ↔ a < b