mathlib-initiative/mathlib-types huggingface dataset:
-- 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 α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).get! k = default
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_sSup_of_directedOn : ∀ {K : Type u} [inst : DivisionRing K] {S : Set (Subfield K)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : K}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimit_smul_mk_eq : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R)) (r : R)
  (x : (j : J) × ↑(F.obj j)),
  r • ModuleCat.FilteredColimits.M.mk F x = ModuleCat.FilteredColimits.M.mk F ⟨x.fst, r • x.snd⟩
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The functor `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, on objects.  -/
AlgebraicTopology.DoldKan.Γ₀.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] → ChainComplex C ℕ → CategoryTheory.SimplicialObject C
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of `dvd_sub`. -/
Dvd.dvd.sub : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → a ∣ c → a ∣ b - c
-- Mathlib.Topology.Separation.Basic
/-- Given a closed set `S` in a compact T₀ space, there is some `x ∈ S` such that `{x}` is
closed.  -/
IsClosed.exists_closed_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T0Space X] [CompactSpace X] {S : Set X},
  IsClosed S → S.Nonempty → ∃ x ∈ S, IsClosed {x}
-- Std.Data.Internal.List.Associative
Std.Internal.List.beq_of_getEntry?_eq_some : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a},
  Std.Internal.List.getEntry? a l = some p → (p.fst == a) = true
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.IsCommComonObj.comul_comm : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) {inst_3 : CategoryTheory.ComonObj X}
  [self : CategoryTheory.IsCommComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul (β_ X X).hom = CategoryTheory.ComonObj.comul
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.inv_congr : ∀ {R : Type u_2} [inst : Semifield R] {a a' b : R}, a = a' → a'⁻¹ = b → a⁻¹ = b
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousSMulCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] {G : Type u_4} [inst_2 : TopologicalSpace G]
  [inst_3 : (i : ι) → SMul G (R i)] [inst_4 : ∀ (i : ι), SMulMemClass (S i) G (R i)]
  [∀ (i : ι), ContinuousSMul G (R i)],
  ContinuousSMul G (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
/-- The composition of a section of `f₁` and `f₂`. It is proven below that it
is the identity, see `g_eq_id`.  -/
_private.Mathlib.AlgebraicTopology.SimplicialSet.Degenerate.0.SSet.unique_nonDegenerate.g : {n m₁ m₂ : ℕ} →
  {f₁ : { len := n } ⟶ { len := m₁ }} →
    CategoryTheory.SplitEpi f₁ → ({ len := n } ⟶ { len := m₂ }) → ({ len := m₁ } ⟶ { len := m₂ })
-- Init.Data.Option.Basic
Option.map_id : ∀ {α : Type u_1}, Option.map id = id
-- Init.Data.Option.Basic
Option.getM_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Alternative m], none.getM = failure
-- Mathlib.Data.Finset.Max
Finset.max'_mem : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty), s.max' H ∈ s
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.cancel_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) [CategoryTheory.Epi f] {g h : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h ↔ g = h
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The Riemann zeta function is positive in `ComplexOrder` for real arguments greater than 1.
This means it is a positive real number:
both `(riemannZeta x).re > 0` and `(riemannZeta x).im = 0`.  -/
riemannZeta_pos_of_one_lt : ∀ {x : ℝ}, 1 < x → 0 < riemannZeta ↑x
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.homologyι_opcyclesToCycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι)
  [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j] {Z : C} (h : K.cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.homologyι i) (CategoryTheory.CategoryStruct.comp (K.opcyclesToCycles i j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.exists_dist_le_coveringRadius : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) (x : X), ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMulDistribMulAction : {M : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace A] →
      [inst_1 : Monoid M] →
        [inst_2 : Monoid A] →
          [inst_3 : MulDistribMulAction M A] →
            [inst_4 : ContinuousMul A] → [ContinuousConstSMul M A] → MulDistribMulAction M (SeparationQuotient A)
-- Mathlib.Logic.Relation
Relation.TransGen.instIsTrans : ∀ {α : Type u_1} {r : α → α → Prop}, IsTrans α (Relation.TransGen r)
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest_corec : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} {β : Type u} (g : β → ↑P (α ::: β)) (x : β),
  MvPFunctor.M.dest P (MvPFunctor.M.corec P g x) = MvFunctor.map (TypeVec.id ::: MvPFunctor.M.corec P g) (g x)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_2 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (val : BitVec w),
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.const val) = val
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.comap_quotientMk_bijective_of_le_nilradical : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R},
  I ≤ nilradical R → Function.Bijective (PrimeSpectrum.comap (Ideal.Quotient.mk I))
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toListRev_eq_toListRev_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.toListRev = s.iter.toListRev
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- If `f` is absolutely continuous on `uIcc a b`, then `f` has bounded variation on `uIcc a b`.  -/
AbsolutelyContinuousOnInterval.boundedVariationOn : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → BoundedVariationOn f (Set.uIcc a b)
-- Aesop.RuleTac.Basic
/-- The goal on which the rule is run.  -/
Aesop.RuleTacInput.goal : Aesop.RuleTacInput → Lean.MVarId
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- This lemma is included mostly for comparison with the informal literature. Usually
`RootPairing.Base.IsPos.induction_on_add` will be more useful.  -/
RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι},
  b.IsPos i →
    ∃ n f,
      Set.range f ⊆ ↑b.support ∧
        P.root i = ∑ m, P.root (f m) ∧ ∀ (m : Fin n), ∑ m' ≤ m, P.root (f m') ∈ Set.range ⇑P.root
-- Mathlib.Algebra.Ring.CompTypeclasses
/-- This cannot be an instance as there is no way to infer `σ₁₂` and `σ₂₃`.  -/
RingHomSurjective.comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂]
  [RingHomSurjective σ₂₃], RingHomSurjective σ₁₃
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.target_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  I.target = Set.range ↑I
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_id_eq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat),
  CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.Functor.id F.CoGrothendieck
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.lcoeff_comp_mapAlgHom_eq : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (n : ℕ),
  ↑R (Polynomial.lcoeff B n) ∘ₗ (Polynomial.mapAlgHom f).toLinearMap = f.toLinearMap ∘ₗ ↑R (Polynomial.lcoeff A n)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.fromFunctionField_restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) [inst : IrreducibleSpace ↥X] {U : X.Opens} (hU : Dense ↑U)
  (hU' : U ≤ f.domain), (f.restrict U hU hU').fromFunctionField = f.fromFunctionField
-- Lean.Meta.Tactic.Simp.Attr
/-- Marks `declName` to be unfolded in the given `SimpExtension`.
 -/
Lean.Meta.addDeclToUnfold : Lean.Meta.SimpExtension → Lean.Name → Bool → Bool → ℕ → Lean.AttributeKind → Lean.MetaM Bool
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.isGadget : Lean.Name → Bool
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DTreeMap.filterMap f t).get? k = (t.get? k).bind (f k)
-- Mathlib.Order.Cover
not_covBy_of_lt_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < b → b < c → ¬a ⋖ c
-- Mathlib.Analysis.ODE.Gronwall
/-- Let `f : [a, b] → E` be a differentiable function such that `f a = 0`
and `‖f'(x)‖ ≤ K ‖f(x)‖` for some constant `K`. Then `f = 0` on `[a, b]`.  -/
eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → E} {K a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      f a = 0 → (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ K * ‖f x‖) → ∀ x ∈ Set.Icc a b, f x = 0
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.compactSpace : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [Finite 𝒰.I₀] [H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)],
  CompactSpace ↥X
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.isSetSemiring_measurableCylinders : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)},
  MeasureTheory.IsSetSemiring (MeasureTheory.measurableCylinders α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_union_of_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_right_strictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a : α}, StrictMono fun x => a * x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
