mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  FaithfulSMul ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Two vector measures `v` and `w` are said to be mutually singular if there exists a measurable
set `s`, such that for all `t ⊆ s`, `v t = 0` and for all `t ⊆ sᶜ`, `w t = 0`.

We note that we do not require the measurability of `t` in the definition since this makes it easier
to use. This is equivalent to the definition which requires measurability. To prove
`MutuallySingular` with the measurability condition, use
`MeasureTheory.VectorMeasure.MutuallySingular.mk`.  -/
MeasureTheory.«term_⟂ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.StdBasis
/-- The product of finitely many free modules is free (non-dependent version to help with typeclass
search).  -/
Module.Free.function : ∀ (ι : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Finite ι] [Module.Free R M], Module.Free R (ι → M)
-- Lean.Syntax
Lean.SourceInfo.updateTrailing : Substring.Raw → Lean.SourceInfo → Lean.SourceInfo
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonOpenNamespace.fromJson : Lean.Json → Except String Lean.Lsp.OpenNamespace
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.rightCancelSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₁] [inst_1 : RightCancelSemigroup M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Injective.rightCancelSemigroup f hf mul =
    { toSemigroup := Function.Injective.semigroup f hf mul, toIsRightCancelMul := ⋯ }
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.id_of_le_cof : ∀ {o : Ordinal.{u}}, o ≤ o.cof.ord → o.IsFundamentalSequence o fun a x => a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_zero : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), SkewPolynomial.coeff 0 n = 0
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instCoeSortType : CoeSort AddMonCat (Type u)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.normedSpaceCore : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n], NormedSpace.Core ℂ (CStarMatrix m n A)
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.anti : ∀ {α : Type u} {s t : Set α}, t.Subsingleton → s ⊆ t → s.Subsingleton
-- Init.Data.Option.Monadic
Option.forIn'_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (a : α) (b : β)
  (f : (a' : α) → a' ∈ some a → β → m (ForInStep β)),
  forIn' (some a) b f = do
    let r ← f a ⋯ b
    pure r.value
-- Aesop.Frontend.Extension
_private.Aesop.Frontend.Extension.0.Aesop.Frontend.eraseGlobalRules.go : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [MonadLiftT IO m] →
        [MonadLiftT Lean.CoreM m] → [Lean.MonadEnv m] → Aesop.RuleFilter → Bool → Aesop.RuleSetName → m Bool
-- Mathlib.Testing.Plausible.Functions
/-- Remove a slice of length `m` at index `n` in a list and a permutation, maintaining the property
that it is a permutation.
 -/
Plausible.InjectiveFunction.Perm.slice : {α : Type u} →
  [DecidableEq α] →
    ℕ →
      ℕ →
        (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup →
          (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instFinite : ∀ {α : Type u} {β : α → Type v} [inst : Ord α], Std.Iterators.Finite (Std.DTreeMap.Internal.RxcIterator α β) Id
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on set `s` is `μ` restricted to `s`
and scaled by the inverse of `μ s` (to make it a probability measure):
`(μ s)⁻¹ • μ.restrict s`.  -/
ProbabilityTheory.cond : {Ω : Type u_1} → {m : MeasurableSpace Ω} → MeasureTheory.Measure Ω → Set Ω → MeasureTheory.Measure Ω
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.findIdx.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (a : α) (l : List α) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n),
  (match a :: l, n with
    | [], n => h_1 n
    | a :: l, n => h_2 a l n) =
    h_2 a l n
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousAdd M] {f : ℤ → M},
  HasSum (fun n => f ↑n) m → HasSum (fun n => f (-(↑n + 1))) m' → HasSum f (m + m')
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
ConformalAt.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y]
  [inst_2 : NormedAddCommGroup Z] [inst_3 : NormedSpace ℝ X] [inst_4 : NormedSpace ℝ Y] [inst_5 : NormedSpace ℝ Z]
  {f : X → Y} {g : Y → Z} (x : X), ConformalAt g (f x) → ConformalAt f x → ConformalAt (g ∘ f) x
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instExpChar : ∀ {K : Type v} [inst : Field K] (f : Polynomial K) (p : ℕ) [ExpChar K p], ExpChar f.SplittingField p
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- A subring `R` of `K` such that for all `x : K` either `x ∈ R` or `x⁻¹ ∈ R` is
a valuation subring of `K`.  -/
ValuationSubring.ofSubring : {K : Type u} → [inst : Field K] → (R : Subring K) → (∀ (x : K), x ∈ R ∨ x⁻¹ ∈ R) → ValuationSubring K
-- Mathlib.NumberTheory.Pell
/-- A fundamental solution has positive `x`.  -/
Pell.IsFundamental.x_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → 0 < a.x
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The composition functor is also the composition on commutative monoid objects.  -/
CategoryTheory.Functor.mapCommMonCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {E : Type u₃} →
                  [inst_6 : CategoryTheory.Category.{v₃, u₃} E] →
                    [inst_7 : CategoryTheory.MonoidalCategory E] →
                      [inst_8 : CategoryTheory.BraidedCategory E] →
                        {F : CategoryTheory.Functor C D} →
                          {G : CategoryTheory.Functor D E} →
                            [inst_9 : F.LaxBraided] →
                              [inst_10 : G.LaxBraided] → (F.comp G).mapCommMon ≅ F.mapCommMon.comp G.mapCommMon
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.epi_iff_cancel_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C} (f : P ⟶ Q),
  CategoryTheory.Epi f ↔ ∀ (R : C) (g : Q ⟶ R), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- A version of `liftPropWithinAt_indep_chart`, only for the source.  -/
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {e : OpenPartialHomeomorph M H} {P : (H → H') → Set H → H → Prop} {g : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    e ∈ StructureGroupoid.maximalAtlas M G →
      x ∈ e.source →
        (ChartedSpace.LiftPropWithinAt P g s x ↔ ChartedSpace.LiftPropWithinAt P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x))
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.alts.sizeOf_spec : ∀ (args : List Lean.Parser.Tactic.MCasesPat), sizeOf (Lean.Parser.Tactic.MCasesPat.alts args) = 1 + sizeOf args
-- Init.Data.String.Defs
/-- Appends two strings. Usually accessed via the `++` operator.

The internal implementation will perform destructive updates if the string is not shared.

Examples:
* `"abc".append "def" = "abcdef"`
* `"abc" ++ "def" = "abcdef"`
* `"" ++ "" = ""`
 -/
String.append : String → String → String
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m γ}
  (it : Std.IterM Id β), (Std.IterM.mapM f it).toListRev = List.reverse <$> List.mapM f it.toList.run
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
/-- The adic topology on an `R` module coming from the ideal `WithIdeal.I`.
This cannot be an instance because `R` cannot be inferred from `M`.  -/
WithIdeal.topologicalSpaceModule : (R : Type u_1) →
  [inst : CommRing R] → [WithIdeal R] → (M : Type u_2) → [inst_2 : AddCommGroup M] → [Module R M] → TopologicalSpace M
