mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Internal
/-- `LocationLink` with additional meta-data that allows the watchdog to resolve the range of this
`LocationLink`. This is necessary because the position information from the .olean may be stale
(e.g. if the user has edited the file that the definition is from, but neither saved or built it),
while file workers sync their current reference information into the watchdog using ilean info
notifications, which is up-to-date.
 -/
Lean.Lsp.LeanLocationLink : Type
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.const_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.CosimplicialObject.Augmented.const.obj X).left = X
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_pow_iff_right₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} {m n : ℕ} [PosMulStrictMono M₀]
  [ZeroLEOneClass M₀], 1 < a → (a ^ n ≤ a ^ m ↔ n ≤ m)
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.lift_comp_lift : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : PerfectRing N p] [inst_11 : IsPRadical j p],
  (PerfectRing.lift j k p).comp (PerfectRing.lift i j p) = PerfectRing.lift i k p
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.is_left_invariant_addCHaar : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} (g : G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.addCHaar K₀ (TopologicalSpace.Compacts.map (fun x => g + x) ⋯ K) =
    MeasureTheory.Measure.haar.addCHaar K₀ K
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.fromLeftNeg.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg), S.fromLeftNeg x = Exists.choose ⋯
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.IsCompactElement.exists_finset_of_le_iSup : ∀ (α : Type u_2) [inst : CompleteLattice α] {k : α},
  IsCompactElement k → ∀ {ι : Type u_3} (f : ι → α), k ≤ ⨆ i, f i → ∃ s, k ≤ ⨆ i ∈ s, f i
-- Mathlib.Data.Seq.Computation
/-- Attribute expressing bisimilarity over two `Computation`s  -/
Computation.IsBisimulation : {α : Type u} → (Computation α → Computation α → Prop) → Prop
-- Init.Meta.Defs
Lean.versionStringCore : String
-- Lean.Elab.PreDefinition.WF.FloatRecApp
/-- Preprocesses the expressions to improve the effectiveness of `wfRecursion`.

* Floats out the RecApp markers.
  Example:
  ```
  def f : Nat → Nat
    | 0 => 1
    | i+1 => (f x) i
  ```

Unlike `Lean.Elab.Structural.preprocess`, do _not_ beta-reduce, as it could
remove `let_fun`-lambdas that contain explicit termination proofs.
(Note(kmill): this last statement no longer affects `let_fun`/`have`.)
 -/
Lean.Elab.WF.floatRecApp : Lean.Expr → Lean.CoreM Lean.Expr
-- Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear
/-- Building continuous bilinear maps from bilinear maps between finite dimensional topological
vector spaces over a complete field.  -/
LinearMap.toContinuousBilinearMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : AddCommGroup E] →
          [inst_3 : Module 𝕜 E] →
            [inst_4 : TopologicalSpace E] →
              [IsTopologicalAddGroup E] →
                [ContinuousSMul 𝕜 E] →
                  [FiniteDimensional 𝕜 E] →
                    [T2Space E] →
                      {F : Type u_3} →
                        [inst_9 : AddCommGroup F] →
                          [inst_10 : Module 𝕜 F] →
                            [inst_11 : TopologicalSpace F] →
                              [IsTopologicalAddGroup F] →
                                [ContinuousSMul 𝕜 F] →
                                  [FiniteDimensional 𝕜 F] →
                                    [T2Space F] →
                                      {G : Type u_4} →
                                        [inst_16 : AddCommGroup G] →
                                          [inst_17 : Module 𝕜 G] →
                                            [inst_18 : TopologicalSpace G] →
                                              [inst_19 : IsTopologicalAddGroup G] →
                                                [inst_20 : ContinuousSMul 𝕜 G] → (E →ₗ[𝕜] F →ₗ[𝕜] G) → E →L[𝕜] F →L[𝕜] G
-- Mathlib.Data.Finset.Functor
Finset.seqLeft_def : ∀ {α β : Type u} [inst : (P : Prop) → Decidable P] (s : Finset α) (t : Finset β), s <* t = if t = ∅ then ∅ else s
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_last_of_ne_last : ∀ {n : ℕ} {i : Fin (n + 2)} (hi : i ≠ Fin.last (n + 1)), (Fin.last n).predAbove i = i.castPred hi
-- Mathlib.Algebra.Order.Ring.Cone
RingConeClass.toAddGroupConeClass : ∀ {S : Type u_1} {R : outParam (Type u_2)} {inst : Ring R} {inst_1 : SetLike S R} [self : RingConeClass S R],
  AddGroupConeClass S R
