mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofDarts_singleton' : ∀ {V : Type u} {G : SimpleGraph V} (d : G.Dart), SimpleGraph.Walk.ofDarts [d] ⋯ ⋯ = ⋯.toWalk
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι),
  ((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f).f n).f = f.f.f n
-- Init.Data.List.Int.Sum
List.min_mul_length_le_sum_int : ∀ {xs : List ℤ} (h : xs ≠ []), xs.min h * ↑xs.length ≤ xs.sum
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- The radius of convergence of `ordinaryHypergeometricSeries` is unity if none of the parameters
are non-positive integers.  -/
ordinaryHypergeometricSeries_radius_eq_one : ∀ {𝕂 : Type u_1} (𝔸 : Type u_2) [inst : RCLike 𝕂] [inst_1 : NormedDivisionRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  (a b c : 𝕂), (∀ (kn : ℕ), ↑kn ≠ -a ∧ ↑kn ≠ -b ∧ ↑kn ≠ -c) → (ordinaryHypergeometricSeries 𝔸 a b c).radius = 1
-- Mathlib.Order.Hom.CompleteLattice
/-- `sSupHomClass F α β` states that `F` is a type of `⨆`-preserving morphisms.

You should extend this class when you extend `sSupHom`.  -/
sSupHomClass : (F : Type u_8) → (α : Type u_9) → (β : Type u_10) → [SupSet α] → [SupSet β] → [FunLike F α β] → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_closure`.

---

The edist to a set and to its closure coincide  -/
EMetric.infEdist_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, Metric.infEDist x (closure s) = Metric.infEDist x s
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.zipIdx_eq_zipIdxTR.go : ∀ (α : Type u_1) (l : List α) (i : ℕ),
  have f := fun a x =>
    match x with
    | (n, acc) => (n - 1, (a, n - 1) :: acc);
  List.foldr f (i + l.length, []) l = (i, l.zipIdx i)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_union_Ioi' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c < b → Set.Ioo a b ∪ Set.Ioi c = Set.Ioi (min a c)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.toLinearMap_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (x : M₁), f x ∈ p), ↑(f.codRestrict p h) = LinearMap.codRestrict p (↑f) h
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.obj F).left = F.obj CategoryTheory.WithInitial.star
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops_eq_self : ∀ {α : Type u_1} (M : Matroid α) [M.Loopless], M.removeLoops = M
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.toTopCat : AlexDisc → TopCat
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c))
  (s : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.toOne : {α : Type u_1} → [self : NonAssocRing α] → One α
-- Mathlib.CategoryTheory.Grothendieck
/-- The inclusion of a fiber `F.obj c` of a functor `F : C ⥤ Cat` into its Grothendieck
construction.  -/
CategoryTheory.Grothendieck.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C CategoryTheory.Cat) →
      (c : C) → CategoryTheory.Functor (↑(F.obj c)) (CategoryTheory.Grothendieck F)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.instNatCast : NatCast Cardinal.{u}
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {x y : CategoryTheory.PresheafOfGroups.OneCochain G U}, x = y ↔ x.ev = y.ev
-- Mathlib.Data.Nat.PSub
Nat.psub_eq_some : ∀ {m n k : ℕ}, m.psub n = some k ↔ k + n = m
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- The function `(x ^ n) / (b * exp x + c)` tends to `0` at `+∞`, for any natural number
`n` and any real numbers `b` and `c` such that `b` is nonzero.  -/
Real.tendsto_div_pow_mul_exp_add_atTop : ∀ (b c : ℝ) (n : ℕ), 0 ≠ b → Filter.Tendsto (fun x => x ^ n / (b * Real.exp x + c)) Filter.atTop (nhds 0)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.FormatType.match_1.eq_1 : ∀ (motive : Std.Time.FormatString → Sort u_1) (entry : Std.Time.Modifier) (xs : List Std.Time.FormatPart)
  (h_1 :
    (entry : Std.Time.Modifier) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.modifier entry :: xs))
  (h_2 : (val : String) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.string val :: xs))
  (h_3 : Unit → motive []),
  (match Std.Time.FormatPart.modifier entry :: xs with
    | Std.Time.FormatPart.modifier entry :: xs => h_1 entry xs
    | Std.Time.FormatPart.string val :: xs => h_2 val xs
    | [] => h_3 ()) =
    h_1 entry xs
-- Init.Data.List.Sublist
List.isInfixOf_internal.eq_2 : ∀ {α : Type u} [inst : BEq α] (l₁ : List α) (a : α) (as : List α),
  l₁.isInfixOf_internal (a :: as) = (l₁.isPrefixOf (a :: as) || l₁.isInfixOf_internal as)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.id_toPrefunctor : ∀ (B : Type u₁) [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)],
  (CategoryTheory.PrelaxFunctorStruct.id B).toPrefunctor = 𝟭q B
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.differentiableAt_negMulLog_iff : ∀ {x : ℝ}, DifferentiableAt ℝ Real.negMulLog x ↔ x ≠ 0
-- Lean.Meta.Tactic.Grind.Util
/-- Abstracts metavariables occurring in the target.  -/
Lean.MVarId.abstractMVars : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Tactic.DefEqAbuse
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.VisitStep.ascend.injEq : ∀ {α : Type u_1} (returning returning_1 : Option α),
  (Lean.MessageData.VisitStep.ascend✝ returning = Lean.MessageData.VisitStep.ascend✝ returning_1) =
    (returning = returning_1)
-- Aesop.Tree.UnsafeQueue
Aesop.instInhabitedUnsafeQueueEntry.default : Aesop.UnsafeQueueEntry
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.toPullback_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] (k : E.I₁ i₁ i₂),
  CategoryTheory.CategoryStruct.comp (E.toPullback k) (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂)) = E.p₂ k
-- Lean.Meta.Match.Match
Lean.Meta.Match.isExFalsoTransition : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α},
  a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedProofInstArgInfo : Inhabited Lean.Meta.Sym.ProofInstArgInfo
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasColimitsOfShapeWalkingParallelPairInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair C],
  CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind C)
-- Mathlib.Analysis.Convex.Deriv
/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`.  -/
ConvexOn.monotoneOn_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConvexOn ℝ S f → DifferentiableOn ℝ f S → MonotoneOn (derivWithin f S) S
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Concatenate two bitvectors.
 -/
Std.Tactic.BVDecide.BVExpr.append : {l r w : ℕ} → Std.Tactic.BVDecide.BVExpr l → Std.Tactic.BVDecide.BVExpr r → w = l + r → Std.Tactic.BVDecide.BVExpr w
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.beq_one_eq_ite : ∀ {b : Bool} {a : BitVec 1}, ((a == 1#1) == b) = (a == bif b then 1#1 else 0#1)
-- Mathlib.Data.Finsupp.Basic
Finsupp.curryEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α →₀ β →₀ M), Finsupp.curryEquiv.symm f = f.uncurry
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_uIcc : ∀ {n : ℕ} (a b : Fin n), Finset.image Fin.val (Finset.uIcc a b) = Finset.uIcc ↑a ↑b
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterWithPostcondition.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := true })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := true }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_2 h'
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_or : ∀ {w : ℕ} {y x : BitVec w} {hi lo : ℕ},
  BitVec.extractLsb lo hi (x ||| y) = BitVec.extractLsb lo hi x ||| BitVec.extractLsb lo hi y
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_eq_false_iff_not_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {k : α}, m.contains k = false ↔ k ∉ m
-- Mathlib.CategoryTheory.Sites.Monoidal
/-- Relation between `functorEnrichedHom` and `presheafHom`.  -/
CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
        [inst_2 : CategoryTheory.MonoidalCategory A] →
          [inst_3 : CategoryTheory.MonoidalClosed A] →
            (M : A) →
              (F G : CategoryTheory.Functor Cᵒᵖ A) →
                [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] →
                  (X : C) →
                    ((CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G).comp
                            (CategoryTheory.coyoneda.obj (Opposite.op M))).obj
                        (Opposite.op X) ≃
                      (CategoryTheory.presheafHom
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj F
                              ((CategoryTheory.Functor.const Cᵒᵖ).obj M))
                            G).obj
                        (Opposite.op X)
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- A linear transformation `f` is orthogonal with respect to a bilinear form `B` if `B` is
bi-invariant with respect to `f`.  -/
LinearMap.IsOrthogonal : {R : Type u_20} →
  {M : Type u_21} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → (M → M) → Prop
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int64
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.idealX.eq_1 : ∀ (K : Type u_2) [inst : Field K],
  PowerSeries.idealX K = { asIdeal := Ideal.span {PowerSeries.X}, isPrime := ⋯, ne_bot := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonUnitalNonAssocSemiring : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [IsOrderedCancelAddMonoid Γ] → [inst : NonUnitalNonAssocSemiring R] → NonUnitalNonAssocSemiring (HahnSeries Γ R)
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.of.inj : ∀ {carrier : Type u} {semiring : Semiring carrier} {carrier_1 : Type u} {semiring_1 : Semiring carrier_1},
  SemiRingCat.of carrier = SemiRingCat.of carrier_1 → carrier = carrier_1 ∧ semiring ≍ semiring_1
-- Init.Tactics
/-- `norm_cast_add_elim foo` registers `foo` as an elim-lemma in `norm_cast`.
 -/
Lean.Parser.Tactic.normCastAddElim : Lean.ParserDescr
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Given a Freiman isomorphism `f` from `A` to `B`, if `g` maps `B` into `A`, and is a right inverse
to `f` on `B`, then `g` is a Freiman isomorphism from `B` to `A`.
 -/
IsMulFreimanIso.symm : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ} {g : β → α}, Set.MapsTo g B A → Set.RightInvOn g f B → IsMulFreimanIso n A B f → IsMulFreimanIso n B A g
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.exists_left_inv : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a → ∃ b, b * a = 1
-- Mathlib.Order.Filter.Basic
Filter.NeBot.mono : ∀ {α : Type u} {f g : Filter α}, f.NeBot → f ≤ g → g.NeBot
-- Init.Data.SInt.Basic
instMaxInt32 : Max Int32
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α} {h' : a ∈ t}, t.getKey a h' = t.getKey! a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ \ m₂).size = m₁.size
-- Init.Data.OfScientific
/-- The `OfScientific Float` must have priority higher than `mid` since
the default instance `Neg Int` has `mid` priority.
```
#check -42.0 -- must be Float
```
 -/
