mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- For technical reasons we introduce two type tags:

* `ModelProd H H'` is the same as `H × H'`;
* `ModelPi H` is the same as `∀ i, H i`, where `H : ι → Type*` and `ι` is a finite type.

In both cases the reason is the same, so we explain it only in the case of the product. A charted
space `M` with model `H` is a set of charts from `M` to `H` covering the space. Every space is
registered as a charted space over itself, using the only chart `id`, in `chartedSpaceSelf`. You
can also define a product of charted space `M` and `M'` (with model space `H × H'`) by taking the
products of the charts. Now, on `H × H'`, there are two charted space structures with model space
`H × H'` itself, the one coming from `chartedSpaceSelf`, and the one coming from the product of
the two `chartedSpaceSelf` on each component. They are equal, but not defeq (because the product
of `id` and `id` is not defeq to `id`), which is bad as we know. This expedient of renaming `H × H'`
solves this problem.  -/
LibraryNote.Manifold_type_tags : Batteries.Util.LibraryNote
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → Set.EqOn f g U → IsOpen U → MeromorphicOn g U
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.isCompact : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α), IsCompact ↑s
-- Mathlib.NumberTheory.Multiplicity
pow_two_pow_sub_pow_two_pow : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} (n : ℕ),
  x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ Finset.range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `mfderivWithin I I' f s x`, given a function `f` between two manifolds,
is the derivative of `f` at `x` within `s`,
as a continuous linear map from the tangent space at `x` to the tangent space at `f x`.  -/
mfderivWithin : {𝕜 : 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) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (f : M → M') → Set M → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (f x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF →
    (Array.find? (fun x => compare x.fst k == Ordering.eq) t.toArray = none ↔
      Std.DTreeMap.Internal.Impl.contains k t = false)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.X₁),
  (CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom) ((CategoryTheory.ConcreteCategory.hom S.toCycles) x) =
    S.moduleCatToCycles x
-- Lean.Elab.PreDefinition.Basic
/-- Applies `Meta.letToHave` to the values of defs, instances, and abbrevs.
Does not apply the transformation to values that are proofs, or to unsafe definitions.
 -/
