mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.PiLex
Pi.instOrderBotLexForallOfWellFoundedLT : {ι : Type u_1} →
  {β : ι → Type u_2} →
    [inst : LinearOrder ι] →
      [WellFoundedLT ι] →
        [inst_2 : (a : ι) → PartialOrder (β a)] → [(a : ι) → OrderBot (β a)] → OrderBot (Lex ((a : ι) → β a))
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ofNat_snd : ∀ {q : ℕ} (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).2 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.instIsRegularOfIso : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) {Y : SSet} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B)
  [P.IsRegular], (P.ofIso e hA).IsRegular
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zero_zpow' : ∀ {α : Type u_1} [inst : GroupWithZero α] (n : ℤ), Mathlib.Tactic.FieldSimp.zpow' 0 n = 0
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.packingNumber ε A = ⨆ C, ⨆ (_ : C ⊆ A), ⨆ (_ : Metric.IsSeparated (↑ε) C), C.encard
-- Mathlib.Algebra.Group.Action.Option
Option.instFaithfulVAdd : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [FaithfulVAdd M α], FaithfulVAdd M (Option α)
-- Mathlib.Data.Seq.Computation
Computation.rel_of_liftRel : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca : Computation α} {cb : Computation β},
  Computation.LiftRel R ca cb → ∀ {a : α} {b : β}, a ∈ ca → b ∈ cb → R a b
-- Mathlib.Order.Filter.Extr
IsMaxFilter.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
  {l : Filter α} {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsMaxFilter f l a → ∀ {g : α → γ}, IsMaxFilter g l a → IsMaxFilter (fun x => op (f x) (g x)) l a
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- The composition of `C^n` functions within domains at points is `C^n`.  -/
ContMDiffWithinAt.comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] {E'' : Type u_8} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E'']
  {H'' : Type u_9} [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10}
  [inst_12 : TopologicalSpace M''] [inst_13 : ChartedSpace H M] [inst_14 : ChartedSpace H' M']
  [inst_15 : ChartedSpace H'' M''] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {t : Set M'} {g : M' → M''} (x : M),
  ContMDiffWithinAt I' I'' n g t (f x) →
    ContMDiffWithinAt I I' n f s x → ContMDiffWithinAt I I'' n (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_zpow : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : DivisionRing R]
  (v : Valuation R Γ₀) (x : R) (z : ℤ), WithVal.toVal v (x ^ z) = WithVal.toVal v x ^ z
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.op_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.X₁ = Opposite.op S.X₃
-- Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
FiniteField.Matrix.charpoly_pow_card : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_2} [inst_2 : Field K] [inst_3 : Fintype K]
  (M : Matrix n n K), (M ^ Fintype.card K).charpoly = M.charpoly
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If `J` is an algebraic extension of `K` and `L` is an algebraic closure of `J`, then it is
also an algebraic closure of `K`.  -/
IsAlgClosure.ofAlgebraic : ∀ (K : Type u_1) (J : Type u_2) (L : Type v) [inst : Field K] [inst_1 : Field J] [inst_2 : Field L]
  [inst_3 : Algebra K J] [inst_4 : Algebra J L] [IsAlgClosure J L] [inst_6 : Algebra K L] [IsScalarTower K J L]
  [Algebra.IsAlgebraic K J], IsAlgClosure K L
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.self_le_maxKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- A map `f : α → α` is said to be pre-ergodic with respect to a measure `μ` if any measurable
strictly invariant set is either almost empty or full.  -/
PreErgodic : {α : Type u_1} → {m : MeasurableSpace α} → (α → α) → autoParam (MeasureTheory.Measure α) PreErgodic._auto_1 → Prop
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instToFormatKey : Std.ToFormat Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instQuasiIsoAtMapOppositeSymmUnopFunctorOp : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [QuasiIsoAt φ i],
  QuasiIsoAt ((HomologicalComplex.unopFunctor V c).map φ.op) i
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage'_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B)
  [inst_3 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).source = Subtype.val ⁻¹' e.toPretrivialization.source
