mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S T : CategoryTheory.Subgroupoid C} (h : S ≤ T),
  CategoryTheory.Subgroupoid.inclusion h =
    { obj := fun s => ⟨↑s, ⋯⟩, map := fun {X Y} f => ⟨↑f, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.CStarAlgebra.Basic
dist_star_star : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [NormedStarGroup E] (x y : E),
  dist (star x) (star y) = dist x y
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.guitartExact_iff_initial : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B),
  w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
-- Init.Tactics
/-- In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
```
by_cases t
· tac1
· tac2
```
It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
add anything to the context and hence would be useless for proving theorems. To actually insert an
`ite` application use `refine if t then ?_ else ?_`.)

The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
alternative syntax for:
```
by_cases h : t
· tac1
· tac2
```
It performs case distinction on `h : t` or `h : ¬t`.

You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
by the end of the block.
 -/
Lean.Parser.Tactic.tacDepIfThenElse : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.not_ge_of_lt : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT a b → ¬Std.PRange.UpwardEnumerable.LE b a
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningHom_injective : ∀ {V : Type u} {G : SimpleGraph V} {x : G.Subgraph}, Function.Injective ⇑x.spanningHom
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_union_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α}, Set.Ici a ∪ Set.Iic a = Set.univ
-- Init.Data.Iterators.Consumers.Access
/-- If possible, takes `n` steps with the iterator `it` and
returns the `n`-th emitted value, or `none` if `it` finished
before emitting `n` values.

If the iterator is not productive, this function might run forever in an endless loop of iterator
steps. The variant `it.ensureTermination.atIdxSlow?` is guaranteed to terminate after finitely many
steps.
 -/
Std.Iter.atIdxSlow? : {α β : Type u_1} → [Std.Iterator α Id β] → ℕ → Std.Iter β → Option β
-- Mathlib.RingTheory.Polynomial.Tower
Polynomial.aeval_map_algebraMap : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B] (x : B) (p : Polynomial R),
  (Polynomial.aeval x) (Polynomial.map (algebraMap R A) p) = (Polynomial.aeval x) p
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.preimage_closedBall : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E₂) (r : ℝ), ⇑e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r
-- Mathlib.Topology.MetricSpace.Holder
/-- **Alias** of `convex_setOfPred_holderWith`.

---

For fixed `f : X → Y` and `C : ℝ≥0`, the set of all parameters `r : ℝ≥0` such that
`f` is `(C, r)`-Hölder is convex.  -/
convex_setOf_holderWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (f : X → Y) (C : NNReal),
  Convex NNReal {r | HolderWith C r f}
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The functor of adjoining a neutral element `one` to a semigroup.  -/
MonCat.adjoinOne : CategoryTheory.Functor Semigrp MonCat
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.injective_ringHom_or_subsingleton_codomain : ∀ {R : Type u_2} {S : Type u_3} [inst : NonAssocRing R] [IsSimpleRing R] [inst_2 : NonAssocSemiring S] (f : R →+* S),
  Function.Injective ⇑f ∨ Subsingleton S
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → 0 < n → a ^ n < 1
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.union : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X} {s t : Set X},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R x t → Convexity.IsStarConvexSet R x (s ∪ t)
-- Mathlib.LinearAlgebra.Matrix.Integer
Matrix.den_ofNat : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : DecidableEq m] (a : ℕ) [inst_2 : a.AtLeastTwo], (OfNat.ofNat a).den = 1
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app : ∀ {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] [inst_2 : CategoryTheory.IsIdempotentComplete D]
  {F G : CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi C) D}
  (τ : (CategoryTheory.Idempotents.toKaroubi C).comp F ⟶ (CategoryTheory.Idempotents.toKaroubi C).comp G)
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Idempotents.Karoubi C) D).obj
              (CategoryTheory.Idempotents.toKaroubi C)).preimage
          τ).app
      P =
    CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
      (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p))
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂)
  (g : T₂ ⟶ T₃) (X : T₃.Algebra),
  ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).inv.app X).f =
    (CategoryTheory.Iso.refl
        ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).inv
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.parent_empty : ∀ {a : ℕ}, Batteries.UnionFind.empty.parent a = a
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.blunt_iff_not_pointed : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {C : ConvexCone R M}, C.Blunt ↔ ¬C.Pointed
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.start_mem_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), u ∈ p.support
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_congr_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)),
      (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The existence of a left Kan lift of `g` along `f`.  -/
CategoryTheory.Bicategory.HasLeftKanLift : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (b ⟶ a) → (c ⟶ a) → Prop
-- Mathlib.Algebra.Order.Field.Basic
left_lt_add_div_two : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  a < (a + b) / 2 ↔ a < b
-- Mathlib.GroupTheory.Solvable
/-- **Alias** of `Group.IsSolvable.commutator_lt_top_of_nontrivial`. -/
IsSolvable.commutator_lt_top_of_nontrivial : ∀ (G : Type u_1) [inst : Group G] [hG : Group.IsSolvable G] [Nontrivial G], commutator G < ⊤
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.leibniz_smul_right : ∀ {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing A₁] [inst_1 : LieRing L₁] [inst_2 : Module A₁ L₁]
  [inst_3 : LieRingModule L₁ A₁] [LieRinehartRing A₁ L₁] (x y : L₁) (a : A₁), ⁅x, a • y⁆ = a • ⁅x, y⁆ + ⁅x, a⁆ • y
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.State.mk : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem →
  Lean.Meta.Simp.State →
    Lean.Name →
      Lean.Meta.Grind.Counters →
        Lean.PArray Lean.Meta.Grind.SplitDiagInfo →
          Lean.PArray Lean.Meta.Grind.EMatchDiagInfo →
            Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr) →
              Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr) →
                Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64 →
                  Std.HashMap Lean.Name Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.State