Lean.Elab.letToHaveValue : Lean.Elab.PreDefinition → Lean.MetaM Lean.Elab.PreDefinition
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJNeZeroNF.a₁ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsCharTwoJNeZeroNF], W.a₁ = 1
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_iff_mul_rearrangement`.

---

Two functions monovary iff the rearrangement inequality holds.  -/
Monovary.mul_add_mul_le_mul_add_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Monovary f g → ∀ (i j : ι), f i * g j + f j * g i ≤ f i * g i + f j * g j
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvOfIsUnit_eq_substInv : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) (hP' : IsUnit ((PowerSeries.coeff 1) P)),
  P.substInvOfIsUnit hP' = P.substInv
-- Mathlib.Topology.Compactification.OnePoint.Sphere
/-- A homeomorphism from the one-point compactification of a finite-dimensional real vector space to
the sphere.  -/
onePointEquivSphereOfFinrankEq : {ι : Type u_1} →
  {V : Type u_2} →
    [inst : Fintype ι] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module ℝ V] →
          [FiniteDimensional ℝ V] →
            [inst_4 : TopologicalSpace V] →
              [IsTopologicalAddGroup V] →
                [ContinuousSMul ℝ V] →
                  [T2Space V] → Module.finrank ℝ V + 1 = Fintype.card ι → OnePoint V ≃ₜ ↑(Metric.sphere 0 1)
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_empty : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ¬a < b → Set.Ico a b = ∅
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord.eq_1 : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (i : ι),
  b.coord i =
    { toFun := fun q => 1 - (b.basisOf i).sumCoords (q -ᵥ b i), linear := -(b.basisOf i).sumCoords, map_vadd' := ⋯ }
-- Std.Http.Data.Method
/-- Remove a resource.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.5
 -/
Std.Http.Method.delete : Std.Http.Method
-- Init.Prelude
/-- Wraps a value to increase its type's universe level.  -/
ULift.up : {α : Type s} → α → ULift.{r, s} α
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.shuffleIt.go.eq_def : ∀ {α : Type u} (xs : Array α) (gen : StdGen) (i : ℕ),
  Std.Async.shuffleIt.go✝ xs gen i =
    if x : i < xs.size - 1 then
      match randNat gen i (xs.size - 1) with
      | (j, gen) =>
        have xs := xs.swapIfInBounds i j;
        Std.Async.shuffleIt.go✝ xs gen (i + 1)
    else (xs, gen)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.min_eq : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ → SSet.prodStdSimplex.pairingCore.min x hd = l.succ
-- Init.Data.Dyadic.Basic
Dyadic.pow_zero : ∀ (x : Dyadic), x ^ 0 = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
CategoryTheory.Pseudofunctor.ObjectProperty.map_obj_obj : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X Y : B} (f : X ⟶ Y) (X_1 : P.Obj X),
  ((P.map f).obj X_1).obj = (F.map f).toFunctor.obj X_1.obj
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.inv_hom_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f] {Z : C}
  (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) (CategoryTheory.CategoryStruct.comp f h) = h
-- Mathlib.Order.Basic
le_of_forall_ge : ∀ {α : Type u_2} [inst : Preorder α] {a b : α}, (∀ (c : α), a ≤ c → b ≤ c) → b ≤ a
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instModuleIsTorsionFree : ∀ {α : Type u_1} {R : Type u_6} {m0 : MeasurableSpace α} [inst : Semiring R] [inst_1 : Module R ENNReal]
  [inst_2 : IsScalarTower R ENNReal ENNReal] [Module.IsTorsionFree R ENNReal],
  Module.IsTorsionFree R (MeasureTheory.Measure α)
-- Lean.DocString.DeferredCheck
/-- The open declarations in scope at the reference site.  -/
Lean.Doc.DeferredCheck.openDecls : Lean.Doc.DeferredCheck → List Lean.OpenDecl
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Prokhorov theorem**: Given a sequence of compact sets `Kₙ` and a sequence `uₙ` tending to
zero, the finite measures of mass `C` giving mass at most `uₙ` to the complement of `Kₙ` form a
compact set.  -/
isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  {u : ℕ → NNReal} {K : ℕ → Set E} (C : NNReal),
  Filter.Tendsto u Filter.atTop (nhds 0) →
    (∀ (n : ℕ), IsCompact (K n)) → NormalSpace E ∨ Monotone K → IsCompact {μ | μ.mass = C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}
-- Init.SimpLemmas
Bool.or_false : ∀ (b : Bool), (b || false) = b
-- Mathlib.Order.Preorder.Chain
succChain_spec : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, (∃ t, IsChain r s ∧ SuperChain r s t) → SuperChain r s (SuccChain r s)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.symm_symm_apply : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (equiv : S.Equiv S') (a : E), equiv.symm.symm a = equiv a
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_le_apply : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Nonempty ι] [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) →
    ∀ {a b : Ordinal.{u}}, (∃ i, Ordinal.nfpFamily f a ≤ f i b) ↔ Ordinal.nfpFamily f a ≤ b
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.Config.mk.sizeOf_spec : ∀ (transparency : Lean.Meta.TransparencyMode) (occs : Lean.Meta.Occurrences)
  (castMode : Mathlib.Tactic.DepRewrite.CastMode) (castTransparency : Lean.Meta.TransparencyMode),
  sizeOf { transparency := transparency, occs := occs, castMode := castMode, castTransparency := castTransparency } =
    1 + sizeOf transparency + sizeOf occs + sizeOf castMode + sizeOf castTransparency
-- Mathlib.LinearAlgebra.Trace
/-- The trace of the identity endomorphism is the dimension of the free module.  -/
LinearMap.trace_one : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M], (LinearMap.trace R M) 1 = ↑(Module.finrank R M)
-- Mathlib.Data.Finset.Basic
Finset.subset_insert_iff_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∉ s → (s ⊆ insert a t ↔ s ⊆ t)
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.epi_of_surjective : ∀ {P : TopCat → Prop} {X Y : CompHausLike P} (f : X ⟶ Y),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.Epi f
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.neLocus_add_right : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : AddRightCancelMonoid N]
  (f g h : α →₀ N), (f + h).neLocus (g + h) = f.neLocus g
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isIso_of_subset : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y),
  ↑U ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) → CategoryTheory.IsIso (f.c.app (Opposite.op U))
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `G₀` is a commutative “group with zero”
if it is a commutative monoid with zero element (distinct from `1`)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of `0` must be `0`.  -/
CommGroupWithZero : Type u_2 → Type u_2
-- Init.Core
List.cons.injEq : ∀ {α : Type u} (head : α) (tail : List α) (head_1 : α) (tail_1 : List α),
  (head :: tail = head_1 :: tail_1) = (head = head_1 ∧ tail = tail_1)
-- Aesop.Tree.State
Aesop.Goal.isProvenByRuleApplicationNoCache : Aesop.Goal → BaseIO Bool
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_pair : ∀ {α : Type u_1} (a b : α), {a, b}.card = 2
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instPartialOrder : {α : Type u_1} → [PartialOrder α] → PartialOrder (Topology.WithUpper α)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigO_neg_right`. -/
Asymptotics.IsBigO.neg_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' → f =O[l] fun x => -g' x
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- The coercion `C(X, R)₀ → C(X, R)` bundled as a continuous linear map.  -/
ContinuousMapZero.toContinuousMapCLM : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : TopologicalSpace R] →
          [inst_3 : CommSemiring R] →
            [inst_4 : IsTopologicalSemiring R] →
              (M : Type u_3) →
                [inst_5 : Semiring M] →
                  [inst_6 : Module M R] → [inst_7 : ContinuousConstSMul M R] → ContinuousMapZero X R →L[M] C(X, R)
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncConsts.mk.injEq : ∀ (size : ℕ) (revList : List Lean.AsyncConst✝) (map : Lean.NameMap Lean.AsyncConst✝)
  (normalizedTrie : Lean.NameTrie Lean.AsyncConst✝) (size_1 : ℕ) (revList_1 : List Lean.AsyncConst✝)
  (map_1 : Lean.NameMap Lean.AsyncConst✝) (normalizedTrie_1 : Lean.NameTrie Lean.AsyncConst✝),
  ({ size := size, revList := revList, map := map, normalizedTrie := normalizedTrie } =
      { size := size_1, revList := revList_1, map := map_1, normalizedTrie := normalizedTrie_1 }) =
    (size = size_1 ∧ revList = revList_1 ∧ map = map_1 ∧ normalizedTrie = normalizedTrie_1)
