mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.End
/-- The category of endofunctors of any category is a monoidal category,
with tensor product given by composition of functors
(and horizontal composition of natural transformations).

Note: due to the fact that composition of functors in mathlib is reversed compared to the
one usually found in the literature, this monoidal structure is in fact the monoidal
opposite of the one usually considered in the literature.
 -/
CategoryTheory.endofunctorMonoidalCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MonoidalCategory (CategoryTheory.Functor C C)
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves
/-- The coherent topology on a precoherent category is subcanonical.  -/
CategoryTheory.coherentTopology.subcanonical : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C],
  (CategoryTheory.coherentTopology C).Subcanonical
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.ofSurjective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'} [Group.IsPerfect G],
  Function.Surjective ⇑f → Group.IsPerfect G'
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- The iInf of the sequence `n ↦ μ(x ^ (n : ℕ)))^(1 / (n : ℝ)`.  -/
smoothingFun : {R : Type u_1} → [inst : CommRing R] → RingSeminorm R → R → ℝ
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.isEqvAux.match_1.eq_1 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (x : 0 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Mathlib.Order.Lattice
inf_sup_left : ∀ {α : Type u} [inst : DistribLattice α] (a b c : α), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sinh_neg : ∀ (x : ℂ), Complex.sinh (-x) = -Complex.sinh x
-- Std.Http.Data.Headers.Basic
Std.Http.Header.ContentLength.mk.injEq : ∀ (length length_1 : ℕ), ({ length := length } = { length := length_1 }) = (length = length_1)
-- Init.Data.Nat.Basic
Nat.pred_mul : ∀ (n m : ℕ), n.pred * m = n * m - m
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_5.eq_1 : ∀ {n : ℕ}
  (motive :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
        Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool →
      Sort u_1)
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (derivedEmpty encounteredError : Bool)
  (h_1 :
    (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
      (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
        (derivedEmpty encounteredError : Bool) → motive (assignments, derivedLits, derivedEmpty, encounteredError)),
  (match (assignments, derivedLits, derivedEmpty, encounteredError) with
    | (assignments, derivedLits, derivedEmpty, encounteredError) =>
      h_1 assignments derivedLits derivedEmpty encounteredError) =
    h_1 assignments derivedLits derivedEmpty encounteredError
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYoneda.congr_simp : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F],
  Condensed.isoFinYoneda F = Condensed.isoFinYoneda F
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is convex on `S` and differentiable at `x ∈ S`, then the slope of any secant
line with left endpoint at `x` is bounded below by the derivative of `f` at `x`.  -/
ConvexOn.le_slope_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ}, ConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' x → f' ≤ slope f x y
-- Mathlib.RingTheory.LaurentSeries
RatFunc.single_zpow : ∀ {F : Type u} [inst : Field F] (n : ℤ), (HahnSeries.single n) 1 = (HahnSeries.single 1) 1 ^ n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter m₂ ⋯).getKey? k = m₁.getKey? k
-- Mathlib.Order.CompleteLattice.Chain
_private.Mathlib.Order.CompleteLattice.Chain.0.chainClosure_succ_total_aux : ∀ {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α},
  ChainClosure r c₁ →
    (∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂) → SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l →
    (∀ a ∈ m, l.contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.algEquiv_ofAlgEquiv : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : Ring T] [inst_4 : Algebra R T] (h' : IsAdjoinRoot T f) {U : Type u_2}
  [inst_5 : Ring U] [inst_6 : Algebra R U] (e : T ≃ₐ[R] U), h.algEquiv (h'.ofAlgEquiv e) = (h.algEquiv h').trans e
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.pseudofunctorOfIsLocallyDiscrete_map : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_5)
  {X Y : B} (a : X ⟶ Y),
  (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).map
      a =
    map a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.map_target : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : β}, x ∈ e.target → ↑e.symm x ∈ e.source
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.totalDegree 0 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.natCast_strictMono : StrictMono fun x => ↑x
-- Mathlib.Algebra.Star.Subalgebra
/-- The `StarAlgEquiv` onto the range corresponding to an injective `StarAlgHom`.  -/
StarAlgEquiv.ofInjective : {R : Type u_2} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] →
              [inst_4 : StarRing A] →
                [inst_5 : Semiring B] →
                  [inst_6 : Algebra R B] →
                    [inst_7 : StarRing B] →
                      [inst_8 : StarModule R B] → (f : A →⋆ₐ[R] B) → Function.Injective ⇑f → A ≃⋆ₐ[R] ↥f.range