-- Mathlib.Order.Concept
Concept.extent_copy : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r) (e : Set α) (i : Set β) (he : e = c.extent)
  (hi : i = c.intent), (c.copy e i he hi).extent = e
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instInhabited : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → Inhabited (M →ₗ⁅R,L⁆ N)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AddMonoidHom.coe_ofMapMidpoint : ∀ (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [inst : Ring R] [inst_1 : Invertible 2]
  [inst_2 : AddCommGroup E] [inst_3 : Module R E] [inst_4 : Ring R'] [inst_5 : Invertible 2] [inst_6 : AddCommGroup F]
  [inst_7 : Module R' F] (f : E → F) (h0 : f 0 = 0) (hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)),
  ⇑(AddMonoidHom.ofMapMidpoint R R' f h0 hm) = f
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.h : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.filteredClosure.below.base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsFiltered.filteredClosure f a → Prop} (x : α),
  CategoryTheory.IsFiltered.filteredClosure.below ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.braid_natural : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
      (CategoryTheory.Limits.prod.braiding Y W).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding X Z).hom
      (CategoryTheory.Limits.prod.map g f)
-- Mathlib.Data.Bool.Basic
Bool.false_lt_true : false < true
-- Mathlib.Tactic.Lift
/-- Enable automatic handling of pi types in `CanLift`.  -/
Pi.canLift : ∀ (ι : Sort u_1) (α : ι → Sort u_2) (β : ι → Sort u_3) (coe : (i : ι) → β i → α i) (P : (i : ι) → α i → Prop)
  [∀ (i : ι), CanLift (α i) (β i) (coe i) (P i)],
  CanLift ((i : ι) → α i) ((i : ι) → β i) (fun f i => coe i (f i)) fun f => ∀ (i : ι), P i (f i)
-- Mathlib.Order.Filter.Basic
Filter.mem_inf_iff : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂
-- Init.Data.Array.Lemmas
Array.foldl_eq_apply_foldr : ∀ {α : Type u_1} {init x : α} {xs : Array α} {f : α → α → α} [Std.Associative f] [Std.LawfulRightIdentity f init],
  Array.foldl f x xs = f x (Array.foldr f init xs)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF → ∀ {k fallback : α}, Std.DTreeMap.Internal.Impl.contains k t = true → t.getKeyD k fallback = k
-- Mathlib.Topology.Homotopy.LocallyContractible
/-- The strong notion (contractible neighborhood basis)
implies the classical notion (null-homotopic inclusions).
The converse is false by the Borsuk-Mazurkiewicz counterexample [borsuk_mazurkiewicz1934];
see also [MO88628] for discussion and the Whitehead manifold example.  -/
StronglyLocallyContractibleSpace.locallyContractible : ∀ {X : Type u_1} [inst : TopologicalSpace X] [StronglyLocallyContractibleSpace X], LocallyContractibleSpace X
-- Mathlib.Order.Ideal
Order.Ideal.IsProper.notMem_of_compl_mem : ∀ {P : Type u_1} [inst : BooleanAlgebra P] {x : P} {I : Order.Ideal P}, I.IsProper → xᶜ ∈ I → x ∉ I
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.sc'MapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) (h₂ : S₂.IsComplex)
  (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'MapIso._auto_1)
  (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'MapIso._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'MapIso._auto_5),
  (CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k hij hjk hk).inv =
    CategoryTheory.ComposableArrows.sc'Map e.inv h₂ h₁ i j k hij hjk hk
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplex.congr_simp : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (F F_1 : CategoryTheory.Functor W₁ W₂) (e_F : F = F_1)
  [inst_4 : F.PreservesZeroMorphisms] (c : ComplexShape ι), F.mapHomologicalComplex c = F_1.mapHomologicalComplex c
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasInjectiveDimensionLT S.X₃ n →
        CategoryTheory.HasInjectiveDimensionLT S.X₂ (n + 1) → CategoryTheory.HasInjectiveDimensionLT S.X₁ (n + 1)
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenRatio_add_goldenConj : Real.goldenRatio + Real.goldenConj = 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
/-- If `P` holds for `0`, units and powers of primes,
and `P x ∧ P y` for coprime `x, y` implies `P (x * y)`,
then `P` holds on all `a : α`.  -/
UniqueFactorizationMonoid.induction_on_coprime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α),
  P 0 →
    (∀ {x : α}, IsUnit x → P x) →
      (∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) → (∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) → P a
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.gen_mem_nhds : ∀ {α : Type u_1} (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
  s ∈ 𝔖 →
    ∀ {V : Set (β × β)},
      V ∈ uniformity β → {g | ∀ x ∈ s, ((UniformOnFun.toFun 𝔖) f x, (UniformOnFun.toFun 𝔖) g x) ∈ V} ∈ nhds f
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.divOf_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G), x.divOf 0 = x
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in a slice `s`. If there
is no match `s.endPos` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".find Char.isWhitespace).get! == ' '`

* `"tea".find (fun (c : Char) => c == 'X') == "tea".endPos`

* `("coffee tea water".find "tea").get! == 't'`
 -/
String.find : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        (s : String) → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → s.Pos
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.contains_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α}, (Std.DTreeMap.Raw.Const.ofList l cmp).contains k = (List.map Prod.fst l).contains k
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] {x : L →ₗ⁅R⁆ LieDerivation R K K} [inst_5 : SizeOf R]
  [inst_6 : SizeOf K] [inst_7 : SizeOf L] (left : K) (right : L),
  sizeOf { left := left, right := right } = 1 + sizeOf left + sizeOf right
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_X' : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (i : σ), (MvPolynomial.eval₂Hom f g) (MvPolynomial.X i) = g i
-- Mathlib.Data.Vector.Basic
List.Vector.mapAccumr₂_cons : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} {φ : Type u_5} {n : ℕ} {x : α} {y : β} {s : σ} (xs : List.Vector α n)
  (ys : List.Vector β n) {f : α → β → σ → σ × φ},
  List.Vector.mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s =
    have r := List.Vector.mapAccumr₂ f xs ys s;
    have q := f x y r.1;
    (q.1, q.2 ::ᵥ r.2)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative 1 = 0
