mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
  {j j' : J} (φ : j ⟶ j'),
  ((CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P).map φ).f =
    CategoryTheory.CategoryStruct.comp (P.p.app j) (P.X.map φ)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_le_op_iff : ∀ {R : Type u_2} [inst : NonAssocSemiring R] {S₁ S₂ : Subsemiring R}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Std.Async.System
/-- time spent in kernel mode.
 -/
Std.Async.System.CPUTimes.systemTime : Std.Async.System.CPUTimes → Std.Time.Millisecond.Offset
-- Std.Time.Duration
/-- Subtracts a `Day.Offset` from a `Duration`
 -/
Std.Time.Duration.subDays : Std.Time.Duration → Std.Time.Day.Offset → Std.Time.Duration
-- Init.Data.Char.Basic
/-- One character is less than or equal to another if its code point is less than or equal to the
other's.
 -/
Char.le : Char → Char → Prop
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.comp_ι_sq_scalar : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Semiring A] [inst_4 : Algebra R A] (g : CliffordAlgebra Q →ₐ[R] A)
  (m : M), g ((CliffordAlgebra.ι Q) m) * g ((CliffordAlgebra.ι Q) m) = (algebraMap R A) (Q m)
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.fibration_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  {f : X ⟶ Y} (self : HomotopicalAlgebra.FibrantBrownFactorization f), HomotopicalAlgebra.Fibration self.r
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- A prelax functor `F` sends 2-isomorphisms `η : f ≅ g` to 2-isomorphisms
`F.map f ≅ F.map g`.  -/
CategoryTheory.PrelaxFunctor.map₂Iso : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.PrelaxFunctor B C) → {a b : B} → {f g : a ⟶ b} → (f ≅ g) → (F.map f ≅ F.map g)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.opEquiv_functor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {x y : (CategoryTheory.WithInitial C)ᵒᵖ} (x_1 : x ⟶ y),
  (CategoryTheory.WithInitial.opEquiv C).functor.map x_1 =
    match x_1 with
    | Opposite.op f =>
      match x, y, f, x_1 with
      | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
        (CategoryTheory.WithTerminal.down f).op
      | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
        CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of (Opposite.op a))
      | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 =>
        CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star
-- Mathlib.Order.Filter.Pointwise
Filter.not_nonneg_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {f g : Filter α}, ¬0 ≤ f - g ↔ Disjoint f g
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_7 : Lean.ModuleData × Lean.CompactedRegion →
  Lean.ModuleData × Lean.CompactedRegion → System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.mk : Option Lean.Lsp.RefInfo.Location → Array Lean.Lsp.RefInfo.Location → Lean.Lsp.RefInfo
-- Init.Data.Array.MapIdx
Array.mk_mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {k i : ℕ} {x : α} {xs : Array α}, (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x
-- Init.Data.List.Sort.Lemmas
/-- This merge sort algorithm is stable,
in the sense that breaking ties in the ordering function using the position in the list
has no effect on the output.

That is, elements which are equal with respect to the ordering function will remain
in the same order in the output list as they were in the input list.

See also:
* `sublist_mergeSort`: if `c <+ l` and `c.Pairwise le`, then `c <+ mergeSort le l`.
* `pair_sublist_mergeSort`: if `[a, b] <+ l` and `le a b`, then `[a, b] <+ mergeSort le l`)
 -/
List.mergeSort_zipIdx : ∀ {α : Type u_1} {le : α → α → Bool} {l : List α},
  List.map (fun x => x.1) (l.zipIdx.mergeSort (List.zipIdxLE le)) = l.mergeSort le
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getLED k fallback = t₂.getLED k fallback
-- Mathlib.Algebra.Module.Submodule.Union
Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  (s : Finset ι) (p : ι → Submodule K M), (∀ (i : ι), p i ≠ ⊤) → ↑s.card < ENat.card K → ⋃ i ∈ s, ↑(p i) ⊂ Set.univ
-- Init.Data.UInt.Lemmas
USize.lt_ofNat_iff : ∀ {n : USize} {m : ℕ}, m < USize.size → (n < USize.ofNat m ↔ n.toNat < m)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.bind_eq_pbind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} (x : Std.Iterators.HetT m α)
  (f : α → Std.Iterators.HetT m β), x.bind f = x.pbind fun a x => f a
-- Batteries.Data.AssocList
Batteries.AssocList.all.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.all p (Batteries.AssocList.cons a b es) = (p a b && Batteries.AssocList.all p es)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingEquiv_symm_apply_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] (G : CategoryTheory.Functor (C × D) E) (X : C) {X_1 Y : D}
  (g : X_1 ⟶ Y),
  ((CategoryTheory.Functor.curryingEquiv.symm G).obj X).map g =
    G.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
