mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in both arguments.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' B' : C} (f : A ⟶ A') (g : B ⟶ B') {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) h)
-- Init.Data.Nat.Lemmas
Nat.mod_two_not_eq_one : ∀ {n : ℕ}, ¬n % 2 = 1 ↔ n % 2 = 0
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Information about the rewrite position. This is used to determine whether to suggest
`rw`, `rw!`, `nth_rw`, or `simp_rw`.  -/
Mathlib.Tactic.ClickSuggestions.RwKind : Type
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_5 : ∀ (coeff : ℕ) (a : Nat.Internal.Linear.Expr) (k : ℕ),
  Nat.Internal.Linear.Expr.toPoly.go coeff (a.mulR k) =
    bif k == 0 then id else Nat.Internal.Linear.Expr.toPoly.go (coeff * k) a
-- Std.Data.DTreeMap.Internal.Model
/-- Needle was less than key at this node: return key-value pair and unexplored right subtree,
recursion will continue in left subtree.  -/
Std.DTreeMap.Internal.Impl.ExplorationStep.lt : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {k : α → Ordering} →
        (a : α) → k a = Ordering.lt → β a → List ((a : α) × β a) → Std.DTreeMap.Internal.Impl.ExplorationStep α β k
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.FunctorToTypes.prod F G).map f =
    TypeCat.ofHom fun a =>
      ((CategoryTheory.ConcreteCategory.hom (F.map f)) a.1, (CategoryTheory.ConcreteCategory.hom (G.map f)) a.2)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_card : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → Norm (β i)] (f : PiLp 0 β),
  ‖f‖ = ↑⋯.toFinset.card
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_eq_map' : ∀ (n : ℕ),
  Finset.HasAntidiagonal.antidiagonal n = Finset.map { toFun := fun i => (n - i, i), inj' := ⋯ } (Finset.range (n + 1))
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.piObjIso_inv_comp_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piObjIso f d).inv ((CategoryTheory.Limits.Pi.π f s).app d) =
    CategoryTheory.Limits.Pi.π (fun s => (f s).obj d) s
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.extension_coe_to_fun : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  [inst_2 : T0Space H] [inst_3 : CompleteSpace H] (f : NormedAddGroupHom G H),
  ⇑f.extension = UniformSpace.Completion.extension ⇑f
-- Mathlib.Probability.Notation
/-- `P[X]` is the expectation of `X` under the measure `P`.

Note that this notation can conflict with the `GetElem` notation for lists. Usually if you see an
error about ambiguous notation when trying to write `l[i]` for a list, it means that Lean could
not find `i < l.length`, and so fell back to trying this notation as well.  -/
ProbabilityTheory.«term__[_]» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Group.Defs
NormedAddCommGroup.ofSeparation.eq_1 : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0),
  NormedAddCommGroup.ofSeparation h =
    { toNorm := inst.toNorm, toAddCommGroup := inst.toAddCommGroup, toPseudoMetricSpace := inst.toPseudoMetricSpace,
      eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
/-- `zeroLocus` and `vanishingIdeal` form a Galois connection.  -/
ProjectiveSpectrum.gc_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  GaloisConnection (fun I => ProjectiveSpectrum.zeroLocus 𝒜 ↑I) fun t => (ProjectiveSpectrum.vanishingIdeal t).toIdeal
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WindowClientCapabilities.mk : Option Lean.Lsp.ShowDocumentClientCapabilities → Lean.Lsp.WindowClientCapabilities
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.self_iff_nonZeroDivisors_le_isUnit : ∀ {R : Type u_1} [inst : CommRing R], IsFractionRing R R ↔ nonZeroDivisors R ≤ IsUnit.submonoid R
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.mk_toGerm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α → β) (hf : MeasureTheory.AEStronglyMeasurable f μ), (MeasureTheory.AEEqFun.mk f hf).toGerm = ↑f
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- The everywhere positive subset of a set is the subset made of those points all of whose
neighborhoods have positive measure inside the set.  -/
MeasureTheory.Measure.everywherePosSubset : {α : Type u_1} → [TopologicalSpace α] → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Set α → Set α
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Equivalence.induced_unitIso : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D),
  (CategoryTheory.Equivalence.induced e).unitIso =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.map_volume_mul_left : ∀ {a : ℝ},
  a ≠ 0 → MeasureTheory.Measure.map (fun x => a * x) MeasureTheory.volume = ENNReal.ofReal |a⁻¹| • MeasureTheory.volume
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSingletonClass.mk : ∀ {α : Type u_7} [inst : MeasurableSpace α], (∀ (x : α), MeasurableSet {x}) → MeasurableSingletonClass α
-- Std.Async.UDP
/-- Gets the remote address of the UDP socket. On unconnected handles, it throws the `.invalidArgument`.
error.
 -/