-- Mathlib.Topology.MetricSpace.Congruence
Congruent.comp_left_iff : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {f : P₁ → P₃},
  Isometry f → (Congruent (f ∘ v₁) v₂ ↔ Congruent v₁ v₂)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (X : C)
  [CategoryTheory.Projective X], CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.condition_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {Z : C} (h : CategoryTheory.Limits.cokernel f ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      Std.DTreeMap.Raw.Const.get? (Std.DTreeMap.Raw.Const.insertMany t l) k =
        (List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l).or
          (Std.DTreeMap.Raw.Const.get? t k)
-- Mathlib.Data.Set.Lattice.Image
Set.bijOn_iUnion_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s →
    ∀ {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.BijOn f (⋃ i, s i) (⋃ i, t i)
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
and `B ⟶ X` is an arrow of `S`. This is the hom `B ⟶ X`.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.fromMiddleHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {X : C} → {S : J.Cover X} → {T : (I : S.Arrow) → J.Cover I.Y} → (I : (S.bind T).Arrow) → I.middle ⟶ X
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Specialized constructor for `IsLocalization.Away`.  -/
IsLocalization.Away.mk : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R),
  IsUnit ((algebraMap R S) r) →
    (∀ (s : S), ∃ n a, s * (algebraMap R S) r ^ n = (algebraMap R S) a) →
      (∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ n, r ^ n * a = r ^ n * b) → IsLocalization.Away r S
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsImmersion (CategoryTheory.CategoryStruct.comp f g)], AlgebraicGeometry.IsImmersion f
-- Init.Data.Ord.Vector
Vector.instLawfulEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp] {n : ℕ}, Std.LawfulEqCmp (Vector.compareLex cmp)
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K],
  Module.Finite ℤ (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_X_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.natTrailingDegree ≤ 1
-- Mathlib.Data.Nat.Basic
/-- A subset of `ℕ` containing zero and closed under `Nat.succ` contains all of `ℕ`.  -/
Nat.set_induction : ∀ {S : Set ℕ}, 0 ∈ S → (∀ k ∈ S, k + 1 ∈ S) → ∀ (n : ℕ), n ∈ S
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.not_isLongestRevMatch_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice},
  ¬String.Slice.Pattern.Model.IsLongestRevMatch pat s.endPos
-- Mathlib.Data.List.Sort
List.sublist_orderedInsert : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] (x : α) (xs : List α),
  xs.Sublist (List.orderedInsert r x xs)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C).obj F =
    F.mapAddMon.obj (CategoryTheory.AddMon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))
-- Lean.Parser.Term
Lean.Parser.Term.borrowed.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- Continuity of interval integral with respect to a parameter at a point.
Given `F : X → ℝ → E`, assume `F x` is ae-measurable on `[a, b]` for `x` in a
neighborhood of `x₀`, and assume it is bounded by a function integrable on
`[a, b]` independent of `x` in a neighborhood of `x₀`. If `(fun x ↦ F x t)`
is continuous at `x₀` for almost every `t` in `[a, b]`
then the same holds for `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`.  -/
intervalIntegral.continuousAt_of_dominated_interval : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3}
  [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ},
  (∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousAt (fun x => F x t) x₀) →
          ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀
-- Mathlib.CategoryTheory.Adjunction.Whiskering
/-- Given an adjunction `F ⊣ G`, this provides the natural adjunction
`(whiskeringRight C _ _).obj F ⊣ (whiskeringRight C _ _).obj G`.  -/
CategoryTheory.Adjunction.whiskerRight : (C : Type u_1) →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {F : CategoryTheory.Functor D E} →
              {G : CategoryTheory.Functor E D} →
                (F ⊣ G) →
                  ((CategoryTheory.Functor.whiskeringRight C D E).obj F ⊣
                    (CategoryTheory.Functor.whiskeringRight C E D).obj G)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.contMDiff_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : AddMonoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : AddMonoid G'] (self : ContMDiffAddMonoidMorphism I I' n G G'),
  ContMDiff I I' n (↑self.toAddMonoidHom).toFun
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_neg : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f : MvPolynomial σ R},
  m.degree (-f) = m.degree f
