mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
/-- `sigma l₁ l₂` is the list of dependent pairs `(a, b)` where `a ∈ l₁` and `b ∈ l₂ a`.
```
sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]
```  -/
List.sigma : {α : Type u_1} → {σ : α → Type u_2} → List α → ((a : α) → List (σ a)) → List ((a : α) × σ a)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.mk.sizeOf_spec : ∀ {K : Type u_1} [inst : SizeOf K] (b : ℤ) (fr : K), sizeOf { b := b, fr := fr } = 1 + sizeOf b + sizeOf fr
-- Mathlib.Order.Defs.LinearOrder
instLawfulBCmpCompare_mathlib : ∀ {α : Type u_1} [inst : LinearOrder α], Std.LawfulBCmp compare
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.topologicalClosure_mono : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [inst_2 : IsSemitopologicalSemiring R]
  {s t : NonUnitalSubsemiring R}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Init.Data.List.Nat.Modify
List.length_modifyHead : ∀ {α : Type u_1} {f : α → α} {l : List α}, (List.modifyHead f l).length = l.length
-- Mathlib.Analysis.LocallyConvex.Basic
/-- **Alias** of the forward direction of `absorbs_iff_eventually_nhdsNE_zero`. -/
Absorbs.eventually_nhdsNE_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s t : Set E}, Absorbs 𝕜 s t → ∀ᶠ (c : 𝕜) in nhdsWithin 0 {0}ᶜ, Set.MapsTo (fun x => c • x) t s
-- Init.Data.Array.Lemmas
Array.back?_eq_none_iff : ∀ {α : Type u_1} {xs : Array α}, xs.back? = none ↔ xs = #[]
-- Mathlib.Data.Num.Bitwise
Num.lor_eq_or : ∀ (p q : Num), p.lor q = p ||| q
-- Init.Data.SInt.Lemmas
Int32.toBitVec_inj : ∀ {a b : Int32}, a.toBitVec = b.toBitVec ↔ a = b
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionResultCore.subgoal.injEq : ∀ (mvarId : Lean.MVarId) (numNewEqs : ℕ) (mvarId_1 : Lean.MVarId) (numNewEqs_1 : ℕ),
  (Lean.Meta.InjectionResultCore.subgoal mvarId numNewEqs =
      Lean.Meta.InjectionResultCore.subgoal mvarId_1 numNewEqs_1) =
    (mvarId = mvarId_1 ∧ numNewEqs = numNewEqs_1)
-- Mathlib.Topology.Sets.Compacts
/-- Reinterpret a compact open as a clopen.  -/
TopologicalSpace.CompactOpens.toClopens : {α : Type u_1} →
  [inst : TopologicalSpace α] → [T2Space α] → TopologicalSpace.CompactOpens α → TopologicalSpace.Clopens α
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_algebraMap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (r : R),
  (CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r)) d = 0
-- Init.Data.BitVec.Bootstrap
BitVec.setWidth'.congr_simp : ∀ {n w : ℕ} (le : n ≤ w) (x x_1 : BitVec n), x = x_1 → BitVec.setWidth' le x = BitVec.setWidth' le x_1
-- Mathlib.Data.Real.Basic
Real.instInv : Inv ℝ
-- Mathlib.Data.Nat.Nth
Nat.lt_of_nth_lt_nth_of_lt_card : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {m n : ℕ}, Nat.nth p m < Nat.nth p n → m < hf.toFinset.card → m < n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ}, (Std.ExtTreeMap.filterMap f t).size ≤ t.size
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousLinearMap.curry_uncurryLeft : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G),
  f.uncurryLeft.curryLeft = f
-- Lean.Parser.Term
Lean.Parser.Term.pipeCompletion.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Path
Path.truncate_zero_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b), γ.truncate 0 1 = γ.cast ⋯ ⋯
-- Lean.Meta.Tactic.Rfl
/-- `MetaM` version of the `rfl` tactic.

This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, equality or another relation which has a reflexive lemma tagged with the
attribute [refl].
 -/
Lean.MVarId.applyRfl : Lean.MVarId → Lean.MetaM Unit
-- Mathlib.Topology.Instances.CantorSet
cantorSequence_get_succ : ∀ (x : ℝ) (n : ℕ),
  (cantorSequence x).get (n + 1) = 3 * ((cantorSequence x).get n - 3 ^ n * Real.ofDigitsTerm (cantorToTernary x).get n)
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_smul_comp : ∀ {E : Type u_2} {mE : MeasurableSpace E} [inst : SeminormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  {X : Type u_3} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} [BorelSpace E] {f : X → E},
  AEMeasurable f μ →
    ∀ (r : ℝ) (t : E),
      MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => r • f x) μ) t =
        MeasureTheory.charFun (MeasureTheory.Measure.map f μ) (r • t)