-- Mathlib.Geometry.Manifold.Instances.Real
/-- The left chart for the topological space `[x, y]`, defined on `[x,y)` and sending `x` to `0` in
`EuclideanHalfSpace 1`.
 -/
IccLeftChart : (x y : ℝ) → [h : Fact (x < y)] → OpenPartialHomeomorph (↑(Set.Icc x y)) (EuclideanHalfSpace 1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- Preserving biproducts at a bigger universe level implies preserving biproducts at a
smaller universe level.  -/
CategoryTheory.Limits.preservesBiproducts_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesBiproducts F],
  CategoryTheory.Limits.PreservesBiproducts F
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] (s : Set E),
  balancedCore 𝕜 s = ⋃₀ {t | Balanced 𝕜 t ∧ t ⊆ s}
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_le_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (f : β → α) {a : α} {b : β} (hb : b ∈ s),
  f b ≤ a → s.inf' ⋯ f ≤ a
-- Init.Data.SInt.Lemmas
Int32.zero_ne_one : 0 ≠ 1
-- Init.Core
/-- `PEmpty.elim : Empty → C` says that a value of any type can be constructed from
`PEmpty`. This can be thought of as a compiler-checked assertion that a code path is unreachable.
 -/
PEmpty.elim : {C : Sort u_1} → PEmpty.{u_2} → C
-- Mathlib.Data.Finset.Preimage
Finset.sigma_image_fst_preimage_mk : ∀ {α : Type u} {β : α → Type u_1} [inst : DecidableEq α] (s : Finset ((a : α) × β a)),
  ((Finset.image Sigma.fst s).sigma fun a => s.preimage (Sigma.mk a) ⋯) = s
-- Mathlib.Order.InitialSeg
/-- The supremum of the principal segment  -/
PrincipalSeg.top : {α : Type u_4} → {β : Type u_5} → {r : α → α → Prop} → {s : β → β → Prop} → PrincipalSeg r s → β
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], Ordinal.preOmega (OfNat.ofNat n) = ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.ofArrowIso_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  (F : CategoryTheory.Limits.ImageFactorisation f.hom) (sq : f ⟶ g) [inst_1 : CategoryTheory.IsIso sq],
  (F.ofArrowIso sq).F = F.F.ofArrowIso sq
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_hom_toFunctor_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D),
  (CategoryTheory.curryingIso.hom.toFunctor.obj F).obj X = (F.obj X.1).obj X.2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg : ∀ {θ : Real.Angle} {ψ : ℝ}, θ.cos = Real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ
-- Mathlib.Data.Rel
SetRel.image_inter_dom : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α), R.image (s ∩ R.dom) = R.image s
-- Mathlib.Data.List.Range
List.ranges.eq_def : ∀ (x : List ℕ),
  x.ranges =
    match x with
    | [] => []
    | a :: l => List.range a :: List.map (List.map fun x => a + x) l.ranges
-- Mathlib.Data.Stream.Init
Stream'.exists_of_mem_map : ∀ {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Stream' α}, b ∈ Stream'.map f s → ∃ a ∈ s, f a = b
-- Std.Http.Data.Headers
Std.Http.instMembershipNameHeaders : Membership Std.Http.Header.Name Std.Http.Headers
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Every diagram is naturally isomorphic (actually, equal) to a `wideSpan`  -/
CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) C) →
        F ≅
          CategoryTheory.Limits.WidePushoutShape.wideSpan (F.obj none) (fun j => F.obj (some j)) fun j =>
            F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j)
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_le_maximal : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α}, s.Finite → a ∈ s → ∃ b, a ≤ b ∧ Maximal (fun x => x ∈ s) b
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the angle ∠ABC at a point is π, the angle ∠BAC is 0.  -/
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → EuclideanGeometry.angle p₂ p₁ p₃ = 0
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_3.splitter : {α₁ β₁ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β₁] →
      (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) →
        (memo : Option { out // ∃ it, it.IsPlausibleOutput out }) →
          (Unit → motive none) → ((out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)) → motive memo
-- Mathlib.Algebra.Group.Basic
eq_mul_of_div_eq' : ∀ {G : Type u_3} [inst : CommGroup G] {a b c : G}, a / b = c → a = b * c
-- Init.Data.Ord.Basic
Ordering.isNe_gt : Ordering.gt.isNe = true
-- Mathlib.Order.Hom.Lattice
InfHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : SupHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ),
  (InfHom.dual.symm f) a = f a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightUnmopIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  (X_1 : C),
  X.tensorRightUnmopIso.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X.unmop)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq.eq_3 : ∀ (x x_1 : Lean.Grind.Linarith.Poly),
  (x = Lean.Grind.Linarith.Poly.nil → x_1 = Lean.Grind.Linarith.Poly.nil → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var)
        (b_2 : Lean.Grind.Linarith.Poly),
        x = Lean.Grind.Linarith.Poly.add a a_1 a_2 → x_1 = Lean.Grind.Linarith.Poly.add b b_1 b_2 → False) →
      Lean.Grind.Linarith.instBEqPoly.beq x x_1 = false
