mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit_lift_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cone D),
  ((CategoryTheory.Monad.ForgetCreatesLimits.liftedConeIsLimit D c t).lift s).f = t.lift (T.forget.mapCone s)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.exists_mem_algebraMap_eq : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [loc : IsLocalization S P] {x : R} {I : Ideal R},
  S ≤ nonZeroDivisors R → ((∃ x' ∈ I, (algebraMap R P) x' = (algebraMap R P) x) ↔ x ∈ I)
-- Mathlib.RingTheory.Smooth.Locus
Algebra.basicOpen_subset_smoothLocus_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] {f : A},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Algebra.smoothLocus R A ↔ Algebra.FormallySmooth R (Localization.Away f)
-- Mathlib.Order.Irreducible
/-- In a cowell-founded lattice, any element is the infimum of finitely many inf-irreducible
elements. This is the order-theoretic analogue of prime factorisation.  -/
exists_infIrred_decomposition : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [WellFoundedGT α] (a : α),
  ∃ s, s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → InfIrred b
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.equivNum.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsDomain R] [inst_4 : Module.IsTorsionFree R P] [inst_5 : Nontrivial P] {I : FractionalIdeal S P}
  (h_nz : ↑I.den ≠ 0), FractionalIdeal.equivNum h_nz = FractionalIdeal.equivNumOfIsSMulRegular ⋯
-- Std.Http.Server.Handler
/-- Concrete body type produced by `onRequest`.
Defaults to `Body.Any`, but handlers may override it with any reader/writer-compatible body.
 -/
Std.Http.Server.Handler.ResponseBody : (σ : Type) → [self : Std.Http.Server.Handler σ] → Type
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.isUnit_iff_isUnit_val : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] (𝒜 : ι → σ) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜] (𝔭 : Ideal A) [inst_6 : 𝔭.IsPrime] (f : HomogeneousLocalization.AtPrime 𝒜 𝔭),
  IsUnit (HomogeneousLocalization.val f) ↔ IsUnit f
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Free
FreeAddSemigroup.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α),
  (FreeAddSemigroup.map f) (FreeAddSemigroup.of x) = FreeAddSemigroup.of (f x)
