mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.Lattice
SupHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] {g₁ g₂ : SupHom β γ}
  {f : SupHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Computability.Partrec
Computable.list_ofFn : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
  (∀ (i : Fin n), Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionContext.toJson : Lean.Lsp.CodeActionContext → Lean.Json
-- Init.Data.SInt.Lemmas
Int32.iSizeMinValue_le_toInt : ∀ (x : Int32), ISize.minValue.toInt ≤ x.toInt
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_foldrM_fold : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → α → β → m β) (xs : Array α) (stop i : ℕ)
  (h : i ≤ xs.size) (b : β), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.foldrM.fold (f x) xs stop i h b
-- Mathlib.Topology.Category.TopCat.Opens
/-- The functor `Opens X ⥤ Opens X` given by taking preimages under the identity function
is naturally isomorphic to the identity functor.
 -/
TopologicalSpace.Opens.mapId : (X : TopCat) →
  TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X) ≅
    CategoryTheory.Functor.id (TopologicalSpace.Opens ↑X)
-- Init.Data.UInt.BasicAux
instAddUSize : Add USize
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.card_support_eq_three : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → p.support.card = 3
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.splitToSubslice.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} (s : String.Slice) (pat : ρ)
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ],
  s.splitToSubslice pat =
    {
      internalState :=
        String.Slice.SplitIterator.operating s.startPos (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s) }
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticWithinAt.zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {s : Set E} {n : ℤ}, AnalyticWithinAt 𝕜 f s z → 0 ≤ n → AnalyticWithinAt 𝕜 (f ^ n) s z
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_false_iff_two_mul_lt : ∀ {w : ℕ} {x : BitVec w}, x.msb = false ↔ 2 * x.toNat < 2 ^ w
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instSDiff : {V : Type u} → {G : SimpleGraph V} → SDiff G.Finsubgraph
-- Mathlib.Data.ULift
PLift.instUnique : {α : Sort u} → [Unique α] → Unique (PLift α)
-- Mathlib.CategoryTheory.Category.Preorder
Monotone.functor_obj : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] {f : X → Y} (h : Monotone f), h.functor.obj = f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst.inj : ∀ {n n_1 : ℕ},
  Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n = Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst n_1 → n = n_1
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.below.emptyWff : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2}
  {motive : (a : Lean.PrefixTreeNode α β cmp) → Lean.PrefixTreeNode.WellFormed cmp a → Prop},
  Lean.PrefixTreeNode.WellFormed.below ⋯
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coprodSubtypeLEquivOfIsCompl.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f : E →L[𝕜] F) {G : Submodule 𝕜 F} (h : IsCompl (↑f).range G)
  [inst_7 : CompleteSpace ↥G] (hker : (↑f).ker = ⊥),
  f.coprodSubtypeLEquivOfIsCompl h hker = ContinuousLinearEquiv.ofBijective (f.coprod G.subtypeL) ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensor_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).f = CategoryTheory.MonoidalCategoryStruct.tensorHom f.f g.f
-- Mathlib.Data.Finset.Range
coe_notMemRangeEquiv_symm : ∀ (k : ℕ), ⇑(notMemRangeEquiv k).symm = fun j => ⟨j + k, ⋯⟩
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l →
      k ∈ l → ∀ {h' : k' ∈ Std.HashSet.Raw.ofList l}, (Std.HashSet.Raw.ofList l).get k' h' = k
-- Mathlib.Data.List.DropRight
List.rdrop_zero : ∀ {α : Type u_1} (l : List α), l.rdrop 0 = l
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal : ∀ (R : Type u) [inst : CommSemiring R] (t : Set (PrimeSpectrum R)) (s : Set R),
  t ⊆ PrimeSpectrum.zeroLocus s ↔ s ⊆ ↑(PrimeSpectrum.vanishingIdeal t)
-- Init.Data.List.Lex
List.lex.eq_2 : ∀ {α : Type u} [inst : BEq α] (l₁ : List α) (lt : α → α → Bool), l₁.lex [] lt = false
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.extern.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (externAttrData externAttrData_1 : Lean.ExternAttrData),
  (Lean.Compiler.LCNF.DeclValue.extern externAttrData = Lean.Compiler.LCNF.DeclValue.extern externAttrData_1) =
    (externAttrData = externAttrData_1)
