mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Types
Lean.Elab.MacroExpansionInfo.lctx : Lean.Elab.MacroExpansionInfo → Lean.LocalContext
-- Init.Data.Array.Lemmas
Array.size_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, (Array.map f xs).size = xs.size
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentSpaceBasis.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι),
  P.cotangentSpaceBasis = Module.Basis.baseChange S (KaehlerDifferential.mvPolynomialBasis R ι)
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ematch : Lean.Meta.Grind.EMatchTheoremKind → Lean.Meta.Grind.AttrKind
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι),
  CategoryTheory.CategoryStruct.comp (P.p.f n) (P.p.f n) = P.p.f n
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
_private.Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_2 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (isLt_1 : 1 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨1, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_2 isLt isLt_1 x
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
constant, then `f` tends to `∞`.  -/
Filter.Tendsto.num : ∀ {α : Type u_4} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : TopologicalSpace K] [OrderTopology K] {f g : α → K} {l : Filter α},
  Filter.Tendsto g l Filter.atTop →
    ∀ {a : K}, 0 < a → Filter.Tendsto (fun x => f x / g x) l (nhds a) → Filter.Tendsto f l Filter.atTop
-- Mathlib.Tactic.Positivity.Basic
/-- The `positivity` extension which identifies expressions of the form `NNRat.num q`,
such that `positivity` successfully recognises `q`.  -/
Mathlib.Meta.Positivity.evalNNRatNum : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Data.Multiset.FinsetOps
Multiset.zero_ndunion : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), Multiset.ndunion 0 s = s
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- In a semisimple Lie algebra, the atoms are non-abelian.  -/
LieAlgebra.IsSemisimple.non_abelian_of_isAtom : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsSemisimple R L] (I : LieIdeal R L), IsAtom I → ¬IsLieAbelian ↥I
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_comp_obj : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↑Z),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).obj U =
    (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj U)
-- Mathlib.Computability.RE
ComputablePred.computable_iff_re_compl_re' : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a
-- Mathlib.Data.Nat.Factorial.SuperFactorial
Nat.superFactorial_zero : Nat.superFactorial 0 = 1
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : X ⟶ Y),
  CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.map f =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprSourceInfo_mathlib.toExpr : Lean.SourceInfo → Lean.Expr
-- Mathlib.Geometry.Diffeology.Basic
/-- The predicate that the diffeology built from this structure will use. Can be overwritten
to allow for better definitional equalities.  -/
DiffeologicalSpace.CorePlotsOn.isPlot : {X : Type u_1} → DiffeologicalSpace.CorePlotsOn X → {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.IsStableUnderCobaseChange
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.quasicategory_iff_innerFibration : ∀ (X : SSet), X.Quasicategory ↔ SSet.InnerFibration (CategoryTheory.Limits.terminal.from X)
-- Mathlib.Order.SuccPred.Tree
RootedTree.mk.inj : ∀ {α : Type u_2} {semilatticeInf : SemilatticeInf α} {orderBot : OrderBot α} {predOrder : PredOrder α}
  {isPredArchimedean : IsPredArchimedean α} {α_1 : Type u_2} {semilatticeInf_1 : SemilatticeInf α_1}
  {orderBot_1 : OrderBot α_1} {predOrder_1 : PredOrder α_1} {isPredArchimedean_1 : IsPredArchimedean α_1},
  { α := α, semilatticeInf := semilatticeInf, orderBot := orderBot, predOrder := predOrder,
        isPredArchimedean := isPredArchimedean } =
      { α := α_1, semilatticeInf := semilatticeInf_1, orderBot := orderBot_1, predOrder := predOrder_1,
        isPredArchimedean := isPredArchimedean_1 } →
    α = α_1 ∧ semilatticeInf ≍ semilatticeInf_1 ∧ orderBot ≍ orderBot_1 ∧ predOrder ≍ predOrder_1
-- Mathlib.RingTheory.Congruence.Basic
RingCon.ringConGen_monotone : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R], Monotone ringConGen
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin_symm_apply_succ : ∀ {n : ℕ} (e : Equiv.Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n),
  (Equiv.Perm.decomposeFin.symm (p, e)) x.succ = (Equiv.swap 0 p) (e x).succ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (vec : aig.RefVec w)
  (idx w_1 : ℕ) (vec_1 : aig.RefVec w_1) (idx_1 : ℕ),
  ({ w := w, vec := vec, idx := idx } = { w := w_1, vec := vec_1, idx := idx_1 }) =
    (w = w_1 ∧ vec ≍ vec_1 ∧ idx = idx_1)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.below.of_limitPresentation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.limitsClosure J a → Prop} {X : C} {a : α}
  (pres : CategoryTheory.Limits.LimitPresentation (J a) X) (h : ∀ (j : J a), P.limitsClosure J (pres.diag.obj j)),
  (∀ (j : J a), CategoryTheory.ObjectProperty.limitsClosure.below ⋯) →
    (∀ (j : J a), motive (pres.diag.obj j) ⋯) → CategoryTheory.ObjectProperty.limitsClosure.below ⋯
