mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.NameTrie
Lean.NameTrie.forM : {m : Type → Type u_1} → {β : Type u_2} → [Monad m] → Lean.NameTrie β → (β → m Unit) → m Unit
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.StrictMono.mk_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] {a : ℕ → ℕ} (ha : StrictMono a)
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ a n • ⊤) (hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m)
  [inst_5 : IsAdicComplete I N] {n : ℕ} (x : M),
  Submodule.Quotient.mk ((IsAdicComplete.StrictMono.lift I ha f ⋯) x) = (f n) x
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
/-- A set `s` is Carathéodory-measurable for an outer measure `m` if for all sets `t` we have
`m t = m (t ∩ s) + m (t \ s)`.  -/
MeasureTheory.OuterMeasure.IsCaratheodory : {α : Type u} → MeasureTheory.OuterMeasure α → Set α → Prop
-- Lean.Server.FileWorker.ExampleHover
/-- In an `output` code block indented `indent` columns opened with `ticks` backtick characters  -/
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.output : ℕ → ℕ → Lean.Server.FileWorker.Hover.RWState✝
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.post_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post F G)
      (G.map (CategoryTheory.Limits.colimit.desc F c)) =
    CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone c)
-- Mathlib.GroupTheory.Order.Min
AddMonoid.minOrder_le_addOrderOf : ∀ {α : Type u_2} [inst : AddMonoid α] {a : α}, a ≠ 0 → IsOfFinAddOrder a → AddMonoid.minOrder α ≤ ↑(addOrderOf a)
-- Mathlib.Combinatorics.Enumerative.Bell
_private.Mathlib.Combinatorics.Enumerative.Bell.0.Multiset.bell_mul_eq_lemma : ∀ {x : ℕ},
  x ≠ 0 →
    ∀ (c : ℕ), x.factorial ^ c * c.factorial * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1) = (x * c).factorial
-- Mathlib.Data.Nat.Count
/-- **Alias** of the reverse direction of `Nat.count_succ_eq_count_iff`. -/
Nat.count_succ_eq_count : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, ¬p n → Nat.count p (n + 1) = Nat.count p n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MonotoneOn.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulRightMono α], MonotoneOn f s → ∀ (a : α), MonotoneOn (fun x => f x * a) s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_add_lt_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [i : AddRightReflectLT α] {a b c : α}, b + a < c + a → b < c
-- Mathlib.Data.Nat.Totient
/-- Euler's product formula for the totient function.  -/
Nat.totient_eq_div_primeFactors_mul : ∀ (n : ℕ), n.totient = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)
-- Mathlib.Data.Finset.Defs
Finset.exists_coe : ∀ {α : Type u_4} (s : Finset α) (p : ↥s → Prop), (∃ x, p x) ↔ ∃ x, ∃ (h : x ∈ s), p ⟨x, h⟩
-- Mathlib.Analysis.ODE.PicardLindelof
/-- `α` is a fixed point of `next` if and only if it satisfies the integral equation
`α t = x + ∫_{t₀}^t f τ (α τ) dτ` for all `t`.  -/
ODE.FunSpace.isFixedPt_next_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) {α : ODE.FunSpace t₀ x₀ r L},
  Function.IsFixedPt (ODE.FunSpace.next hf hx) α ↔
    ∀ (t : ↑(Set.Icc tmin tmax)), α.toFun t = ODE.picard f (↑t₀) x α.compProj ↑t
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.leftTriple_adj₁ : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R), q.leftTriple.adj₁ = q.adj₁
-- Mathlib.FieldTheory.Minpoly.Field
/-- If an element `x` is a root of a nonzero polynomial `p`, then the degree of `p` is at least the
degree of the minimal polynomial of `x`. See also `minpoly.IsIntegrallyClosed.degree_le_of_ne_zero`
which relaxes the assumptions on `A` in exchange for stronger assumptions on `B`.  -/
minpoly.degree_le_of_ne_zero : ∀ (A : Type u_1) {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B) {p : Polynomial A},
  p ≠ 0 → (Polynomial.aeval x) p = 0 → (minpoly A x).degree ≤ p.degree
-- Mathlib.Analysis.SpecificLimits.Normed
/-- `v (1 / (1 + a ^n))` tends to `0` whenever `v : AbsoluteValue R S` for fields `R` and `S`,
provided `1 < v a`.  -/
AbsoluteValue.tendsto_div_one_add_pow_nhds_zero : ∀ {R : Type u_2} {S : Type u_3} [inst : Field R] [inst_1 : Field S] [inst_2 : LinearOrder S]
  [inst_3 : TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S] {v : AbsoluteValue R S}
  {a : R}, 1 < v a → Filter.Tendsto (fun n => v (1 / (1 + a ^ n))) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.δ₀Functor_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {X Y : CategoryTheory.ComposableArrows C (n + 1)}
  (f : X ⟶ Y) (X_1 : Fin (n + 1)), (CategoryTheory.ComposableArrows.δ₀Functor.map f).app X_1 = f.app X_1.succ
