mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_le_size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)}, m.size ≤ (Std.DHashMap.Const.insertMany m l).size
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.instCommRing : {R : Type u_1} → [inst : CommRing R] → (f : Polynomial R) → CommRing (AdjoinRoot f)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.support_toPath_subset_support`. -/
SimpleGraph.Walk.support_toPath_subset : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).support ⊆ p.support
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a standard Borel space,
then its image under a measurable injective map taking values in a
countably separate measurable space is also Borel-measurable.  -/
MeasurableSet.image_of_measurable_injOn : ∀ {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace α] {s : Set γ} {f : γ → α}
  [MeasurableSpace.CountablySeparated α] [inst_2 : MeasurableSpace γ] [StandardBorelSpace γ],
  MeasurableSet s → Measurable f → Set.InjOn f s → MeasurableSet (f '' s)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_iff_forall_le_3 : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {σ₁ σ₂ σ₃ : Type v} {P Q : σ₁ → σ₂ → σ₃ → l},
  Lean.Order.PartialOrder.rel P Q ↔
    ∀ (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃), Lean.Order.PartialOrder.rel (P s₁ s₂ s₃) (Q s₁ s₂ s₃)
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.isTorsion_def : ∀ {A : Type u_1} [inst : Ring A] (F : IdealFilter A) (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module A M],
  F.IsTorsion M ↔ ∀ (m : M), F.IsTorsionElem m
-- Mathlib.Order.Concept
Concept.instPartialOrder : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → PartialOrder (Concept α β r)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_closedBall : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : PseudoMetricSpace α] [OpensMeasurableSpace α] {x : α} {r : ι → ℝ},
  Filter.Tendsto r l Filter.atTop → MeasureTheory.AECover μ l fun i => Metric.closedBall x (r i)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.isSimplyLaced_D : ∀ (n : ℕ), (CartanMatrix.D n).IsSimplyLaced
-- Init.Data.BitVec.Basic
/-- `twoPow w i` is the bitvector `2^i` if `i < w`, and `0` otherwise. In other words, it is 2 to the
power `i`.

From the bitwise point of view, it has the `i`th bit as `1` and all other bits as `0`.
 -/
BitVec.twoPow : (w : ℕ) → ℕ → BitVec w
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.foldlM_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.normalCore ≤ H
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {a : α}, a • Set.univ = Set.univ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt16.reduceLT : Lean.Meta.Simp.Simproc
-- Init.Data.List.ToArray
List.pop_toArray : ∀ {α : Type u_1} (l : List α), l.toArray.pop = l.dropLast.toArray
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.symm_bijective : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y],
  Function.Bijective DilationEquiv.symm
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsLocalHomValuationInteger : ∀ {R : Type u_1} [inst : CommRing R] {ΓR : Type u_6} [inst_1 : LinearOrderedCommGroupWithZero ΓR] {vR : Valuation R ΓR}
  {S : Type u_9} {ΓS : Type u_10} [inst_2 : CommRing S] [inst_3 : LinearOrderedCommGroupWithZero ΓS]
  [inst_4 : Algebra R S] [IsLocalHom (algebraMap R S)] {vS : Valuation S ΓS} [inst_6 : vR.HasExtension vS],
  IsLocalHom (algebraMap ↥vR.integer ↥vS.integer)
-- Init.Data.Ord.Vector
Vector.instOrientedCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {n : ℕ}, Std.OrientedCmp (Vector.compareLex cmp)
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.descShortComplex_triangleOfSESδ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map (CochainComplex.mappingCone.descShortComplex S))
      (DerivedCategory.triangleOfSESδ hS) =
    CategoryTheory.CategoryStruct.comp (DerivedCategory.Q.map (CochainComplex.mappingCone.triangle S.f).mor₃)
      ((CategoryTheory.Functor.commShiftIso DerivedCategory.Q 1).hom.app S.X₁)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instDFunLike : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → DFunLike (Π₀ (i : ι), β i) ι β
-- Init.Data.Format.Basic
Std.Format.group.injEq : ∀ (a : Std.Format) (behavior : Std.Format.FlattenBehavior) (a_1 : Std.Format) (behavior_1 : Std.Format.FlattenBehavior),
  (a.group behavior = a_1.group behavior_1) = (a = a_1 ∧ behavior = behavior_1)
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.orthogonalProjection.congr_simp : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  EuclideanGeometry.orthogonalProjection s = EuclideanGeometry.orthogonalProjection s
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- **Alias** of `AlgebraicGeometry.smooth_isStableUnderBaseChange`.

---

Smooth is stable under base change.  -/
AlgebraicGeometry.isSmooth_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Smooth
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedHomogeneousComponent_eq_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {w : σ → M} {n : M}
  {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p n → (MvPolynomial.weightedHomogeneousComponent w n) p = p
-- Mathlib.GroupTheory.Nilpotent
/-- The proof that `upperCentralSeriesStep N` is the preimage of the centre of `G/N`\
under the canonical surjection.  -/
AddSubgroup.upperCentralSeriesStep_eq_comap_center : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [inst_1 : N.Normal],
  N.upperCentralSeriesStep = AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.center (G ⧸ N))
-- Mathlib.Data.Fin.Tuple.Sort
/-- A permutation of a tuple `f` is `f` sorted if and only if it is monotone.  -/
Tuple.comp_sort_eq_comp_iff_monotone : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
  f ∘ ⇑σ = f ∘ ⇑(Tuple.sort f) ↔ Monotone (f ∘ ⇑σ)
-- Mathlib.Algebra.MonoidAlgebra.Opposite
AddMonoidAlgebra.opRingEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Add M] (r : Rᵐᵒᵖ) (x : Mᵃᵒᵖ),
  AddMonoidAlgebra.opRingEquiv.symm (AddMonoidAlgebra.single x r) =
    MulOpposite.op (AddMonoidAlgebra.single (AddOpposite.unop x) (MulOpposite.unop r))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ.congr_simp : ∀ {R : Type u_3} {A : Type u_4} {p p_1 : A → Prop} (e_p : p = p_1) [inst : CommSemiring R] [inst_1 : Nontrivial R]
  [inst_2 : StarRing R] [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : IsScalarTower R A A] [inst_11 : SMulCommClass R A A]
  [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f f_1 : R → R),
  f = f_1 → ∀ (a a_1 : A), a = a_1 → cfcₙ f a = cfcₙ f_1 a_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ : Lean.Meta.Grind.Arith.Cutsat.CooperSplit → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.LinearAlgebra.UnitaryGroup
/-- `Matrix.specialOrthogonalGroup n` is the group of orthogonal `n` by `n` where the determinant
is one. (This definition is only correct if 2 is invertible.)  -/
Matrix.specialOrthogonalGroup : (n : Type u) →
  [inst : DecidableEq n] → [inst_1 : Fintype n] → (R : Type v) → [inst_2 : CommRing R] → Submonoid (Matrix n n R)
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `MulOneClass` across an `Equiv`  -/
Equiv.mulOneClass : {α : Type u_2} → {β : Type u_3} → α ≃ β → [MulOneClass β] → MulOneClass α
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.galEquivZMod.eq_1 : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K],
  IsCyclotomicExtension.Rat.galEquivZMod n K = IsCyclotomicExtension.autEquivPow K ⋯
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_smul : ∀ {ι : Type u_1} {R₁ : Type u_9} {S : Type u_10} [inst : CommSemiring R₁] [inst_1 : Semiring S] [inst_2 : Algebra R₁ S]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (x : S) (b : Module.Basis ι R₁ S) (w : ι → S),
  b.toMatrix (x • w) = (Algebra.leftMulMatrix b) x * b.toMatrix w
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.ofReal_essSup : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f →
      ENNReal.ofReal (essSup f μ) = essSup (fun a => ENNReal.ofReal (f a)) μ
-- Mathlib.Analysis.Calculus.MeanValue
IsOpen.is_const_of_deriv_eq_zero : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜},
  IsOpen s → IsPreconnected s → DifferentiableOn 𝕜 f s → Set.EqOn (deriv f) 0 s → ∀ {x y : 𝕜}, x ∈ s → y ∈ s → f x = f y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.fold_filterMapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_10 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n (Option γ)} {g : δ → γ → δ} {init : δ}
  {it : Std.IterM m β},
  Std.IterM.fold g init (Std.IterM.filterMapM f it) =
    Std.IterM.foldM
      (fun d b => do
        let __x ← f b
        match __x with
          | some c => pure (g d c)
          | x => pure d)
      init it
-- Std.Sync.Broadcast
/-- Send a value through the channel, blocking until the transmission could be completed.
 -/
Std.Broadcast.Sync.send : {α : Type} → Std.Broadcast.Sync α → α → IO ℕ
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        {A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} →
          (val : A.obj ⟶ B.obj) →
            autoParam ((CategoryTheory.ConcreteCategory.hom (F.map val)) A.pt = B.pt)
                CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp._autoParam →
              A.Hom B
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getKeyLE? k = Std.DTreeMap.Internal.Impl.getKeyLE?.go k none
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.stabilizer_smul_eq_right : ∀ {G : Type u_1} {β : Type u_3} [inst : Group G] [inst_1 : MulAction G β] {α : Type u_4} [inst_2 : Group α]
  [inst_3 : MulAction α β] [SMulCommClass G α β] (a : α) (b : β),
  MulAction.stabilizer G (a • b) = MulAction.stabilizer G b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The addition of two projective point representatives on a Weierstrass curve.  -/
WeierstrassCurve.Projective.add : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → Fin 3 → R
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_sup : ∀ {R : Type u_2} [inst : NonAssocRing R] (S₁ S₂ : Subring Rᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Init.Data.List.Basic
List.lex_nil : ∀ {α : Type u} {lt : α → α → Bool} [inst : BEq α] {as : List α}, as.lex [] lt = false
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.MkNameState.mk.injEq : ∀ (seen : Lean.ExprSet) (consts : Lean.NameSet) (seen_1 : Lean.ExprSet) (consts_1 : Lean.NameSet),
  ({ seen := seen, consts := consts } = { seen := seen_1, consts := consts_1 }) = (seen = seen_1 ∧ consts = consts_1)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.isGroupLikeElem_of : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M] (m : M), IsGroupLikeElem R ((MonoidAlgebra.of A M) m)
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
/-- Measure version of `preVariation.exists_Finpartition_sum_ge`.  -/
MeasureTheory.VectorMeasure.exists_variation_le_add : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] (μ : MeasureTheory.VectorMeasure X V) {s : Set X},
  MeasurableSet s →
    ∀ {ε : NNReal},
      0 < ε →
        μ.variation s ≠ ⊤ →
          ∃ P,
            (∀ t ∈ P, t ⊆ s) ∧
              (↑P).PairwiseDisjoint id ∧ (∀ t ∈ P, MeasurableSet t) ∧ μ.variation s ≤ ∑ p ∈ P, ‖μ p‖ₑ + ↑ε
-- Mathlib.Analysis.InnerProductSpace.TwoDim
_private.Mathlib.Analysis.InnerProductSpace.TwoDim.0.Orientation.termω : Lean.ParserDescr
-- Lean.Util.NumApps
Lean.Expr.NumApps.State.counters : Lean.Expr.NumApps.State → Lean.NameMap ℕ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ)
  {Y Z : Cᵒᵖ} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).unop =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.unop X) f.unop
-- Mathlib.Order.RelSeries
SetRel.IsWellFounded.eq_1 : ∀ {α : Type u_1} (R : SetRel α α), R.IsWellFounded = WellFounded fun x1 x2 => (x1, x2) ∈ R
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.zero_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.zero h₁ h₂).φK = 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
ContinuousLinearMap.restrictScalars_smul : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : Semiring S] [inst_3 : AddCommMonoid M₁] [inst_4 : Module A M₁] [inst_5 : Module R M₁]
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module A M₂] [inst_9 : Module R M₂]
  [inst_10 : TopologicalSpace M₂] [inst_11 : LinearMap.CompatibleSMul M₁ M₂ R A] [inst_12 : Module S M₂]
  [inst_13 : ContinuousConstSMul S M₂] [inst_14 : SMulCommClass A S M₂] [inst_15 : SMulCommClass R S M₂] (c : S)
  (f : M₁ →L[A] M₂), ContinuousLinearMap.restrictScalars R (c • f) = c • ContinuousLinearMap.restrictScalars R f
-- Mathlib.NumberTheory.NumberField.CMField
/-- The complex conjugation is the conjugation of any complex embedding of a CM-field.
 -/
NumberField.IsCMField.isConj_complexConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K] (φ : K →+* ℂ),
  NumberField.ComplexEmbedding.IsConj φ (NumberField.IsCMField.complexConj K)
-- Mathlib.Data.Nat.Nth
Nat.nth_add_one : ∀ {p : ℕ → Prop} {n : ℕ}, ¬p 0 → Nat.nth p n ≠ 0 → Nat.nth (fun i => p (i + 1)) n + 1 = Nat.nth p n
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul.mk : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : MeasurableSpace M] [inst_2 : MeasurableSpace α]
  [toMeasurableConstSMul : MeasurableConstSMul M α],
  autoParam (∀ (x : α), Measurable fun x_1 => x_1 • x) MeasurableSMul.measurable_smul_const._autoParam →
    MeasurableSMul M α
-- Init.Prelude
/-- Applies a function that returns a list to each element of a list, and concatenates the resulting
lists.

Examples:
* `[2, 3, 2].flatMap List.range = [0, 1, 0, 1, 2, 0, 1]`
* `["red", "blue"].flatMap String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']`
 -/