-- Std.Time.DateTime.WallTime
/-- Converts a `WallTime` to a `Second.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.toSeconds : Std.Time.WallTime → Std.Time.Second.Offset
-- Lean.Parser.Attr
Lean.Parser.Priority.numPrio.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_congr_ae : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {f g : α → F'}
  (hm : m ≤ m0), f =ᵐ[μ] g → MeasureTheory.condExpL1 hm μ f = MeasureTheory.condExpL1 hm μ g
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- Composing the preadditive yoneda embedding with the forgetful functor yields the regular
Yoneda embedding.
 -/
CategoryTheory.whiskering_preadditiveYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveYoneda.comp
      ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ AddCommGrpCat (Type v)).obj (CategoryTheory.forget AddCommGrpCat)) =
    CategoryTheory.yoneda
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.quasiMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb → MeasureTheory.Measure.QuasiMeasurePreserving f μa μb
-- Lean.Data.Lsp.Internal
/-- Identifier of a reference.
 -/
Lean.Lsp.RefIdent : Type
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₂_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ 2) (groupCohomology.isoCocycles₂ B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom (groupCohomology.mapCocycles₂ f φ)
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.instContinuousMul : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜], ContinuousMul ↑(Metric.closedBall 0 1)
-- Init.Data.Array.Subarray
Std.Slice.Internal.SubarrayData.mk.injEq : ∀ {α : Type u} (array : Array α) (start stop : ℕ) (start_le_stop : start ≤ stop)
  (stop_le_array_size : stop ≤ array.size) (array_1 : Array α) (start_1 stop_1 : ℕ) (start_le_stop_1 : start_1 ≤ stop_1)
  (stop_le_array_size_1 : stop_1 ≤ array_1.size),
  ({ array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size } =
      { array := array_1, start := start_1, stop := stop_1, start_le_stop := start_le_stop_1,
        stop_le_array_size := stop_le_array_size_1 }) =
    (array = array_1 ∧ start = start_1 ∧ stop = stop_1)
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Simple function defined on the empty type.  -/
MeasureTheory.SimpleFunc.ofIsEmpty : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [IsEmpty α] → MeasureTheory.SimpleFunc α β
-- Mathlib.Algebra.Group.Defs
/-- Any `LeftCancelSemigroup` satisfies `IsLeftCancelMul`.  -/
LeftCancelSemigroup.toIsLeftCancelMul : ∀ {G : Type u} [self : LeftCancelSemigroup G], IsLeftCancelMul G
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus : Type
-- Mathlib.Data.ENNReal.Real
ENNReal.ofReal_le_ofReal_iff' : ∀ {p q : ℝ}, ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q ∨ p ≤ 0
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_pos_of_ne_zero : ∀ {p : Polynomial ℂ}, p ≠ 0 → 0 < p.mahlerMeasure
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false →
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter m₂ ⋯) k = default
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β k}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl = true},
  (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.getKey a h₁ =
    if h₂ : compare k a = Ordering.eq then k else t.getKey a ⋯
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.integral_one_div_log_sq_isBigO : (fun x => ∫ (t : ℝ) in 2..x, 1 / Real.log t ^ 2) =O[Filter.atTop] fun x => x / Real.log x ^ 2
-- Init.GetElem
List.getElem_cons_zero : ∀ {α : Type u_1} (a : α) (as : List α) (h : 0 < (a :: as).length), (a :: as)[0] = a
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Normalized GCD monoid: a cancellative `CommMonoidWithZero` with normalization and `gcd`
(greatest common divisor) and `lcm` (least common multiple) operations. In this setting `gcd` and
`lcm` form a bounded lattice on the associated elements where `gcd` is the infimum, `lcm` is the
supremum, `1` is bottom, and `0` is top. The type class focuses on `gcd` and we derive the
corresponding `lcm` facts from `gcd`.  -/
NormalizedGCDMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Type u_2
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.of_finite : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [Finite α] [MeasurableSingletonClass α] [MeasureTheory.IsFiniteMeasure μ] {f : α → β}, MeasureTheory.Integrable f μ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsOverOverObjOfRespectsIso : ∀ {T : Type u_3} [inst : CategoryTheory.Category.{v_3, u_3} T] {W : CategoryTheory.MorphismProperty T} {X : T}
  [W.RespectsIso], W.overObj.IsClosedUnderIsomorphisms
-- Init.Data.SInt.Lemmas
Int64.toBitVec_mod : ∀ {a b : Int64}, (a % b).toBitVec = a.toBitVec.srem b.toBitVec
-- Mathlib.Topology.Order
instTopologicalSpaceEmpty : TopologicalSpace Empty
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero : ∀ (a : ℝ),
  HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun n => Ring.choose (a + ↑n - 1) n) 0 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toArray_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Raw.filter f t).toArray = Array.filter (fun p => f p.fst p.snd) t.toArray
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pos.revSkip?_string_eq_revSkip?_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos}, pos.revSkip? pat = pos.revSkip? pat.toSlice
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_rco_eq_none_iff : ∀ {m n i : ℕ}, (m...n).toArray[i]? = none ↔ n ≤ i + m
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
/-- `0` is a lower bound of `smoothingSeminormSeq`.  -/
zero_mem_lowerBounds_smoothingSeminormSeq_range : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) (x : R),
  0 ∈ lowerBounds (Set.range fun n => μ (x ^ ↑n) ^ (1 / ↑↑n))
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (𝒰 : X.OpenCover),
  P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The length of reduced words provides a norm on a free group.  -/
FreeGroup.norm : {α : Type u_1} → [DecidableEq α] → FreeGroup α → ℕ
-- Mathlib.Analysis.Complex.Norm
Complex.isCauSeq_im : ∀ (f : CauSeq ℂ fun x => ‖x‖), IsCauSeq abs fun n => (↑f n).im
-- Mathlib.Data.EReal.Operations
EReal.neg_top : -⊤ = ⊥
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.maxValueSealed_def : Int64.maxValueSealed✝ = Int64.maxValue
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.insert.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (a : ℕ) (as : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (a : ℕ) → (as : List ℕ) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
Unitary.conjStarAlgAut_symm_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : SMul S R]
  [inst_3 : IsScalarTower S R R] [inst_4 : SMulCommClass S R R] (u : ↥(unitary R)) (x : R),
  ((Unitary.conjStarAlgAut S R) u).symm x = star ↑u * x * ↑u
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_coe_angle_eq_iff : ∀ {x y : ℂ}, ↑x.arg = ↑y.arg ↔ x.arg = y.arg
-- Mathlib.Data.Complex.Basic
Complex.ofReal_re : ∀ (r : ℝ), (↑r).re = r
-- Mathlib.GroupTheory.GroupAction.Period
MulAction.period_dvd_orderOf : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (m : M) (a : α), MulAction.period m a ∣ orderOf m
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.coeff_map : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (x : AddMonoidAlgebra R M), (AddMonoidAlgebra.map f x).coeff = Finsupp.mapRange ⇑f ⋯ x.coeff
-- Mathlib.Algebra.MvPolynomial.Rename
/-- Given a function between sets of variables `f : σ → τ` that is injective with proof `hf`,
`MvPolynomial.killCompl hf` is the `AlgHom` from `R[τ]` to `R[σ]` that is left inverse to
`rename f : R[σ] → R[τ]` and sends the variables in the complement of the range of `f` to `0`.  -/
MvPolynomial.killCompl : {σ : Type u_1} →
  {τ : Type u_2} →
    {R : Type u_4} →
      [inst : CommSemiring R] → {f : σ → τ} → Function.Injective f → MvPolynomial τ R →ₐ[R] MvPolynomial σ R
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.equivElements_symm_apply_dim : ∀ {X : SSet} (a : CategoryTheory.Functor.Elements X), (SSet.S.equivElements.symm a).dim = a.1.1.len
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_of_isZero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsZero → LieAlgebra.IsKilling.chainLength α β = 0
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.mk.congr_simp : ∀ {V : Type u_1} {G : SimpleGraph V} (toProd toProd_1 : V × V) (e_toProd : toProd = toProd_1)
  (adj : G.Adj toProd.1 toProd.2), { toProd := toProd, adj := adj } = { toProd := toProd_1, adj := ⋯ }
-- Mathlib.Topology.Separation.Regular
/-- In a locally compact regular space, given a compact set `K` inside an open set `U`, we can find
an open set `V` between these sets with compact closure: `K ⊆ V` and the closure of `V` is
inside `U`.  -/
exists_open_between_and_isCompact_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U ∧ IsCompact (closure V)
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulWithCancel.congr_simp : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ φ_1 : ↥A ≃* ↥B),
  φ = φ_1 →
    ∀ {d : HNNExtension.NormalWord.TransversalPair G A B} (u u_1 : ℤˣ) (e_u : u = u_1)
      (w w_1 : HNNExtension.NormalWord d) (e_w : w = w_1) (a : HNNExtension.NormalWord.Cancels u w),
      HNNExtension.NormalWord.unitsSMulWithCancel φ u w a = HNNExtension.NormalWord.unitsSMulWithCancel φ_1 u_1 w_1 ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
map_neg_le_map_neg_iff_map_le_map : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddMonoid β] {F : Type u_6} [inst_2 : FunLike F α β]
  [AddMonoidHomClass F α β] [inst_4 : LE β] [AddRightMono β] [AddLeftMono β] {f g : F} {x : α},
  f (-x) ≤ g (-x) ↔ g x ≤ f x
-- Init.Data.Array.Find
Array.finIdxOf?_eq_some_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size},
  xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ j < i, ¬xs[j] = a
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.biInf_mem : ∀ {α : Type u_2} [inst : CompleteBooleanAlgebra α] {L : BooleanSubalgebra α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  t.Finite → (∀ i ∈ t, f i ∈ L) → ⨅ i ∈ t, f i ∈ L
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.constantCoeff_divXPowOrder : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R},
  PowerSeries.constantCoeff f.divXPowOrder = (PowerSeries.coeff f.order.toNat) f
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
/-- Compose two morphisms in a bicategorical category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.bicategoricalComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} → {f g h i : a ⟶ b} → [CategoryTheory.BicategoricalCoherence g h] → (f ⟶ g) → (h ⟶ i) → (f ⟶ i)
-- Mathlib.Order.Interval.Finset.Basic
not_lt_of_denselyOrdered_of_locallyFinite : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] (a b : α), ¬a < b
-- Mathlib.Order.Disjoint
IsCompl.inf_right_eq_bot_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl y z → (x ⊓ z = ⊥ ↔ x ≤ y)
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamily.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B W : C} {α : Type u_2} (X : α → C)
  (π : (a : α) → X a ⟶ B) [inst_1 : CategoryTheory.EffectiveEpiFamily X π] (e : (a : α) → X a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
  (a : α) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (π a)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpiFamily.desc X π e ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp (e a) h_1
-- Mathlib.Data.UInt
UInt32.toBitVec_natCast : ∀ (n : ℕ), (↑n).toBitVec = ↑n
-- Init.Data.List.Nat.Count
List.IsInfix.le_count : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α},
  l₁ <:+: l₂ → ∀ (a : α), List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
-- Mathlib.Topology.Closure
frontier_subset_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, frontier s ⊆ closure s
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length.eq_def : ∀ {V : Type u} [inst : Quiver V] {a : V} (x : V) (x_1 : Quiver.Path a x),
  x_1.length =
    match x, x_1 with
    | .(a), Quiver.Path.nil => 0
    | x, p.cons a_1 => p.length + 1
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_mul_finrank_top : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E},
  A ≤ B → A.relfinrank B * Module.finrank (↥B) E = Module.finrank (↥A) E
-- Mathlib.Data.Nat.Factorization.Basic
/-- Exactly `n / p` naturals in `(0, n]` are multiples of `p`.  -/
Nat.Ioc_filter_dvd_card_eq_div : ∀ (n p : ℕ), {x ∈ Finset.Ioc 0 n | p ∣ x}.card = n / p
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.iterationFunctorObjObjRightIso I κ f j).hom
      (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f)) =
    (CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- For any `f : Arrow C`, the object `((iteration I κ).obj f).right`
identifies to `f.right`.  -/
CategoryTheory.SmallObject.iterationObjRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              (f : CategoryTheory.Arrow C) → f.right ≅ ((CategoryTheory.SmallObject.iteration I κ).obj f).right
-- Std.Data.String.ToNat
String.isNat_of_toNat?_eq_some : ∀ {n : ℕ} {s : String}, s.toNat? = some n → s.isNat = true
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.allM_eq_not_anyM_not : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p it =
    (fun x => { down := !x.down }) <$> Std.IterM.anyM (fun x => (fun x => { down := !x.down }) <$> p x) it
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_apply_univ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} {x : α × γ} [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η], ((κ.parallelComp η) x) Set.univ = (κ x.1) Set.univ * (η x.2) Set.univ
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.le_iff_specializes : ∀ {R : Type u} [inst : CommSemiring R] (x y : PrimeSpectrum R), x ≤ y ↔ x ⤳ y
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasFDerivAt.comp_hasDerivWithinAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {s : Set 𝕜} {l : F → E} {l' : F →L[𝕜] E} {y : F},
  HasFDerivAt l l' y → HasDerivWithinAt f f' s x → y = f x → HasDerivWithinAt (l ∘ f) (l' f') s x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq CategoryTheory.Limits.WalkingPair
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l → ∀ {h' : k' ∈ m.insertMany l}, (m.insertMany l)[k'] = v
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_one : ∀ {α : Type u_2} {s : Set α}, Equiv.Perm.IsCycleOn 1 s ↔ s.Subsingleton
-- Lean.ReducibilityAttrs
Lean.instBEqReducibilityStatus : BEq Lean.ReducibilityStatus
-- Mathlib.Topology.UniformSpace.Basic
/-- **Alias** of `uniformContinuous_iff_le_comap`. -/
uniformContinuous_iff : ∀ {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β},
  UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_ne_zero : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {F : Type u_8} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {x : E} {y : F},
  x ≠ 0 → y ≠ 0 → ((InnerProductSpace.rankOne 𝕜) x) y ≠ 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- The open cover of the domain of `f : X ⤏ Y`,
consisting of all the domains of the partial maps in the equivalence class.  -/
AlgebraicGeometry.Scheme.RationalMap.openCoverDomain : {X Y : AlgebraicGeometry.Scheme} → (f : X.RationalMap Y) → (↑f.domain).OpenCover
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
Std.IterM.stepAsHetT.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  (it : Std.IterM m β),
  it.stepAsHetT =
    { Property := it.IsPlausibleStep, small := ⋯,
      operation := (fun step => Std.Internal.USquash.deflate step.inflate) <$> it.step }
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CochainComplex.Plus.instIsKInjectiveObjHomologicalComplexIntInjectiveObjectUpMapHomologicalComplexιObjPlus : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex.Plus (CategoryTheory.InjectiveObject C)),
  CochainComplex.IsKInjective
    (((CategoryTheory.InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K.obj)