-- Lean.Setup
Lean.Plugin.mk.sizeOf_spec : ∀ (path : System.FilePath) (initFn? : Option String),
  sizeOf { path := path, initFn? := initFn? } = 1 + sizeOf path + sizeOf initFn?
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink.targetUri : Lean.Lsp.LocationLink → Lean.Lsp.DocumentUri
-- Init.Data.List.Lemmas
List.getLast_concat : ∀ {α : Type u_1} {a : α} {l : List α}, (l ++ [a]).getLast ⋯ = a
-- Mathlib.Tactic.Algebra.AlgebraNF
/-- The core of `algebra_nf with R` - normalize the expression `e` over the base ring `R`
Also used internally in `polynomial_nf`.  -/
Mathlib.Tactic.Algebra.evalExpr : {u : Lean.Level} → Q(Type u) → Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_toMonoidHomEquiv : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M),
  ⇑(AddChar.toMonoidHomEquiv ψ) = ⇑ψ ∘ ⇑Multiplicative.toAdd
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.mul.sizeOf_spec : ∀ (a b : Lean.Grind.CommRing.Expr), sizeOf (a.mul b) = 1 + sizeOf a + sizeOf b
-- Mathlib.Analysis.Normed.Group.InfiniteSum
summable_iff_vanishing_norm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ι → E},
  Summable f ↔ ∀ ε > 0, ∃ s, ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, f i‖ < ε
-- Mathlib.Data.List.Defs
/-- `mapDiagM' f l` calls `f` on all elements in the upper triangular part of `l × l`.
That is, for each `e ∈ l`, it will run `f e e` and then `f e e'`
for each `e'` that appears after `e` in `l`.

Example: suppose `l = [1, 2, 3]`. `mapDiagM' f l` will evaluate, in this order,
`f 1 1`, `f 1 2`, `f 1 3`, `f 2 2`, `f 2 3`, `f 3 3`.
 -/
List.mapDiagM' : {m : Type → Type u_7} → [Monad m] → {α : Type u_8} → (α → α → m Unit) → List α → m Unit
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
/-- `RightPreLieRings` are examples of `LieAdmissibleRings` by the commutativity assumption on
the associator.  -/
RightPreLieRing.instLieAdmissibleRing : {L : Type u_2} → [RightPreLieRing L] → LieAdmissibleRing L
-- Mathlib.Data.Sign.Defs
SignType.nonneg_iff_ne_neg_one : ∀ {a : SignType}, 0 ≤ a ↔ a ≠ -1
-- Init.Data.List.Perm
List.Perm.append_cons : ∀ {α : Type u_1} (a : α) {l₁ l₂ r₁ r₂ : List α}, l₁.Perm l₂ → r₁.Perm r₂ → (l₁ ++ a :: r₁).Perm (l₂ ++ a :: r₂)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsRight : ∀ (a : ℝ), intervalIntegral.FTCFilter a (nhdsWithin a (Set.Ici a)) (nhdsWithin a (Set.Ioi a))
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
ConvexOn.integrable_comp_rnDeriv_trim : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧),
  μ.AbsolutelyContinuous ν →
    MeasureTheory.StronglyMeasurable f →
      ConvexOn ℝ (Set.Ici 0) f →
        ContinuousWithinAt f (Set.Ici 0) 0 →
          MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
            MeasureTheory.Integrable (fun x => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) (ν.trim hm)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A cocircuit is a minimal set that intersects every base.  -/
Matroid.isCocircuit_iff_minimal : ∀ {α : Type u_1} {M : Matroid α} {K : Set α},
  M.IsCocircuit K ↔ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.WeakRankFunction.lt : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] (self : P.WeakRankFunction α)
  {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → self.rank x < self.rank y
-- Mathlib.CategoryTheory.MorphismProperty.Ind
/-- Let `P` be a property of morphisms. `P.ind` is satisfied for `f : X ⟶ Y`
if there exists a family of natural maps `tᵢ : X ⟶ Yᵢ` and `sᵢ : Yᵢ ⟶ Y` indexed by `J`
such that
- `J` is filtered
- `Y ≅ colim Yᵢ` via `{sᵢ}ᵢ`
- `tᵢ` satisfies `P` for all `i`
- `f = tᵢ ≫ sᵢ` for all `i`.

See `CategoryTheory.MorphismProperty.ind_iff_ind_under_mk` for an equivalent characterization
in terms of `Y` as an object of `Under X`.
 -/
CategoryTheory.MorphismProperty.ind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Init.Data.SInt.Basic
instMinInt64 : Min Int64
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_mul_natTrailingDegree_add_natTrailingDegree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_smul_iff : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {𝕜 : Type u_9} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] {f : X → E} (c : 𝕜),
  MeasureTheory.LocallyIntegrable (c • f) μ ↔ c = 0 ∨ MeasureTheory.LocallyIntegrable f μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- the (weak) rank function  -/
