mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.Omega.OmegaM
Lean.Elab.Tactic.Omega.Context.mk : Lean.Meta.Omega.OmegaConfig → Lean.Elab.Tactic.Omega.Context
-- Mathlib.Analysis.Distribution.Support
Distribution.TemperedDistribution.dsupport_lineDerivOp_subset : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℂ F] {f : TemperedDistribution E F} (m : E),
  Distribution.dsupport ⇑(LineDeriv.lineDerivOp m f) ⊆ Distribution.dsupport ⇑f
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.Algebra.Polynomial.Lifts
/-- If `R` and `S` are rings, `p` is in the subring of polynomials that lift if and only if it is in
the subsemiring of polynomials that lift.  -/
Polynomial.lifts_iff_liftsRing : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (f : R →+* S) (p : Polynomial S),
  p ∈ Polynomial.lifts f ↔ p ∈ Polynomial.liftsRing f
-- Aesop.Search.Expansion.Norm
Aesop.NormStep.unfold : Aesop.NormStep
-- Mathlib.Data.Finset.Insert
Finset.toList_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Finset α}, a ∉ s → (insert a s).toList.Perm (a :: s.toList)
-- Mathlib.Data.Finsupp.Defs
Finsupp.mk.inj : ∀ {α : Type u_9} {M : Type u_10} {inst : Zero M} {support : Finset α} {toFun : α → M}
  {mem_support_toFun : ∀ (a : α), a ∈ support ↔ toFun a ≠ 0} {support_1 : Finset α} {toFun_1 : α → M}
  {mem_support_toFun_1 : ∀ (a : α), a ∈ support_1 ↔ toFun_1 a ≠ 0},
  { support := support, toFun := toFun, mem_support_toFun := mem_support_toFun } =
      { support := support_1, toFun := toFun_1, mem_support_toFun := mem_support_toFun_1 } →
    support = support_1 ∧ toFun = toFun_1
-- Mathlib.Order.SupClosed
LinearOrder.isSublattice : ∀ {α : Type u_3} [inst : LinearOrder α] (s : Set α), IsSublattice s
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff_k : Int.Internal.Linear.Poly → Int.Internal.Linear.Var → ℤ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.rhs : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.Poly
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffWithinAt.iteratedFDerivWithin_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x₀ : E}
  {m n : WithTop ℕ∞} {i : ℕ},
  ContDiffWithinAt 𝕜 n f s x₀ →
    UniqueDiffOn 𝕜 s → m + ↑i ≤ n → x₀ ∈ s → ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f s) s x₀
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.maxEntry? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Init.Prelude
instAddNat : Add ℕ
-- Init.Data.Int.Lemmas
Int.eq_neg_comm : ∀ {a b : ℤ}, a = -b ↔ b = -a
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.eq_zero : ∀ {R : Type u_3} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [IsReduced R], IsNilpotent x → x = 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A commutative monoid object is a monoid object in the category of monoid objects.  -/
CategoryTheory.Mon.instMonObjOfIsCommMonObjX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M : CategoryTheory.Mon C} → [CategoryTheory.IsCommMonObj M.X] → CategoryTheory.MonObj M
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
measurable_fderiv_apply_const : ∀ (𝕜 : 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)
  [inst_5 : MeasurableSpace E] [OpensMeasurableSpace E] [CompleteSpace F] [inst_8 : MeasurableSpace F] [BorelSpace F]
  (y : E), Measurable fun x => (fderiv 𝕜 f x) y
-- Mathlib.Topology.Inseparable
continuous_congr_of_inseparable : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : X → Y},
  (∀ (x : X), Inseparable (f x) (g x)) → (Continuous f ↔ Continuous g)