-- Mathlib.Topology.MetricSpace.Infsep
Finset.coe_infsep_of_offDiag_empty : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Finset α}, s.offDiag = ∅ → (↑s).infsep = 0
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  (X : CategoryTheory.Sheaf K A) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
  ((F.sheafPushforwardContinuous A J K).obj X).obj.map f = X.obj.map (F.map f.unop).op
-- Mathlib.Data.Fintype.Perm
permsOfList.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], permsOfList [] = [1]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.triangle_inv : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.CategoryStruct.comp (ψ.associator (CategoryTheory.Limits.CatCospanTransform.id F' G') φ).inv
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight ψ.rightUnitor.hom φ) =
    CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ φ.leftUnitor.hom
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.retractClosure = ⊤
-- Mathlib.Data.Multiset.Pi
/-- Given `δ : α → Sort*`, `Pi.empty δ` is the trivial dependent function out of the empty
multiset.  -/
Multiset.Pi.empty : {α : Type u_1} → (δ : α → Sort u_3) → (a : α) → a ∈ 0 → δ a
-- Aesop.Tree.Traversal
Aesop.postTraverseDown : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Unit) → (Aesop.RappRef → m Unit) → (Aesop.MVarClusterRef → m Unit) → Aesop.TreeRef → m Unit
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_lieSpan : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {s : Set M} {x : M},
  x ∈ LieSubmodule.lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N
-- Lean.Parser.Term
Lean.Parser.Term.matchExprAlts : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.core_map_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Core C} (f : X ⟶ Y), (F.core.map f).iso.inv = F.map f.iso.inv
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, s / t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Order.FixedPoints
OrderHom.map_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), f (OrderHom.lfp f) = OrderHom.lfp f
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.mk : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Elab.Term.ExtractMonadResult
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {a b c : B'}
  (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapComp f g).hom.iso = F.mapComp f g
-- Mathlib.Algebra.Star.StarRingHom
/-- Reinterpret a star ring equivalence as a `RingEquiv` by forgetting the interaction with the star
operation.  -/
StarRingEquiv.toRingEquiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → (A ≃⋆+* B) → A ≃+* B
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.inr_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (y : N),
  (AddMonoidHom.inr M N) y = (0, y)
-- Mathlib.Tactic.FunProp.Mor
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]` where `f` can be bundled morphism.

`∀ x, p x` is represented as `Forall p`.  -/
Mathlib.Meta.FunProp.Mor.withApp : {α : Type} → Lean.Expr → (Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.MetaM α) → Lean.MetaM α
-- Lean.Message
/-- Renders an expression `e` inline in a message unless it will exceed `maxInlineLength` characters, in
which case the expression is indented on a new line.

Note that the output of this function is formatted with preceding and trailing space included. Thus,
in `m₁ ++ inlineExpr e ++ m₂`, `m₁` should not end with a space or new line, nor should `m₂` begin
with one.
 -/
Lean.inlineExpr : Lean.Expr → optParam ℕ 30 → Lean.MessageData
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
span_coeff_minpolyDiv : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → Submodule.span R (Set.range (minpolyDiv R x).coeff) = Subalgebra.toSubmodule R[x]
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.CompStruct.compId_simplex : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁),
  (SSet.Edge.CompStruct.compId e).simplex =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X 1)) e.edge
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Icc_pi_toReal : ∀ {ι : Type u_1} [inst : Fintype ι] {a b : ι → ℝ},
  a ≤ b → (MeasureTheory.volume (Set.Icc a b)).toReal = ∏ i, (b i - a i)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : 𝕜 → 𝕜` is continuous on a compact set `s` and `a : X → A` is continuous at `x₀` within
