mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.isAddLeftInvariant_map : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G]
  {H : Type u_3} [inst_3 : MeasurableSpace H] [inst_4 : Add H] [MeasurableAdd H] [μ.IsAddLeftInvariant] (f : G →ₙ+ H),
  Measurable ⇑f → Function.Surjective ⇑f → (MeasureTheory.Measure.map (⇑f) μ).IsAddLeftInvariant
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.comp₂ : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_6}
  {E₂ : Type u_7} [inst_5 : NormedAddCommGroup E₁] [inst_6 : NormedAddCommGroup E₂] [inst_7 : NormedSpace 𝕜 E₁]
  [inst_8 : NormedSpace 𝕜 E₂] {g : E₁ × E₂ → G} {f₁ : F → E₁} {f₂ : F → E₂} {x : F},
  ContDiffAt 𝕜 n g (f₁ x, f₂ x) → ContDiffAt 𝕜 n f₁ x → ContDiffAt 𝕜 n f₂ x → ContDiffAt 𝕜 n (fun x => g (f₁ x, f₂ x)) x
-- Mathlib.Analysis.Complex.Exponential
Real.expNear_succ : ∀ (n : ℕ) (x r : ℝ), Real.expNear (n + 1) x r = Real.expNear n x (1 + x / (↑n + 1) * r)
-- Lean.Meta.Tactic.Grind.Simp
/-- A lighter version of `preprocess` which produces a definitionally equal term,
but ensures assumptions made by `grind` are satisfied.
 -/
Lean.Meta.Grind.preprocessLight : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.RingTheory.DedekindDomain.Instances
/-- Let `R ⊆ S ⊆ T` be a tower of rings. Let `Sₚ` and `Tₚ` denote the localizations of `S` and `T` at
the prime ideal `P` of `R`. Then `Tₚ` is a `Sₚ`-algebra.
This cannot be an instance since it creates a diamond when `S = T`.
 -/