-- Init.Data.Int.DivMod.Lemmas
Int.self_le_ediv_of_nonpos_of_nonneg : ∀ {x y : ℤ}, x ≤ 0 → 0 ≤ y → x ≤ x / y
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasFiniteColimits : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasFiniteColimits T],
  CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Arrow T)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Return the maximum generation allowed for the current theorem.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.getMaxGeneration : Lean.Meta.Grind.EMatch.M ℕ
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.PrelocalPredicate.mk.sizeOf_spec : ∀ {X : TopCat} {T : ↑X → Type u_1} [inst : (a : ↑X) → SizeOf (T a)]
  (pred : {U : TopologicalSpace.Opens ↑X} → ((x : ↥U) → T ↑x) → Prop)
  (res : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (f : (x : ↥V) → T ↑x), pred f → pred fun x => f (i x)),
  sizeOf { pred := pred, res := res } = 1
-- Mathlib.Analysis.Analytic.Basic
/-- If a function `f` has a power series `p` on a ball and `g` is linear, then `g ∘ f` has the
power series `g ∘ p` on the same ball.  -/
ContinuousLinearMap.comp_hasFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}
  {r : ENNReal} (g : F →L[𝕜] G),
  HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall (⇑g ∘ f) (g.compFormalMultilinearSeries p) x r
-- Mathlib.MeasureTheory.Integral.Marginal
/-- Peel off a single integral from a `lmarginal` integral at the end (compare with
`lmarginal_erase`, which peels off an integral at the beginning).  -/
MeasureTheory.lmarginal_erase' : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] {s : Finset δ} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (f : ((i : δ) → X i) → ENNReal),
  Measurable f →
    ∀ {i : δ}, i ∈ s → ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x => ∫⁻ (xᵢ : X i), f (Function.update x i xᵢ) ∂μ i ∂μ
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence],
  F.ReflectsEffectiveEpiFamilies
-- Mathlib.Data.ENat.BigOperators
/-- A sum is infinite iff one of the summands is infinite.  -/
ENat.sum_eq_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, ∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
-- Qq.SortLocalDecls
Qq.SortLocalDecls.visitLocalDecl : Lean.LocalDecl → Qq.SortLocalDecls.M Unit
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.forget₁_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {X Y : CategoryTheory.Bicategory.Adj B} (x : X ⟶ Y),
  CategoryTheory.Bicategory.Adj.forget₁.map x = x.l
-- Mathlib.Analysis.Convex.Combination
convexHull_multiset_sum : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Multiset (Set E)),
  (convexHull R) s.sum = (Multiset.map (⇑(convexHull R)) s).sum
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.bell_succ' : ∀ (n : ℕ), (n + 1).bell = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 * ij.2.bell
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow_of_exponent_ge : ∀ {x y z : ℝ}, 0 < x → x ≤ 1 → z ≤ y → x ^ y ≤ x ^ z
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The `Meta.Config` used by this entry.  -/
Lean.Meta.RefinedDiscrTree.ExprInfo.cfg : Lean.Meta.RefinedDiscrTree.ExprInfo → Lean.Meta.Config
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.run : Lean.Elab.Command.ModuleLinter → Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Logic.Function.Basic
Function.Surjective.exists : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Surjective f → ∀ {p : β → Prop}, (∃ y, p y) ↔ ∃ x, p (f x)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_3.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_tendsto_atBot_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜], Filter.Tendsto (fun x => |Polynomial.eval x P|) Filter.atBot Filter.atTop ↔ 0 < P.degree
-- Mathlib.Algebra.GroupWithZero.Idempotent
IsIdempotentElem.iff_eq_zero_or_one : ∀ {G₀ : Type u_2} [inst : MonoidWithZero G₀] [IsLeftCancelMulZero G₀] {p : G₀}, IsIdempotentElem p ↔ p = 0 ∨ p = 1
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `lipschitzWith_inv_iff`. -/
LipschitzWith.inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  LipschitzWith K f → LipschitzWith K f⁻¹
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_lt_top_of_finite : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} [Finite α] [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.eLpNorm f p μ < ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  k ∈ (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl ↔ (f (t.get? k)).isSome = true
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find.eq_1 : ∀ (self : Batteries.UnionFind) (x : Fin self.size),
  self.find x = ⟨{ arr := (self.findAux x).s, parentD_lt := ⋯, rankD_lt := ⋯ }, ⟨⟨↑(self.findAux x).root, ⋯⟩, ⋯⟩⟩
-- Mathlib.FieldTheory.Fixed
FixedPoints.coe_algebraMap : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F],
  algebraMap (↥(FixedPoints.subfield M F)) F = (FixedPoints.subfield M F).subtype
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_reachable_of_right_degree_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : Fintype ↑(G.neighborSet v)],
  u ≠ v → G.degree v = 0 → ¬G.Reachable u v