-- Mathlib.Algebra.BigOperators.Fin
Fin.partialSum_contractNth : ∀ {G : Type u_3} [inst : AddMonoid G] {n : ℕ} (g : Fin (n + 1) → G) (a : Fin (n + 1)),
  Fin.partialSum (a.contractNth (fun x1 x2 => x1 + x2) g) = Fin.partialSum g ∘ a.succ.succAbove
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : Preorder α] [AddLeftStrictMono α] {a b c d : α},
  a < b → c < d → a - d < b - c
-- Init.Data.List.Range
List.length_range' : ∀ {s step n : ℕ}, (List.range' s n step).length = n
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
CongruenceSubgroup.Gamma_one_top : CongruenceSubgroup.Gamma 1 = ⊤
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.closure_coe_completion_v_mul_v_lt : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {r s : K},
  r ≠ 0 →
    s ≠ 0 →
      closure (UniformSpace.Completion.coe' '' {x | Valued.v x * Valued.v r < Valued.v s}) =
        {x | Valued.extensionValuation x * Valued.v r < Valued.v s}
-- Init.Data.List.Nat.TakeDrop
List.take_subset_take_left : ∀ {α : Type u_1} (l : List α) {i j : ℕ}, i ≤ j → List.take i l ⊆ List.take j l
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of `Topology.IsInducing.setOfPred_isOpen`. -/
Topology.IsInducing.setOf_isOpen : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → {s | IsOpen s} = Set.preimage f '' {t | IsOpen t}
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.mul_def : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Mul (M i)] (f g : (i : ι) → M i), f * g = fun i => f i * g i
-- Mathlib.Data.EReal.Basic
EReal.toReal_image_Ioo_zero_top : EReal.toReal '' Set.Ioo 0 ⊤ = Set.Ioi 0
-- Mathlib.Order.Disjoint
codisjoint_ofDual_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : αᵒᵈ},
  Codisjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Disjoint a b
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofiltered_op_iff_isFiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.IsCofiltered Cᵒᵖ ↔ CategoryTheory.IsFiltered C
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.ofNat_eq_coe : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo] (m : α),
  OfNat.ofNat n = ↑m ↔ OfNat.ofNat n = m
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_map : ∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {γ' : Type u_8} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} (f : α → β → γ) (g : γ → γ') (A : Matrix l m α) (B : Matrix n p β),
  (Matrix.kroneckerMap f A B).map g = Matrix.kroneckerMap (fun a b => g (f a b)) A B
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_eq_zero_iff : ∀ {E : Type u_5} [inst : NormedGroup E] {a b : E}, ‖a / b‖ = 0 ↔ a = b
-- Lean.Elab.InfoTree.Types
Lean.Elab.FieldRedeclInfo.mk.inj : ∀ {stx stx_1 : Lean.Syntax}, { stx := stx } = { stx := stx_1 } → stx = stx_1
-- Mathlib.Data.FunLike.Graded
/-- The class `GradedFunLike F 𝒜 ℬ` expresses that terms of type `F` have an injective coercion to
grading-preserving functions from `A` to `B`, where `𝒜` is a grading on `A` and `ℬ` is a grading on
`B`. This typeclass has `[FunLike F A B]` as one of the assumptions. This typeclass is used in the
characterisation of certain types of graded homomorphisms, such as `GradedRingHom` and
`GradedAlgHom`. For example, what would be called `"GradedRingHomClass F 𝒜 ℬ`" would be expressed
as `[FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B]`.
 -/
GradedFunLike : (F : Type u_1) →
  {A : outParam (Type u_2)} →
    {B : outParam (Type u_3)} →
      {σ : outParam (Type u_4)} →
        {τ : outParam (Type u_5)} →
          {ι : outParam (Type u_6)} →
            [SetLike σ A] → [SetLike τ B] → outParam (ι → σ) → outParam (ι → τ) → [FunLike F A B] → Prop
-- Lean.LibrarySuggestions.Basic
/-- Get the currently registered library suggestions selector by looking up the stored declaration name.
Returns `none` if no selector is registered or if evaluation fails.
 -/
