mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Factorial.Basic
Nat.pow_lt_ascFactorial' : ∀ (n k : ℕ), (n + 1) ^ (k + 2) < (n + 1).ascFactorial (k + 2)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_ratCast : ∀ (q : ℚ), ↑↑q = ↑q
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integrable_neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l (-f) vol ↔ BoxIntegral.Integrable I l f vol
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.coeff_toPowerSeries : ∀ {R : Type u_2} [inst : Semiring R] {f : HahnSeries ℕ R} {n : ℕ},
  (PowerSeries.coeff n) (HahnSeries.toPowerSeries f) = f.coeff n
-- Mathlib.Data.Set.Disjoint
/-- **Alias** of the forward direction of `Set.disjoint_right`. -/
Disjoint.notMem_of_mem_right : ∀ {α : Type u} {s t : Set α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s t : Set E},
  InnerProductSpace.HarmonicContOnCl f s → t ⊆ s → InnerProductSpace.HarmonicContOnCl f t
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- `sets β`  -/
_private.Mathlib.SetTheory.Cardinal.SchroederBernstein.0.Function.Embedding.sets : {ι : Type u} → (β : ι → Type v) → Set (Set ((i : ι) → β i))
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.equivalence_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.equivalence C).functor = CategoryTheory.ShrinkHoms.functor C
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A}
  (H : g.IsWeierstrassFactorization f h),
  (PowerSeries.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g (↑⋯.unit⁻¹)
    (Polynomial.X ^ ((PowerSeries.map (IsLocalRing.residue A)) g).order.toNat - f)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.iso₂Mk_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (el : α.l ≅ β.l) (er : β.r ≅ α.r)
  (h :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) el.hom = er.hom)
      CategoryTheory.Bicategory.Adj.iso₂Mk._auto_1),
  (CategoryTheory.Bicategory.Adj.iso₂Mk el er h).hom.τr = er.hom
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedGroupInfo.default : Std.Internal.UV.System.GroupInfo
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- The implementation of `IteratorLoop.forIn` in `i` is equal to the default implementation.  -/
Std.LawfulIteratorLoop.lawful : ∀ {β α : Type w} {m : Type w → Type w'} {n : Type x → Type x'} {inst : Monad m} {inst_1 : Monad n}
  {inst_2 : Std.Iterator α m β} {i : Std.IteratorLoop α m n} [self : Std.LawfulIteratorLoop α m n]
  (lift : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) [Std.Internal.LawfulMonadLiftBindFunction lift]
  (γ : Type x) (it : Std.IterM m β) (init : γ) (Pl : β → γ → ForInStep γ → Prop),
  Std.IteratorLoop.WellFounded α m Pl →
    ∀ (f : (b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))),
      Std.IteratorLoop.forIn lift γ Pl it init f = Std.IteratorLoop.forIn lift γ Pl it init f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.ofMonoidHom : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] → [inst_5 : Module R V] → (G →* V →L[R] V) → ContRepresentation R G V
-- Mathlib.Tactic.Translate.Core
/-- `(reorder := ...)` reorders the arguments/hypotheses in the generated declaration.
This is used in `to_dual` to swap the arguments in `≤`, `<` and `⟶`,
and it is used in `to_additive` to translate from `a ^ n` to `n • a`.
It uses disjoint cycle notation for the permutation. For reordering arguments of an argument `a`,
it uses the notation `a (...)` where `...` can be any reorder.

For example:
- `(reorder := α β, 5 6)` swaps the arguments `α` and `β` with each other and the fifth and
  the sixth argument.
- `(reorder := 3 4 5)` will move the fifth argument before the third argument.
- `(reorder := H (x y))` will swap the arguments `x` and `y` that appear in the hypothesis `H`.