SSet.Subcomplex.PairingCore.WeakRankFunction.rank : {X : SSet} →
  {A : X.Subcomplex} → {h : A.PairingCore} → {α : Type v} → [inst : PartialOrder α] → h.WeakRankFunction α → h.ι → α
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instCommSemigroup : {R : Type u_2} →
  [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → CommSemigroup ↑(Set.Ioc 0 1)
-- Mathlib.Data.Num.Lemmas
PosNum.add_one : ∀ (n : PosNum), n + 1 = n.succ
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
multiples_eq_top_of_prime_card : ∀ {G : Type u_2} [inst : AddGroup G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g : G}, g ≠ 0 → AddSubmonoid.multiples g = ⊤
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.isoMk_inv_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom),
  (CategoryTheory.Bicategory.InducedBicategory.isoMk φ).inv.hom = φ.inv
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Suppose an indexed family of points is given, along with a subset
of the index type.  A point can be expressed as an
`affineCombination` using a `Finset` lying within that subset and
with sum of weights 1 if and only if it can be expressed an
`affineCombination` with sum of weights 1 for the corresponding
indexed family whose index type is the subtype corresponding to that
subset.  -/
Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {p0 : P} {s : Set ι} {p : ι → P},
  (∃ fs, ↑fs ⊆ s ∧ ∃ w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs p) w) ↔
    ∃ fs w, ∑ i ∈ fs, w i = 1 ∧ p0 = (Finset.affineCombination k fs fun i => p ↑i) w
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.leftOp : Cᵒᵖ ⥤ D` creates
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.createsColimitLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (K : CategoryTheory.Functor J Cᵒᵖ) →
              (F : CategoryTheory.Functor C Dᵒᵖ) →
                [CategoryTheory.CreatesLimit K.leftOp F] → CategoryTheory.CreatesColimit K F.leftOp
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.instIsCountablyGeneratedUniformity : ∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).IsCountablyGenerated
-- Mathlib.Algebra.Lie.Submodule
LieSubalgebra.mem_toLieSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {K : LieSubalgebra R L}
  (x : L), x ∈ K.toLieSubmodule ↔ x ∈ K
-- Init.Notation
/-- `#discr_tree_key  t` prints the discrimination tree keys for a term `t` (or, if it is a single identifier, the type of that constant).
It uses the default configuration for generating keys.

For example,
```
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
```

`#discr_tree_simp_key` is similar to `#discr_tree_key`, but treats the underlying type
as one of a simp lemma, i.e. transforms it into an equality and produces the key of the
left-hand side.
 -/
Lean.Parser.discrTreeKeyCmd : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, returning `fallback` if
the tree map is empty.
 -/
Std.DTreeMap.Raw.minEntryD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Homology.Homotopy
/-- An auxiliary construction for `mkCoinductive`.

Here we build by induction a family of diagrams,
but don't require at the type level that these successive diagrams actually agree.
They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy)
in `mkCoinductive`.

At this stage, we don't check the homotopy condition in degree 0,
because it "falls off the end", and is easier to treat using `xNext` and `xPrev`,
which we do in `mkInductiveAux₂`.
 -/
Homotopy.mkCoinductiveAux₁ : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : CochainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 1 ⟶ Q.X 0) →
            (one : P.X 2 ⟶ Q.X 1) →
              e.f 1 =
                  CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one →
                ((n : ℕ) →
                    (p :
                        (f : P.X (n + 1) ⟶ Q.X n) ×'
                          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                            e.f (n + 1) =
                              CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                                CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
                      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
                        e.f (n + 2) =
                          CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
                            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') →
                  (n : ℕ) →
                    (f : P.X (n + 1) ⟶ Q.X n) ×'
                      (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                        e.f (n + 1) =
                          CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                            CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {p})),
  ↑((PrimeSpectrum.preimageHomeomorphFiber R S p) q).asIdeal =
    ⇑(Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (Algebra.ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯) ⁻¹'
      {0}