-- Mathlib.Tactic.NormNum.LegendreSymbol
Mathlib.Meta.NormNum.isInt_jacobiSym : ∀ {a na : ℤ} {b nb : ℕ} {r : ℤ},
  Mathlib.Meta.NormNum.IsInt a na →
    Mathlib.Meta.NormNum.IsNat b nb → jacobiSym na nb = r → Mathlib.Meta.NormNum.IsInt (jacobiSym a b) r
-- Mathlib.Algebra.Quandle
Rack.toEnvelGroup.mapAux.eq_1 : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G)),
  Rack.toEnvelGroup.mapAux f Rack.PreEnvelGroup.unit = 1
-- Init.Data.Option.Basic
Option.getDM_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Pure m] (a : α) (y : m α), (some a).getDM y = pure a
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.mem_antidiagonalTuple : ∀ {n k : ℕ} {x : Fin k → ℕ}, x ∈ Finset.Nat.antidiagonalTuple k n ↔ ∑ i, x i = n
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.coe_comp : ∀ {X Y Z : AddGrpCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
eq_div_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c : G₀}, b ≠ 0 → (c = a / b ↔ c * b = a)
-- Mathlib.Analysis.Convex.Topology
Convex.interior_closure_eq_interior_of_nonempty_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [inst_7 : TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → (interior s).Nonempty → interior (closure s) = interior s
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkLeft_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (ca : γ × α),
  (ProbabilityTheory.Kernel.prodMkLeft γ κ) ca = κ ca.2
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.infinitesimal_sub : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → (x - ↑r).Infinitesimal
-- Mathlib.Logic.UnivLE
/-- This is the crucial instance that subsumes `univLE_max`.  -/
univLE_of_max : ∀ [UnivLE.{max u v, v}], UnivLE.{u, v}
-- Lean.PrettyPrinter.Parenthesizer
/-- Registers a parenthesizer for a parser.

`@[parenthesizer k]` registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` to be used
for parenthesizing syntax of kind `k`.
 -/
Lean.PrettyPrinter.parenthesizerAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Prod
Set.offDiag_inter : ∀ {α : Type u_1} (s t : Set α), (s ∩ t).offDiag = s.offDiag ∩ t.offDiag
-- Mathlib.Order.BoundedOrder.Basic
Prod.snd_top : ∀ (α : Type u) (β : Type v) [inst : Top α] [inst_1 : Top β], ⊤.2 = ⊤
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderiv 𝕜 (f x) (g x) (k x)` is smooth.  -/
ContDiff.fderiv_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {m n : WithTop ℕ∞} {f : E → F → G} {g k : E → F},
  ContDiff 𝕜 m (Function.uncurry f) →
    ContDiff 𝕜 n g → ContDiff 𝕜 n k → n + 1 ≤ m → ContDiff 𝕜 n fun x => (fderiv 𝕜 (f x) (g x)) (k x)
-- Std.Sync.CancellationToken
/-- The central state structure for a `CancellationToken`.
 -/
Std.CancellationToken.State : Type
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map₂IdIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor C D} (T : D) (α : T ⟶ (CategoryTheory.Functor.id D).obj T)
  (β : R.comp (CategoryTheory.Functor.id D) ⟶ (CategoryTheory.Functor.id C).comp R)
  (hα : autoParam (α = CategoryTheory.CategoryStruct.id T) CategoryTheory.StructuredArrow.map₂IdIso._auto_1)
  (hβ :
    autoParam (β = CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
      CategoryTheory.StructuredArrow.map₂IdIso._auto_3)
  (X : CategoryTheory.StructuredArrow T R),
  ((CategoryTheory.StructuredArrow.map₂IdIso T α β hα hβ).hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.mulI_inf : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H] (S T : ClosedSubmodule ℝ H),
  (S ⊓ T).mulI = S.mulI ⊓ T.mulI
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_orElse_EStateM_apply_eq : ∀ {ε σ α : Type} {post : α → σ → Prop} {epost : ε → σ → Prop} (x : EStateM ε σ α) (h : Unit → EStateM ε σ α),
  Std.Internal.Do.wp (OrElse.orElse x h) post epost = fun s =>
    Std.Internal.Do.wp x post (fun x s' => Std.Internal.Do.wp (h ()) post epost s') s
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_zero : ∀ (x : ℝ), x ^ 0 = 1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable : ∀ {α : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {p : ENNReal} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ↥(MeasureTheory.Lp F p μ)},
  f ∈ MeasureTheory.lpMeas F 𝕜 m p μ ↔ MeasureTheory.AEStronglyMeasurable (↑↑f) μ
-- Std.Do.SPred.Laws
Std.Do.SPred.entails.eq_2 : ∀ (σ : Type u) (tail : List (Type u)) (P_2 Q_2 : Std.Do.SPred (σ :: tail)), (P_2 ⊢ₛ Q_2) = ∀ (s : σ), P_2 s ⊢ₛ Q_2 s
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Returns `true` if `declName` is the name of a `match`-expression congruence equation.  -/
Lean.Meta.Grind.isMatchCongrEqDeclName : Lean.Name → Lean.CoreM Bool
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- To construct a morphism between right lifts, we need a 2-morphism between the lifts,
and to check that it is compatible with the counits.  -/
CategoryTheory.Bicategory.RightLift.homMk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.RightLift f g} →
            (η : s.lift ⟶ t.lift) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η f) t.counit = s.counit)
                  CategoryTheory.Bicategory.RightLift.homMk._auto_1 →
                (s ⟶ t)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If `f : X → Z` is a surjective Borel measurable map from a standard Borel space
