mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Raw.Const.get! (m.insertIfNew k v) a =
        if (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Raw.Const.get! m a
-- Mathlib.Algebra.GroupWithZero.Units.Basic
isUnit_ringInverse : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a : M₀}, IsUnit (Ring.inverse a) ↔ IsUnit a
-- Mathlib.GroupTheory.Perm.Fin
Fin.isCycle_cycleRange : ∀ {n : ℕ} {i : Fin n} [inst : NeZero n], i ≠ 0 → i.cycleRange.IsCycle
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_modify_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ [Inhabited α] {k : α} {f : β k → β k} {hc : k ∈ Std.DTreeMap.Internal.Impl.modify k f t},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKey k hc = k
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierInvAdd : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V]
  [inst_6 : BorelSpace V], FourierInvAdd (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.edgeDensity.congr_simp : ∀ {α : Type u_4} (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst : DecidableRel G.Adj} [inst_1 : DecidableRel G_1.Adj] (a a_1 : Finset α),
      a = a_1 → ∀ (a_2 a_3 : Finset α), a_2 = a_3 → G.edgeDensity a a_2 = G_1.edgeDensity a_1 a_3
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrictGm_apply : ∀ {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousAdd M] {α : Type u_4}
  [inst_3 : MeasurableSpace α] (i : Set α) (v : MeasureTheory.VectorMeasure α M),
  (MeasureTheory.VectorMeasure.restrictGm i) v = v.restrict i
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.cotangentCompLocalizationAwayEquiv.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι)
  {x x_1 : ((Algebra.Generators.localizationAway T g).comp P).toExtension.Cotangent} (e_x : x = x_1)
  (hx :
    (Algebra.Extension.Cotangent.map ((Algebra.Generators.localizationAway T g).ofComp P).toExtensionHom) x =
      Algebra.Generators.cMulXSubOneCotangent T g),
  Algebra.Generators.cotangentCompLocalizationAwayEquiv g P hx =
    Algebra.Generators.cotangentCompLocalizationAwayEquiv g P ⋯
-- Mathlib.Order.CompleteBooleanAlgebra
sup_iInf_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] (a : α) (f : ι → α), a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.union_mem_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (α i)] {s t : Set ((i : ι) → α i)},
  s ∈ MeasureTheory.measurableCylinders α →
    t ∈ MeasureTheory.measurableCylinders α → s ∪ t ∈ MeasureTheory.measurableCylinders α
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
DiscreteUniformity.relId_mem_uniformity : ∀ (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X], SetRel.id ∈ uniformity X
-- Mathlib.Data.Nat.Nth
Nat.count_nth_succ_of_infinite : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (Set.ofPred p).Infinite → ∀ (n : ℕ), Nat.count p (Nat.nth p n + 1) = n + 1
-- Mathlib.GroupTheory.Finiteness
/-- A group is finitely generated if and only if it is finitely generated as a monoid.  -/
Group.fg_iff_monoid_fg : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ Monoid.FG G
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasCountableColimits_of_hasColimits : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasColimits C],
  CategoryTheory.Limits.HasCountableColimits C
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.nonempty : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M),
  (↑p).Nonempty
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of `Cardinal.le_mk_sdiff_add_mk`. -/
Cardinal.le_mk_diff_add_mk : ∀ {α : Type u} (S T : Set α), Cardinal.mk ↑S ≤ Cardinal.mk ↑(S \ T) + Cardinal.mk ↑T
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.trans_right : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ t₁ ↑x → t₂.Bounded (↑x) o₂ → Ordnode.Valid' o₁ t₁ o₂
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ContinuousOn.rpow_const : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {p : ℝ},
  ContinuousOn f s → (∀ x ∈ s, f x ≠ 0 ∨ 0 ≤ p) → ContinuousOn (fun x => f x ^ p) s
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- The identity map as an ordered monoid with zero homomorphism.  -/
OrderMonoidWithZeroHom.id : (α : Type u_2) → [inst : Preorder α] → [inst_1 : MulZeroOneClass α] → α →*₀o α
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.instBEqRealizeConstKey : BEq Lean.Environment.RealizeConstKey✝
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring isomorphism `(𝓞 K) ≃+* (𝓞 L)` given by restricting
a ring isomorphism `e : K ≃+* L` to `𝓞 K`.  -/
NumberField.RingOfIntegers.mapRingEquiv : {K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] → [inst_1 : Field L] → K ≃+* L → NumberField.RingOfIntegers K ≃+* NumberField.RingOfIntegers L
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_hom_app : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [inst_5 : G.CommShift A] (X : C),
  (CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).hom.app X =
    CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X)))
      (CategoryTheory.CategoryStruct.comp
        (F.map
          ((CategoryTheory.shiftFunctor C a).map
            (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b h).inv.app (F.obj X)))))
        (CategoryTheory.CategoryStruct.comp
          (F.map
            ((CategoryTheory.shiftFunctor C a).map
              ((CategoryTheory.Functor.commShiftIso G b).hom.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X)))))
          (CategoryTheory.CategoryStruct.comp
            (F.map
              ((CategoryTheory.shiftFunctorCompIsoId C b a ⋯).hom.app
                (G.obj ((CategoryTheory.shiftFunctor D a).obj (F.obj X)))))
            (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj (F.obj X))))))