Localization.AtPrime.algebra_localization_localization : {R : Type u_1} →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              {P : Ideal R} →
                [inst_4 : P.IsPrime] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : Algebra R T] →
                      [IsScalarTower R S T] →
                        Algebra (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
                          (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_surjective_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Surjective ⇑(AdicCompletion.of I M) ↔ IsPrecomplete I M
-- Mathlib.Data.Set.Finite.Basic
Set.finite_univ_iff : ∀ {α : Type u}, Set.univ.Finite ↔ Finite α
-- Mathlib.Tactic.TermCongr
/-- For holding onto the hole's value along with the value of either the LHS or RHS of the hole.
These occur wrapped in metadata so that they always appear as function application
with exactly four arguments.

Note that there is no relation between `val` and the proof.
We need to decouple these to support letting the proof's elaboration be deferred until
we know whether we want an iff, eq, or heq, while also allowing it to choose
to elaborate as an iff, eq, or heq.
Later, the congruence generator handles any discrepancies.
See `CongrResult` below.  -/
Mathlib.Tactic.TermCongr.cHole : {α : Sort u} → α → {p : Prop} → p → α
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point.0.termY : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp ((t.insertIfNew k v).minKey ⋯) k).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- To show `i` is an exponential ideal it suffices to show that `A ⟹ iB` is "in" `D` for any `A` in
`C` and `B` in `D`.
 -/
CategoryTheory.ExponentialIdeal.mk' : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalClosed C],
  (∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) → CategoryTheory.ExponentialIdeal i
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.block_stabilizerOrderIso.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] [htGX : AddAction.IsPretransitive G X]
  (a : X),
  AddAction.block_stabilizerOrderIso G a =
    {
      toFun := fun x =>
        match x with
        | ⟨B, ⋯⟩ => ⟨AddAction.stabilizer G B, ⋯⟩,
      invFun := fun x =>
        match x with
        | ⟨H, hH⟩ => ⟨AddAction.orbit (↥H) a, ⋯⟩,
      left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.RingTheory.Valuation.Basic
ValuationClass.mk : ∀ {F : Type u_7} {R : outParam (Type u_5)} {Γ₀ : outParam (Type u_6)} [inst : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_1 : Ring R] [inst_2 : FunLike F R Γ₀] [toMonoidWithZeroHomClass : MonoidWithZeroHomClass F R Γ₀],
  (∀ (f : F) (x y : R), f (x + y) ≤ max (f x) (f y)) → ValuationClass F R Γ₀
-- Mathlib.AlgebraicGeometry.Normalization
/-- Given a morphism `f : X ⟶ Y`, this is the presheaf of integral closure of `Y` in `X`.  -/
AlgebraicGeometry.Scheme.Hom.normalizationDiagram : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → CategoryTheory.Functor Y.Opensᵒᵖ CommRingCat
-- Lean.CoreM
Lean.Core.SavedState.toState : Lean.Core.SavedState → Lean.Core.State
-- Mathlib.Algebra.GroupWithZero.Divisibility
isPrimal_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α], IsPrimal 0
-- Mathlib.Order.Category.Preord
Preord.str : (self : Preord) → Preorder ↑self
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNat' : ∀ (n : ℕ), (UInt64.ofNat n).toUSize = USize.ofNat n
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`.  -/
VectorField.leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U V W : E → E} {s : Set E} {x : E},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      ContDiffWithinAt 𝕜 2 U s x →
        ContDiffWithinAt 𝕜 2 V s x →
          ContDiffWithinAt 𝕜 2 W s x →
            IsSymmSndFDerivWithinAt 𝕜 U s x →
              IsSymmSndFDerivWithinAt 𝕜 V s x →
                IsSymmSndFDerivWithinAt 𝕜 W s x →
                  VectorField.lieBracketWithin 𝕜 U (VectorField.lieBracketWithin 𝕜 V W s) s x =
                    VectorField.lieBracketWithin 𝕜 (VectorField.lieBracketWithin 𝕜 U V s) W s x +
                      VectorField.lieBracketWithin 𝕜 V (VectorField.lieBracketWithin 𝕜 U W s) s x
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.upperSemicontinuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {f : α → γ}, ContinuousAt f x → UpperSemicontinuousAt f x
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_pos_eq_iff : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ}, 0 < n → ((⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_eventually_monotone : ∀ {u v : ℕ → EReal}, u ≤ᶠ[Filter.atTop] v → LinearGrowth.linearGrowthInf u ≤ LinearGrowth.linearGrowthInf v
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Given a function such that `f` and `x ^ (k + l) * f` are bounded for a suitable `l`, then
one can bound explicitly the integral of `x ^ k * f`.  -/
integral_pow_mul_le_of_le_of_pow_mul_le : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E]
  [inst_2 : NormedAddCommGroup F] {μ : MeasureTheory.Measure E} [μ.HasTemperateGrowth] {f : E → F} {C₁ C₂ : ℝ} {k : ℕ},
  (∀ (x : E), ‖f x‖ ≤ C₁) →
    (∀ (x : E), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂) →
      ∫ (x : E), ‖x‖ ^ k * ‖f x‖ ∂μ ≤
        (2 ^ μ.integrablePower * ∫ (x : E), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)
-- Mathlib.Algebra.MvPolynomial.CommRing
/-- Subtracting `monomial d c - monomial d' c` from `p`, where `c = coeff d p` and `d ≠ d'`,
leaves the support inside `p.support.erase d ∪ {d'}`.  -/
MvPolynomial.support_sub_monomial_sub_monomial_subset : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) [inst_1 : DecidableEq σ] (d d' : σ →₀ ℕ)
  (c : R),
  d ≠ d' →
    MvPolynomial.coeff d p = c →
      (p - ((MvPolynomial.monomial d) c - (MvPolynomial.monomial d') c)).support ⊆ p.support.erase d ∪ {d'}
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_mul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃),
  (a * b).re = a.re * b.re + c₁ * a.imI * b.imI + c₃ * a.imJ * b.imJ + c₂ * c₃ * a.imJ * b.imK - c₁ * c₃ * a.imK * b.imK
-- Mathlib.Data.Stream.Init
Stream'.corec'_eq : ∀ {α : Type u} {β : Type v} (f : α → β × α) (a : α),
  Stream'.corec' f a = Stream'.cons (f a).1 (Stream'.corec' f (f a).2)
-- Lean.Meta.Tactic.Grind.Anchor
/-- Example: `{ numDigits := 4, anchorPrefix := 0x0c88 }.matches 0x0c88ab10ef20206a` returns `true`
 -/
Lean.Meta.Grind.AnchorRef.matches : Lean.Meta.Grind.AnchorRef → UInt64 → Bool
-- Init.System.FilePath
/-- Returns the parent directory of a path, if there is one.

If the path is that of the root directory or the root of a drive letter, `none` is returned.
Otherwise, the path's parent directory is returned.
 -/
System.FilePath.parent : System.FilePath → Option System.FilePath
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Interpret a `CStarMatrix m n A` as a continuous linear map acting on `C⋆ᵐᵒᵈ (n → A)`.  -/
CStarMatrix.toCLM : {m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_5} →
      [Fintype m] →
        [inst : NonUnitalCStarAlgebra A] →
          CStarMatrix m n A →ₗ[ℂ] WithCStarModule A (m → A) →L[ℂ] WithCStarModule A (n → A)
-- Mathlib.Algebra.Free
FreeAddSemigroup.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
/-- Compute the composition of two open partial homeomorphisms induced by fiberwise linear
equivalences.  -/
FiberwiseLinear.trans_openPartialHomeomorph_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {φ φ' : B → F ≃L[𝕜] F} {U U' : Set B} (hU : IsOpen U)
  (hφ : ContinuousOn (fun x => ↑(φ x)) U) (h2φ : ContinuousOn (fun x => ↑(φ x).symm) U) (hU' : IsOpen U')
  (hφ' : ContinuousOn (fun x => ↑(φ' x)) U') (h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U') (b : B) (v : F),
  ↑((FiberwiseLinear.openPartialHomeomorph φ hU hφ h2φ).trans (FiberwiseLinear.openPartialHomeomorph φ' hU' hφ' h2φ'))
      (b, v) =
    (b, (φ' b) ((φ b) v))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, (Std.TreeMap.filterMap f t)[k]? = t[k]?.pbind fun x h' => f (t.getKey k ⋯) x
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.splitter : (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) →
  (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
    (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
          (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned) → motive a
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.nonempty_compl_range : ∀ {ι : Type u} (f : ι → Ordinal.{max u v}), (Set.range f)ᶜ.Nonempty
-- Mathlib.Order.RelClasses
/-- Set notation form of `LE.le.eq_or_lt` -/
LE.le.eq_or_ssubset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a = b ∨ a ⊂ b
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.le_div_iff_of_ne_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I J J' : FractionalIdeal (nonZeroDivisors R₁) K},
  J' ≠ 0 → (I ≤ J / J' ↔ ∀ x ∈ I, ∀ y ∈ J', x * y ∈ J)
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The isomorphism `L.obj X ≅ L.obj Y` that is deduced from a morphism `f : X ⟶ Y` which
belongs to `W`, when `L.IsLocalization W`.  -/
CategoryTheory.Localization.isoOfHom : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] → {X Y : C} → (f : X ⟶ Y) → W f → (L.obj X ≅ L.obj Y)
-- Mathlib.Topology.AlexandrovDiscrete
isOpen_sInter : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {S : Set (Set α)},
  (∀ s ∈ S, IsOpen s) → IsOpen (⋂₀ S)
-- Mathlib.RingTheory.LocalProperties.FinitePresentation
Module.FinitePresentation.of_localizationSpan' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ {Mₚ : ↑s → Type u_3} [inst_3 : (g : ↑s) → AddCommGroup (Mₚ g)] [inst_4 : (g : ↑s) → Module R (Mₚ g)]
      {Rₚ : ↑s → Type u_4} [inst_5 : (g : ↑s) → CommRing (Rₚ g)] [inst_6 : (g : ↑s) → Algebra R (Rₚ g)]
      [∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)] [inst_8 : (g : ↑s) → Module (Rₚ g) (Mₚ g)]
      [∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)] (ϕ : (g : ↑s) → M →ₗ[R] Mₚ g)
      [∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)],
      (∀ (g : ↑s), Module.FinitePresentation (Rₚ g) (Mₚ g)) → Module.FinitePresentation R M
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
/-- In 2D, the line defined by `s.orthRadius p` intersects `s` at at most two points so long as `p`
lies within `s` and not at its center.