Std.Async.UDP.Socket.getPeerName : Std.Async.UDP.Socket → IO Std.Net.SocketAddress
-- Mathlib.Data.Multiset.MapFold
Multiset.mem_map_of_mem : ∀ {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α}, a ∈ s → f a ∈ Multiset.map f s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGE.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α) (x : Std.DTreeMap.Internal.Impl α β)
  (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.getKeyGE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match h : compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyGED k l ky
      | Ordering.eq => ky
      | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyGE k r ⋯ ⋯
-- Mathlib.FieldTheory.Normal.Defs
/-- Restrict algebra homomorphism to image of normal subfield  -/
AlgHom.restrictNormalAux : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ →ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra E K₁] →
                          [inst_8 : Algebra E K₂] →
                            [inst_9 : IsScalarTower F E K₁] →
                              [inst_10 : IsScalarTower F E K₂] →
                                [h : Normal F E] →
                                  ↥(IsScalarTower.toAlgHom F E K₁).range →ₐ[F] ↥(IsScalarTower.toAlgHom F E K₂).range
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.cfcHom_eq_restrict : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S]
  [inst_10 : Ring A] [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S]
  [inst_18 : TopologicalSpace A] [inst_19 : ContinuousFunctionalCalculus S A q]
  [inst_20 : ContinuousFunctionalCalculus R A p] [ContinuousMap.UniqueHom R A] (f : C(S, R)) {a : A} (hpa : p a)
  (hqa : q a) (h : SpectrumRestricts a ⇑f), cfcHom hpa = SpectrumRestricts.starAlgHom (cfcHom hqa) h
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M},
  MDiff[s] f → (∀ y ∈ s, f₁ y = f y) → MDiff[s] f₁
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgHom.liftOfSurjective_surjective : ∀ {R : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (hf : Function.Surjective ⇑f) (g : A →ₐ[R] C) (H : RingHom.ker f.toRingHom ≤ RingHom.ker g.toRingHom),
  Function.Surjective ⇑g → Function.Surjective ⇑(f.liftOfSurjective hf g H)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Type.adhesive : CategoryTheory.Adhesive (Type u)
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContDiffPointwiseHolderAt.fst : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E × F}, ContDiffPointwiseHolderAt k α Prod.fst a
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.goto : {K : Type u_1} → {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → (σ → Λ) → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.Probability.Kernel.Composition.CompNotation
/-- Composition of a measure and a kernel.

Notation for `MeasureTheory.Measure.bind`  -/
ProbabilityTheory.«term_∘ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_lt_iff_succ_le : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i < p ↔ i.succ ≤ p
-- Mathlib.Topology.ClusterPt
accPt_iff_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, AccPt x F ↔ ClusterPt x (Filter.principal {x}ᶜ ⊓ F)
-- Mathlib.Analysis.Complex.Convex
convex_halfSpace_re_le : ∀ (r : ℝ), Convex ℝ {c | c.re ≤ r}
-- Lean.Data.Json.Basic
Lean.JsonNumber.instOfScientific : OfScientific Lean.JsonNumber
-- Mathlib.NumberTheory.Height.Basic
/-- The nonarchimedean absolute values as a set of `ℝ`-valued absolute values on `K`.  -/
Height.AdmissibleAbsValues.nonarchAbsVal : {K : Type u_1} → {inst : Field K} → [self : Height.AdmissibleAbsValues K] → Set (AbsoluteValue K ℝ)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.semilatticeInf : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} → [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → SemilatticeInf (E →ₛₗ.[σ] F)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.tensorObj_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X.X Y.X X.X Y.X)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
        (CategoryTheory.Mon C)
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.incMatrix_apply_mul_incMatrix_apply : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : MulZeroOneClass R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {a b : α} {e : Sym2 α},
  SimpleGraph.incMatrix R G a e * SimpleGraph.incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffOn.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : DivInvMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {s : Set M} (c : G),
  ContMDiffOn I' I n f s → ContMDiffOn I' I n (fun x => f x / c) s