instOfScientificFloat : OfScientific Float
-- Mathlib.Order.WithBot
WithBot.coe_le_coe : ∀ {α : Type u_1} {a b : α} [inst : LE α], ↑a ≤ ↑b ↔ a ≤ b
-- Std.Internal.UV.System
/-- Returns the amount of free system memory in bytes.
 -/
Std.Internal.UV.System.freeMemory : IO UInt64
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_sSup : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M]
  (s : Set (Submodule R M)), Submodule.restrictScalars S (sSup s) = sSup (Submodule.restrictScalars S '' s)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finite
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Finite.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instSub : Sub ONote
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_3.eq_1 : ∀ (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) (f : ℕ → ONote) (h_1 : (f : ℕ → ONote) → motive (Sum.inr f))
  (h_2 : (b' : ONote) → motive (Sum.inl (some b'))) (h_3 : Unit → motive (Sum.inl none)),
  (match Sum.inr f with
    | Sum.inr f => h_1 f
    | Sum.inl (some b') => h_2 b'
    | Sum.inl none => h_3 ()) =
    h_1 f
-- Mathlib.Topology.PartialHomeomorph.Basic
Topology.IsEmbedding.toPartialHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsEmbedding f) [inst_2 : Nonempty X], ↑(Topology.IsEmbedding.toPartialHomeomorph f h) = f
-- Init.Data.SInt.Lemmas
Int16.mod_zero : ∀ {a : Int16}, a % 0 = a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The isomorphism in `Localization W` that is induced by a morphism in `W`.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        {X Y : C} →
          (s : X ⟶ Y) →
            W s →
              ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X ≅
                (CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj Y)