a set `t : Set X`, and eventually `a x` satisfies the predicate `p` associated to `𝕜` and has
spectrum contained in `s`, then `fun x ↦ cfc f (a x)` is continuous at `x₀` within `t`.  -/
ContinuousWithinAt.cfc : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X},
      x₀ ∈ t →
        ContinuousWithinAt a t x₀ →
          (∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum 𝕜 (a x) ⊆ s) →
            (∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) →
              autoParam (ContinuousOn f s) ContinuousWithinAt.cfc._auto_1 →
                ContinuousWithinAt (fun x => cfc f (a x)) t x₀
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {l : List ((a : α) × β a)} {k k' fallback : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(t.insertMany l ⋯)).getKeyD k' fallback = k
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_sub : ∀ (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G →
      Derivative.normalizedDerivOfComplex (F - G) =
        Derivative.normalizedDerivOfComplex F - Derivative.normalizedDerivOfComplex G
-- Mathlib.Topology.Path
Path.map_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.map ⋯ = γ
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instCompleteLattice : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → CompleteLattice (TwoSidedIdeal R)
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- Characterization of `a / b = c` assuming `c ≠ 0`.
See `div_eq_iff` for a version assuming `b ≠ 0` instead.  -/
Ordinal.div_eq_iff' : ∀ {a b c : Ordinal.{u_4}}, c ≠ 0 → (a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_eq_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {fallback : β a} {h : a ∈ t}, t.get a h = t.getD a fallback
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonMessageKind : Lean.FromJson Lean.JsonRpc.MessageKind
-- Init.Prelude
/-- Parses the literal symbol.

The symbol is automatically included in the set of reserved tokens ("keywords").
Keywords cannot be used as identifiers, unless the identifier is otherwise escaped.
For example, `"fun"` reserves `fun` as a keyword; to refer an identifier named `fun` one can write `«fun»`.
Adding a `&` prefix prevents it from being reserved, for example `&"true"`.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.
 -/
Lean.ParserDescr.symbol : String → Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).get? k = none
-- Mathlib.Algebra.Group.Defs
AddMonoid.toZero : {M : Type u} → [self : AddMonoid M] → Zero M
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) (c : CategoryTheory.Limits.CokernelCofork S.f)
  (hc : CategoryTheory.Limits.IsColimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork S hg c hc).π =
    CategoryTheory.Limits.Cofork.π c
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_rel : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {v : α → M} {k : ℕ} {R : L.Relations k}
  {ts : Fin k → L.Term α},
  (R.formula ts).Realize v ↔ FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize v (ts i)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mk0_val : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (u : G₀ˣ) (h : ↑u ≠ 0), Units.mk0 (↑u) h = u
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E),
  μ.toSphere =
    Module.finrank ℝ E •
      ((MeasureTheory.Measure.comap (Subtype.val ∘ ⇑(homeomorphUnitSphereProd E).symm) μ).restrict
          (Set.univ ×ˢ Set.Iio ⟨1, MeasureTheory.Measure.toSphere._proof_1⟩)).fst
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.of_add_eq_zero : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {a : M} (b : M), a + b = 0 → IsAddUnit a
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.mk.sizeOf_spec : ∀ {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}
  {H : CategoryTheory.Functor C D} [inst_2 : SizeOf C] [inst_3 : SizeOf D] (adj₁ : F ⊣ G) (adj₂ : G ⊣ H),
  sizeOf { adj₁ := adj₁, adj₂ := adj₂ } = 1 + sizeOf adj₁ + sizeOf adj₂
-- Init.Data.Array.Attach
Array.mem_attach : ∀ {α : Type u_1} (xs : Array α) (x : { x // x ∈ xs }), x ∈ xs.attach
-- Init.PropLemmas
or_rotate : ∀ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ c ∨ a
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.needEscape.go : String → ℕ → Bool
-- Init.Data.String.TakeDrop
String.Slice.trimRight : String.Slice → String.Slice
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.eq_symm_comp : ∀ {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),
  f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_apply_le_norm : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  p ≠ 0 → ∀ (f : ↥(lp E p)) (i : α), ‖↑f i‖ ≤ ‖f‖
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.bot_mem' : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (self : BooleanSubalgebra α), ⊥ ∈ self.carrier
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z)
      (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) f)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) g)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` is bounded.  -/
FormalMultilinearSeries.norm_le_div_pow_of_pos_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal}, 0 < r → ↑r < p.radius → ∃ C > 0, ∀ (n : ℕ), ‖p n‖ ≤ C / ↑r ^ n
-- Mathlib.Control.Monad.Writer
WriterT.instMonadLiftOfEmptyCollection : {M : Type u → Type v} → {ω : Type u} → [Monad M] → [EmptyCollection ω] → MonadLift M (WriterT ω M)
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesFiniteEffectiveEpiFamilies]
  [G.PreservesFiniteEffectiveEpiFamilies], (F.comp G).PreservesFiniteEffectiveEpiFamilies