-- Lean.Meta.ArgsPacker
/-- Given a type `t` of the form `(x : A) → (y : B[x]) → … → (z : D[x,y]) → R[x,y,z]`
returns the curried type `(x : A ⊗' B ⊗' … ⊗' D) → R[x.1, x.2.1, x.2.2]`.
 -/
Lean.Meta.ArgsPacker.Unary.uncurryType : Array Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.eq_one_of_dvd_one : ∀ {a : ℤ}, 0 ≤ a → a ∣ 1 → a = 1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.leftUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Bicategory.leftUnitor η).inv.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.denselyOrdered_range_norm : ∀ (α : Type u_2) [inst : DenselyNormedField α], DenselyOrdered ↑(Set.range norm)
-- Mathlib.Topology.DiscreteSubset
mem_codiscreteWithin_accPt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S T : Set X},
  S ∈ Filter.codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (Filter.principal (T \ S))
-- Mathlib.CategoryTheory.Action
/-- The stabilizer of a point is isomorphic to the endomorphism monoid at the
corresponding point. In fact they are definitionally equivalent.  -/
CategoryTheory.ActionCategory.stabilizerIsoEnd : (M : Type u_1) →
  [inst : Monoid M] →
    {X : Type u} →
      [inst_1 : MulAction M X] → (x : X) → ↥(MulAction.stabilizerSubmonoid M x) ≃* CategoryTheory.End ⟨(), x⟩
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
 -/
Batteries.PairingHeapImp.Heap.fold : {α : Type u_1} → {β : Type u_2} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → β → (β → α → β) → β
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.measureReal_eq_coe_coeFn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω) (s : Set Ω), (↑ν).real s = ↑(ν s)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic
structure.  -/
CategoryTheory.Comonad.forget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (G : CategoryTheory.Comonad C) → CategoryTheory.Functor G.Coalgebra C
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_injective : ∀ {R : Type u_1} [inst : Ring R] (r : R), Function.Injective ⇑(Polynomial.taylor r)
-- Lean.Server.FileWorker.Utils
/-- Appends a sticky diagnostic and marks the next publish as non-incremental.
Removes any existing sticky diagnostic whose `message.stripTags` matches the new one.
 -/
Lean.Server.FileWorker.EditableDocumentCore.appendStickyDiagnostic : Lean.Server.FileWorker.EditableDocumentCore → Lean.Widget.InteractiveDiagnostic → BaseIO Unit
-- Mathlib.Control.Traversable.Instances
Sum.map_traverse : ∀ {σ : Type u} {G : Type u → Type u} [inst : Applicative G] [LawfulApplicative G] {α : Type u_1} {β γ : Type u}
  (g : α → G β) (f : β → γ) (x : σ ⊕ α), (fun x => f <$> x) <$> Sum.traverse g x = Sum.traverse (fun x => f <$> g x) x
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.size.eq_def : ∀ {α : Type u_1} (x : Batteries.BinomialHeap.Imp.Heap α),
  x.size =
    match x with
    | Batteries.BinomialHeap.Imp.Heap.nil => 0
    | Batteries.BinomialHeap.Imp.Heap.cons r val node s => 1 <<< r + s.size
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.mk.sizeOf_spec : ∀ {n : ℕ} (length : ℕ) (partSize : Fin length → ℕ) (partSize_pos : ∀ (m : Fin length), 0 < partSize m)
  (emb : (m : Fin length) → Fin (partSize m) → Fin n) (emb_strictMono : ∀ (m : Fin length), StrictMono (emb m))
  (parts_strictMono : StrictMono fun m => emb m ⟨partSize m - 1, ⋯⟩)
  (disjoint : Set.univ.PairwiseDisjoint fun m => Set.range (emb m)) (cover : ∀ (x : Fin n), ∃ m, x ∈ Set.range (emb m)),
  sizeOf
      { length := length, partSize := partSize, partSize_pos := partSize_pos, emb := emb,
        emb_strictMono := emb_strictMono, parts_strictMono := parts_strictMono, disjoint := disjoint, cover := cover } =
    1 + sizeOf length
-- Mathlib.Order.Lattice
min_min_min_comm : ∀ {α : Type u} [inst : LinearOrder α] (a b c d : α), min (min a b) (min c d) = min (min a c) (min b d)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_map_map_of_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'} (H K : Subgroup G),
  Function.Injective ⇑f → (Subgroup.map f H).relIndex (Subgroup.map f K) = H.relIndex K