-- Mathlib.Data.DFinsupp.Interval
/-- Finitely supported product of finsets.  -/
Finset.dfinsupp : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [DecidableEq ι] → [inst : (i : ι) → Zero (α i)] → Finset ι → ((i : ι) → Finset (α i)) → Finset (Π₀ (i : ι), α i)
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u : ↥(unitary R)) (x : R),
  ((Unitary.conjStarAlgAut S R) u) x = ↑u * x * star ↑u
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.exists_isNonloop : ∀ {α : Type u_1} (M : Matroid α) [M.RankPos], ∃ e, M.IsNonloop e
-- Mathlib.MeasureTheory.Group.GeometryOfNumbers
/-- The **Minkowski Convex Body Theorem**. If `s` is a convex symmetric domain of `E` whose volume
is large enough compared to the covolume of a lattice `L` of `E`, then it contains a non-zero
lattice point of `L`.  -/
MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {F s : Set E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {L : AddSubgroup E}
  [Countable ↥L],
  MeasureTheory.IsAddFundamentalDomain (↥L) F μ →
    (∀ x ∈ s, -x ∈ s) → Convex ℝ s → μ F * 2 ^ Module.finrank ℝ E < μ s → ∃ x, x ≠ 0 ∧ ↑x ∈ s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.C_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo], Polynomial.C (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_sum : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} {ι : Type u_1} (f : ι → (M ⟶ N)) (s : Finset ι),
  SemimoduleCat.Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, SemimoduleCat.Hom.hom (f i)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {w : Fin (n + 1) → ℝ},
      ∑ j, w j = 1 →
        ((Finset.affineCombination ℝ Finset.univ s.points) w = s.excenter signs ↔ w = s.excenterWeights signs)
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.instInhabited : Inhabited Std.Http.Header.Name
-- Mathlib.Algebra.Lie.Matrix
/-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
is compatible with the Lie algebra structures.  -/
lieEquivMatrix' : {R : Type u} →
  [inst : CommRing R] →
    {n : Type w} → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → Module.End R (n → R) ≃ₗ⁅R⁆ Matrix n n R
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.coe_ofSupportedIn : ∀ {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 : ℕ∞} {K : TopologicalSpace.Compacts E}
  (K_sub_Ω : ↑K ⊆ ↑Ω) (f : ContDiffMapSupportedIn E F n K), ⇑(TestFunction.ofSupportedIn K_sub_Ω f) = ⇑f
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.mk : {μ : YoungDiagram} →
  (entry : ℕ → ℕ → ℕ) →
    (∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2) →
      (∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j) →
        (∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0) → SemistandardYoungTableau μ