-- Mathlib.Logic.IsEmpty.Defs
Fin.isEmpty' : IsEmpty (Fin Nat.zero)
-- Lean.Data.AssocList
Lean.AssocList.contains : {α : Type u} → {β : Type v} → [BEq α] → α → Lean.AssocList α β → Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Y_eq_of_equiv : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P ≈ Q → P 1 * Q 2 = Q 1 * P 2
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.num.inj : ∀ {i i_1 : ℕ}, Nat.Internal.SOM.Expr.num i = Nat.Internal.SOM.Expr.num i_1 → i = i_1
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_addMonoidHom_trans : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Lean.CoreM
Lean.diagnostics : Lean.Option Bool
-- Mathlib.Algebra.Ring.Ext
CommRing.toRing_injective : ∀ {R : Type u}, Function.Injective (@CommRing.toRing R)
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer_le : ∀ {M : Type u_1} {S T : Set M} [inst : AddMonoid M], S ⊆ T → AddSubmonoid.centralizer T ≤ AddSubmonoid.centralizer S
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.base.inj : ∀ {m m_1 : Aesop.BaseRuleSetMember}, Aesop.GlobalRuleSetMember.base m = Aesop.GlobalRuleSetMember.base m_1 → m = m_1
-- Mathlib.Topology.Closure
IsClosed.closure_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s → closure s = s
-- Init.Data.String.Basic
String.Slice.Pos.utf8Encode_get_eq_extract : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  [pos.get h].utf8Encode =
    s.str.toByteArray.extract (s.startInclusive.offset.byteIdx + pos.offset.byteIdx)
      (s.startInclusive.offset.byteIdx + pos.offset.byteIdx + (pos.get h).utf8Size)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.PosDef.nonneg : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {Q : QuadraticMap R₂ M N},
  Q.PosDef → ∀ (x : M), 0 ≤ Q x
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_mk : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {v : ι → E} (hon : Orthonormal 𝕜 v)
  (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)), ⇑(OrthonormalBasis.mk hon hsp) = v
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- If `η` is an oplax transformation between `F` and `G`, we have a 1-morphism
`η.app a : F.obj a ⟶ G.obj a` for each object `a : B`. We also have a 2-morphism
`η.naturality f : F.map f ≫ app b ⟶ app a ≫ G.map f` for each 1-morphism `f : a ⟶ b`.
These 2-morphisms satisfy the naturality condition, and preserve the identities and
the compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Lax.OplaxTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.LaxFunctor B C → CategoryTheory.LaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBot'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : OrderBot β] (f : LatticeHom α β)
  (a : WithBot α), f.withBot' a = Option.elim a ⊥ ⇑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The inclusion and a conjugation commute.  -/