-- Mathlib.Tactic.GCongr.Core
/-- Determine whether `e` contains a `gcongrHole` mdata annotation in any subexpression.
This tells `gcongr` whether to continue applying `gcongr` lemmas.  -/
Mathlib.Tactic.GCongr.containsHoleAnnotation : Lean.Expr → Bool
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_le_iff : ∀ {w : ℕ} {x : BitVec w}, BitVec.allOnes w ≤ x ↔ x = BitVec.allOnes w
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.instInhabited : Inhabited TwoP
-- Mathlib.RingTheory.PolynomialAlgebra
/-- `polyEquivTensor' R A` is the same as `polyEquivTensor R A` as a function.  -/
coe_polyEquivTensor' : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  ⇑(polyEquivTensor' R A) = ⇑(polyEquivTensor R A)
-- Mathlib.Data.Vector.MapLemmas
/-- If `f` returns the same output and next state for every value of it's first argument, then
`xs : Vector` is ignored, and we can rewrite `mapAccumr₂` into `map`.
 -/
List.Vector.mapAccumr₂_unused_input_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} {n : ℕ} {s : σ} {xs : List.Vector α n}
  {ys : List.Vector β n} (f : α → β → σ → σ × γ) (f' : β → σ → σ × γ),
  (∀ (a : α) (b : β) (s : σ), f a b s = f' b s) → List.Vector.mapAccumr₂ f xs ys s = List.Vector.mapAccumr f' ys s
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.insphere_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] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.insphere.radius = s.inradius
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- Repeated pointwise multiplication/division (not the same as pointwise repeated
multiplication/division!) of a `Set`. See note [pointwise nat action].  -/
Set.ZPow : {α : Type u_2} → [One α] → [Mul α] → [Inv α] → Pow (Set α) ℤ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {f : α → β → Bool} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filter f m)[k]? = m[k]?.pfilter fun x h' => f (m.getKey k ⋯) x
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.mk.inj : ∀ {aig : Std.Sat.AIG ℕ} {cnf : Std.Sat.CNF ℕ} {cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf}
  {inv : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf} {cnf_1 : Std.Sat.CNF ℕ} {cache_1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf_1}
  {inv_1 : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf_1},
  { cnf := cnf, cache := cache, inv := inv } = { cnf := cnf_1, cache := cache_1, inv := inv_1 } →
    cnf = cnf_1 ∧ cache ≍ cache_1
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_eq_ramificationIdx' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [IsDedekindDomain S] [q.LiesOver p] [hq : q.IsPrime],
  Ideal.map (algebraMap R S) p ≠ ⊥ → p.ramificationIdx' q = q.ramificationIdx R