-- Init.Data.SInt.Lemmas
Int16.toISize_ne_minValue : ∀ (a : Int16), a.toISize ≠ ISize.minValue
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul₂.mk : ∀ {M : Type u_2} [inst : MeasurableSpace M] [inst_1 : Mul M], (Measurable fun p => p.1 * p.2) → MeasurableMul₂ M
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.two_mul_C_half_eq_one : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2], 2 * Polynomial.C ⅟2 = 1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.erase_same : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (Polynomial.erase n p).coeff n = 0
-- Mathlib.ModelTheory.Definability
/-- A `TermDefinable₁` function has a graph that's `Definable₂`.  -/
Set.TermDefinable₁.definable₂_graph : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {f : M → M},
  Set.TermDefinable₁ L f → A.Definable₂ L (Function.graph f)
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.getAppArgsN.loop : ℕ → Lean.Expr → Array Lean.Expr → Array Lean.Expr
-- Mathlib.Algebra.Algebra.Unitization
Unitization.ext : ∀ {R : Type u_1} {A : Type u_2} {x y : Unitization R A}, x.toProd.1 = y.toProd.1 → x.toProd.2 = y.toProd.2 → x = y
-- Mathlib.Algebra.MvPolynomial.Eval
/-- `MvPolynomial.eval₂` as a `RingHom`.  -/
MvPolynomial.eval₂Hom : {R : Type u} →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] → [inst_1 : CommSemiring S₁] → (R →+* S₁) → (σ → S₁) → MvPolynomial σ R →+* S₁
-- Lean.Server.Completion.CompletionCollectors
/-- Generate completion items for a syntax object generated by `identWithPartialTrailingDot` given a
known collection of completion candidates. Should only be used in contexts where namespaces do not
affect the set of eligible completion candidates.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.trailingDotCompletion : {Coll : Type u_1} →
  {α : Type u_2} →
    [ForIn Id Coll (Lean.Name × α)] →
      Coll →
        Lean.Syntax →
          Lean.Lsp.ClientCapabilities →
            Lean.Elab.ContextInfo →
              (Lean.Name → α → Option Lean.Lsp.InsertReplaceEdit → Lean.Lsp.ResolvableCompletionItem) →
                Array Lean.Lsp.ResolvableCompletionItem
-- Init.Data.Nat.Fold
Nat.all_succ : ∀ {n : ℕ} (f : (i : ℕ) → i < n + 1 → Bool), (n + 1).all f = ((n.all fun i h => f i ⋯) && f n ⋯)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.pullback_sieve₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) {T : C} (f : T ⟶ W),
  CategoryTheory.Sieve.pullback f (E.sieve₁ p₁ p₂) =
    E.sieve₁ (CategoryTheory.CategoryStruct.comp f p₁) (CategoryTheory.CategoryStruct.comp f p₂)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (f : α →*o β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.RingTheory.Nilpotent.Exp
IsNilpotent.exp.eq_1 : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Module ℚ A] (a : A),
  IsNilpotent.exp a = ∑ i ∈ Finset.range (nilpotencyClass a), (↑i.factorial)⁻¹ • a ^ i
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.MeasuredSets.real_sub_real_le_dist : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  (s t : MeasureTheory.MeasuredSets μ), μ.real ↑s - μ.real ↑t ≤ dist s t
-- Lean.DocString.Markdown
/-- Concatenates two strings that are the result of rendering consecutive inliens, inserting a U+200B
zero-width space when both concatenated ends are backticks. Markdown has no syntactic way to place
two code spans consecutively, so the zero-width space disambiguates them without introducing visible
whitespace.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.glueInlineBoundary : String → String → String
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  k ∈ m₂ → Std.DHashMap.Const.get! (m₁.inter m₂) k = Std.DHashMap.Const.get! m₁ k
-- Mathlib.Algebra.Tropical.Basic
Tropical.tropOrderIso_coe_fn : ∀ {R : Type u} [inst : Preorder R], ⇑Tropical.tropOrderIso = Tropical.trop
-- Mathlib.Order.WithBot
Equiv.withBotCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a : WithBot α), e.withBotCongr a = WithBot.map (⇑e) a
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instAddCommMonoid : {𝕜 : Type u_2} →
  {E : Type u_1} →
    {F : Type u_3} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : AddCommMonoid F] → [inst_4 : Module 𝕜 F] → (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → AddCommMonoid (WeakBilin B)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.coeFn_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7}
  [inst_1 : NormedAddCommGroup G] [inst_2 : PartialOrder G] (f : ↥(MeasureTheory.Lp.simpleFunc G p μ)),
  0 ≤ᵐ[μ] ↑↑↑f ↔ 0 ≤ f
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- a map `I₂ × I₃ → I₂₃`  -/
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.p : {I₁ : Type u_7} →
  {I₂ : Type u_8} →
    {I₃ : Type u_9} →
      {J : Type u_10} →
        {r : I₁ × I₂ × I₃ → J} → (self : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) → I₂ × I₃ → self.I₂₃
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_le : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {a : α} {b : β}, a ≤ u b → l a ≤ b
-- Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus
/-- The right derived functor `DerivedCategory.Plus C ⥤ DerivedCategory.Plus D`
when `F : C ⥤ D` is an additive functor between abelian categories and
`C` has enough injectives.  -/
CategoryTheory.Functor.rightDerivedFunctorPlus : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.Abelian D] →
            [inst_4 : HasDerivedCategory C] →
              [inst_5 : HasDerivedCategory D] →
                (F : CategoryTheory.Functor C D) →
                  [F.Additive] →
                    [CategoryTheory.EnoughInjectives C] →
                      CategoryTheory.Functor (DerivedCategory.Plus C) (DerivedCategory.Plus D)
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- In a normed algebra `F` over a normed field `𝕜` that is a proper space, the function
`z : 𝕜 ↦ ‖x - algebraMap 𝕜 F z‖` achieves a global minimum for every `x : F`.  -/
NormedAlgebra.exists_isMinOn_norm_sub_smul : ∀ (𝕜 : Type u_1) {F : Type u_2} [inst : NormedField 𝕜] [ProperSpace 𝕜] [inst_2 : SeminormedRing F]
  [inst_3 : NormedAlgebra 𝕜 F] [NormOneClass F] (x : F), ∃ z, IsMinOn (fun x_1 => ‖x - (algebraMap 𝕜 F) x_1‖) Set.univ z
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.nonneg_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E), 0 ≤ f.normed μ x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : IntermediateField F E},
  Module.finrank F ↥K = 1 ↔ K = ⊥