-- Mathlib.RingTheory.RingInvo
/-- `RingInvoClass F R` states that `F` is a type of ring involutions.
You should extend this class when you extend `RingInvo`.  -/
RingInvoClass : (F : Type u_3) → (R : Type u_4) → [Semiring R] → [EquivLike F R Rᵐᵒᵖ] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The trivial factorisation of a monomorphism satisfies the universal property.  -/
CategoryTheory.Limits.IsImage.self : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Mono f] →
          CategoryTheory.Limits.IsImage (CategoryTheory.Limits.MonoFactorisation.self f)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.ofRingEquiv : ∀ {F : Type u_1} [inst : Field F] {K : Type u_2} [inst_1 : Field K] [NumberField.IsTotallyReal F] (f : F ≃+* K),
  NumberField.IsTotallyReal K
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_map_of_gt : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) (j : Fin (n + 2)),
  i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) self.map = SSet.const x
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Given `f : α → β` with `β` an additive group, the canonical map
`List (α × Bool) → β`  -/
FreeAddGroup.Lift.aux : {α : Type u} → {β : Type v} → [AddGroup β] → (α → β) → List (α × Bool) → β
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The inverse Fourier transform from `L1` functions to bounded continuous functions as a
continuous linear map.  -/
Real.Lp.fourierTransformInvCLM : (V : Type u_1) →
  (E : Type u_3) →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℂ E] →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [inst_4 : MeasurableSpace V] →
              [inst_5 : BorelSpace V] →
                [inst_6 : FiniteDimensional ℝ V] →
                  ↥(MeasureTheory.Lp E 1 MeasureTheory.volume) →L[ℂ] BoundedContinuousFunction V E
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal : ∀ {X : AlgebraicGeometry.Scheme} (Z : TopologicalSpace.Closeds ↥X),
  ↑(AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z).support = ↑Z
-- Init.Prelude
ReaderT.instMonad : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → Monad (ReaderT ρ m)
-- Mathlib.Order.CountableSupClosed
/-- **Alias** of the reverse direction of `countableInfClosure_eq_self`. -/
CountableInfClosed.countableInfClosure_eq : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], CountableInfClosed s → countableInfClosure s = s
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_inj : ∀ {a b : Cardinal.{u}}, Cardinal.lift.{v, u} a = Cardinal.lift.{v, u} b ↔ a = b
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.mangleAux.eq_def : ∀ (s : String) (pos : s.Pos) (r : String),
  String.mangleAux✝ s pos r =
    if h : pos = s.endPos then r
    else
      have c := pos.get h;
      have pos := pos.next h;
      if (c.isAlpha || c.isDigit) = true then String.mangleAux✝ s pos (r.push c)
      else
        if c = '_' then String.mangleAux✝ s pos (r ++ "__")
        else
          if c.toNat < 256 then String.mangleAux✝ s pos (String.pushHex✝ 2 c.val (r ++ "_x"))
          else
            if c.toNat < 65536 then String.mangleAux✝ s pos (String.pushHex✝ 4 c.val (r ++ "_u"))
            else String.mangleAux✝ s pos (String.pushHex✝ 8 c.val (r ++ "_U"))
-- Mathlib.Algebra.Order.Module.Equiv
coe_toLexLinearEquiv : ∀ (α : Type u_1) (β : Type u_2) [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β],
  ⇑(toLexLinearEquiv α β) = ⇑toLex
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_natCast : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : ℕ), (↑n).untop₀ = ↑n
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.instFunLikeContMDiffMapRealModelWithCornersSelfSomeENatTop : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    {s : Set M} →
                      FunLike (SmoothPartitionOfUnity ι I M s) ι (ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤)
-- Mathlib.Order.RelIso.Basic
RelIso.refl_apply : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), (RelIso.refl r) a = a
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.mem_iff : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R ↔ A * Matrix.J l R * A.transpose = Matrix.J l R
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.instAddAction : {α : Type u_1} → {f : α → α} → AddAction (IterateAddAct f) α
-- Init.Data.List.Lemmas
List.get_cons_succ : ∀ {α : Type u_1} {i : ℕ} {a : α} {as : List α} {h : i + 1 < (a :: as).length}, (a :: as).get ⟨i + 1, h⟩ = as.get ⟨i, ⋯⟩
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lmarginal_univ : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [inst_3 : Fintype δ]
  {f : ((i : δ) → X i) → ENNReal},
  ∫⋯∫⁻_Finset.univ, f ∂μ = fun x => ∫⁻ (x : (i : δ) → X i), f x ∂MeasureTheory.Measure.pi μ
