mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Exact
Module.Basis.ofSplitExact.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K} (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g)
  {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {a : κ → ι} {b : σ → ι} (hg : Function.Surjective ⇑g)
  (v : Module.Basis ι R M) (hainj : Function.Injective a) (hsa : ∀ (i : κ), s (v (a i)) = 0)
  (hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)) (hab : Codisjoint (Set.range a) (Set.range b)),
  Module.Basis.ofSplitExact hs hfg hg v hainj hsa hlib hab = Module.Basis.mk ⋯ ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_div_right : ∀ {α : Type u_2} [inst : Group α] {t : Set α} {b : α}, (fun x => x / b) '' t = (fun x => x * b) ⁻¹' t
-- Mathlib.Topology.Instances.ZMultiples
/-- For nonzero `a`, the "multiples of `a`" map `zmultiplesHom` from `ℤ` to `ℝ` is discrete, i.e.
inverse images of compact sets are finite.  -/
Int.tendsto_zmultiplesHom_cofinite : ∀ {a : ℝ}, a ≠ 0 → Filter.Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (Filter.cocompact ℝ)
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- A type synonym used for the compact coherentification of a topological space.  -/
CompactCoherentification.«term𝐤_» : Lean.ParserDescr
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.prod_mk_fst_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.fst x, AddMonoid.Coprod.snd x) = AddMonoid.Coprod.toProd x
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.elem.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α) (as : Array α), Array.elem a as = as.contains a
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (j : J),
  ¬IsMax j → Φ.prop ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE ⋯))
-- Init.Data.Iterators.Producers.List
/-- Returns a finite iterator for the given list.
The iterator yields the elements of the list in order and then terminates.

The monadic version of this iterator is `List.iterM`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
List.iter : {α : Type w} → List α → Std.Iter α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).contains k = true
-- Std.Time.DateTime
/-- Creates a new `DateTime` by adjusting the `minute` component.
 -/