to a countably separated measurable space, then the preimage of a set `s`
is measurable if and only if the set is measurable.
One implication is the definition of measurability, the other one heavily relies on `X` being a
standard Borel space.  -/
Measurable.measurableSet_preimage_iff_of_surjective : ∀ {X : Type u_3} {Z : Type u_5} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : MeasurableSpace Z]
  [MeasurableSpace.CountablySeparated Z] {f : X → Z},
  Measurable f → Function.Surjective f → ∀ {s : Set Z}, MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise_le_piecewise : ∀ {ι : Type u_1} (s : Finset ι) [inst : (j : ι) → Decidable (j ∈ s)] {π : ι → Type u_3} {f g f' g' : (i : ι) → π i}
  [inst_1 : (i : ι) → Preorder (π i)], f ≤ f' → g ≤ g' → s.piecewise f g ≤ s.piecewise f' g'
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.toMulLeftReflectLT : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α], MulLeftReflectLT α
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.instMax : {α : Type u_1} → [inst : CommMonoidWithZero α] → [UniqueFactorizationMonoid α] → Max (Associates α)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The natural transformation `K.homologyι i : K.homology i ⟶ K.opcycles i`
for all `K : HomologicalComplex C c`.  -/
HomologicalComplex.natTransHomologyι : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          (i : ι) →
            [inst_2 : CategoryTheory.CategoryWithHomology C] →
              HomologicalComplex.homologyFunctor C c i ⟶ HomologicalComplex.opcyclesFunctor C c i
-- Lean.Elab.Binders
Lean.Elab.Term.elabHaveDecl : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.coe_single : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (i : I),
  ⇑(AddMonoidHom.single f i) = Pi.single i
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerMVarErrorHoleInfo : Lean.MVarId → Lean.Syntax → Lean.Elab.TermElabM Unit
-- Lean.Parser.Command
/-- Mark a syntax kind as deprecated. When this syntax is elaborated, a warning will be emitted.

```
deprecated_syntax Lean.Parser.Term.let_fun "use `have` instead" (since := "2026-03-18")
```
 -/
Lean.Parser.Command.deprecatedSyntax : Lean.Parser.Parser
-- Mathlib.RingTheory.ClassGroup.Basic
instCommGroupClassGroup : (R : Type u_1) → [inst : CommRing R] → [inst_1 : IsDomain R] → CommGroup (ClassGroup R)
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.diag 1 = 1
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_eq_toBitVec : ∀ (a : USize) (h : System.Platform.numBits = 32), a.toBitVec32 h = BitVec.cast h a.toBitVec
-- Mathlib.LinearAlgebra.Prod
/-- Product of linear equivalences; the maps come from `Equiv.prodCongr`.  -/
LinearEquiv.prodCongr : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        {M₄ : Type z} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid M₄] →
                    {module_M : Module R M} →
                      {module_M₂ : Module R M₂} →
                        {module_M₃ : Module R M₃} →
                          {module_M₄ : Module R M₄} → (M ≃ₗ[R] M₂) → (M₃ ≃ₗ[R] M₄) → (M × M₃) ≃ₗ[R] M₂ × M₄
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_one : ∀ {α : Type u_2} [inst : AddMonoidWithOne α], WithTop.untop₀ 1 = 1
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_one' : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  uniformity G = Filter.comap (fun p => p.2 * p.1⁻¹) (nhds 1)
-- Mathlib.GroupTheory.FreeGroup.GeneratorEquiv
/-- Isomorphic free abelian groups (as modules) have equivalent bases.  -/
Equiv.ofFreeAbelianGroupLinearEquiv : {α : Type u_1} → {β : Type u_2} → (FreeAbelianGroup α ≃ₗ[ℤ] FreeAbelianGroup β) → α ≃ β
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasProd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (a : α)
  (L : SummationFilter β), HasProd f a L = Filter.Tendsto (fun s => ∏ b ∈ s, f b) L.filter (nhds a)