-- Lean.Message
/-- An empty message.  -/
Lean.MessageData.nil : Lean.MessageData
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M),
  Function.Injective ⇑solution.fromQuotient ↔ solution.π.ker = Submodule.span A (Set.range relations.relation)
-- Aesop.RuleSet
/-- Normalisation rules registered in this rule set.
 -/
Aesop.BaseRuleSet.normRules : Aesop.BaseRuleSet → Aesop.Index Aesop.NormRuleInfo
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_comp_eq : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N),
  ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
/-- Measurable equivalence between `WithTop ι` and `ι ⊕ Unit`.  -/
WithTop.measurableEquivSum : {ι : Type u_1} →
  [inst : LinearOrder ι] →
    [inst_1 : TopologicalSpace ι] →
      [inst_2 : OrderTopology ι] → [inst_3 : MeasurableSpace ι] → [BorelSpace ι] → WithTop ι ≃ᵐ ι ⊕ Unit
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.toUpperSet_specializes_toUpperSet : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Topology.WithUpperSet.toUpperSet a ⤳ Topology.WithUpperSet.toUpperSet b ↔ b ≤ a
-- Lean.Meta.Sym.SymM
/-- For functions with a fixed prefix of implicit/instance arguments followed by
explicit non-dependent arguments that can be rewritten independently.

- `prefixSize`: Number of leading arguments (types, instances) that are determined
  by the suffix arguments and should not be rewritten directly.
- `suffixSize`: Number of trailing arguments that can be rewritten using simple congruence.

Examples (showing `prefixSize`, `suffixSize`):
- `HAdd.hAdd {α β γ} [HAdd α β γ] (a : α) (b : β)`: `(4, 2)` — rewrite `a` and `b`
- `And (p q : Prop)`: `(0, 2)` — rewrite both propositions
- `Eq {α} (a b : α)`: `(1, 2)` — rewrite `a` and `b`, type `α` is fixed
- `Neg.neg {α} [Neg α] (a : α)`: `(2, 1)` — rewrite just `a`
 -/
Lean.Meta.Sym.CongrInfo.fixedPrefix : ℕ → ℕ → Lean.Meta.Sym.CongrInfo
-- Mathlib.Algebra.Lie.Basic
LieEquiv.one_apply : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] (x : L₁), 1 x = x
-- Mathlib.Analysis.Calculus.DiffContOnCl
DiffContOnCl.differentiableAt' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E},
  DiffContOnCl 𝕜 f s → s ∈ nhds x → DifferentiableAt 𝕜 f x
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_transpose : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o),
  M.transpose.blockDiag k = (M.blockDiag k).transpose