This version provides expressions for those points in terms of an arbitrary vector in
`s.orthRadius p`.  -/
EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hf2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p : P},
  dist p s.center ≤ s.radius →
    p ≠ s.center →
      ∀ {v : V},
        v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ →
          v ≠ 0 →
            Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
              {(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p,
                -(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • v +ᵥ p}
-- Mathlib.Analysis.Quaternion
Quaternion.norm_coe : ∀ (a : ℝ), ‖↑a‖ = ‖a‖
-- Lean.Elab.Tactic.Config
/-- `declare_command_config_elab_legacy elabName TypeName` declares a function `elabName : Syntax → CommandElabM TypeName`
that elaborates a command configuration.
The configuration can be from `Lean.Parser.Tactic.optConfig` or `Lean.Parser.Tactic.config`,
and these can also be wrapped in null nodes (for example, from `(config)?`).

The elaborator has error recovery enabled.

This command has been deprecated since 2026-05-14. Use `declare_command_config_elab` instead.
 -/
Lean.Elab.Tactic.commandConfigElab : Lean.ParserDescr
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.lift_unique : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : X → A) (g : FreeAlgebra R X →ₐ[R] A), ⇑g ∘ FreeAlgebra.ι R = f ↔ g = (FreeAlgebra.lift R) f
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.irreducible_X : ∀ {R : Type u} [inst : CommRing R] [IsDomain R], Irreducible Polynomial.X
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.KernelFork.IsLimit.ofι.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {W : C} (g : W ⟶ X) (eq : CategoryTheory.CategoryStruct.comp g f = 0)
  (lift lift_1 : {W' : C} → (g' : W' ⟶ X) → CategoryTheory.CategoryStruct.comp g' f = 0 → (W' ⟶ W))
  (e_lift : lift = lift_1)
  (fac :
    ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0),
      CategoryTheory.CategoryStruct.comp (lift g' eq') g = g')
  (uniq :
    ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0) (m : W' ⟶ W),
      CategoryTheory.CategoryStruct.comp m g = g' → m = lift g' eq'),
  CategoryTheory.Limits.KernelFork.IsLimit.ofι g eq lift fac uniq =
    CategoryTheory.Limits.KernelFork.IsLimit.ofι g eq lift_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasLeftCalculusOfFractions] ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X),
  W s →
    CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂ →
      ∃ Y' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp f₁ t = CategoryTheory.CategoryStruct.comp f₂ t
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.trans : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J},
  CategoryTheory.Zigzag j₁ j₂ → CategoryTheory.Zigzag j₂ j₃ → CategoryTheory.Zigzag j₁ j₃
-- Std.Time.Date.Unit.Day
/-- Creates an ordinal for a specific day within the year, ensuring that the provided day (`data`)
is within the valid range for the year, which can be 1 to 365 or 366 for leap years.
 -/
Std.Time.Day.Ordinal.OfYear.ofNat : {leap : Bool} →
  (data : ℕ) →
    autoParam (data ≥ 1 ∧ data ≤ if leap = true then 366 else 365) Std.Time.Day.Ordinal.OfYear.ofNat._auto_3 →
      Std.Time.Day.Ordinal.OfYear leap
-- Mathlib.Algebra.Notation.Defs
ite_sub_ite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Sub α] (a b c d : α),
  ((if P then a else b) - if P then c else d) = if P then a - c else b - d
-- Init.Data.List.Sublist
List.Sublist.append : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α}, l₁.Sublist l₂ → r₁.Sublist r₂ → (l₁ ++ r₁).Sublist (l₂ ++ r₂)
-- Mathlib.Logic.Equiv.Set
/-- If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ PUnit`.  -/
Equiv.Set.insert : {α : Type u} → {s : Set α} → [DecidablePred fun x => x ∈ s] → {a : α} → a ∉ s → ↑(insert a s) ≃ ↑s ⊕ PUnit.{u + 1}
-- Init.Data.Bool
Bool.toInt_false : false.toInt = 0
-- Mathlib.RingTheory.Ideal.Quotient.Defs
/-- On `Ideal`s, `Submodule.quotientRel` is a ring congruence.  -/
Ideal.Quotient.ringCon : {R : Type u} → [inst : Ring R] → (I : Ideal R) → [I.IsTwoSided] → RingCon R
-- Init.Data.Nat.Bitwise.Lemmas
Nat.exists_ge_and_testBit_of_ge_two_pow : ∀ {n x : ℕ}, x ≥ 2 ^ n → ∃ i ≥ n, x.testBit i = true
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn'_rco : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : LE α]
  [inst_5 : LT α] [inst_6 : DecidableLT α] [inst_7 : Std.PRange.UpwardEnumerable α] [inst_8 : Std.Rxo.IsAlwaysFinite α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerable α] [inst_10 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_11 : Std.PRange.LawfulUpwardEnumerableLT α] {xs : Std.Rco α} {init : β}
  {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur ⋯ b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn' xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofCompletionInfo.inj : ∀ {i i_1 : Lean.Elab.CompletionInfo}, Lean.Elab.Info.ofCompletionInfo i = Lean.Elab.Info.ofCompletionInfo i_1 → i = i_1
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Checking exactness of colimits of shape `Discrete ℕ` and `Discrete J` for finite `J` is enough for
countable AB4.
 -/
CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat_and_finite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCountableCoproducts C]
  [CategoryTheory.Limits.HasFiniteLimits C]
  [∀ (J : Type) [inst_3 : Finite J], CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete J) C]
  [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C], CategoryTheory.CountableAB4 C
-- Mathlib.Data.PFunctor.Univariate.M
/-- destructor for M-types  -/
PFunctor.M.cases : {F : PFunctor.{uA, uB}} → {r : F.M → Sort w} → ((x : ↑F F.M) → r (PFunctor.M.mk x)) → (x : F.M) → r x
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.slope_le_of_hasDerivWithinAt_Iio` using `derivWithin`.  -/
ConvexOn.slope_le_leftDeriv : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Iio y) y → slope f x y ≤ derivWithin f (Set.Iio y) y
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.canNestIn : ℕ → Lean.VersoModuleDocs.Snippet → Bool
-- Mathlib.Computability.Partrec
Nat.Partrec.prec' : ∀ {f g h : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g →
      Nat.Partrec h →
        Nat.Partrec fun a =>
          (f a).bind fun n =>
            Nat.rec (g a)
              (fun y IH => do
                let i ← IH
                h (Nat.pair a (Nat.pair y i)))
              n
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.ulift : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.IsStablyFree R M],
  Module.IsStablyFree R (ULift.{w, v} M)