If the translated declaration already exists (i.e. when using `existing` or `self`), the reorder
argument is automatically inferred using the function `guessReorder`.  -/
Mathlib.Tactic.Translate.reorderOption : Lean.ParserDescr
-- Batteries.Lean.Meta.DiscrTree
Lean.Meta.DiscrTree.Key.instOrd_batteries : Ord Lean.Meta.DiscrTree.Key
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
LinearIsometry.angle_map : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] (f : E →ₗᵢ[ℝ] F) (u v : E),
  InnerProductGeometry.angle (f u) (f v) = InnerProductGeometry.angle u v
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.isNegInvariant : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → AddGroup (α i)] [∀ (i : ι), MeasurableNeg (α i)] [∀ (i : ι), (μ i).IsNegInvariant],
  (MeasureTheory.Measure.pi μ).IsNegInvariant
-- Mathlib.Data.Nat.Factorization.Basic
Nat.pairwise_coprime_pow_primeFactors_factorization : ∀ {n : ℕ}, Pairwise (Function.onFun Nat.Coprime fun p => ↑p ^ n.factorization ↑p)
-- Mathlib.Data.Nat.Digits.Defs
/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding.  -/
Nat.digitsAux1 : ℕ → List ℕ
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
multipliableUniformlyOn_iff_hasProdUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], MultipliableUniformlyOn f s ↔ HasProdUniformlyOn f (fun x => ∏' (i : ι), f i x) s
-- Mathlib.Topology.NhdsWithin
nhdsWithin_pi_eq' : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {I : Set ι},
  I.Finite →
    ∀ (s : (i : ι) → Set (X i)) (x : (i : ι) → X i),
      nhdsWithin x (I.pi s) = ⨅ i, Filter.comap (fun x => x i) (nhds (x i) ⊓ ⨅ (_ : i ∈ I), Filter.principal (s i))
-- Mathlib.Order.Interval.Set.ProjIcc
Set.range_projIic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.range (Set.projIic a) = Set.univ
-- Mathlib.MeasureTheory.Function.Egorov
/-- Egorov's theorem for finite measure spaces.
Version with measurable distances.  -/
MeasureTheory.tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} [inst_1 : SemilatticeSup ι] [Nonempty ι] [Countable ι] {f : ι → α → β} {g : α → β}
  [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
    (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
      ∀ {ε : ℝ}, 0 < ε → ∃ t, MeasurableSet t ∧ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g Filter.atTop tᶜ
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorLId_toLinearEquiv : ∀ {R : Type uR} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [inst_3 : Invertible 2] (Q₂ : QuadraticForm R M₂), Q₂.tensorLId.toLinearEquiv = TensorProduct.lid R M₂
-- Batteries.Control.OptionT
OptionT.instLawfulMonadStateOfOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadStateOf σ m]
  [LawfulMonadStateOf σ m], LawfulMonadStateOf σ (OptionT m)
-- Mathlib.Analysis.Calculus.Deriv.Abs
hasDerivAt_abs_pos : ∀ {x : ℝ}, 0 < x → HasDerivAt (fun x => |x|) 1 x
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.zeroHom_comp : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero O]
  (f : ZeroHom N O) (f₂ : ZeroHom M N),
  Finsupp.mapRange.zeroHom (f.comp f₂) = (Finsupp.mapRange.zeroHom f).comp (Finsupp.mapRange.zeroHom f₂)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.connected_top : ∀ {V : Type u} [Nonempty V], (SimpleGraph.completeGraph V).Connected
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppMatchState.mk.inj : ∀ {info : Lean.Meta.MatcherInfo} {matcherTy : Lean.SubExpr} {motive : Option (Lean.Term × Lean.Expr)}
  {motiveNamed : Bool} {discrs : Array Lean.Term} {hNames? : Array (Option Lean.Name)} {alts : Array Lean.SubExpr}
  {varNames : Array (Array Lean.Name)} {rhss : Array Lean.Term} {info_1 : Lean.Meta.MatcherInfo}
  {matcherTy_1 : Lean.SubExpr} {motive_1 : Option (Lean.Term × Lean.Expr)} {motiveNamed_1 : Bool}
  {discrs_1 : Array Lean.Term} {hNames?_1 : Array (Option Lean.Name)} {alts_1 : Array Lean.SubExpr}
  {varNames_1 : Array (Array Lean.Name)} {rhss_1 : Array Lean.Term},
  { info := info, matcherTy := matcherTy, motive := motive, motiveNamed := motiveNamed, discrs := discrs,
        hNames? := hNames?, alts := alts, varNames := varNames, rhss := rhss } =
      { info := info_1, matcherTy := matcherTy_1, motive := motive_1, motiveNamed := motiveNamed_1, discrs := discrs_1,
        hNames? := hNames?_1, alts := alts_1, varNames := varNames_1, rhss := rhss_1 } →
    info = info_1 ∧
      matcherTy = matcherTy_1 ∧
        motive = motive_1 ∧
          motiveNamed = motiveNamed_1 ∧
            discrs = discrs_1 ∧ hNames? = hNames?_1 ∧ alts = alts_1 ∧ varNames = varNames_1 ∧ rhss = rhss_1