List.flatMap : {α : Type u} → {β : Type v} → (α → List β) → List α → List β
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.mem_cylinder_comm : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) (n : ℕ), y ∈ PiNat.cylinder x n ↔ x ∈ PiNat.cylinder y n
-- Mathlib.Util.Delaborators
/-- Delaborator for `∉`.  -/
delabNotIn : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteCoproducts F],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
/-- Given `x : CohomologyClass K L n`, this is the element in the type
`SmallShiftedHom` relatively to quasi-isomorphisms that is associated
to the `x`.  -/
CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          [inst_2 :
              CategoryTheory.Localization.HasSmallLocalizedShiftedHom
                (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L] →
            CochainComplex.HomComplex.CohomologyClass K L n →
              CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coeCLE_apply : ∀ {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) (a : A), ↑e a = e a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.forIn_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {b : δ}
  {f : (a : α) × β a → δ → m (ForInStep δ)}, t₁.WF → t₂.WF → t₁.Equiv t₂ → forIn t₁ b f = forIn t₂ b f
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcyclesE._auto_3),
  (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₁ =
    (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.filtration_of_isSuccLimit : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι) [OrderBot ι]
  [SuccOrder ι] (i : ι), Order.IsSuccLimit i → f.filtration i = ⨆ j, ⨆ (_ : j < i), f.filtration j
-- Mathlib.Topology.Instances.Rat
NNRat.instContinuousSub : ContinuousSub ℚ≥0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₂ → (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.Iso.mk_inv : ∀ {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd), (FinPartOrd.Iso.mk e).inv = FinPartOrd.ofHom ↑e.symm
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min?_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k kmi : α},
  (t.insert k).min?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Topology.Instances.RatLemmas
_private.Mathlib.Topology.Instances.RatLemmas.0.«termℚ∞» : Lean.ParserDescr
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instToMessageDataMutVar : Lean.ToMessageData Lean.Elab.Do.MutVar
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAlgebra : {R : Type u_1} →
  {S : Type u_2} → [inst : CommSemiring R] → [inst_1 : Semiring S] → [Algebra R S] → Algebra R (ArithmeticFunction S)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- The action of a lax prefunctor on 2-morphisms.  -/
CategoryTheory.PrelaxFunctorStruct.map₂ : {B : Type u₁} →
  [inst : Quiver B] →
    [inst_1 : (a b : B) → Quiver (a ⟶ b)] →
      {C : Type u₂} →
        [inst_2 : Quiver C] →
          [inst_3 : (a b : C) → Quiver (a ⟶ b)] →
            (self : CategoryTheory.PrelaxFunctorStruct B C) →
              {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (self.map f ⟶ self.map g)
-- Mathlib.Data.EReal.Operations
EReal.neg_eq_top_iff : ∀ {x : EReal}, -x = ⊤ ↔ x = ⊥
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.closedBallAddSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (c : ArchimedeanClass M), c.closedBallAddSubgroup = ArchimedeanClass.addSubgroup (UpperSet.Ici c)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- If `M` is an `R`-module, then the set of `R`-linear maps `S →ₗ[R] M` is an `S`-module with
scalar multiplication defined by `s • l := x ↦ l (x • s)`.

This is an implementation detail: use `(coextendScalars f).obj` instead.
 -/
ModuleCat.CoextendScalars.obj' : {R : Type u₁} → {S : Type u₂} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → ModuleCat R → ModuleCat S
-- Init.Data.AC
Lean.Data.AC.Variable.mk : {α : Sort u} → {op : α → α → α} → (value : α) → Option (PLift (Std.LawfulIdentity op value)) → Lean.Data.AC.Variable op
-- Mathlib.Order.Category.PartOrd
/-- `OrderDual` as a functor.  -/
PartOrd.dual : CategoryTheory.Functor PartOrd PartOrd
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.prod_one : ∀ {α : Type u_1} {n : ℤ} {f : α → ℤ} {s : Finset α}, (∀ x ∈ s, f x ≡ 1 [ZMOD n]) → ∏ x ∈ s, f x ≡ 1 [ZMOD n]