GroupExtension.inl_conjAct_comm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  (S : GroupExtension N E G) {e : E} {n : N}, S.inl ((S.conjAct e) n) = e * S.inl n * e⁻¹
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.map_apply : ∀ {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → AddCommMonoid (α i)]
  [inst_1 : (i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) (i : ι) (x : DirectSum ι fun i => α i),
  ((DirectSum.map f) x) i = (f i) (x i)
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.State.mk.sizeOf_spec : ∀ (atoms : Array Lean.Expr), sizeOf { atoms := atoms } = 1 + sizeOf atoms
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousOn.upperSemicontinuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ}, ContinuousOn f s → UpperSemicontinuousOn f s
-- Mathlib.Order.Compare
lt_iff_lt_of_cmp_eq_cmp : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : α} {β : Type u_3} [inst_1 : LinearOrder β] {x' y' : β},
  cmp x y = cmp x' y' → (x < y ↔ x' < y')
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The map that sends a vector `E` to the `fundamentalDomain` of the lattice,
see `ZSpan.fract_mem_fundamentalDomain`, and `fractRestrict` for the map with the codomain
restricted to `fundamentalDomain`.  -/
ZSpan.fract : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            Module.Basis ι K E →
              [inst_3 : LinearOrder K] → [IsStrictOrderedRing K] → [FloorRing K] → [Fintype ι] → E → E
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedCommMonoid.toUniqueUnits : {α : Type u} → [inst : Monoid α] → [inst_1 : PartialOrder α] → [CanonicallyOrderedMul α] → Unique αˣ
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One pair of implications of the portmanteau theorem:
For a sequence of Borel probability measures, the following two are equivalent:

(C) The limsup of the measures of any closed set is at most the measure of the closed set
under a candidate limit measure.

(O) The liminf of the measures of any open set is at least the measure of the open set
under a candidate limit measure.
 -/
MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2}
  {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)],
  (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) ↔
    ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.copy_eq : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} (f : TestFunction Ω F n) (f' : E → F)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_mul_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (U : ↥(unitary R)), ↑U * ↑(star U) = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.snd_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.snd = p.penultimate
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_inversion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c : P) {R : ℝ},
  R ≠ 0 → ∀ (x : P), EuclideanGeometry.inversion c R (EuclideanGeometry.inversion c R x) = x
-- Init.Data.UInt.Lemmas
USize.ofBitVec_mul : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a * b } = { toBitVec := a } * { toBitVec := b }
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inv_left : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (a : N ⋊[φ] G),
  a⁻¹.left = (φ a.right⁻¹) a.left⁻¹
-- Mathlib.Topology.DiscreteSubset
/-- In a T1Space, punctured neighborhoods are stable under removing finite sets of points.  -/
nhdsNE_of_nhdsNE_sdiff_finite : ∀ {X : Type u_3} [inst : TopologicalSpace X] [T1Space X] {x : X} {U s : Set X},
  U ∈ nhdsWithin x {x}ᶜ → Finite ↑s → U \ s ∈ nhdsWithin x {x}ᶜ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.spectrum_algebraMap_eq : ∀ {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 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] (r : R),
  spectrum R ((algebraMap R A) r) = {r}
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance is invariant under isometries.  -/
Metric.hausdorffDist_image : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {s t : Set α} {Φ : α → β},
  Isometry Φ → Metric.hausdorffDist (Φ '' s) (Φ '' t) = Metric.hausdorffDist s t
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y)
  (h : P.Factors f), CategoryTheory.CategoryStruct.comp (P.factorThru f h) P.arrow = f