Std.Time.DateTime.withMinutes : Std.Time.DateTime → Std.Time.Minute.Ordinal → Std.Time.DateTime
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- An affine combination of finitely many `C^k` connections on `u` is a `C^k` connection on `u`.  -/
ContMDiffCovariantDerivativeOn.finite_affine_combination : ∀ {𝕜 : 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] [inst_15 : IsManifold I 1 M]
  {n : WithTop ℕ∞} [inst_16 : VectorBundle 𝕜 F V] {ι : Type u_7} {s : Finset ι} {u : Set M}
  {cov : ι → ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x},
  (∀ i ∈ s, ContMDiffCovariantDerivativeOn F n (cov i) u) →
    ∀ {f : ι → M → 𝕜},
      (∀ i ∈ s, ContMDiffOn I (modelWithCornersSelf 𝕜 𝕜) n (f i) u) →
        ContMDiffCovariantDerivativeOn F n (fun σ x => ∑ i ∈ s, f i x • cov i σ x) u
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.instNormedFieldValuedAdicCompletion`.

---

The `v`-adic completion of `K` is a normed field.  -/
NumberField.instNormedFieldValuedAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                [Module.Finite ℤ R] →
                  [Module.Free ℤ R] → NormedField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Nat.Ico_zero : ∀ (m : ℕ), Finset.Ico m 0 = ∅
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily_add : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V} (f g : PowerSeries R),
  HahnSeries.SummableFamily.powerSeriesFamily x (f + g) =
    HahnSeries.SummableFamily.powerSeriesFamily x f + HahnSeries.SummableFamily.powerSeriesFamily x g
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    ∀ {h : Std.Internal.List.containsKey k (Std.Internal.List.Const.modifyKey k f l) = true},
      Std.Internal.List.getValue k (Std.Internal.List.Const.modifyKey k f l) h = f (Std.Internal.List.getValue k l ⋯)
-- Mathlib.Topology.Neighborhoods
IsClosed.interior_union_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.irreducible_iff_natDegree : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic →
    (Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsBigO.natCast_atTop : ∀ {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {R : Type u_17} [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : R → E} {g : R → F},
  f =O[Filter.atTop] g → (fun n => f ↑n) =O[Filter.atTop] fun n => g ↑n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_insertMany!_list : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Init.Data.Ord.Basic
Ordering.swap_eq_lt : ∀ {o : Ordering}, o.swap = Ordering.lt ↔ o = Ordering.gt
-- Mathlib.CategoryTheory.Sites.Continuous
/-- The condition that a functor `F : C ⥤ D` sends 1-hypercovers for
`J : GrothendieckTopology C` to 1-hypercovers for `K : GrothendieckTopology D`.  -/
CategoryTheory.Functor.PreservesOneHypercovers : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.GrothendieckTopology C → CategoryTheory.GrothendieckTopology D → Prop
-- Mathlib.Topology.MetricSpace.Basic
/-- A finite product of metric spaces is a metric space, with the sup distance.  -/
metricSpacePi : {β : Type v} → {X : β → Type u_2} → [Fintype β] → [(b : β) → MetricSpace (X b)] → MetricSpace ((b : β) → X b)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
_private.Mathlib.GroupTheory.Perm.Cycle.Factors.0.Equiv.Perm.isCycleOn_support_cycleOf_aux : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) [inst_2 : DecidableRel f.SameCycle]
  (x : α), f.IsCycleOn ↑(f.cycleOf x).support
-- Mathlib.Order.Filter.CountablyGenerated
Filter.CountableFilterBasis.mk.inj : ∀ {α : Type u_6} {toFilterBasis : FilterBasis α} {countable : toFilterBasis.sets.Countable}
  {toFilterBasis_1 : FilterBasis α} {countable_1 : toFilterBasis_1.sets.Countable},
  { toFilterBasis := toFilterBasis, countable := countable } =
      { toFilterBasis := toFilterBasis_1, countable := countable_1 } →
    toFilterBasis = toFilterBasis_1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.orderTop_vAdd_le_orderTop_smul : ∀ {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid V] {Γ : Type u_6} {Γ' : Type u_7} [inst_1 : LinearOrder Γ]
  [inst_2 : LinearOrder Γ'] [inst_3 : VAdd Γ Γ'] [inst_4 : IsOrderedCancelVAdd Γ Γ'] [inst_5 : MulZeroClass R]
  [inst_6 : SMulWithZero R V] {x : HahnSeries Γ R} [inst_7 : VAdd (WithTop Γ) (WithTop Γ')] {y : HahnModule Γ' R V},
  (∀ (γ : Γ) (γ' : Γ'), ↑(γ +ᵥ γ') = ↑γ +ᵥ ↑γ') →
    x.orderTop +ᵥ ((HahnModule.of R).symm y).orderTop ≤ ((HahnModule.of R).symm (x • y)).orderTop
-- Mathlib.Topology.Compactness.SigmaCompact
sigmaCompactSpace_of_locallyCompact_secondCountable : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X], SigmaCompactSpace X
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j) (F.map f) = CategoryTheory.Limits.limit.π F j'
-- Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
/-- Continuous maps from a compact space to an ultrametric space are an ultrametric space.  -/
ContinuousMap.isUltrametricDist : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : MetricSpace Y]
  [IsUltrametricDist Y], IsUltrametricDist C(X, Y)
-- Batteries.Data.Nat.Bisect
Nat.bisect.eq_def : ∀ {start stop : ℕ} {p : ℕ → Bool} (h : start < stop) (hstart : p start = true) (hstop : p stop = false),
  Nat.bisect h hstart hstop =
    let mid := start.avg stop;
    have hmidstop := ⋯;
    if hstartmid : start < mid then
      match hmid : p mid with
      | false => Nat.bisect hstartmid hstart hmid
      | true => Nat.bisect hmidstop hmid hstop
    else mid
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_mem : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α], s.Nonempty → sInf s ∈ s
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasCoproducts_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasCoproducts C
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.range_mk : ∀ (R ι : Type u) [inst : CommSemiring R] (M : Type v) [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (SymmetricPower.mk R ι M).range = ⊤
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
/-- **Alias** of `MeasureTheory.OuterMeasure.isCaratheodory_sdiff`. -/
MeasureTheory.OuterMeasure.isCaratheodory_diff : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α},
  m.IsCaratheodory s₁ → m.IsCaratheodory s₂ → m.IsCaratheodory (s₁ \ s₂)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsLittleO.right_isTheta_add : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] f₂ → f₂ =Θ[l] (f₁ + f₂)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow.congr_simp : ∀ {p p_1 : ℕ} (e_p : p = p_1) {k k_1 : ℕ} (e_k : k = k_1) {K : Type u} [inst : Field K] {ζ ζ_1 : K} (e_ζ : ζ = ζ_1)
  [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K] [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K]
  (hζ : IsPrimitiveRoot ζ (p ^ k)), hζ.subOneIntegralPowerBasisOfPrimePow = ⋯.subOneIntegralPowerBasisOfPrimePow
-- Mathlib.Tactic.Translate.GuessName
/-- Dictionary used by `guessName` to autogenerate names.
This only transforms single name components, unlike `abbreviationDict`.

Note: `guessName` capitalizes the output according to the capitalization of the input.
In order for this to work, the input should always start with a lower case letter, and the output
should always start with an upper case letter.
 -/
Mathlib.Tactic.GuessName.GuessNameData.nameDict : Mathlib.Tactic.GuessName.GuessNameData → Std.HashMap String (List String)
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_eq : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) {y : N} (r : R)
  (hr : r • y ∈ (Module.Baer.extensionOfMax i f).domain),
  (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r =
    ↑(Module.Baer.extensionOfMax i f).toLinearPMap ⟨r • y, hr⟩
-- Mathlib.Data.Matrix.Mul
/-- Bilinear form identity: `x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x` for commutative semirings.  -/
Matrix.dotProduct_transpose_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalCommSemiring α] [inst_1 : Fintype m] [inst_2 : Fintype n]
  (A : Matrix m n α) (x : n → α) (y : m → α), x ⬝ᵥ A.transpose.mulVec y = y ⬝ᵥ A.mulVec x
-- Lean.Data.SMap
Lean.SMap.empty : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.le_coverMincard_image : ∀ {X : Type u_1} {Y : Type u_2} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) [V.IsSymm] (n : ℕ),
      Dynamics.coverMincard S F (Prod.map φ φ ⁻¹' V.comp V) n ≤ Dynamics.coverMincard T (φ '' F) V n
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : EInt) (X : C),
  (t.eTruncGEToGEGE a b).app X = (t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.edist_eval_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace β] {f g : UniformFun α β} {x : α},
  edist (UniformFun.toFun f x) (UniformFun.toFun g x) ≤ edist f g
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Let `e` be an open partial homeomorphism. If for every `x ∈ e.source`, the restriction of e
to some open set around `x` lies in the groupoid, then `e` lies in the groupoid.  -/
StructureGroupoid.locality' : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : StructureGroupoid H) (e : OpenPartialHomeomorph H H),
  (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ self.members) → e ∈ self.members
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_map : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'}
  {μ : MeasureTheory.Measure Ω'} {Z : Ω' → Ω},
  MeasureTheory.AEStronglyMeasurable X (MeasureTheory.Measure.map Z μ) →
    MeasureTheory.AEStronglyMeasurable Y (MeasureTheory.Measure.map Z μ) →
      AEMeasurable Z μ →
        ProbabilityTheory.covariance X Y (MeasureTheory.Measure.map Z μ) =
          ProbabilityTheory.covariance (X ∘ Z) (Y ∘ Z) μ
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ioc_eq_card_Icc_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Finset.Ioc a b).card = (Finset.Icc a b).card - 1
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.pure.injEq : ∀ (h h_1 : Lean.TSyntax `term),
  (Lean.Parser.Tactic.MRefinePat.pure h = Lean.Parser.Tactic.MRefinePat.pure h_1) = (h = h_1)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- Elementary tensors are members of the maximal tensor product.  -/
