mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- A rank function for `h : A.PairingCore` is a function from the index type `h.ι`
to a partially ordered type which maps the ancestrality relations to strict inequalities.  -/
SSet.Subcomplex.PairingCore.RankFunction : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → (α : Type v) → [PartialOrder α] → Type (max u_1 v)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.of_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, (s * t).Nonempty → t.Nonempty
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.Context.mk.inj : ∀ {toContext : Lean.Elab.Tactic.Context} {ctx : Lean.Meta.Grind.Context} {sctx : Lean.Meta.Sym.Context}
  {methods : Lean.Meta.Grind.Methods} {params : Lean.Meta.Grind.Params} {sym : Bool}
  {toContext_1 : Lean.Elab.Tactic.Context} {ctx_1 : Lean.Meta.Grind.Context} {sctx_1 : Lean.Meta.Sym.Context}
  {methods_1 : Lean.Meta.Grind.Methods} {params_1 : Lean.Meta.Grind.Params} {sym_1 : Bool},
  { toContext := toContext, ctx := ctx, sctx := sctx, methods := methods, params := params, sym := sym } =
      { toContext := toContext_1, ctx := ctx_1, sctx := sctx_1, methods := methods_1, params := params_1,
        sym := sym_1 } →
    toContext = toContext_1 ∧ ctx = ctx_1 ∧ sctx = sctx_1 ∧ methods = methods_1 ∧ params = params_1 ∧ sym = sym_1
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_vaddConst_symm : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (p : P),
  ⇑(Equiv.vaddConst p).symm = fun p' => p' -ᵥ p
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_1 lls k v l r lrs lrk lrv lrl lrr
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
    | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) =
    h_2 size k v l r
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_of_contains_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool}
  {k : α}, (Std.HashSet.filter f m).contains k = true → m.contains k = true
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.mem_transvections_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {e : V ≃ₗ[R] V},
  e ∈ LinearEquiv.transvections R V ↔ ∃ f v, ∃ (hfv : f v = 0), e = LinearEquiv.transvection hfv
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_symm : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β), h.symm.symm = h
-- Mathlib.Tactic.Linarith.Parsing
/-- `elimMonom s map` eliminates the monomial level of the `Sum` `s`.

`map` is a lookup map from monomials to variable numbers.
The output `TreeMap ℕ ℤ` has the same structure as `s : Sum`,
but each monomial key is replaced with its index according to `map`.
If any new monomials are encountered, they are assigned variable numbers and `map` is updated.
 -/
Mathlib.Tactic.Linarith.elimMonom : Mathlib.Tactic.Linarith.Sum →
  Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare →
    Std.TreeMap Mathlib.Tactic.Linarith.Monom ℕ compare × Std.TreeMap ℕ ℤ compare
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral norm is nonarchimedean.  -/
isNonarchimedean_spectralNorm : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] [IsUltrametricDist K]
  [h_alg : Algebra.IsAlgebraic K L], IsNonarchimedean (spectralNorm K L)
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
/-- The "unipotent radical" attached to a subspace `L ⊆ ι → F`: the subgroup of
`SL ι F` consisting of matrices `A` such that `A - 1` sends every vector into `L`.
When `L` is one-dimensional this is an abelian subgroup of the stabilizer of `L` in `SL`.  -/
Matrix.SpecialLinearGroup.lineStab : {F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] → [inst_2 : Fintype ι] → Submodule F (ι → F) → Subgroup (Matrix.SpecialLinearGroup ι F)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instReprHeader.repr : Std.Time.TimeZone.TZif.Header → ℕ → Std.Format
-- Mathlib.Topology.MetricSpace.Closeds
Metric.hausdorffEDist_le_of_mem_hausdorffEntourage : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {s t : Set α} {δ : ENNReal},
  (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ} → Metric.hausdorffEDist s t ≤ δ