-- Mathlib.CategoryTheory.Generator.Sheaf
CategoryTheory.Sheaf.isSeparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasCoproducts A]
  [inst_3 : CategoryTheory.HasWeakSheafify J A] {ι : Type w} {S : ι → A},
  (CategoryTheory.ObjectProperty.ofObj S).IsSeparating →
    (CategoryTheory.ObjectProperty.ofObj fun x =>
        match x with
        | (X, i) => CategoryTheory.Sheaf.freeYoneda J X (S i)).IsSeparating
-- Init.Data.String.Lemmas.Order
String.Pos.getUTF8Byte_offset : ∀ {s : String} {p : s.Pos} {h : p.offset < s.rawEndPos}, s.getUTF8Byte p.offset h = p.byte ⋯
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- The forgetful functor from schemes étale over `X` to schemes over `X` is fully faithful.  -/
AlgebraicGeometry.Scheme.Etale.forgetFullyFaithful : (X : AlgebraicGeometry.Scheme) → (AlgebraicGeometry.Scheme.Etale.forget X).FullyFaithful
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Packs the given float into the format given by the specification.

This function assumes that the float is already correctly rounded for the given specification.
This means that the exponent must be equal to the exponent computed by `spec.targetExponent`.
 -/
Float.Model.UnpackedFloat.pack : (spec : Float.Model.Format) → Float.Model.UnpackedFloat → BitVec spec.numBits
-- Mathlib.LinearAlgebra.Trace
/-- Trace of an endomorphism independent of basis.  -/
LinearMap.trace : (R : Type u) →
  [inst : CommSemiring R] → (M : Type v) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) →ₗ[R] R
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDeriv_prod_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_2} {A' : Type u_4} [inst_3 : NormedCommRing A'] [inst_4 : NormedAlgebra 𝕜 A']
  [inst_5 : DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'} {N : WithTop ℕ∞},
  (∀ i ∈ u, ContDiff 𝕜 N (f i)) →
    ∀ {x : E} {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDeriv 𝕜 n (fun x => ∏ j ∈ u, f j x) x‖ ≤
          ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖
-- Mathlib.Order.Cover
covBy_iff_wcovBy_and_not_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter : Type
-- Std.Sync.Broadcast
/-- A multi-subscriber broadcast that delivers each message to all current subscribers.
Supports only bounded buffering and an asynchronous API.

It's the sync version of `Broadcast`.
 -/
Std.Broadcast.Sync : Type → Type
-- Mathlib.Analysis.LocallyConvex.Separation
/-- See also `SeparatingDual.eq_iff_forall_dual_eq`.  -/
geometric_hahn_banach_point_point : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {x y : E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T1Space E], x ≠ y → ∃ f, f x < f y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∉ t → Std.DTreeMap.Raw.Const.get? t a = none
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.InitResults.tree : {α : Type} → Lean.Meta.RefinedDiscrTree.InitResults✝ α → Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
  {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
  {x y : CategoryTheory.Limits.ImageMap sq}, x.map = y.map → x = y
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.mk.injEq : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Finite σ] (toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ)
  (jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian)
  (toPreSubmersivePresentation_1 : Algebra.PreSubmersivePresentation R S ι σ)
  (jacobian_isUnit_1 : IsUnit toPreSubmersivePresentation_1.jacobian),
  ({ toPreSubmersivePresentation := toPreSubmersivePresentation, jacobian_isUnit := jacobian_isUnit } =
      { toPreSubmersivePresentation := toPreSubmersivePresentation_1, jacobian_isUnit := jacobian_isUnit_1 }) =
    (toPreSubmersivePresentation = toPreSubmersivePresentation_1)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_closure_iff_exists_term : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} {x : M},
  x ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∃ t, FirstOrder.Language.Term.realize Subtype.val t = x
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {f : E →ₗ[ℝ] E},
  LinearMap.det f ≠ 0 → MeasureTheory.Measure.map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
-- Mathlib.Data.Set.Lattice
Set.iUnion_psigma : ∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : PSigma γ → Set β), ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩
-- Aesop.Tree.Traversal
Aesop.TreeRef.goal.inj : ∀ {gref gref_1 : Aesop.GoalRef}, Aesop.TreeRef.goal gref = Aesop.TreeRef.goal gref_1 → gref = gref_1
-- Init.Data.Sum.Basic
/-- Case analysis for sums that applies the appropriate function `f` or `g` after checking which
constructor is present.
 -/
Sum.elim : {α : Type u_1} → {β : Type u_2} → {γ : Sort u_3} → (α → γ) → (β → γ) → α ⊕ β → γ
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.hasFDerivAt_cpow : ∀ {p : ℂ × ℂ},
  p.1 ∈ Complex.slitPlane →
    HasFDerivAt (fun x => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ +
        (p.1 ^ p.2 * Complex.log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ)
      p
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.mk.injEq : ∀ (s : String.Slice) (offset : String.Pos.Raw) (hinv : offset ≤ s.rawEndPos) (s_1 : String.Slice)
  (offset_1 : String.Pos.Raw) (hinv_1 : offset_1 ≤ s_1.rawEndPos),
  ({ s := s, offset := offset, hinv := hinv } = { s := s_1, offset := offset_1, hinv := hinv_1 }) =
    (s = s_1 ∧ offset = offset_1)
-- Lean.Meta.Tactic.Clear
/-- Erase the given free variable from the goal `mvarId`.
 -/
Lean.MVarId.clear : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasEigenvalue.mem_spectrum : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasEigenvalue μ → μ ∈ spectrum R f
-- Batteries.Recycling.RBTree.Basic
/-- An auxiliary data structure (an iterator) over an `RBNode` which lazily
pulls elements from the left.
 -/
RBTree.RBNode.Stream : Type u_1 → Type u_1
-- Mathlib.Data.PNat.Xgcd
/-- `q = ap / bp`: quotient  -/
PNat.XgcdType.q : PNat.XgcdType → ℕ
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_le_centralizer_centralizer : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (s : Set A),
  NonUnitalAlgebra.adjoin R s ≤ NonUnitalSubalgebra.centralizer R ↑(NonUnitalSubalgebra.centralizer R s)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.keysArray_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → Bool},
  t.WF → (Std.TreeMap.Raw.filter (fun k x => f k) t).keysArray = Array.filter f t.keysArray
-- Mathlib.Algebra.GradedMonoid
Monoid.gMonoid_gnpow : ∀ (ι : Type u_1) {R : Type u_2} [inst : AddMonoid ι] [inst_1 : Monoid R] (n : ℕ) (x : ι) (a : R),
  GradedMonoid.GMonoid.gnpow n a = a ^ n
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSMul : {M : Type u_2} →
  {α : Type u_5} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : Monoid M] →
        [inst_2 : DistribMulAction M α] → [SMulCommClass M α α] → [IsScalarTower M α α] → SMul M (CentroidHom α)
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkXorCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkXorCached input =
    ((aig.mkGateCached input).aig.mkGateCached ((input.cast ⋯).invert true true)).aig.mkGateCached
      { lhs := ((aig.mkGateCached input).ref.cast ⋯).not,
        rhs := ((aig.mkGateCached input).aig.mkGateCached ((input.cast ⋯).invert true true)).ref.not }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.map_w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') (G : CategoryTheory.Functor C D) (j : J),
  CategoryTheory.CategoryStruct.comp (G.map f.hom) (G.map (c'.π.app j)) = G.map (c.π.app j)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.toImage_ι_assoc : ∀ {X Y : SSet} (A : X.Subcomplex) (f : X ⟶ Y) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.toImage f) (CategoryTheory.CategoryStruct.comp (A.image f).ι h) =
    CategoryTheory.CategoryStruct.comp A.ι (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.isConstructible : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} [PrespectralSpace X] [QuasiSeparatedSpace X] [CompactSpace X],
  Topology.IsLocallyConstructible s → Topology.IsConstructible s
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_norm_sum_mul_range_of_summable_norm : ∀ {R : Type u_1} [inst : NormedRing R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) → Summable fun n => ‖∑ k ∈ Finset.range (n + 1), f k * g (n - k)‖
-- Init.Data.Int.Order
Int.instTransLeLt : Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.galoisConnection : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.eq_of_le_of_under_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (P Q : Ideal S) [P.IsPrime] [Q.IsPrime], P ≤ Q → Ideal.under R P = Ideal.under R Q → P = Q
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.eqToHom_domain_lift_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {a b : 𝒳} (hab : a = b) {R : 𝒮},
  p.obj a = R → p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.eqToHom hab)
-- Mathlib.Topology.Algebra.ConstMulAction
Inseparable.const_vadd : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α] {x y : α},
  Inseparable x y → ∀ (c : M), Inseparable (c +ᵥ x) (c +ᵥ y)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.instInhabited : {K : Type u} → [inst : DivisionRing K] → Inhabited (Subfield K)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t₁ ∩ t₂).getKey! k = if k ∈ t₂ then t₁.getKey! k else default
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.ofAscListAux₁.eq_def : ∀ {α : Type u_1} (x : List α),
  Ordnode.ofAscListAux₁ x =
    match (motive := (x : List α) → ℕ → Ordnode α × { l' // l'.length ≤ x.length }) x with
    | [] => fun x => (Ordnode.nil, ⟨[], ⋯⟩)
    | x :: xs => fun s =>
      if s = 1 then (Ordnode.singleton x, ⟨xs, ⋯⟩)
      else
        match Ordnode.ofAscListAux₁ xs (s <<< 1) with
        | (t, ⟨[], property⟩) => (t, ⟨[], ⋯⟩)
        | (l, ⟨y :: ys, h⟩) =>
          have this := ⋯;
          match Ordnode.ofAscListAux₁ ys (s <<< 1) with
          | (r, ⟨zs, h'⟩) => (l.link y r, ⟨zs, ⋯⟩)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_of_ge : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, b ≤ a → ∫ (x : ℝ) in a..b, f x ∂μ = -∫ (x : ℝ) in Set.Ioc b a, f x ∂μ
-- Mathlib.Topology.Closure
isClosed_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed (closure s)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_bijective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Bijective ContinuousLinearMapWOT.toCLM
-- Lean.DocString.Types
/-- An image. `alt` should be displayed if the image can't be shown.
 -/
Lean.Doc.Inline.image : {i : Type u} → String → String → Lean.Doc.Inline i
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instHashableAuxLemmaKey : Hashable Lean.Meta.AuxLemmaKey
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instCoeSortType : CoeSort ωCPO (Type u_1)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newLocal.inj : ∀ {fvarId : Lean.FVarId} {goal : Lean.Meta.Grind.Goal} {fvarId_1 : Lean.FVarId} {goal_1 : Lean.Meta.Grind.Goal},
  Lean.Meta.Grind.IntroResult.newLocal✝ fvarId goal = Lean.Meta.Grind.IntroResult.newLocal✝ fvarId_1 goal_1 →
    fvarId = fvarId_1 ∧ goal = goal_1