PointedCone.tmul_mem_maxTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H] {x : G}
  {y : H} {C₁ : PointedCone R G} {C₂ : PointedCone R H}, x ∈ C₁ → y ∈ C₂ → x ⊗ₜ[R] y ∈ C₁.maxTensorProduct C₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.keys.isEmpty = t.isEmpty
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- A monad equipped with the ability to construct `WhiskerRight` terms.  -/
Mathlib.Tactic.BicategoryLike.MonadWhiskerRight : (Type → Type) → Type
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer_append : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w)
  (hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet),
  (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ObjectProperty.IsClosedUnderExtensions CategoryTheory.Limits.IsZero
-- Mathlib.Algebra.Order.Group.Cyclic
/-- Given an additive cyclic linearly ordered commutative group, this is a
negative generator of it.  -/
LinearOrderedAddCommGroup.negGen : (G : Type u_1) →
  [inst : AddCommGroup G] → [inst_1 : LinearOrder G] → [IsOrderedAddMonoid G] → [Nontrivial G] → [IsAddCyclic G] → G
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.support_rename_of_injective : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ}
  [inst_1 : DecidableEq τ],
  Function.Injective f → ((MvPolynomial.rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- Given the set `i` and the natural number `n`, `ExistsOneDivLT s i j` is the property that
there exists a measurable set `k ⊆ i` such that `1 / (n + 1) < s k`.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.ExistsOneDivLT : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → Set α → ℕ → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.IsLimit.lift_ι_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {c : CategoryTheory.Limits.Wedge F}
  (hc : CategoryTheory.Limits.IsLimit c) {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J) {Z : C} (h : (CategoryTheory.Limits.multicospanIndexEnd F).left j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Wedge.IsLimit.lift hc f hf)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multifork.ι c j) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Mathlib.Topology.Algebra.Monoid
addMonoidHomOfTendsto.eq_1 : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂]
  [inst_2 : AddZeroClass M₁] [inst_3 : AddZeroClass M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8}
  [inst_5 : FunLike F M₁ M₂] [inst_6 : AddMonoidHomClass F M₁ M₂] {l : Filter α} (f : M₁ → M₂) (g : α → F)
  [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  addMonoidHomOfTendsto f g h = addMonoidHomOfMemClosureRangeCoe f ⋯
-- Std.Sync.CancellationToken
/-- A cancellation token is a synchronization primitive that allows multiple consumers to wait
until cancellation is requested.
 -/
Std.CancellationToken : Type
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.image_closure : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set A), ⇑e '' closure S = closure (⇑e '' S)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.iff_of_isoObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)} {Y : C} (e : Y ≅ X),
  F.IsRepresentedBy ((CategoryTheory.ConcreteCategory.hom (F.map e.hom.op)) x) ↔ F.IsRepresentedBy x
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.HasProductsOfShapeAux.instCatCommSqFunctorDiscreteLimObjWhiskeringRightLimitFunctor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : L.IsLocalization W] →
              (J : Type) →
                [inst_3 : CategoryTheory.Limits.HasProductsOfShape J C] →
                  [inst_4 : W.IsStableUnderProductsOfShape J] →
                    [inst_5 : W.ContainsIdentities] →
                      [inst_6 : Finite J] →
                        CategoryTheory.CatCommSq CategoryTheory.Limits.lim
                          ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Discrete J) C D).obj L) L
                          (CategoryTheory.Localization.HasProductsOfShapeAux.limitFunctor L W J)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.desc.multicofork_π_three : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₀₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁),
  (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨3, SSet.horn₃₂.desc.multicofork_π_three._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 3).inv f₃
-- Init.Control.State
StateT.instMonadFunctor : (σ : Type u_1) → (m : Type u_1 → Type u_2) → MonadFunctor m (StateT σ m)
-- Mathlib.Algebra.Module.Submodule.Defs
SubmoduleClass.module' : {S : Type u'} →
  {R : Type u} →
    {M : Type v} →
      {T : Type u_1} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Semiring S] →
              [inst_3 : Module R M] →
                [inst_4 : SMul S R] →
                  [inst_5 : Module S M] →
                    [IsScalarTower S R M] →
                      [inst_7 : SetLike T M] →
                        [inst_8 : AddSubmonoidClass T M] → [SMulMemClass T R M] → (t : T) → Module S ↥t
-- Mathlib.Algebra.Ring.Equiv
/-- A ring is isomorphic to the opposite of its opposite.  -/
RingEquiv.opOp : (R : Type u_7) → [inst : Add R] → [inst_1 : Mul R] → R ≃+* Rᵐᵒᵖᵐᵒᵖ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffOn_arcsin : ∀ {n : WithTop ℕ∞}, ContDiffOn ℝ n Real.arcsin {-1, 1}ᶜ