-- Mathlib.Tactic.Explode.Datatypes
/-- `Entry.depth` * `│` + `├` Continuation intro  -/
Mathlib.Explode.Status.cintro : Mathlib.Explode.Status
-- Mathlib.Algebra.Group.Ideal
/-- The semigroup ideal generated by a set `s`.  -/
SemigroupIdeal.closure : {M : Type u_1} → [inst : Mul M] → Set M → SemigroupIdeal M
-- Mathlib.CategoryTheory.Category.Pairwise
/-- Given a function `U : ι → α` for `[SemilatticeInf α]`, we obtain a functor
`CategoryTheory.Pairwise ι ⥤ α`,
sending `single i` to `U i` and `pair i j` to `U i ⊓ U j`,
and the morphisms to the obvious inequalities.
 -/
CategoryTheory.Pairwise.diagram : {ι : Type v} → {α : Type u} → (ι → α) → [inst : SemilatticeInf α] → CategoryTheory.Functor (CategoryTheory.Pairwise ι) α
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₃_eq_some_iff_utf8EncodeChar_eq : ∀ {w x y : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.twoMore ∧
      ByteArray.utf8DecodeChar?.assemble₃ w x y = some c ↔
    String.utf8EncodeChar c = [w, x, y]
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.functorEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (F : CategoryTheory.Functor C D), CategoryTheory.FreeGroupoid.functorEquiv.symm F = CategoryTheory.FreeGroupoid.lift F
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
/-- The presheaf of dependently typed functions on `X`, with fibres given by a type family `T`.
There is no requirement that the functions are continuous, here.
 -/
TopCat.presheafToTypes : (X : TopCat) → (↑X → Type u_1) → TopCat.Presheaf (Type (max u_1 u_2)) X
-- Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
PiTensorProduct.ofDFinsuppEquiv_tprod_single : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i)
  (x : (i : ι) → M i (p i)),
  PiTensorProduct.ofDFinsuppEquiv ((PiTensorProduct.tprod R) fun i => fun₀ | p i => x i) =
    fun₀ | p => (PiTensorProduct.tprod R) fun i => x i
-- Mathlib.Data.Set.Function
Set.InvOn.symm : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.InvOn f' f s t → Set.InvOn f f' t s
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_X_sub_C : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.Splits → ∀ (a : R), (f.comp (Polynomial.X - Polynomial.C a)).Splits
-- Mathlib.NumberTheory.NumberField.AdeleRing
/-- `𝔸[K]` is notation for `NumberField.AdeleRing (𝓞 K) K`.  -/
NumberField.AdeleRing.«term𝔸[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.mk : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {A B : CategoryTheory.Limits.Cocone F} →
            (hom : A.pt ⟶ B.pt) →
              autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom = B.ι.app j)
                  CategoryTheory.Limits.CoconeMorphism.w._autoParam →
                CategoryTheory.Limits.CoconeMorphism A B