-- Mathlib.Geometry.Euclidean.Volume.Measure
instIsAddLeftInvariantEuclideanHausdorffMeasureOfIsIsometricVAdd : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] [inst_3 : AddGroup X]
  [IsIsometricVAdd X X] (d : ℕ), (MeasureTheory.Measure.euclideanHausdorffMeasure d).IsAddLeftInvariant
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.mk.sizeOf_spec : ∀ (value : String)
  (isValidHeaderValue :
    autoParam (Std.Http.Header.IsValidHeaderName value) Std.Http.Header.Name.isValidHeaderValue._autoParam)
  (isLowerCase : autoParam (Std.Http.Internal.IsLowerCase value) Std.Http.Header.Name.isLowerCase._autoParam),
  sizeOf { value := value, isValidHeaderValue := isValidHeaderValue, isLowerCase := isLowerCase } =
    1 + sizeOf value + sizeOf isValidHeaderValue + sizeOf isLowerCase
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.instSmallOfSmallI₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (E : J.ZeroHypercover S) [Small.{w', w} E.I₀], E.Small
-- Init.Data.Vector.OfFn
Vector.ofFnM_pure_comp : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α},
  Vector.ofFnM (pure ∘ f) = pure (Vector.ofFn f)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.id.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithTerminal.star.id = PUnit.unit
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Iio : ∀ (a : ENNReal), ENat.toENNReal ⁻¹' Set.Iio a = Set.Iio ⌈a⌉ₑ
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_const : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} [CompleteSpace F] [MeasureTheory.IsFiniteMeasure μ]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (x : E),
  (MeasureTheory.setToFun μ T hT fun x_1 => x) = (T Set.univ) x
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableWithinAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {s : Set G} {x : G},
  DifferentiableWithinAt ℝ f s x →
    DifferentiableWithinAt ℝ g s x → DifferentiableWithinAt ℝ (fun x => inner 𝕜 (f x) (g x)) s x
-- Mathlib.Data.List.Lookmap
List.lookmap.go.eq_1 : ∀ {α : Type u_1} (f : α → Option α) (a : Array α), List.lookmap.go f [] a = a.toList
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T2Space M], T2Space Mᵃᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.mk.injEq : ∀ {V : Type u_1} {G : SimpleGraph V} (toProd : V × V) (adj : G.Adj toProd.1 toProd.2) (toProd_1 : V × V)
  (adj_1 : G.Adj toProd_1.1 toProd_1.2),
  ({ toProd := toProd, adj := adj } = { toProd := toProd_1, adj := adj_1 }) = (toProd = toProd_1)
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsReducedXScheme : ∀ (X : AlgebraicGeometry.Scheme) {𝒰 : X.OpenCover} [AlgebraicGeometry.IsReduced X] (i : 𝒰.I₀),
  AlgebraicGeometry.IsReduced (𝒰.X i)