Lean.LibrarySuggestions.getSelectorImpl : Lean.MetaM (Option Lean.LibrarySuggestions.Selector)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.instVAddAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : VAdd M α] →
              [MeasurableConstVAdd M α] → [MeasureTheory.VAddInvariantMeasure M α μ] → VAdd Mᵈᵃᵃ (α →ₘ[μ] β)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `neg_apply`. -/
ContinuousLinearMap.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Init.Data.Nat.Lcm
Nat.instLawfulIdentityLcmOfNat : Std.LawfulIdentity Nat.lcm 1
-- Mathlib.Data.Set.Function
Set.InjOn.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → Set.InjOn (Set.image f) (𝒫 s)
-- Lean.Server.Requests
Lean.Server.RequestError.requestCancelled : Lean.Server.RequestError
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.coe_subtype : ∀ {K : Type u} [inst : Field K] (R : ValuationSubring K), ⇑R.subtype = Subtype.val
-- Mathlib.Analysis.Normed.Ring.Basic
RingHomIsometric.ids : ∀ {R₁ : Type u_5} [inst : SeminormedRing R₁], RingHomIsometric (RingHom.id R₁)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.toFreeAddGroup_apply : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] (a : G),
  (IsFreeAddGroup.toFreeAddGroup G) a = (IsFreeAddGroup.addEquiv G).symm a
-- Mathlib.Order.RelIso.Basic
RelIso.map_rel_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s) {a b : α}, s (f a) (f b) ↔ r a b
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.isUnaryNode : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β → Option (α × β)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.measureReal_eq_coe_coeFn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {s : Set Ω}, (↑μ).real s = ↑(μ s)
-- Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization
/-- A localization of a unique factorization monoid is still a unique factorization monoid.  -/
UniqueFactorizationMonoid.of_isLocalization : ∀ {M : Type u_1} [inst : CommSemiring M] (S : Submonoid M) (N : Type u_3) [inst_1 : CommSemiring N]
  [inst_2 : Algebra M N] [IsLocalization S N] [UniqueFactorizationMonoid M], UniqueFactorizationMonoid N
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- `LinearMap.normDet` equals the norm of `LinearMap.det` for an endomorphism.
 -/