-- Mathlib.Logic.Equiv.PartialEquiv
Set.InjOn.toPartialEquiv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Nonempty α] (f : α → β) (s : Set α) (hf : Set.InjOn f s),
  Set.InjOn.toPartialEquiv f s hf = Set.BijOn.toPartialEquiv f s (f '' s) ⋯
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter : Type
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.hom_eq_hom : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring S₂]
  (f g : MvPolynomial σ R →+* S₂),
  f.comp MvPolynomial.C = g.comp MvPolynomial.C →
    (∀ (n : σ), f (MvPolynomial.X n) = g (MvPolynomial.X n)) → ∀ (p : MvPolynomial σ R), f p = g p
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- Helper lemma to pass between the orders on `ℕ∞` and `ℤᵐ⁰` (which notably have different behaviour at
`∞`). Note that here we're using the fact that the order of any non zero divisor is finite, hence
the assumptions on the ring.
 -/
Ring.ord_le_iff : ∀ {R : Type u_2} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] [inst_3 : Nontrivial R] {a b : R},
  a ∈ nonZeroDivisors R →
    b ∈ nonZeroDivisors R →
      (Ring.ord R a ≤ Ring.ord R b ↔ (Ring.ordMonoidWithZeroHom R) a ≤ (Ring.ordMonoidWithZeroHom R) b)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.ιColimitType_map : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J (Type w₀)) {j j' : J}
  (f : j ⟶ j') (x : F.obj j), F.ιColimitType j' ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) = F.ιColimitType j x
-- Lean.Meta.Sym.Arith.Poly
/-- Returns `true` if the leading monomial of `p` divides `m`.  -/
Lean.Grind.CommRing.Poly.divides : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Mon → Bool
-- Mathlib.Combinatorics.Enumerative.Composition
instDecidableEqCompositionAsSet.decEq : {n : ℕ} → (x x_1 : CompositionAsSet n) → Decidable (x = x_1)
-- Mathlib.Util.Superscript
/-- Collects runs of text satisfying `p` followed by whitespace. Fails if the first character does
not satisfy `p`. If `many` is true, it will parse 1 or more many whitespace-separated runs,
otherwise it will parse only 1. If successful, it passes the result to `k` as an array `(a, b, c)`
where `a..b` is a token and `b..c` is whitespace.
 -/
Mathlib.Tactic.Superscript.satisfyTokensFn : (Char → Bool) →
  String →
    optParam Bool true →
      (Array (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) → Lean.Parser.ParserState → Lean.Parser.ParserState) →
        Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Hom.Monoid
/-- The inverse of an isomorphism is an isomorphism.  -/
OrderMonoidIso.symm : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → β ≃*o α
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {e : PUnit.{u + 1}}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (MonadExceptOf.throw e)).apply Q = Q.2.1 e
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_rightUnitor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_or : ∀ {w k : ℕ} {x y : BitVec w}, BitVec.setWidth k (x ||| y) = BitVec.setWidth k x ||| BitVec.setWidth k y
-- Mathlib.Analysis.Convex.Strong
StrongConvexOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ} {m n : ℝ},
  m ≤ n → StrongConvexOn s n f → StrongConvexOn s m f
-- Mathlib.Analysis.Asymptotics.Completion
Asymptotics.isBigO_completion_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F] {f : α → E}
  {g : α → F} {l : Filter α}, (fun x => ↑(g x)) =O[l] f ↔ g =O[l] f