-- Mathlib.GroupTheory.DivisibleHull
/-- `ArchimedeanClass.mk` of an element from `DivisibleHull` only depends on the numerator.  -/
DivisibleHull.archimedeanClassMk_mk_eq : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (m : M) (s s' : ℕ+),
  ArchimedeanClass.mk (DivisibleHull.mk m s) = ArchimedeanClass.mk (DivisibleHull.mk m s')
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshRef.mk : IO.Ref ProofWidgets.RefreshComponent.RefreshState → ProofWidgets.RefreshComponent.RefreshRef
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_C_mul : ∀ {F : Type u} [inst : Field F] (f : Polynomial F) {x : F}, x ≠ 0 → (Polynomial.C x * f).natSepDegree = f.natSepDegree
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_iInf_of_directed' : ∀ {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} [Nonempty ι] {l : ι → Filter α} (s : (i : ι) → ι' i → Set α)
  (p : (i : ι) → ι' i → Prop),
  (∀ (i : ι), (l i).HasBasis (p i) (s i)) →
    Directed (fun x1 x2 => x1 ≥ x2) l → (⨅ i, l i).HasBasis (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.cons_iff : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  Tactic.ComputeAsymptotics.UnitMonomial.AllZero (hd :: tl) ↔ hd = 0 ∧ tl.AllZero
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.map : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : α → β} {g : Filter α},
  g.TotallyBounded → UniformContinuous f → (Filter.map f g).TotallyBounded
-- Lean.Parser.Basic
Lean.Parser.binNumberFn : String.Pos.Raw → optParam Bool true → Lean.Parser.ParserFn