LinearMap.normDet_eq_norm_det : ∀ {𝕜 : Type u_1} {U : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U] [inst_2 : InnerProductSpace 𝕜 U]
  [inst_3 : FiniteDimensional 𝕜 U] (f : U →ₗ[𝕜] U), f.normDet = ‖LinearMap.det f‖
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddMonoidHom.pi`.

---

A family of additive monoid homomorphisms `f a : γ →+ β a` defines a monoid homomorphism
`Pi.addMonoidHom f : γ →+ Π a, β a` given by `Pi.addMonoidHom f x b = f b x`.  -/
Pi.addMonoidHom : {I : Type u} →
  {f : I → Type v} →
    [inst : (i : I) → AddZeroClass (f i)] →
      {γ : Type w} → [inst_1 : AddZeroClass γ] → ((i : I) → γ →+ f i) → γ →+ (i : I) → f i
-- Mathlib.Data.Finset.Slice
Finset.subset_powersetCard_univ_iff : ∀ {α : Type u_1} [inst : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  𝒜 ⊆ Finset.powersetCard r Finset.univ ↔ Set.Sized r ↑𝒜
-- Init.Data.Format.Basic
Std.Format.text.sizeOf_spec : ∀ (a : String), sizeOf (Std.Format.text a) = 1 + sizeOf a
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.root_link : ∀ {self : Batteries.UnionFind} {x y : Fin self.size},
  self.parent ↑x = ↑x →
    ∀ (yroot : self.parent ↑y = ↑y),
      ∃ r,
        (r = x ∨ r = y) ∧
          ∀ (i : ℕ), (self.link x y yroot).rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑r else self.rootD i
-- Init.Data.SInt.Lemmas
ISize.toInt_add : ∀ (a b : ISize), (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ System.Platform.numBits)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.ker_inclusion : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K), (Subgroup.inclusion h).ker = ⊥
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- **Alias** of `CovariantDerivative.ofIsCovariantDerivativeOnOfOpenCover`.

---

If `cov` is a covariant derivative on each set in an open cover, it is a covariant derivative.
 -/
CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            {ι : Type u_7} →
                                              {s : ι → Set M} →
                                                {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} →
                                                  (∀ (i : ι), IsCovariantDerivativeOn F cov (s i)) →
                                                    ⋃ i, s i = Set.univ → CovariantDerivative I F V
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_eq_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] {M : Matrix n n α} {v : n → α},
  M.transpose = Matrix.diagonal v ↔ M = Matrix.diagonal v
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.Label.elim.sizeOf_spec : sizeOf Lean.Meta.NormCast.Label.elim = 1
-- Mathlib.MeasureTheory.Function.EssSup
essInf_const' : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLattice β] [NeZero μ] (c : β), essInf (fun x => c) μ = c
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.sunday.sizeOf_spec : sizeOf Std.Time.Weekday.sunday = 1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.underObj_iff : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  (Y : CategoryTheory.Under X), W.underObj Y ↔ W Y.hom
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
/-- The property of reflecting coproducts expressed in terms of binary cofans.  -/
CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {P X Y : C} →
            (f : X ⟶ P) →
              (g : Y ⟶ P) →
                [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.pair X Y) G] →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map f) (G.map g)) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)
-- Init.Data.Vector.Range
Vector.map_sub_range' : ∀ {step a s : ℕ}, a ≤ s → ∀ (n : ℕ), Vector.map (fun x => x - a) (Vector.range' s n step) = Vector.range' (s - a) n step
-- Init.Prelude
Div.mk : {α : Type u} → (α → α → α) → Div α
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The second triangle identity for the counit and unit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.coev_ev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  (Y : CategoryTheory.Over I),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ExponentiableMorphism.coev f).app ((CategoryTheory.ExponentiableMorphism.pushforward f).obj Y))
      ((CategoryTheory.ExponentiableMorphism.pushforward f).map ((CategoryTheory.ExponentiableMorphism.ev f).app Y)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ExponentiableMorphism.pushforward f).obj Y)
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
NNReal.orderIsoRpow.congr_simp : ∀ (y y_1 : ℝ) (e_y : y = y_1) (hy : 0 < y), NNReal.orderIsoRpow y hy = NNReal.orderIsoRpow y_1 ⋯
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_zero_iff_even : ∀ {n : ℕ}, ↑n = 0 ↔ Even n
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.as_bijective : ∀ {α : Type u_1}, Function.Bijective CategoryTheory.Discrete.as
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_closure_of_univ : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α],
  (∀ (ε : ENNReal), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε) → μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxo.Iterator.nodup_toList : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  {it : Std.Iter α}, it.toList.Nodup
-- Mathlib.CategoryTheory.Functor.Basic
/-- Notation for a functor between categories.  -/
CategoryTheory.«term_⥤_» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.eraseListₘ : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → List α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.instCoalgebra : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : AddCommMonoid A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Algebra R S] →
                  [inst_5 : Module R A] →
                    [inst_6 : Module S A] →
                      [inst_7 : Module R B] →
                        [inst_8 : IsScalarTower R S A] →
                          [Coalgebra R B] → [Coalgebra S A] → Coalgebra S (TensorProduct R A B)
-- Mathlib.Computability.Encoding
_private.Mathlib.Computability.Encoding.0.Computability.decodePosNum.match_1.eq_2 : ∀ (motive : List Bool → Sort u_1) (l : List Bool) (h_1 : (l : List Bool) → motive (false :: l))
  (h_2 : (l : List Bool) → motive (true :: l)) (h_3 : (x : List Bool) → motive x),
  (match true :: l with
    | false :: l => h_1 l
    | true :: l => h_2 l
    | x => h_3 x) =
    h_2 l
-- Init.Omega.Constraint
Lean.Omega.Constraint.add_sat : ∀ {c₁ c₂ : Lean.Omega.Constraint} {x₁ x₂ : ℤ}, c₁.sat x₁ = true → c₂.sat x₂ = true → (c₁.add c₂).sat (x₁ + x₂) = true
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (W X Y Z : C) {Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          (CategoryTheory.CategoryStruct.id Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
              Z).hom
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        h)
-- Mathlib.Analysis.Complex.Basic
Complex.equivRealProdCLM_symm_apply_im : ∀ (a : ℝ × ℝ), (Complex.equivRealProdCLM.symm a).im = a.2
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddLocalization.Away.mk_eq_addMonoidOf_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M),
  AddLocalization.mk = AddSubmonoid.LocalizationMap.mk' (AddLocalization.Away.addMonoidOf x)
-- Mathlib.Order.UpperLower.Hom
/-- `LowerSet.Iic` as an `sInfHom`.  -/
LowerSet.iicsInfHom : {α : Type u_1} → [inst : CompleteLattice α] → sInfHom α (LowerSet α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one_ne_top : ∀ {α : Type u} [inst : One α], 1 ≠ ⊤
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.MutuallySingular.singularPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν → ∀ (ν' : MeasureTheory.Measure α), (μ.singularPart ν').MutuallySingular ν