-- Mathlib.Order.GaloisConnection.Basic
GaloisConnection.isLUB_u : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → ∀ {a : α}, IsLUB {b | l b ≤ a} (u a)
-- Mathlib.Data.Complex.Basic
Complex.ratCast_re : ∀ (q : ℚ), (↑q).re = ↑q
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Push a sieve `R` on `Y` forward along an arrow `f : Y ⟶ X`: `gf : Z ⟶ X` is in the sieve if `gf`
factors through some `g : Z ⟶ Y` which is in `R`.
 -/
CategoryTheory.Sieve.pushforward : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (Y ⟶ X) → CategoryTheory.Sieve Y → CategoryTheory.Sieve X
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1` is positive,
then `L a x` is positive real for all real `x` larger than `abscissaOfAbsConv a`.  -/
LSeries.positive : ∀ {a : ℕ → ℂ}, 0 ≤ a → 0 < a 1 → ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a < ↑x → 0 < LSeries a ↑x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℤ`.
 -/
HurwitzZeta.hasSum_int_hurwitzZetaEven : ∀ (a : ℝ) {s : ℂ}, 1 < s.re → HasSum (fun n => 1 / ↑|↑n + a| ^ s / 2) (HurwitzZeta.hurwitzZetaEven (↑a) s)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.iso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)],
  CategoryTheory.Limits.PreservesPushout.iso G f g = CategoryTheory.Limits.PreservesPushout.iso G f g
-- Mathlib.Data.Fintype.Basic
PLift.fintype : (α : Type u_4) → [Fintype α] → Fintype (PLift α)
-- Init.Control.Except
Except.instMonad : {ε : Type u} → Monad (Except ε)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_uIoc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) '' Set.uIoc i j = Set.uIoc (i.addNat m) (j.addNat m)
-- Mathlib.Topology.Algebra.UniformConvergence
instPowUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → {M : Type u_5} → [Pow β M] → Pow (UniformOnFun α β 𝔖) M
-- Mathlib.Data.Finset.Card
/-- See also `Finset.card_le_card_of_injOn`, which is a more general version of this lemma.
TODO: consider deprecating, since this is just a special case of `Finset.card_le_card_of_injOn`.
 -/
Finset.le_card_of_inj_on_range : ∀ {α : Type u_1} {s : Finset α} {n : ℕ} (f : ℕ → α),
  (∀ i < n, f i ∈ s) → (∀ i < n, ∀ j < n, f i = f j → i = j) → n ≤ s.card
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.homMk'_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y' : C} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T) (g : f.right ⟶ Y'),
  (f.homMk' g).right = g
-- Mathlib.Algebra.Group.WithOne.Basic
/-- A version of `Equiv.optionCongr` for `WithZero`.  -/
AddEquiv.withZeroCongr : {α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β → WithZero α ≃+ WithZero β
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_8 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.ret k with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_8 (Turing.PartrecToTM2.Λ'.ret k) k ⋯
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
defines a semigroup homomorphism from `Mᵐᵒᵖ`.  -/
MulHom.fromOpposite : {M : Type u_3} →
  {N : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (∀ (x y : M), Commute (f x) (f y)) → Mᵐᵒᵖ →ₙ* N
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center.addCommMonoid'.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.center.addCommMonoid' =
    { toAdd := (AddSubmonoid.center M).toAddZeroClass.toAdd, add_assoc := ⋯,
      toZero := (AddSubmonoid.center M).toAddZeroClass.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instUpwardEnumerableInt : Std.PRange.UpwardEnumerable ℤ
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.instModuleFinite : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} [NeZero n] [Module.Free ℤ G] [Module.Finite ℤ G],
  Module.Finite (ZMod n) (ModN G n)
-- Mathlib.Topology.EMetricSpace.Lipschitz
locallyLipschitzOn_empty : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α → β),
  LocallyLipschitzOn ∅ f
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_comp_tensorHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) (h : V ⟶ W) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f V)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f g) h) h_1
-- ProofWidgets.Component.PenroseDiagram
/-- A monad to easily build Penrose diagrams in.  -/
ProofWidgets.Penrose.DiagramBuilderM : Type → Type
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.match_1.splitter : {α : Type u_1} →
  (motive : List α → List α → Sort u_2) →
    (xs ys : List α) →
      ((ys : List α) → motive [] ys) →
        ((xs : List α) → (xs = [] → False) → motive xs []) →
          ((x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)) → motive xs ys