-- Lean.Meta.Tactic.Apply
/-- Close the given goal using `e`, instantiated with `n` metavariables.  -/
Lean.MVarId.applyN : Lean.MVarId → Lean.Expr → ℕ → optParam Bool true → Lean.MetaM (List Lean.MVarId)
-- Mathlib.Order.Lattice
/-- A subtype forms a lattice if `⊔` and `⊓` preserve the property.
See note [reducible non-instances].  -/
Subtype.lattice : {α : Type u} →
  [inst : Lattice α] →
    {P : α → Prop} → (∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) → (∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) → Lattice { x // P x }
-- Lean.MetavarContext
Lean.MonadMCtx.mk : {m : Type → Type} → m Lean.MetavarContext → ((Lean.MetavarContext → Lean.MetavarContext) → m Unit) → Lean.MonadMCtx m
-- Std.Async.System
Std.Async.System.instInhabitedCPUTimes : Inhabited Std.Async.System.CPUTimes
-- Init.Data.String.Lemmas.Pattern.Memcmp
_private.Init.Data.String.Lemmas.Pattern.Memcmp.0.String.Slice.Pattern.Internal.memcmpStr.eq_1 : ∀ (lhs rhs : String) (lstart rstart len : String.Pos.Raw) (h1 : len.offsetBy lstart ≤ lhs.rawEndPos)
  (h2 : len.offsetBy rstart ≤ rhs.rawEndPos),
  String.Slice.Pattern.Internal.memcmpStr lhs rhs lstart rstart len h1 h2 =
    String.Slice.Pattern.Internal.memcmpStr.go✝ lhs rhs lstart rstart len h1 h2 0
-- Mathlib.CategoryTheory.Sites.Subsheaf
/-- The image sheaf of a morphism between sheaves, defined to be the sheafification of
`image_presheaf`.  -/
CategoryTheory.Sheaf.image : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {F F' : CategoryTheory.Sheaf J (Type w)} → (F ⟶ F') → CategoryTheory.Sheaf J (Type w)
-- Std.Http.Data.URI.Basic
Std.Http.URI.Builder.mk.injEq : ∀ (scheme : Option Std.Http.URI.Scheme) (userInfo : Option Std.Http.URI.UserInfo) (host : Option Std.Http.URI.Host)
  (port : Std.Http.URI.Port) (pathSegments : Array String) (query : Array (String × Option String))
  (fragment : Option String) (scheme_1 : Option Std.Http.URI.Scheme) (userInfo_1 : Option Std.Http.URI.UserInfo)
  (host_1 : Option Std.Http.URI.Host) (port_1 : Std.Http.URI.Port) (pathSegments_1 : Array String)
  (query_1 : Array (String × Option String)) (fragment_1 : Option String),
  ({ scheme := scheme, userInfo := userInfo, host := host, port := port, pathSegments := pathSegments, query := query,
        fragment := fragment } =
      { scheme := scheme_1, userInfo := userInfo_1, host := host_1, port := port_1, pathSegments := pathSegments_1,
        query := query_1, fragment := fragment_1 }) =
    (scheme = scheme_1 ∧
      userInfo = userInfo_1 ∧
        host = host_1 ∧ port = port_1 ∧ pathSegments = pathSegments_1 ∧ query = query_1 ∧ fragment = fragment_1)
-- Lean.Server.Rpc.Basic
_private.Lean.Server.Rpc.Basic.0.Lean.Server.WithRpcRef.mk'.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (val : α) (id : USize), sizeOf { val := val, id := id } = 1 + sizeOf val + sizeOf id
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.add_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Add γ] [inst_4 : ContinuousAdd γ] (f₁ f₂ : C(β, γ)) (g : C(α, β)),
  (f₁ + f₂).comp g = f₁.comp g + f₂.comp g
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  t.isEmpty = true → (t.insertIfNew k v).minKey? = some k
-- Init.Data.Ord.UInt
USize.instLawfulEqOrd : Std.LawfulEqOrd USize
-- Mathlib.Order.Basic
not_lt_iff_eq_or_lt' : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, ¬b < a ↔ a = b ∨ a < b
-- Init.Data.Vector.Lemmas
Vector.set.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (x x_1 : α), x = x_1 → ∀ (h : i < n), xs.set i x h = xs_1.set i_1 x_1 ⋯
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.relations.id : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} (X : C),
  CategoryTheory.Localization.Construction.relations W
    (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.id X))
    (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X))