-- Init.Grind.Offset
Lean.Grind.Nat.of_lo_eq_false_1 : ∀ (u v : ℕ), (u + 1 ≤ v) = False → v ≤ u
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.mk : WantedRefKind✝ → Lean.TSyntax `term → Bool → Array WantedDep✝ → Option (Lean.TSyntax `term) → WantedRefInfo✝
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.of_prod_right : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  IsCoprime x (∏ i ∈ t, s i) → ∀ i ∈ t, IsCoprime x (s i)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_smul_eq_smul_or_disjoint`. -/
MulAction.IsBlock.smul_eq_smul_or_disjoint : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X},
  MulAction.IsBlock G B → ∀ (g₁ g₂ : G), g₁ • B = g₂ • B ∨ Disjoint (g₁ • B) (g₂ • B)
-- Mathlib.CategoryTheory.Galois.Topology
/-- We put the discrete topology on `Aut (F.obj X)`.  -/
CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFintypeCatObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → (X : C) → TopologicalSpace (CategoryTheory.Aut (F.obj X))
-- Mathlib.Algebra.Order.WithTop.Untop0
/-- Elements of ordered additive commutative groups are nonnegative iff their untop₀ is nonnegative.
 -/
WithTop.untop₀_nonneg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] {a : WithTop α}, 0 ≤ a.untop₀ ↔ 0 ≤ a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α), s⁻¹.card = s.card
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMkMor₁MonoidalM : Mathlib.Tactic.BicategoryLike.MkMor₁ Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.subsingleton : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [IsScalarTower R A A]
  [SMulCommClass R A A] [Subsingleton (NonUnitalSubalgebra R A)], Subsingleton (A →ₙₐ[R] B)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom_val : ∀ {X : AlgebraicGeometry.PresheafedSpace CommRingCat} (Y : AlgebraicGeometry.LocallyRingedSpace)
  (f : X ⟶ Y.toPresheafedSpace) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom
      (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom Y f) =
    CategoryTheory.InducedCategory.homMk f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.denote_blast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : BitVec w)
  (assign : α → Bool) (input : aig.BinaryRefVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.blast aig input).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.blast aig input).vec.get idx hidx }⟧ =
          (lhs * rhs).getLsbD idx
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.isTheta_congr_left : ∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (f' =Θ[l] k ↔ g' =Θ[l] k)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_map : ∀ {f : ZFSet.{u_1} → ZFSet.{u_1}} [inst : ZFSet.Definable₁ f] {x y : ZFSet.{u_1}},
  y ∈ ZFSet.map f x ↔ ∃ z ∈ x, z.pair (f z) = y
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.mem_cofinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, s ∈ μ.cofinite ↔ μ sᶜ < ⊤
-- Mathlib.Algebra.Ring.Pi
Pi.semiring : {I : Type u} → {f : I → Type v} → [(i : I) → Semiring (f i)] → Semiring ((i : I) → f i)
-- Init.Data.SInt.Bitwise
ISize.zero_or : ∀ {a : ISize}, 0 ||| a = a
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt.eq_1 : ∀ (x : ℝ), √x = ↑(NNReal.sqrt x.toNNReal)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The arbitrary choice of the coproduct is isomorphic to our constructed coproduct `cofan 𝒜 f`.
 -/
CategoryTheory.Limits.FormalCoproduct.coproductIsoCofanPt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒜 : Type w) →
      (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) → ∐ f ≅ (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).pt
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- **Alias** of the forward direction of `linearIndepOn_id_range_iff`. -/
LinearIndependent.of_linearIndepOn_id_range : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_6}
  {f : ι → M}, Function.Injective f → LinearIndepOn R id (Set.range f) → LinearIndependent R f
-- Mathlib.Order.Atoms
IsSimpleOrder.equivBool_apply : ∀ {α : Type u_4} [inst : DecidableEq α] [inst_1 : LE α] [inst_2 : BoundedOrder α] [inst_3 : IsSimpleOrder α] (x : α),
  IsSimpleOrder.equivBool x = decide (x = ⊤)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.get_skipPrefixWhile_char_ne : ∀ {c : Char} {s : String.Slice} {h : s.skipPrefixWhile c ≠ s.endPos}, (s.skipPrefixWhile c).get h ≠ c
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_eq_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, (absConvexHull 𝕜) s = ∅ ↔ s = ∅
-- Mathlib.RingTheory.Finiteness.Basic
/-- The submodule generated by a single element is `R`-finite.  -/
Module.Finite.span_singleton : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
  Module.Finite R ↥(R ∙ x)
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedMonoid.of.eq_1 : ∀ {α : Type u_1} (rels : FreeMonoid α → FreeMonoid α → Prop) (x : α),
  PresentedMonoid.of rels x = (PresentedMonoid.mk rels) (FreeMonoid.of x)
-- Mathlib.Data.Finsupp.Multiset
Sym.coe_equivNatSumOfFintype_symm_apply : ∀ (α : Type u_1) [inst : DecidableEq α] (n : ℕ) [inst_1 : Fintype α] (P : { P // ∑ i, P i = n }),
  ↑((Sym.equivNatSumOfFintype α n).symm P) = ∑ a, ↑P a • {a}
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.evalDataValueStx : Lean.Term → Lean.Elab.TermElabM (Lean.DataValue × Lean.Expr)
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
PMF.binomial.eq_1 : ∀ (p : NNReal) (h : p ≤ 1) (n : ℕ),
  PMF.binomial p h n = PMF.ofFintype (fun i => ↑(p ^ ↑i * (1 - p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i))) ⋯
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_inv_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z],
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv
      (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.snd) =
    CategoryTheory.Limits.pullback.snd Y.hom Z.hom
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_apply₁₂ : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : m), Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inr j) = B i j
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose.eq_2 : ∀ (n : ℕ), Nat.choose 0 n.succ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_inv_inl_op : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv CategoryTheory.Limits.biprod.inl.op =
    CategoryTheory.Limits.biprod.fst
-- Lean.Meta.Tactic.SplitIf
/-- Default `discharge?` function for `simpIf` methods.
It only uses hypotheses from the local context that have `index < numIndices`.
It is effective after a case-split.

Remark: when `simp` goes inside binders it adds new local declarations to the
local context. We don't want to use these local declarations since the cached result
would depend on them (see issue #3229). `numIndices` is the size of the local
context `decls` field before we start the simplifying the expression.

Remark: this function is now private, and we should use `mkDischarge?`.
 -/
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.SplitIf.discharge? : ℕ → Bool → Lean.Meta.Simp.Discharge
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If the prime spectrum of a commutative semiring R has discrete Zariski topology, then R is
canonically isomorphic to the product of its localizations at the (finitely many) prime ideals.  -/
PrimeSpectrum.toPiLocalizationEquiv : (R : Type u) → [inst : CommSemiring R] → [DiscreteTopology (PrimeSpectrum R)] → R ≃ₐ[R] PrimeSpectrum.PiLocalization R
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.ext : ∀ {G : Type u_1} {X : Type u_2} {inst : Group G} {inst_1 : MulAction G X} {x y : DiscreteTiling.Prototile G X},
  ↑x = ↑y → x.symmetries ≍ y.symmetries → x = y
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.homObjFunctor.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F G : CategoryTheory.Functor C D),
  F.homObjFunctor G =
    { obj := fun A => F.HomObj G (Opposite.unop A),
      map := fun {A A'} f =>
        TypeCat.ofHom fun x =>
          { app := fun X a => x.app X ((CategoryTheory.ConcreteCategory.hom (f.unop.app X)) a), naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Init.Data.List.ToArray
List.zipWith_toArray : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : List α) (bs : List β) (f : α → β → γ),
  Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.coe_inj : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M] {m m' : M}, ↑m = ↑m' ↔ m = m'
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)],
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).get! k = default
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech conerve construction, as a functor from `Arrow C`.  -/
CategoryTheory.CosimplicialObject.augmentedCechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.CosimplicialObject.Augmented C)
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance
`HasForget₂ C`.  -/
CategoryTheory.forget₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            (D : Type u_3) →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
                      [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                        [CategoryTheory.HasForget₂ C D] → CategoryTheory.Functor C D
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.orbit.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α),
  x.orbit = Quotient.liftOn' x (AddAction.orbit G) ⋯
-- Batteries.Data.String.Lemmas
String.valid_next : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.Valid s p → p < s.rawEndPos → String.Pos.Raw.Valid s (String.Pos.Raw.next s p)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- A terminal object in the opposite category is initial in the original category.  -/
CategoryTheory.Limits.initialUnopOfTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : Cᵒᵖ} → CategoryTheory.Limits.IsTerminal X → CategoryTheory.Limits.IsInitial (Opposite.unop X)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The limit cone for a functor `F : J ⥤ C` to a preorder when `pt : C`
is the greatest lower bound of `Set.range F.obj`  -/
Preorder.limitConeOfIsGLB : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) → {pt : C} → IsGLB (Set.range F.obj) pt → CategoryTheory.Limits.LimitCone F
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.toHom_sum : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ↪g G') (g : H ↪g H'), (f.sum g).toHom = f.toHom.sum g.toHom
-- Lean.Meta.Diagnostics
Lean.Meta.mkDiagSynthPendingFailure : Lean.PHashMap Lean.Expr Lean.MessageData → Lean.MetaM Lean.Meta.DiagSummary
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.toComonObj_X : ∀ {R : Type u} [inst : CommRing R] (X : CoalgCat R), X.toComonObj.X = ModuleCat.of R ↑X.toModuleCat
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mk : {G : Type w} →
  [inst : TopologicalSpace G] →
    (toFun : TopologicalSpace.Compacts G → NNReal) →
      (∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂) →
        (∀ (K₁ K₂ : TopologicalSpace.Compacts G),
            Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂) →
          (∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂) → MeasureTheory.Content G
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instModuleOfIsScalarTower : (R : Type u) →
  (X : Type v) →
    [inst : CommRing R] →
      {S : Type u_1} →
        [inst_1 : Semiring S] → [inst_2 : Module S R] → [IsScalarTower S R R] → Module S (FreeLieAlgebra R X)
-- Mathlib.Order.WithBot
WithTop.instOrderTop.eq_1 : ∀ {α : Type u_1} [inst : LE α], WithTop.instOrderTop = { toTop := WithTop.top, le_top := ⋯ }
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_sub : ∀ {a b : ℕ} (ha : a < 2 ^ 8) (hab : b ≤ a), UInt8.ofNatLT (a - b) ⋯ = UInt8.ofNatLT a ha - UInt8.ofNatLT b ⋯
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- A submonoid `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `g^n ∈ H` we have
`n = 0` or `g ∈ H`. We use the name `PowSaturated` to distinguish from `Submonoid.MulSaturated`.  -/
Submonoid.PowSaturated : {G : Type u_1} → [inst : Monoid G] → Submonoid G → Prop
-- Init.Data.Int.Order
Int.lt_add_succ : ∀ (a : ℤ) (n : ℕ), a < a + (↑n + 1)
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State.mk : Bool → Aesop.Script.StaticStructureM.State
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which maps `S : SnakeInput C` to the diagram
`S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃`.  -/
CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ComposableArrows C 5)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.module : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → Module R ↥p
-- Mathlib.Topology.Constructions
isOpenMap_toDual : ∀ {X : Type u} [inst : TopologicalSpace X], IsOpenMap ⇑OrderDual.toDual
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimitsOfShape.reflectsLimit : ∀ {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} {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.ReflectsLimitsOfShape J F] {K : CategoryTheory.Functor J C},
  CategoryTheory.Limits.ReflectsLimit K F
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.map_fst_toList_eq_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp},
  List.map Sigma.fst t.toList = t.keys
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- If a function has a power series on a ball, then so do its iterated derivatives.  -/
HasFPowerSeriesWithinOnBall.iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    AnalyticOn 𝕜 f s →
      ∀ (k : ℕ),
        UniqueDiffOn 𝕜 s →
          x ∈ s → HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.categoryOfGradedObjects_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (β : Type w) {X Y Z : (i : β) → (fun x => C) i}
  (f : (i : β) → X i ⟶ Y i) (g : (i : β) → Y i ⟶ Z i) (i : β),
  CategoryTheory.CategoryStruct.comp f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)
-- Mathlib.Order.WithBot
WithBot.instOrderTop : {α : Type u_1} → [inst : LE α] → [OrderTop α] → OrderTop (WithBot α)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.l_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] {l : α → β} {u : β → α},
  GaloisConnection l u → ∀ {s : Set γ} {f : γ → α}, BddAbove (f '' s) → s.Nonempty → l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)