-- Mathlib.Order.Disjointed
disjointed_eq_inf_compl : ∀ {α : Type u_1} {ι : Type u_2} [inst : CompleteBooleanAlgebra α] [inst_1 : Preorder ι]
  [inst_2 : LocallyFiniteOrderBot ι] (f : ι → α) (i : ι), disjointed f i = f i ⊓ ⨅ j, ⨅ (_ : j < i), (f j)ᶜ
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasDerivWithinAt.finsetProd`. -/
HasDerivWithinAt.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'}
  {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) →
    HasDerivWithinAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {a_1 b_1 c : a ⟶ b}
  (x : CategoryTheory.Bicategory.Adj.Hom₂ a_1 b_1) (y : CategoryTheory.Bicategory.Adj.Hom₂ b_1 c),
  (CategoryTheory.CategoryStruct.comp x y).τl = CategoryTheory.CategoryStruct.comp x.τl y.τl
-- Mathlib.Algebra.Notation.Support
Function.support_update_eq_ite : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] [inst_1 : DecidableEq ι] [inst_2 : DecidableEq M] (f : ι → M) (x : ι)
  (y : M),
  Function.support (Function.update f x y) = if y = 0 then Function.support f \ {x} else insert x (Function.support f)
-- Mathlib.Computability.Ackermann
ack_injective_right : ∀ (m : ℕ), Function.Injective (ack m)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (elts : Array (Array (Array α))), sizeOf { elts := elts } = 1 + sizeOf elts
-- Mathlib.Algebra.Group.Units.Equiv
MulEquiv.inv_apply : ∀ (G : Type u_6) [inst : DivisionCommMonoid G] (a : G), (MulEquiv.inv G) a = a⁻¹
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.Struct.subFn : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_neg : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖-f‖₊ = ‖f‖₊
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonFileEvent.toJson : Lean.Lsp.FileEvent → Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) =
    CategoryTheory.AddMonObj.zero
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent : {R : Type u_3} →
  {S : Type u_4} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R₀ : Type u_1} →
              [inst_3 : CommRing R₀] →
                [inst_4 : Algebra R₀ S] →
                  [inst_5 : Module R₀ P.Cotangent] → [IsScalarTower R₀ S P.Cotangent] → Module R₀ P.H1Cotangent
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.fun_comp_of_injective : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {β : Type u_3} {f : β → M} {g : α → β},
  Function.Injective g → Function.HasFiniteMulSupport f → Function.HasFiniteMulSupport fun a => f (g a)
-- Mathlib.Data.Num.ZNum
Num.toZNum.eq_2 : ∀ (p : PosNum), (Num.pos p).toZNum = ZNum.pos p
-- Init.Data.Int.Order
Int.neg_of_sign_eq_neg_one : ∀ {a : ℤ}, a.sign = -1 → a < 0
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- Auxiliary definition for `MeasureTheory.Measure.condKernel` and
`ProbabilityTheory.Kernel.condKernel`.
A conditional kernel for `κ : Kernel Unit (α × Ω)` where `Ω` is standard Borel.  -/
ProbabilityTheory.Kernel.condKernelUnitBorel : {α : Type u_1} →
  {Ω : Type u_4} →
    {mα : MeasurableSpace α} →
      {mΩ : MeasurableSpace Ω} →
        [StandardBorelSpace Ω] →
          [Nonempty Ω] →
            (κ : ProbabilityTheory.Kernel Unit (α × Ω)) →
              [ProbabilityTheory.IsFiniteKernel κ] → ProbabilityTheory.Kernel (Unit × α) Ω
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit' : Lean.Expr → Bool → Lean.Elab.Command.NameGen.MkNameM✝ String
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.parallelComp_comp_prod : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} {κ : ProbabilityTheory.Kernel X Y} {Y' : Type u_6} {Z' : Type u_7} {mY' : MeasurableSpace Y'}
  {mZ' : MeasurableSpace Z'} [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel Y Z}
  [ProbabilityTheory.IsSFiniteKernel η] {κ' : ProbabilityTheory.Kernel X Y'} [ProbabilityTheory.IsSFiniteKernel κ']
  {η' : ProbabilityTheory.Kernel Y' Z'} [ProbabilityTheory.IsSFiniteKernel η'],
  (η.parallelComp η').comp (κ.prod κ') = (η.comp κ).prod (η'.comp κ')
-- Mathlib.Algebra.Order.Hom.Ring
/-- Any type satisfying `OrderRingHomClass` can be cast into `OrderRingHom` via
`OrderRingHomClass.toOrderRingHom`.  -/
instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : NonAssocSemiring α] →
          [inst_2 : Preorder α] →
            [inst_3 : NonAssocSemiring β] →
              [inst_4 : Preorder β] → [OrderHomClass F α β] → [RingHomClass F α β] → CoeTC F (α →+*o β)
-- Init.Data.Int.Linear
/-- Similar to `Poly.denote`, but produces a denotation better for `simp +arith`.
Remark: we used to convert `Poly` back into `Expr` to achieve that.
 -/
Int.Internal.Linear.Poly.denote' : Int.Internal.Linear.Context → Int.Internal.Linear.Poly → ℤ
-- Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Ideal.Quotient.isUnit_mk_pow_of_notMem : ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S) [I.IsMaximal] {n : ℕ} {x : S},
  x ∉ I → IsUnit ((Ideal.Quotient.mk (I ^ n)) x)
-- Mathlib.RingTheory.RamificationInertia.Inertia
Ideal.natAbs_pow_inertiaDeg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R] [Module.Finite ℤ R]
  (p : ℤ) (P : Ideal R) [P.IsPrime] [P.LiesOver (Ideal.span {p})], p.natAbs ^ P.inertiaDeg ℤ = Ideal.absNorm P
-- Mathlib.Data.Finset.Dedup
Finset.mem_toList : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ s.toList ↔ a ∈ s
-- Mathlib.Order.Filter.IsBounded
Filter.bddAbove_range_of_tendsto_atTop_atBot : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [IsDirectedOrder α] {u : ℕ → α},
  Filter.Tendsto u Filter.atTop Filter.atBot → BddAbove (Set.range u)
-- Mathlib.Data.Finsupp.Ext
/-- If two additive homomorphisms from `α →₀ M` are equal on each `single a b`,
then they are equal.  -/
Finsupp.addHom_ext : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] ⦃f g : (α →₀ M) →+ N⦄,
  (∀ (x : α) (y : M), (f fun₀ | x => y) = g fun₀ | x => y) → f = g