-- Mathlib.Topology.MetricSpace.ProperSpace
proper_of_compact : ∀ {α : Type u} [inst : PseudoMetricSpace α] [CompactSpace α], ProperSpace α
-- Std.Tactic.BVDecide.Normalize.BitVec
/-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`.  -/
Std.Tactic.BVDecide.Normalize.BitVec.udiv_ofNat_eq_of_lt : ∀ (w : ℕ) (x : BitVec w) (n k : ℕ), 2 ^ k = n → k < w → x / BitVec.ofNat w n = x >>> k
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- Right homotopies are compatible with precomposition.  -/
HomotopicalAlgebra.PrepathObject.RightHomotopy.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      {P : HomotopicalAlgebra.PrepathObject Y} →
        {X : C} →
          {f g : X ⟶ Y} →
            P.RightHomotopy f g →
              {Z : C} →
                (i : Z ⟶ X) →
                  P.RightHomotopy (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)
-- Lean.Elab.InfoTree.Types
/-- Used instead of `TermInfo` when a term couldn't successfully be elaborated,
and so there is no complete expression available.

The main purpose of `PartialTermInfo` is to ensure that the sub-`InfoTree`s of a failed elaborator
are retained so that they can still be used in the language server.
 -/
Lean.Elab.PartialTermInfo : Type
-- Init.Data.String.Lemmas.Splits
String.copy_sliceTo_cast : ∀ {s t : String} (hst : s = t) {pos : s.Pos}, (t.sliceTo (pos.cast hst)).copy = (s.sliceTo pos).copy
-- Mathlib.Algebra.Category.Grp.Ulift
AddCommGrpCat.uliftFunctor_preservesLimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J AddCommGrpCat),
  CategoryTheory.Limits.PreservesLimit K AddCommGrpCat.uliftFunctor
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.instGeometricallyIrreducibleMorphismRestrict : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (V : S.Opens) [AlgebraicGeometry.GeometricallyIrreducible f],
  AlgebraicGeometry.GeometricallyIrreducible (f ∣_ V)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_insert_of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp]
  (t : RBTree.RBMap α β cmp), cmp k' k = Ordering.eq → (t.insert k v).find? k' = some v
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} [S.HasHomology] (h : S.LeftHomologyData),
  S.Exact ↔ CategoryTheory.Limits.IsZero h.H
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isMulRightInvariant_smul_nnreal : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant]
  (c : NNReal), (c • μ).IsMulRightInvariant
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_isStableUnderCobaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  T.llp.IsStableUnderCobaseChange
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
ftaylorSeriesWithin_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E}, ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.coe_fn_coe : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : DistribMulAction M A] {B : Type u_5} [inst_4 : AddMonoid B] [inst_5 : DistribMulAction N B]
  (f : A →ₑ+[φ] B), ⇑↑f = ⇑f
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inl_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (x : α), (OrderMonoidHom.inl α β) x = (x, 1)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Ici.sizeOf_spec : ∀ (n : Lean.Term), sizeOf (BigOperators.FinsetResult.Ici✝ n) = 1 + sizeOf n
-- Batteries.Data.DList.Lemmas
Batteries.DList.append.eq_1 : ∀ {α : Type u} (f : List α → List α) (h₁ : ∀ (l : List α), f l = f [] ++ l) (g : List α → List α)
  (h₂ : ∀ (l : List α), g l = g [] ++ l),
  { apply := f, invariant := h₁ }.append { apply := g, invariant := h₂ } = { apply := f ∘ g, invariant := ⋯ }
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.instInhabitedDescr : {α β σ : Type} → [Inhabited α] → Inhabited (Lean.ScopedEnvExtension.Descr α β σ)
-- Std.Tactic.Do.Syntax
/-- `mleft` is like `left`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
  mintro HP
  mleft
  mexact HP
```
 -/
Lean.Parser.Tactic.mleft : Lean.ParserDescr
-- Mathlib.Tactic.Sat.FromLRAT
/-- The bound variable index of the hypothesis asserting `⊢ ctx.proof c`,
_counting from the outside and 1-based_. (We use this numbering because we will need to
reference the variable from multiple binder depths.)  -/
Mathlib.Tactic.Sat.LClause.depth : Mathlib.Tactic.Sat.LClause → ℕ
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim_hom_π_π_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape K C] (j : J) (k : K) {Z : C} (h : (F.obj j).obj k ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitFlipCompLimIsoLimitCompLim F).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.obj j) k) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.comp CategoryTheory.Limits.lim) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.flip.obj k) j) h)
-- Mathlib.Probability.Martingale.Convergence
MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Submartingale f ℱ μ →
    MeasureTheory.UniformIntegrable f 1 μ →
      ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds (MeasureTheory.Filtration.limitProcess f ℱ μ ω))
-- Std.Internal.UV.TCP
_private.Std.Internal.UV.TCP.0.Std.Internal.UV.TCP.SocketImpl : NonemptyType
-- Mathlib.NumberTheory.PrimeCounting
Nat.notMem_primesLE : ∀ (n : ℕ), n + 1 ∉ n.primesLE
-- Init.Prelude
/-- `` `num `` is the node kind of number literals like `42` and `0xa1`  -/
Lean.numLitKind : Lean.SyntaxNodeKind