-- Mathlib.Analysis.Quaternion
Quaternion.hasSum_coe : ∀ {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {r : ℝ}, HasSum (fun a => ↑(f a)) (↑r) L ↔ HasSum f r L
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff.default : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.RatCoeff e
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.insert_isBasis_iff_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → (M.IsBasis I (insert e I) ↔ e ∈ M.closure I)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.equivOp.eq_1 : ∀ {M : Type u_2} [inst : MulOneClass M] (H : Submonoid M), H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.c.eq_1 : ∀ (x : ℝ) (n : ℕ), Chebyshev.c✝ x n = Chebyshev.b✝ x (6 * n - 1) - Chebyshev.b✝ x (6 * n) + Chebyshev.b✝ x (6 * n + 1)
-- Mathlib.Order.Monotone.MonovaryOrder
/-- **Alias** of the forward direction of `antivaryOn_iff_exists_antitoneOn_monotoneOn`. -/
AntivaryOn.exists_antitoneOn_monotoneOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → ∃ x, AntitoneOn f s ∧ MonotoneOn g s
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
/-- An embedding of the graph of a submatrix of an adjacency matrix to the graph of the
adjacency matrix itself, when the submatrix is given by an embedding  -/
Matrix.IsAdjMatrix.toGraphSubmatrixEmbedding : {α : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      (A : Matrix V V α) →
        [inst : MulZeroOneClass α] →
          [inst_1 : Nontrivial α] → (h : A.IsAdjMatrix) → (f : W ↪ V) → ⋯.toGraph ↪g h.toGraph
-- Std.Do.SPred.SVal
Std.Do.SVal.curry.eq_2 : ∀ {α : Type u} (head : Type u) (tail : List (Type u)) (f_2 : Std.Do.SVal.StateTuple (head :: tail) → α),
  Std.Do.SVal.curry f_2 = fun s => Std.Do.SVal.curry fun s' => f_2 (s, s')
-- Init.SimpLemmas
forall_prop_domain_congr : ∀ {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop} (h₁ : p₁ = p₂),
  (∀ (a : p₂), q₁ ⋯ = q₂ a) → (∀ (a : p₁), q₁ a) = ∀ (a : p₂), q₂ a
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.commTensorLeft_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X X_1 : C),
  (CategoryTheory.Functor.Monoidal.commTensorLeft F X).inv.app X_1 = CategoryTheory.Functor.OplaxMonoidal.δ F X X_1
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Cache certificates that are reused by the recursive Bird evaluator.  -/
Mathlib.Tactic.Determinant.CertCache : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Type
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_cons_right : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, Disjoint s (a ::ₘ t) ↔ a ∉ s ∧ Disjoint s t
-- Std.Data.TreeMap.Raw.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.TreeMap.Raw.mergeWith : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      (α → β → β → β) → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_mul : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (f g : P1 →ᵃ[k] P1), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.Ordering.Compares.match_1.eq_1 : ∀ {α : Type u_2} (motive : Ordering → α → α → Sort u_1) (a b : α) (h_1 : (a b : α) → motive Ordering.lt a b)
  (h_2 : (a b : α) → motive Ordering.eq a b) (h_3 : (a b : α) → motive Ordering.gt a b),
  (match Ordering.lt, a, b with
    | Ordering.lt, a, b => h_1 a b
    | Ordering.eq, a, b => h_2 a b
    | Ordering.gt, a, b => h_3 a b) =
    h_1 a b