-- Lean.Elab.MutualInductive
/-- The parameters in the header's initial local context. Used for adding fvar alias terminfo.  -/
Lean.Elab.Command.PreElabHeaderResult.origParams : Lean.Elab.Command.PreElabHeaderResult → Array Lean.Expr
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `f` is strictly differentiable at `x` with derivative `f'` and `K > ‖f'‖₊`, then `f` is
`K`-Lipschitz in a neighborhood of `x`.  -/
HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasStrictFDerivAt f f' x → ∀ (K : NNReal), ‖f'‖₊ < K → ∃ s ∈ nhds x, LipschitzOnWith K f s
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.error.formatter : String → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (X : ↑(Set.Iio j)),
  (CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso c).hom.app X =
    (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c ↑X ⋯).hom
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.compare_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α)
  (a : α), pkg.compare pkg' (pkg.coe a) = pkg'.coe a
-- Mathlib.Algebra.Group.ULift
ULift.monoid : {α : Type u} → [Monoid α] → Monoid (ULift.{u_1, u} α)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hf_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (self : WeakFEPair E) (r : ℝ),
  (fun x => self.f x - self.f₀) =O[Filter.atTop] fun x => x ^ r
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.and.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.AndKind.and = 1
-- Init.Data.Vector.Find
Vector.find?_eq_map_findFinIdx?_getElem : ∀ {α : Type} {n : ℕ} {xs : Vector α n} {p : α → Bool},
  Vector.find? p xs = Option.map (fun x => xs[x]) (Vector.findFinIdx? p xs)
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_id : ∀ {α : Type u} [inst : Add α], WithZero.mapAddHom (AddHom.id α) = AddMonoidHom.id (WithZero α)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If the measure is sigma-finite, all strongly measurable functions are
`FinStronglyMeasurable`.  -/
MeasureTheory.StronglyMeasurable.finStronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] [inst_1 : Zero β] {m0 : MeasurableSpace α},
  MeasureTheory.StronglyMeasurable f →
    ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ], MeasureTheory.FinStronglyMeasurable f μ
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_of_finrank_le : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {i : ℕ}, Module.finrank 𝕜 E ≤ i → T.singularValues i = 0
-- Lean.DocString.Types
Lean.Doc.Block.ol.injEq : ∀ {i : Type u} {b : Type v} (start : ℤ) (items : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) (start_1 : ℤ)
  (items_1 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))),
  (Lean.Doc.Block.ol start items = Lean.Doc.Block.ol start_1 items_1) = (start = start_1 ∧ items = items_1)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int8.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Probability.Distributions.Geometric
/-- The geometric measure with success probability `p` as a measure over `ℕ`.  -/
ProbabilityTheory.geometricMeasure : ↑unitInterval → MeasureTheory.Measure ℕ
-- Std.Async.Signal
/-- Background write attempted to control terminal.
 -/
Std.Async.Signal.sigttou : Std.Async.Signal
-- Mathlib.Tactic.CategoryTheory.Monoidal.Basic
/-- Normalize the both sides of an equality.  -/
Mathlib.Tactic.Monoidal.tacticMonoidal_nf : Lean.ParserDescr
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_top_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U : Submodule 𝕜 E}, U ⟂ ⊤ ↔ U = ⊥
-- Init.Data.BitVec.Basic
/-- Extracts the bits from `hi` down to `lo` (both inclusive) from a bitvector, which is implicitly
zero-extended if necessary.

The resulting bitvector has size `hi - lo + 1`.

SMT-LIB name: `extract`.
 -/
BitVec.extractLsb : {n : ℕ} → (hi lo : ℕ) → BitVec n → BitVec (hi - lo + 1)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.cone_pt : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F],
  (CategoryTheory.Limits.weakLimit.cone F).pt = CategoryTheory.Limits.weakLimit F
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.instEnoughProjectives : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Monoid G], CategoryTheory.EnoughProjectives (Rep.{max w u, u, u} k G)
-- Lean.Data.SMap
Lean.SMap.instForInProdOfMonad : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → {m : Type u_1 → Type u_2} → [Monad m] → ForIn m (Lean.SMap α β) (α × β)
-- Mathlib.Order.SuccPred.Tree
RootedTree.mem_subtrees_disjoint_iff : ∀ {t : RootedTree} {t₁ t₂ : SubRootedTree t},
  t₁ ∈ t.subtrees → t₂ ∈ t.subtrees → ∀ (v₁ v₂ : ↑t), v₁ ∈ t₁ → v₂ ∈ t₂ → (Disjoint v₁ v₂ ↔ t₁ ≠ t₂)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.mk : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, IsCoatom I → I.IsMaximal
-- Lean.Data.KVMap
Lean.KVMap.find : Lean.KVMap → Lean.Name → Option Lean.DataValue