-- Lean.Elab.Tactic.LibrarySearch
_private.Lean.Elab.Tactic.LibrarySearch.0.Lean.Elab.LibrarySearch.instEvalExprLibrarySearchConfig.evalExpr : Lean.Expr → Lean.MetaM Lean.Parser.Tactic.LibrarySearchConfig
-- Mathlib.Order.Interval.Set.ProjIcc
Monotone.IciExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : ↑(Set.Ici a) → β},
  Monotone f → Monotone (Set.IciExtend f)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.δ_δ₀Iter_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 2)) (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.δ_δ₀Iter._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.δ_δ₀Iter._auto_3 →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ j) (CategoryTheory.CategoryStruct.comp (X.δ₀Iter i hi) h) =
        CategoryTheory.CategoryStruct.comp (X.δ₀Iter (i + 1) ⋯) h
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
/-- The canonical isomorphism between the localization of a submodule and its realization
as a submodule in the localized module.  -/
Submodule.localizedEquiv : {R : Type u_1} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (p : Submonoid R) →
            (M' : Submodule R M) → ↥(Submodule.localized p M') ≃ₗ[Localization p] LocalizedModule p ↥M'
-- Init.Data.SInt.Lemmas
ISize.le_toInt_maxValue : 2 ^ 31 - 1 ≤ ISize.maxValue.toInt
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2Computable.mk.injEq : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  (toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ)
  (outputsFun :
    (a : α) →
      Turing.TM2Outputs toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))))
  (toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ)
  (outputsFun_1 :
    (a : α) →
      Turing.TM2Outputs toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a))))),
  ({ toTM2ComputableAux := toTM2ComputableAux, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, outputsFun := outputsFun_1 }) =
    (toTM2ComputableAux = toTM2ComputableAux_1 ∧ outputsFun ≍ outputsFun_1)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_one : CartanMatrix.A 1 = !![2]
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_mk : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {x : M} {s : Submodule R M} {hs : IsClosed s.carrier},
  x ∈ { toSubmodule := s, isClosed' := hs } ↔ x ∈ s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {hc : t.maxKey! ∈ t}, t.getKey t.maxKey! hc = t.maxKey!
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_filter_le_size : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : (a : α) → β a → Bool}, (Std.DHashMap.filter f m).size ≤ m.size
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_smul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L)
  {x : L},
  x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β) →
    ↑(LieAlgebra.IsKilling.chainLength α β) • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
CategoryTheory.Abelian.Ext.subsingleton_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X I : C) [CategoryTheory.Injective I] (n : ℕ),
  Subsingleton (CategoryTheory.Abelian.Ext X I (n + 1))
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.eq_of_smul_eq_smul_left : ∀ {d a : ℤ} {b c : ℤ√d}, a ≠ 0 → ↑a * b = ↑a * c → b = c
-- Init.Data.String.Slice
/-- Splits a slice at each subslice that matches the pattern `pat`, starting from the end of the
slice and traversing towards the start.

The subslices that matched the pattern are not included in any of the resulting subslices. If
multiple subslices in a row match the pattern, the resulting list will contain empty slices.

This function is generic over all currently supported patterns except
`String`/`String.Slice`.

Examples:

* `("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`

* `("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
 -/
String.Slice.revSplit : {σ : String.Slice → Type} →
  {ρ : Type} →
    (s : String.Slice) → (pat : ρ) → [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] → Std.Iter String.Slice
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.nndist_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X} {x y : X},
  HolderOnWith C r f s → x ∈ s → y ∈ s → ∀ {d : NNReal}, nndist x y ≤ d → nndist (f x) (f y) ≤ C * d ^ ↑r
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.mem_pow_iff_prod : ∀ {α : Type u_2} [inst : CommMonoid α] {n : ℕ} {s : Set α} {a : α},
  a ∈ s ^ n ↔ ∃ f, (∀ (i : Fin n), f i ∈ s) ∧ ∏ i, f i = a