-- Aesop.Forward.Match.Types
Aesop.instBEqForwardRuleMatch.beq : Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatch → Bool
-- Mathlib.RingTheory.NoetherNormalization
/-- `T` maps different monomials of `f` to polynomials with different degrees in `X_0`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.degreeOf_t_ne_of_ne : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (v w : Fin (n + 1) →₀ ℕ),
  v ∈ f.support →
    w ∈ f.support →
      v ≠ w →
        MvPolynomial.degreeOf 0 ((NoetherNormalization.T✝ f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f))) ≠
          MvPolynomial.degreeOf 0 ((NoetherNormalization.T✝ f) ((MvPolynomial.monomial w) (MvPolynomial.coeff w f)))
-- Mathlib.LinearAlgebra.Dimension.Basic
lift_rank_range_of_injective : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Injective ⇑f → Cardinal.lift.{v, v'} (Module.rank R ↥f.range) = Cardinal.lift.{v', v} (Module.rank R M)
-- Mathlib.Tactic.Simproc.Divisors
/-- The dsimproc `Nat.divisors_ofNat` computes the finset `Nat.divisors n` when `n` is a
numeral. For instance, this simplifies `Nat.divisors 6` to `{1, 2, 3, 6}`.  -/
Nat.divisors_ofNat : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_inverse_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) {X Y : CategoryTheory.Comma L₂ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeftIso R i).inverse.map f).right = f.right
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.mk.inj : ∀ {globPattern : String} {kind? : Option ℕ} {globPattern_1 : String} {kind?_1 : Option ℕ},
  { globPattern := globPattern, kind? := kind? } = { globPattern := globPattern_1, kind? := kind?_1 } →
    globPattern = globPattern_1 ∧ kind? = kind?_1
-- Mathlib.Algebra.Homology.Homotopy
/-- The isomorphism in homology induced by a homotopy equivalence.  -/
HomotopyEquiv.toHomologyIso : {C : Type u_2} →
  [inst : CategoryTheory.Category.{v_1, u_2} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_3} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            HomotopyEquiv K L →
              (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.homology i ≅ L.homology i
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_denselyOrdered_iff : ∀ {L : FirstOrder.Language} {M : Type w'} [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : Preorder M]
  [L.OrderedStructure M], M ⊨ L.denselyOrderedSentence ↔ DenselyOrdered M
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.type : Lean.Lsp.ShowMessageRequestParams → Lean.Lsp.MessageType
-- Mathlib.Algebra.Category.Ring.Under.Limits
CommRingCat.Under.instPreservesLimitUnderDiscreteFunctorTensorProdOfFinite : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (J : Type u) [Finite J] (f : J → CategoryTheory.Under R),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) (R.tensorProd S)
-- Init.Data.List.Lemmas
List.cons_eq_cons : ∀ {α : Type u_1} {a b : α} {l l' : List α}, a :: l = b :: l' ↔ a = b ∧ l = l'
-- Mathlib.Order.Hom.Basic
OrderIso.eq_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β}, x = e.symm y ↔ e x = y
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.ChosenCoendsOfShape.mk : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        (cowedge : (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.Cowedge F) →
          ((F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
              CategoryTheory.Limits.IsColimit (cowedge F)) →
            CategoryTheory.Limits.ChosenCoendsOfShape J C
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr.eq_def : ∀ (x : ONote),
  x.repr =
    match x with
    | ONote.zero => 0
    | e.oadd n a => Ordinal.omega0 ^ e.repr * ↑↑n + a.repr
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.mkCocone_ι_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) C} {X : C} (f : F.obj none ⟶ X)
  (ι : (j : J) → F.obj (some j) ⟶ X)
  (w :
    ∀ (j : J), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.WidePushoutShape.Hom.init j)) (ι j) = f)
  (j : CategoryTheory.Limits.WidePushoutShape J),
  (CategoryTheory.Limits.WidePushoutShape.mkCocone f ι w).ι.app j =
    match j with
    | none => f
    | some j => ι j