edist_le_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {c : NNReal}, edist x y ≤ ↑c ↔ nndist x y ≤ c
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.instDecidableMemOfDecidableLE : {α : Type u} → {r : Std.Rci α} → {a : α} → [inst : LE α] → [DecidableLE α] → Decidable (a ∈ r)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  (m₁.union! m₂).getKey k ⋯ = m₂.getKey k mem
-- Std.Data.HashSet.Basic
Std.HashSet.mk : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α Unit → Std.HashSet α
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)) (signs : Finset (Fin (m + 1))),
  (s.reindex e).excenter signs = s.excenter (Finset.map e.symm.toEmbedding signs)
-- Batteries.Data.String.Matcher
/-- Returns true iff `pattern` occurs as a substring of `s`.
 -/
Substring.containsSubstr : Substring.Raw → Substring.Raw → Bool
-- Mathlib.Analysis.Complex.Hadamard
/-- The vertical strip in the complex plane containing all `z ∈ ℂ` such that `z.re ∈ Ioo a b`.  -/
Complex.HadamardThreeLines.verticalStrip : ℝ → ℝ → Set ℂ
-- Init.Sym.Lemmas
Lean.Sym.Rat.lt_eq_true : ∀ (a b : ℚ), decide (a < b) = true → (a < b) = True
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.endPos_ofSliceFrom : ∀ {s : String.Slice} {p : s.Pos} {st : String.Slice.Pattern.SearchStep (s.sliceFrom p)},
  st.ofSliceFrom.endPos = String.Slice.Pos.ofSliceFrom st.endPos
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.delabAdjoinNotation : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRatCheck_fold_success : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRatAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
      (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
      (ratHints : Array (ℕ × Array ℕ)),
      pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
        f.ratHintsExhaustive pivot ratHints = true →
          (Array.foldl (fun x ratHint => if x.2 = true then x.1.performRatCheck pivot.negate ratHint else (x.1, false))
                  (((f.insertRupUnits c.negate).1.performRupCheck rupHints).1, true) ratHints).2 =
              true →
            Std.Tactic.BVDecide.LRAT.Internal.Equisat (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)
-- Mathlib.Analysis.Complex.OperatorNorm
/-- The determinant of `conjLIE`, as a linear equiv.  -/
Complex.linearEquiv_det_conjLIE : LinearEquiv.det Complex.conjLIE.toLinearEquiv = -1
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.mk.inj : ∀ {M : Type u_8} {N : Type u_9} {φ : M → N} {X : Type u_10} {inst : VAdd M X} {Y : Type u_11} {inst_1 : VAdd N Y}
  {toFun : X → Y} {map_vadd' : ∀ (m : M) (x : X), toFun (m +ᵥ x) = φ m +ᵥ toFun x} {toFun_1 : X → Y}
  {map_vadd'_1 : ∀ (m : M) (x : X), toFun_1 (m +ᵥ x) = φ m +ᵥ toFun_1 x},
  { toFun := toFun, map_vadd' := map_vadd' } = { toFun := toFun_1, map_vadd' := map_vadd'_1 } → toFun = toFun_1
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabDoubleQuotedName : Lean.Elab.Term.TermElab
-- Lean.Syntax
/-- Return stack of syntax nodes satisfying `visit`, starting with such a node that also fulfills `accept` (default "is leaf"), and ending with the root.  -/
Lean.Syntax.findStack? : Lean.Syntax → (Lean.Syntax → Bool) → (optParam (Lean.Syntax → Bool) fun stx => !stx.hasArgs) → Option Lean.Syntax.Stack
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.invariantsResMap_map_comp : ∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type u_1} {H : Type u_2} [inst_2 : Group G]
  [inst_3 : Group H] {X X' : TopRep k G} {Y : TopRep k H} (φ : H →* G) (f : X ⟶ X') (g : TopRep.res φ X' ⟶ Y),
  TopRep.invariantsResMap φ (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor φ).map f) g) =
    CategoryTheory.CategoryStruct.comp ((TopRep.invariantsFunctor k G).map f) (TopRep.invariantsResMap φ g)
-- Mathlib.CategoryTheory.PUnit
/-- The functor from `Discrete PUnit` sending everything to the given object.  -/
CategoryTheory.Functor.fromPUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → C → CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1}) C
-- Mathlib.CategoryTheory.Simple
CategoryTheory.kernel_zero_of_nonzero_from_simple : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [CategoryTheory.Simple X] {f : X ⟶ Y} [inst_3 : CategoryTheory.Limits.HasKernel f],
  f ≠ 0 → CategoryTheory.Limits.kernel.ι f = 0
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimFlipObjMap_id : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F],
  CategoryTheory.Functor.weightedLimFlipObjMap (CategoryTheory.CategoryStruct.id W) F =
    CategoryTheory.CategoryStruct.id (W.weightedLimObjObj F)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.dist_le : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α},
  Tactic.ComputeAsymptotics.Seq.FriendlyOperation op → ∀ {s t : Stream'.Seq α}, dist (op s) (op t) ≤ dist s t
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.toContinuousOrderHom_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] {f : EsakiaHom α β}, ⇑f.toContinuousOrderHom = ⇑f
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.StringInvariant.eq_1 : ∀ (s : String) (β Pred : Type u), Std.Internal.Do.StringInvariant s β Pred = (s.Pos → β → Pred)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- We can infer that a functor `G : Grothendieck F ⥤ H`, with `F : C ⥤ Cat`, has a colimit from
the fact that each of its fibers has a colimit and that these fiberwise colimits, as a functor
`C ⥤ H` have a colimit.  -/
CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)], CategoryTheory.Limits.HasColimit G
-- Mathlib.Control.Bifunctor
Bifunctor.fst_comp_fst : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁}
  (f : α₀ → α₁) (f' : α₁ → α₂), Bifunctor.fst f' ∘ Bifunctor.fst f = Bifunctor.fst (f' ∘ f)
-- Mathlib.Algebra.Lie.Basic
Module.Dual.instLieModule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule R L (M →ₗ[R] R)
-- Mathlib.Algebra.Quaternion
Quaternion.imK_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), (↑n).imK = 0
-- Mathlib.Topology.Compactness.Compact
isCompact_iff_isCompact_univ : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s ↔ IsCompact Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isIso_inl_iff_id_eq_fst_comp_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsIso CategoryTheory.Limits.biprod.inl ↔
    CategoryTheory.CategoryStruct.id (X ⊞ Y) =
      CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.ofFactorizationData_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.trivialCofibrations C).MapFactorizationData (HomotopicalAlgebra.fibrations C)
      (CategoryTheory.Limits.diag A)),
  (HomotopicalAlgebra.PathObject.ofFactorizationData h).P = h.Z
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_inj : ∀ {z w : ℂ} (hz : ‖z‖ ≤ 1) (hw : ‖w‖ ≤ 1), Complex.UnitClosedDisc.mk z hz = Complex.UnitClosedDisc.mk w hw ↔ z = w
-- Init.Data.Int.Order
Int.lt_of_sub_lt_sub_right : ∀ {a b c : ℤ}, a - c < b - c → a < b
-- Mathlib.RingTheory.LocalProperties.IntegrallyClosed
IsIntegrallyClosed.of_isLocalization_maximal : ∀ {R : Type u_1} [inst : CommRing R] (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3)
  [inst_1 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)]
  [inst_2 : (P : Ideal R) → [inst_2 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_3 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P] [IsDomain R],
  (∀ (P : Ideal R) [inst : P.IsMaximal], IsIntegrallyClosed (Rₚ P)) → IsIntegrallyClosed R
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- Given a function `f : M → N` between magmas, return the corresponding map `R[M] → R[N]` obtained
by summing the coefficients along each fiber of `f`.  -/
MonoidAlgebra.mapDomain : {R : Type u_3} → {M : Type u_6} → {N : Type u_7} → [inst : Semiring R] → (M → N) → MonoidAlgebra R M → MonoidAlgebra R N
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- If a set of points is cospherical, then its image under the inclusion of any affine subspace
containing it is cospherical.  -/
EuclideanGeometry.Cospherical.inclusion : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {S₁ S₂ : AffineSubspace ℝ P} [inst_4 : Nonempty ↥S₁] {ps : Set ↥S₁},
  EuclideanGeometry.Cospherical ps →
    ∀ (hS : S₁ ≤ S₂), EuclideanGeometry.Cospherical (⇑(AffineSubspace.inclusion hS) '' ps)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
List.tail.eq_1 : ∀ {α : Type u}, [].tail = []
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.instQuasiIsoAtιTruncLEF : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] (i : ι), QuasiIsoAt (K.ιTruncLE e) (e.f i)
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.reflexivity₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂),
  CategoryTheory.CategoryStruct.comp self.r p₂ = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.NhdsSet
disjoint_principal_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Disjoint (Filter.principal s) (nhdsSet t) ↔ Disjoint (closure s) t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_pow : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (f : F) (s : Set α) (n : ℕ), ⇑f '' s ^ n = (⇑f '' s) ^ n
-- Init.WF
PSigma.Lex : {α : Sort u} → {β : α → Sort v} → (α → α → Prop) → ((a : α) → β a → β a → Prop) → PSigma β → PSigma β → Prop