-- Mathlib.Topology.Algebra.Ring.Real
Real.uniformContinuous_const_mul : ∀ {x : ℝ}, UniformContinuous fun x_1 => x * x_1
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorems.mk.inj : ∀ {tree : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem} {erased : Lean.PHashSet Lean.Name}
  {tree_1 : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem} {erased_1 : Lean.PHashSet Lean.Name},
  { tree := tree, erased := erased } = { tree := tree_1, erased := erased_1 } → tree = tree_1 ∧ erased = erased_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).mor₂ = (t.truncGEπ b).app j
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.mk.injEq : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  (toLinearMap : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg' : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap)
  (toLinearMap_1 : A₁ →ₗ[ℂ] A₂)
  (map_cstarMatrix_nonneg'_1 : ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap_1),
  ({ toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } =
      { toLinearMap := toLinearMap_1, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'_1 }) =
    (toLinearMap = toLinearMap_1)
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.hyp.injEq : ∀ (fvarId fvarId_1 : Lean.FVarId),
  (Mathlib.Tactic.SplitPosition.hyp✝ fvarId = Mathlib.Tactic.SplitPosition.hyp✝ fvarId_1) = (fvarId = fvarId_1)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instToExprLinearExpr : Lean.ToExpr Lean.Meta.Simp.Arith.Nat.LinearExpr
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesRxoSize.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : Std.Rxo.HasSize α] [inst_3 : Std.Rxo.HasSize β] {f : Std.PRange.UpwardEnumerable.Map α β},
  (∀ {a b : α}, Std.Rxo.HasSize.size a b = Std.Rxo.HasSize.size (f.toFun a) (f.toFun b)) → f.PreservesRxoSize
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instTheoremLikeEMatchTheorem : Lean.Meta.Grind.TheoremLike Lean.Meta.Grind.EMatchTheorem
-- Init.Data.UInt.Lemmas
UInt8.le_refl : ∀ (a : UInt8), a ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is another convenient method to verify that a trident is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same `s` for all parts.  -/
CategoryTheory.Limits.Trident.IsLimit.mk' : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        {f : J → (X ⟶ Y)} →
          [Nonempty J] →
            (t : CategoryTheory.Limits.Trident f) →
              ((s : CategoryTheory.Limits.Trident f) →
                  { l //
                    CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧
                      ∀
                        {m :
                          ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.zero ⟶
                            ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj
                                  t.pt).obj
                              CategoryTheory.Limits.WalkingParallelFamily.zero},
                        CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = l }) →
                CategoryTheory.Limits.IsLimit t
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {a : α} {fallback : β},
  Std.ExtDTreeMap.Const.getD ∅ a fallback = fallback
-- Mathlib.Data.Nat.Log
Nat.clog_lt_clog_succ_iff : ∀ {b n : ℕ}, 1 < b → (Nat.clog b n < Nat.clog b (n + 1) ↔ b ^ Nat.clog b n = n)
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.tendsto_diracProba_iff_tendsto : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [CompletelyRegularSpace X] {x : X} (L : Filter X),
  Filter.Tendsto MeasureTheory.diracProba L (nhds (MeasureTheory.diracProba x)) ↔ Filter.Tendsto id L (nhds x)
-- Mathlib.Util.Export
Lean.Export.Entry.name : Lean.Name → Lean.Export.Entry
-- Mathlib.Lean.Meta
/-- Has the effect of `refine ⟨e₁,e₂,⋯, ?_⟩`.
 -/
Lean.MVarId.existsi : Lean.MVarId → List Lean.Expr → Lean.MetaM Lean.MVarId
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.mkEvalTactic : Lean.Meta.Grind.Params →
  Lean.Elab.Tactic.TacticM
    (Lean.Meta.Grind.Goal → Lean.TSyntax `grind → Lean.Meta.Grind.GrindM (List Lean.Meta.Grind.Goal))
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.add_assoc_rev : ∀ {R : Type u_1} [inst : CommSemiring R] (a b c : R), a + (b + c) = a + b + c
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.isRflProofCore : Bool → Lean.Expr → Lean.Expr → Lean.CoreM Bool
-- Init.Data.SInt.Lemmas
UInt64.toInt64_mul : ∀ (a b : UInt64), (a * b).toInt64 = a.toInt64 * b.toInt64
-- Init.GetElem
/-- The syntax `arr[i]?` gets the `i`'th element of the collection `arr`,
if it is present (and wraps it in `some`), and otherwise returns `none`.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]?` in identifiers is `getElem?`. -/
GetElem?.getElem? : {coll : Type u} →
  {idx : Type v} →
    {elem : outParam (Type w)} →
      {valid : outParam (coll → idx → Prop)} → [self : GetElem? coll idx elem valid] → coll → idx → Option elem
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The type of morphisms in `MonCat`.  -/
MonCat.Hom : MonCat → MonCat → Type u
-- Mathlib.Data.List.Cycle
List.prev_cons_cons_of_ne' : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x y z : α) (h : x ∈ y :: z :: l),
  x ≠ y → x = z → (y :: z :: l).prev x h = y
-- Init.Data.Array.Lemmas
Array.size_swapIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ}, (xs.swapIfInBounds i j).size = xs.size
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.ground_isFlat : ∀ {α : Type u_2} (M : Matroid α), M.IsFlat M.E
-- Mathlib.Topology.Instances.Rat
NNRat.instOrderTopology : OrderTopology ℚ≥0
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Construct a `Mor₂Iso` term from a Lean expression.  -/
Mathlib.Tactic.Monoidal.Mor₂IsoOfExpr : Lean.Expr → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- A smooth embedding is automatically smooth.  -/
Manifold.IsSmoothEmbedding.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} {E₃ : Type u_4} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : NormedAddCommGroup E₃] [inst_4 : NormedSpace 𝕜 E₃] {H : Type u_6} {G : Type u_8}
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E₁ H}
  {J : ModelWithCorners 𝕜 E₃ G} {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsSmoothEmbedding I J n f → ContMDiff I J n f
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.colimit_isOpen_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasColimit F] (U : Set ↑(CategoryTheory.Limits.colimit F)),
  IsOpen U ↔ ∀ (j : J), IsOpen (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) ⁻¹' U)
-- Mathlib.Order.WellFoundedSet
Set.WellFoundedOn.exists_maximal : ∀ {α : Type u_6} [inst : Preorder α] {s : Set α},
  (s.WellFoundedOn fun x1 x2 => x2 < x1) → s.Nonempty → ∃ a, Maximal (fun x => x ∈ s) a
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.IsRegularAtInfty.eq : ∀ {R : Type u_1} [inst : Ring R] (𝒢 : Subgroup (GL (Fin 2) R)), 𝒢.IsRegularAtInfty → 𝒢.strictPeriods = 𝒢.periods
-- Lean.Data.KVMap
Lean.DataValue.ofSyntax : Lean.Syntax → Lean.DataValue
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A function `f` continuous on a set `K` is locally integrable on this set with respect
to any locally finite measure.  -/
ContinuousOn.locallyIntegrableOn : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {K : Set X} {f : X → E}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E],
  ContinuousOn f K → MeasurableSet K → MeasureTheory.LocallyIntegrableOn f K μ