-- Mathlib.CategoryTheory.Sums.Basic
/-- A functor out of a sum is uniquely characterized by its precompositions with `inl_` and `inr_`.
 -/
CategoryTheory.Functor.sumIsoExt : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F G : CategoryTheory.Functor (A ⊕ B) C} →
              ((CategoryTheory.Sum.inl_ A B).comp F ≅ (CategoryTheory.Sum.inl_ A B).comp G) →
                ((CategoryTheory.Sum.inr_ A B).comp F ≅ (CategoryTheory.Sum.inr_ A B).comp G) → (F ≅ G)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.forIn f init m = forIn m.toArray init fun a b => f a.fst a.snd b
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.comp_mem_coverings : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition]
  {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {σ : ι → Type w'} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i),
      (∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) →
        (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x =>
            CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈
          J.coverings S
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.lowerCentralSeries_nilpotencyClass`. -/
lowerCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], ⊤.lowerCentralSeries (Group.nilpotencyClass G) = ⊥
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.invOf_exp_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂] {x : 𝔸},
  x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    ∀ [inst : Invertible (NormedSpace.exp x)], ⅟(NormedSpace.exp x) = NormedSpace.exp (-x)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top left map in the associativity hexagon.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPrePre F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPostPre F)
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.rid_symm_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W) (w : W), (Representation.TensorProduct.rid A σ).symm w = w ⊗ₜ[A] 1
-- Init.PropLemmas
ite_eq_right_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x y : α}, (if p then x else y) = y ↔ p → x = y
-- Mathlib.Topology.Order
TopologicalSpace.nhds_mkOfNhds_single : ∀ {α : Type u} [inst : DecidableEq α] {a₀ : α} {l : Filter α},
  pure a₀ ≤ l → ∀ (b : α), nhds b = Function.update pure a₀ l b
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Composition of bialgebra homomorphisms.  -/
BialgHom.comp : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Semiring C] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Algebra R C] →
                      [inst_7 : CoalgebraStruct R A] →
                        [inst_8 : CoalgebraStruct R B] →
                          [inst_9 : CoalgebraStruct R C] → (B →ₐc[R] C) → (A →ₐc[R] B) → A →ₐc[R] C
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.true.sizeOf_spec : sizeOf Mathlib.Tactic.ITauto.IProp.true = 1
-- Mathlib.Topology.CWComplex.Classical.Basic
_private.Mathlib.Topology.CWComplex.Classical.Basic.0.Topology.CWComplex.OfDiscreteClosed.match_3.eq_2 : ∀ {X : Type u_1} {D : Set X}
  (motive :
    (n : ℕ) →
      (match n with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}) →
        Sort u_2)
  (n : ℕ)
  (i :
    match n + 1 with
    | 0 => ↑D
    | n.succ => PEmpty.{u_1 + 1})
  (h_1 :
    (i :
        match 0 with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}) →
      motive 0 i)
  (h_2 :
    (n : ℕ) →
      (i :
          match n + 1 with
          | 0 => ↑D
          | n.succ => PEmpty.{u_1 + 1}) →
        motive n.succ i),
  (match n.succ, i with
    | 0, i => h_1 i
    | n.succ, i => h_2 n i) =
    h_2 n i
-- Init.Data.Rat.Lemmas
Rat.zpow_nonneg : ∀ {a : ℚ} {n : ℤ}, 0 ≤ a → 0 ≤ a ^ n
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.exists_eq : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (self : RootPairing.RootPositiveForm S P) (i j : ι), ∃ s, (algebraMap S R) s = (self.form (P.root i)) (P.root j)
-- Init.Simproc
/-- Auxiliary attribute for symbolic evaluation procedures.
 -/
Lean.Parser.Attr.sevalprocAttr : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The functor from `OpenNormalAddSubgroup P` to `FiniteAddGrp` sending `U` to
`P ⧸ U`, where `P : ProfiniteAddGrp`.  -/
ProfiniteAddGrp.toFiniteQuotientFunctor : (P : ProfiniteAddGrp.{u_1}) → CategoryTheory.Functor (OpenNormalAddSubgroup ↑P.toProfinite.toTop) FiniteAddGrp.{u_1}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.reverse_transfer : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet),
  (p.transfer H hp).reverse = p.reverse.transfer H ⋯
-- Mathlib.NumberTheory.FLT.Polynomial
FermatLastTheoremWith'.eq_1 : ∀ (R : Type u_2) [inst : CommSemiring R] (n : ℕ),
  FermatLastTheoremWith' R n =
    ∀ (a b c : R),
      a ≠ 0 →
        b ≠ 0 →
          c ≠ 0 →
            a ^ n + b ^ n = c ^ n →
              ∃ d a' b' c', (a = a' * d ∧ b = b' * d ∧ c = c' * d) ∧ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_nnnorm : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {K : NNReal},
  AntilipschitzWith K f → f 0 = 0 → ∀ (x : E), ‖x‖₊ ≤ K * ‖f x‖₊
-- Mathlib.Analysis.Complex.AbsMax
/-- If two complex differentiable functions `f g : E → F` are equal on the boundary of a bounded set
`U`, then they are equal on `closure U`.  -/
Complex.eqOn_closure_of_eqOn_frontier : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [Nontrivial E] {f g : E → F} {U : Set E},
  Bornology.IsBounded U → DiffContOnCl ℂ f U → DiffContOnCl ℂ g U → Set.EqOn f g (frontier U) → Set.EqOn f g (closure U)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The quotient by `AddAction.orbitRel`, given a name to enable dot notation.  -/
AddAction.orbitRel.Quotient : (G : Type u_1) → (α : Type u_2) → [inst : AddGroup G] → [AddAction G α] → Type u_2
-- Mathlib.SetTheory.Ordinal.Basic
/-- Bundled structure registering a well order on a type. Ordinals will be defined as a quotient
of this type.  -/
WellOrder : Type (u + 1)
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (x : F) (c : 𝕜), gradient (Function.const F c) x = 0
-- Mathlib.Data.Setoid.Partition
/-- The non-constructive constructor for `IndexedPartition`.  -/
IndexedPartition.mk' : {ι : Type u_1} →
  {α : Type u_2} →
    (s : ι → Set α) →
      Pairwise (Function.onFun Disjoint s) →
        (∀ (i : ι), (s i).Nonempty) → (∀ (x : α), ∃ i, x ∈ s i) → IndexedPartition s
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant additive monoid homomorphisms.  -/
DistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        (M →* N) →
          (A : Type u_10) →
            [inst_2 : AddMonoid A] →
              [DistribMulAction M A] →
                (B : Type u_11) → [inst : AddMonoid B] → [DistribMulAction N B] → Type (max u_10 u_11)
-- Std.Time.DateTime.PlainDateTime
/-- Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week
and `minDays` as the minimum number of days a week must have in the new year to count as week 1.
 -/
Std.Time.PlainDateTime.weekOfYear : Std.Time.PlainDateTime →
  optParam Std.Time.Weekday Std.Time.Weekday.monday →
    optParam (Std.Time.Internal.Bounded.LE 0 6)
        (Std.Time.Internal.Bounded.LE.mk 4 Std.Time.PlainDateTime.weekOfYear._proof_1) →
      Std.Time.Week.OfYear.Ordinal
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.nonempty_compStruct_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {x₀ x₁ x₂ : C} (f₀₁ : x₀ ⟶ x₁) (f₁₂ : x₁ ⟶ x₂) (f₀₂ : x₀ ⟶ x₂),
  Nonempty
      ((CategoryTheory.nerve.edgeMk f₀₁).CompStruct (CategoryTheory.nerve.edgeMk f₁₂)
        (CategoryTheory.nerve.edgeMk f₀₂)) ↔
    CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAt_iff_hasFDerivAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
  HasGradientAt f f' x ↔ HasFDerivAt f ((InnerProductSpace.toDual 𝕜 F) f') x
-- Mathlib.Data.Finite.Perm
Equiv.Perm.isCyclic_iff_card_le_two : ∀ {α : Type u_1} [Finite α], IsCyclic (Equiv.Perm α) ↔ Nat.card α ≤ 2
-- Mathlib.Algebra.Group.Submonoid.Membership
FreeMonoid.mrange_lift : ∀ {M : Type u_1} [inst : Monoid M] {α : Type u_4} (f : α → M),
  MonoidHom.mrange (FreeMonoid.lift f) = Submonoid.closure (Set.range f)
-- Lean.Util.MonadCache
Lean.MonadCacheT.instMonadLift : {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] → [inst_1 : BEq α] → [inst_2 : Hashable α] → MonadLift m (Lean.MonadCacheT α β m)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compQuasiMeasurePreserving_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {β : Type u_5} [inst_2 : MeasurableSpace β] {f : α → β} {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν),
  (g.compQuasiMeasurePreserving f hf).toGerm = g.toGerm.compTendsto f ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_singleton' : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  [hE : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E},
  MeasureTheory.StronglyMeasurable f → ∀ (a : α), ∫ (a : α) in {a}, f a ∂μ = μ.real {a} • f a
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim_aux : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.aux = c
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instMul : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Mul (AdicCompletion I R)
-- Lean.Util.InstantiateLevelParams
/-- Instantiate level parameters
 -/
Lean.Expr.instantiateLevelParamsCore : (Lean.Name → Option Lean.Level) → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Composition of lax prefunctors.  -/
CategoryTheory.PrelaxFunctorStruct.comp : {B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] →
          [inst_3 : (a b : C) → Quiver (a ⟶ b)] →
            {D : Type u₃} →
              [inst_4 : Quiver D] →
                [inst_5 : (a b : D) → Quiver (a ⟶ b)] →
                  CategoryTheory.PrelaxFunctorStruct B C →
                    CategoryTheory.PrelaxFunctorStruct C D → CategoryTheory.PrelaxFunctorStruct B D
-- Batteries.Data.List.Basic
List.zipWithLeftTR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List α) (a_1 : List β) (a_2 : Array γ),
  List.zipWithLeftTR.go f a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, acc => acc.toList
    | as, [], acc => (List.foldl (fun acc a => acc.push (f a none)) acc as).toList
    | a :: as, b :: bs, acc => List.zipWithLeftTR.go f as bs (acc.push (f a (some b)))
-- Init.Data.Vector.Basic
Vector.take_eq_extract : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.take i = xs.extract 0 i
-- Mathlib.Algebra.Algebra.Unitization
NonUnitalAlgHomClass.toNonUnitalAlgHom.eq_1 : ∀ {F : Type u_3} {R : Type u_4} [inst : Monoid R] {A : Type u_5} {B : Type u_6} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : DistribMulAction R B]
  [inst_5 : FunLike F A B] [inst_6 : NonUnitalAlgHomClass F R A B] (f : F),
  NonUnitalAlgHomClass.toNonUnitalAlgHom f =
    { toFun := ⇑f, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }
-- Init.Data.UInt.Bitwise
USize.xor_right_inj : ∀ {a b : USize} (c : USize), c ^^^ a = c ^^^ b ↔ a = b