-- Mathlib.Algebra.CharZero.Defs
NeZero.charZero_ofNat : ∀ {M : Type u_2} {n : ℕ} [inst : n.AtLeastTwo] [inst_1 : AddMonoidWithOne M] [CharZero M], NeZero (OfNat.ofNat n)
-- Mathlib.Algebra.Group.Basic
add_comm_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b c : α), a - b + c = a + (c - b)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
/-- performRatAdd adds to f.rupUnits and f.ratUnits and then clears both. If f begins with some units in either,
then performRatAdd will clear more than it intended to which will break the correctness of ratAdd_result
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRatAdd : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Prop
-- Mathlib.Topology.Category.TopCat.Basic
/-- The underlying `ContinuousMap`.  -/
TopCat.Hom.hom' : {X Y : TopCat} → X.Hom Y → C(↑X, ↑Y)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiffOn.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (fun x => Complex.exp (f x)) s
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A non-unital `R`-algebra homomorphism from `R[M]` is uniquely defined by its
values on the monomials `single a 1`.  -/
AddMonoidAlgebra.nonUnitalAlgHom_ext : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Add M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A},
  (∀ (x : M), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)) → φ₁ = φ₂
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.smulRight_apply : ∀ {R : Type u_10} {M₁ : Type u_11} {M₂ : Type u_12} {ι : Type u_13} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (f : M₁ [⋀^ι]→ₗ[R] R) (z : M₂)
  (a : (i : ι) → (fun x => M₁) i), (f.smulRight z) a = f a • z
-- Mathlib.Analysis.Convex.Side
AffineEquiv.sSameSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} (f : P ≃ᵃ[R] P'),
  (AffineSubspace.map (↑f) s).SSameSide (f x) (f y) ↔ s.SSameSide x y
-- Lean.Meta.Sym.AlphaShareCommon
/-- Returns `true` if `ctx.checkReducible` is true and `declName` is reducible declaration that
should be unfolded.
 -/
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.isReducible : Lean.Meta.Sym.AlphaShareCommon.Context → Lean.Name → Bool
-- Mathlib.Data.Finsupp.Weight
Finsupp.le_weight : ∀ {σ : Type u_1} (w : σ → ℕ) {s : σ}, w s ≠ 0 → ∀ (f : σ →₀ ℕ), f s ≤ (Finsupp.weight w) f
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_absolutelyContinuous : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ), (μ.tilted f).AbsolutelyContinuous μ
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax left unity.  -/
CategoryTheory.LaxFunctor.map₂_leftUnitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b}
  (h : self.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f))
        (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f) h))
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  ConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Ioi x) x → slope f x y ≤ f'
-- Mathlib.LinearAlgebra.Contraction
rTensorHomEquivHomRTensor_apply : ∀ {R : Type u_2} {M : Type u_3} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M]
  (x : TensorProduct R (M →ₗ[R] P) Q),
  (rTensorHomEquivHomRTensor R M P Q) x = (TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q) x