-- Mathlib.Topology.Closure
/-- **Alias** of `closure_sdiff_interior`. -/
closure_diff_interior : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), closure s \ interior s = frontier s
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inl_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (i : A), (ContinuousMonoidHom.inl A B) i = (i, 1)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.ofHom_apply : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y] (f : X →ₙ* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (MagmaCat.ofHom f)) x = f x
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ι_mapBifunctorComp₂₃MapObjIso_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃]
  [inst_7 :
    ((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj
          X₃).HasMap
      r]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) =
    CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_congr_enorm_ae : ∀ {α : Type u_1} {ε : Type u_2} {ε' : Type u_3} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ) → MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.unop_Y' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.RightFraction X Y), φ.unop.Y' = Opposite.unop φ.X'
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.restrict_rankFinite : ∀ {α : Type u_1} {M : Matroid α} [M.RankFinite] (R : Set α), (M.restrict R).RankFinite
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instRing : {q : ℕ} → Ring (LucasLehmer.X q)
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_zero : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : Zero X], Metric.ediam 0 = 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.id_indexEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (a : ι),
  (RootPairing.Hom.id P).indexEquiv a = a
-- Mathlib.Computability.DFA
DFA.union_start : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2), (M1.union M2).start = (M1.start, M2.start)
-- Mathlib.Topology.Inseparable
SeparationQuotient.map_mk_nhdsWithin_preimage : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set (SeparationQuotient X)) (x : X),
  Filter.map SeparationQuotient.mk (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) = nhdsWithin (SeparationQuotient.mk x) s
-- Mathlib.Analysis.Analytic.IteratedFDeriv
ContDiffAt.domDomCongr_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E},
  ContDiffAt 𝕜 ⊤ f x →
    ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)),
      ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x) = iteratedFDeriv 𝕜 n f x
-- Mathlib.Algebra.Order.Field.Basic
div_pos_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.RingTheory.Etale.StandardEtale
/-- The `Algebra.SubmersivePresentation` associated to a standard etale presentation.  -/
StandardEtalePresentation.toSubmersivePresentation : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → StandardEtalePresentation R S → Algebra.SubmersivePresentation R S (Fin 2) (Fin 2)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
AlgebraicGeometry.PresheafedSpace.colimitCocone : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) → CategoryTheory.Limits.Cocone F
-- Mathlib.Topology.Algebra.Support
/-- The submonoid of functions `α → β` with compact multiplicative support.  -/
HasCompactMulSupport.submonoid : (α : Type u_2) → (β : Type u_4) → [TopologicalSpace α] → [inst : MulOneClass β] → Submonoid (α → β)
-- Init.Data.Array.Basic
Array.size_eq_length_toList : ∀ {α : Type u} {xs : Array α}, xs.size = xs.toList.length
-- Std.Http.Protocol.H1
/-- Reconciles explicit machine framing (`knownSize`) with user-provided framing
headers from `send` and rejects contradictory inputs.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.reconcileOutgoingFraming : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Option Std.Http.Body.Length → Bool → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Order.LiminfLimsup
Filter.liminf_le_liminf : ∀ {β : Type u_2} {α : Type u_6} [inst : ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β},
  (∀ᶠ (a : α) in f, u a ≤ v a) →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) Filter.liminf_le_liminf._auto_1 →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) Filter.liminf_le_liminf._auto_3 →
        Filter.liminf u f ≤ Filter.liminf v f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k fallback : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).getD fallback
-- Mathlib.RingTheory.Binomial
Ring.factorial_nsmul_multichoose_eq_ascPochhammer : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R) (n : ℕ),
  n.factorial • Ring.multichoose r n = (ascPochhammer ℕ n).smeval r