-- Mathlib.Data.Part
Part.none_ne_some : ∀ {α : Type u_1} (x : α), Part.none ≠ Part.some x
-- Init.Data.String.Basic
String.Slice.Pos.byte_copy : ∀ {s : String.Slice} {pos : s.Pos} (h : pos.copy ≠ s.copy.endPos), pos.copy.byte h = pos.byte ⋯
-- Mathlib.FieldTheory.FinTrdeg
finTrdeg_iff_trdeg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  FinTrdeg K L ↔ Algebra.trdeg K L < Cardinal.aleph0
-- Mathlib.Computability.DFA
/-- Lifts an equivalence on states to an equivalence on DFAs.  -/
DFA.reindex : {α : Type u} → {σ : Type v} → {σ' : Type u_2} → σ ≃ σ' → DFA α σ ≃ DFA α σ'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_def : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  (f g : (b : β) → X b), nndist f g = Finset.univ.sup fun b => nndist (f b) (g b)
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.below : {L : FirstOrder.Language} →
  {α : Type u'} →
    {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsUniversal → Prop} →
      {n : ℕ} → {a : L.BoundedFormula α n} → a.IsUniversal → Prop
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.localization_comap_isInducing : ∀ {R : Type u} (S : Type v) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Submonoid R)
  [IsLocalization M S], Topology.IsInducing (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.Data.Multiset.Sections
Multiset.sections_cons : ∀ {α : Type u_1} (s : Multiset (Multiset α)) (m : Multiset α),
  (m ::ₘ s).Sections = m.bind fun a => Multiset.map (Multiset.cons a) s.Sections
-- Mathlib.GroupTheory.Perm.ViaEmbedding
/-- `viaEmbedding` as a group homomorphism  -/
Equiv.Perm.viaEmbeddingHom : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Equiv.Perm α →* Equiv.Perm β
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_of_forall_fin_meas_le' : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {ε : Type u_9} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)],
  ∀ C < ⊤,
    ∀ {f : α → ε},
      MeasureTheory.AEStronglyMeasurable f μ →
        (∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C) → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_zero : ∀ {α : Type u_2} {M : Type u_7} [inst : Zero M], Function.const α 0 = 0
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isPrincipal_iff : ∀ {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 : IsLocalization S P] (I : FractionalIdeal S P), (↑I).IsPrincipal ↔ ∃ x, I = FractionalIdeal.spanSingleton S x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.forM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} {m : Type w → Type w'} [Std.TransCmp cmp]
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, t₁.WF → t₂.WF → t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_mul_natCast : ∀ (x : ENNReal) (y : ℝ) (n : ℕ), x ^ (y * ↑n) = (x ^ y) ^ n
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
CondensedMod.LocallyConstant.functorIsoDiscreteAux₁ : (R : Type (u + 1)) →
  [inst : Ring R] → (M : ModuleCat R) → M ≅ ModuleCat.of R (LocallyConstant ↑(CompHaus.of PUnit.{u + 1}).toTop ↑M)
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_univ : ∀ {X : Type u_1} {F : Set X} (T : X → X), F.Nonempty → Dynamics.coverEntropyEntourage T F Set.univ = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerveAdjunction.isIso_counit : CategoryTheory.IsIso CategoryTheory.nerveAdjunction.counit
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsSchemeTheoreticallyDominant
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.modify.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] (m m_1 : Std.HashMap.Raw α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : β → β), f = f_1 → m.modify a f = m_1.modify a_1 f_1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_μ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X Y : C), (CategoryTheory.Functor.LaxMonoidal.μ (F.prod' G) X Y).1 = CategoryTheory.Functor.LaxMonoidal.μ F X Y
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.drop : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → ∀ (n : ℕ), Substring.Raw.ValidFor (l ++ List.take n m) (List.drop n m) r (s.drop n)
-- Mathlib.Order.Shrink
instWellFoundedLTShrink : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Preorder α] [WellFoundedLT α], WellFoundedLT (Shrink.{u, u_1} α)
-- Mathlib.FieldTheory.Relrank
/-- The `Nat` version of `Subfield.relrank`.
If `B / A ⊓ B` is an infinite extension, then it is zero.  -/
Subfield.relfinrank : {E : Type v} → [inst : Field E] → Subfield E → Subfield E → ℕ
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.forget_commGrp_preserves_mono : (CategoryTheory.forget AddCommGrpCat).PreservesMonomorphisms