-- Lean.Elab.Term.TermElabM
/-- A variant of `withNarrowedTacticReuse` that uses `stx[argIdx]` as the inner syntax and all `stx`
child nodes before that as the outer syntax, i.e. reuse is disabled if there was any change before
`argIdx`.

NOTE: child nodes after `argIdx` are not tested (which would almost always disable reuse as they are
necessarily shifted by changes at `argIdx`) so it must be ensured that the result of `arg` does not
depend on them (i.e. they should not be inspected beforehand).
 -/
Lean.Elab.Term.withNarrowedArgTacticReuse : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadReaderOf Lean.Elab.Term.Context m] →
        [MonadLiftT BaseIO m] →
          [MonadWithReaderOf Lean.Core.Context m] →
            [MonadWithReaderOf Lean.Elab.Term.Context m] →
              [Lean.MonadOptions m] → ℕ → (Lean.Syntax → m α) → Lean.Syntax → m α
-- Init.Data.Nat.Basic
Nat.lt_add_of_pos_right : ∀ {k n : ℕ}, 0 < k → n < n + k
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.encode.eq_def : ∀ (x : Mathlib.Deriving.Encodable.S✝),
  Mathlib.Deriving.Encodable.S.encode✝ x =
    match x with
    | Mathlib.Deriving.Encodable.S.nat✝ n => Nat.pair 0 n
    | Mathlib.Deriving.Encodable.S.cons✝ a b =>
      Nat.pair (Mathlib.Deriving.Encodable.S.encode✝ a + 1) (Mathlib.Deriving.Encodable.S.encode✝ b)
-- Mathlib.Condensed.Discrete.Module
/-- `LightCondMod.LocallyConstant.functor` is naturally isomorphic to the constant sheaf functor from
`R`-modules to light condensed `R`-modules.
 -/
LightCondMod.LocallyConstant.functorIsoDiscrete : (R : Type u) → [inst : Ring R] → LightCondMod.LocallyConstant.functor R ≅ LightCondensed.discrete (ModuleCat R)
-- Mathlib.Algebra.DirectSum.Algebra
DirectSum.algebraMap_apply : ∀ {ι : Type uι} (R : Type uR) (A : ι → Type uA) [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : AddMonoid ι] [inst_4 : DirectSum.GSemiring A]
  [inst_5 : DirectSum.GAlgebra R A] [inst_6 : DecidableEq ι] (r : R),
  (algebraMap R (DirectSum ι fun i => A i)) r = (DirectSum.of A 0) (DirectSum.GAlgebra.toFun r)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' fallback : α} {f : β k → β k},
      (t.modify k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addLeftCancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddLeftCancelMonoid (f i)] → AddLeftCancelMonoid ((i : I) → f i)
-- Mathlib.GroupTheory.Subgroup.Saturated
AddSubmonoid.ker_saturated : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : AddGroup A₁] [inst_1 : AddMonoid A₂] [IsAddTorsionFree A₂] (f : A₁ →+ A₂),
  f.ker.NSMulSaturated
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintEmptyField : Lean.Syntax → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.P : {A : Type u} →
  {B : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          (self : Algebra.Smooth.DescentAux✝ A B) →
            Algebra.Presentation A B (Algebra.Smooth.DescentAux.vars✝ self) (Algebra.Smooth.DescentAux.rels✝ self)
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.ideal_from_ringHom.eq_1 : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} (hf : Ideal.map f I ≤ J),
  hI.ideal_from_ringHom hJ hf =
    { carrier := {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}, add_mem' := ⋯, zero_mem' := ⋯,
      smul_mem' := ⋯ }
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.exists_rightInverse_of_surjective : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [IsTopologicalAddGroup F]
  [inst_10 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] [FiniteDimensional 𝕜 F] (f : E →L[𝕜] F),
  (↑f).range = ⊤ → ∃ g, f ∘SL g = ContinuousLinearMap.id 𝕜 F
-- Mathlib.CategoryTheory.Comma.Basic
/-- The objects of the comma category are triples of an object `left : A`, an object
`right : B` and a morphism `hom : L.obj left ⟶ R.obj right`.  -/
CategoryTheory.Comma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            CategoryTheory.Functor A T → CategoryTheory.Functor B T → Type (max u₁ u₂ v₃)
-- ImportGraph.Imports.RequiredModules
/-- Finds all constants defined in the specified module,
and identifies all modules containing constants which are transitively required by those constants.
 -/
Lean.Environment.transitivelyRequiredModules : Lean.Environment → Lean.Name → Lean.CoreM Lean.NameSet
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.declNames : Lean.Elab.WF.EqnInfo → Array Lean.Name