-- Mathlib.CategoryTheory.Monad.Products
/-- `X ⨿ -` has a monad structure. This is sometimes called the either monad.  -/
CategoryTheory.coprodMonad : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → C → [CategoryTheory.Limits.HasBinaryCoproducts C] → CategoryTheory.Monad C
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coordChange_same_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B},
  b ∈ e.baseSet → ∀ (x : F), e.coordChange e b x = x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.HasPointwiseLeftKanExtensionAt.of_natIso : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L L' : CategoryTheory.Functor C D} {F F' : CategoryTheory.Functor C H} (Y : D) [L.HasPointwiseLeftKanExtensionAt F Y]
  (e₁ : L ≅ L') (e₂ : F ≅ F'), L'.HasPointwiseLeftKanExtensionAt F' Y
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.ext_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (A B : ↥(Matrix.unitaryGroup n α)), A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk'_apply : ∀ {M : Type u_4} {G : Type u_7} [inst : AddGroup G] [inst_1 : AddZeroClass M] (f : M → G)
  (map_add : ∀ (a b : M), f (a + b) = f a + f b), ⇑(AddMonoidHom.mk' f map_add) = f
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_le : ∀ {ι : Type u_1} {c : Cardinal.{u_1}} {f : ι → Ordinal.{u_1}},
  Cardinal.mk ι ≤ c → (∀ (i : ι), (f i).card ≤ c) → (⨆ i, f i).card ≤ c
-- Init.Data.List.ToArray
List.flatMap_toArray : ∀ {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : List α),
  Array.flatMap f as.toArray = (List.flatMap (fun a => (f a).toList) as).toArray
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.trace.printSimpSetName : Lean.Name → String
-- Mathlib.Order.Lex
/-- A recursor for `Lex`. Use as `induction x`.  -/
Lex.rec : {α : Type u_1} → {β : Lex α → Sort u_2} → ((a : α) → β (toLex a)) → (a : Lex α) → β a
-- Lean.Meta.LazyDiscrTree
/-- A match result contains the terms formed from matching a term against
patterns in the discrimination tree.

 -/
Lean.Meta.LazyDiscrTree.MatchResult : Type → Type
-- Mathlib.Testing.Plausible.Functions
Prod.toSigma.eq_1 : ∀ {α : Type u_7} {β : Type u_8} (p : α × β), p.toSigma = ⟨p.1, p.2⟩
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.node : Aesop.Frontend.Feature → Array Aesop.Frontend.RuleExpr → Aesop.Frontend.RuleExpr
-- Init.Data.Array.Monadic
Array.forIn'_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : (a : α) → a ∈ xs → β → β) (init : β),
  (forIn' xs init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (Array.foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init xs.attach)
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.select.injEq : ∀ (finished finished_1 : Std.Async.Waiter (Option Std.Http.Chunk)),
  (Std.Http.Body.Channel.Consumer.select✝ finished = Std.Http.Body.Channel.Consumer.select✝ finished_1) =
    (finished = finished_1)
-- Mathlib.GroupTheory.Coprod.Basic
/-- Isomorphism between `AddMonoid.Coprod M PUnit` and `M`.  -/
AddEquiv.coprodPUnit : (M : Type u_1) → [inst : AddMonoid M] → AddMonoid.Coprod M PUnit.{u_4 + 1} ≃+ M
-- Mathlib.MeasureTheory.Measure.ResolventTransform
/-- The resolvent transform of a measure.  -/
MeasureTheory.resolventTransform : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NormedRing A] →
        [NormedAlgebra ℝ A] → [NormedAlgebra 𝕜 A] → {m𝕜 : MeasurableSpace 𝕜} → MeasureTheory.Measure 𝕜 → A → A
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instSetLike : {α : Type u_2} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.Clopens α) α
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atBot_mul_left_of_ge : ∀ {α : Type u_1} {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  (∀ (x : α), f x ≤ C) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- An irreducible real polynomial has natural degree at most two.  -/
Irreducible.natDegree_le_two : ∀ {p : Polynomial ℝ}, Irreducible p → p.natDegree ≤ 2
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.maxNilpotentSubmodule_eq_top_of_isNilpotent : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  [LieModule.IsNilpotent L M], LieModule.maxNilpotentSubmodule R L M = ⊤