mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- Integrating `f` against `partialTraj κ a b x` is the same as integrating only over the variables
from `x_{a+1}` to `x_b`.  -/
ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] {f : ((n : ℕ) → X n) → ENNReal},
  Measurable f →
    ∀ (x₀ : (n : ℕ) → X n),
      ProbabilityTheory.Kernel.lmarginalPartialTraj κ a b f x₀ =
        ∫⁻ (x : (i : ↥(Finset.Ioc a b)) → X ↑i),
          f
            (Function.updateFinset x₀ (Finset.Ioc a b)
              x) ∂((ProbabilityTheory.Kernel.partialTraj κ a b).map (Finset.restrict₂ ⋯)) (Preorder.frestrictLe a x₀)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_triangle_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x y ≤ nndist x z + nndist y z
-- Init.Data.Array.Lemmas
Array.self_eq_append_right : ∀ {α : Type u_1} {xs ys : Array α}, xs = xs ++ ys ↔ ys = #[]
-- Mathlib.RingTheory.IdealFilter.Topology
/-- Type synonym for a ring that depends on a choice of ideal filter. We use this to assign a
topology generated by the ideal filter.  -/
WithIdealFilter : {A : Type u_1} → [inst : Ring A] → IdealFilter A → Type u_1
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The `i`-th generator of the kernel `(b₁, ..., bᵣ)` of the naive presentation of `T`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.kerGen : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    σ → ↥(Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.ker
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural_right : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] {X Y : C} (X' : C) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
      (CategoryTheory.Functor.LaxMonoidal.μ F X' Y) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X' X)
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.le_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α} (hc : k ∈ t),
  t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Probability.HasLawExists
ProbabilityTheory.exists_hasLaw_indepFun : ∀ {ι : Type v} (𝓧 : ι → Type u) {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} (μ : (i : ι) → MeasureTheory.Measure (𝓧 i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  ∃ Ω x P X,
    (∀ (i : ι), Measurable (X i)) ∧
      (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) ∧
        ProbabilityTheory.iIndepFun X P ∧ MeasureTheory.IsProbabilityMeasure P
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_2 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.infinity s with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_2 s
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Turn an element of a type `F` satisfying `CoalgHomClass F R A B` into an actual
`CoalgHom`. This is declared as the default coercion from `F` to `A →ₗc[R] B`.  -/
CoalgHomClass.toCoalgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {F : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : Module R A] →
              [inst_3 : AddCommMonoid B] →
                [inst_4 : Module R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] → [inst_7 : FunLike F A B] → [CoalgHomClass F R A B] → F → A →ₗc[R] B
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2.eq_1 : ∀ {α : Type u_1} (E : Type u_2) (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0), MeasureTheory.condExpL2 E 𝕜 hm = (MeasureTheory.lpMeas E 𝕜 m 2 μ).orthogonalProjectionOnto
-- Init.Data.Array.Find
Array.findIdx_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.findIdx p #[] = 0
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.le_normalizer_of_normal : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.Normal], K ≤ Subgroup.normalizer ↑H
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N),
  TensorProduct.dualDistrib R M N ∘ₗ TensorProduct.dualDistribInvOfBasis b c = LinearMap.id
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_add_eq_right : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  AddMonoidAlgebra.supDegree D p < AddMonoidAlgebra.supDegree D q →
    AddMonoidAlgebra.supDegree D (p + q) = AddMonoidAlgebra.supDegree D q
-- Mathlib.Analysis.RCLike.Basic
RCLike.le_iff_re_im : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] {z w : K},
  z ≤ w ↔ RCLike.re z ≤ RCLike.re w ∧ RCLike.im z = RCLike.im w
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ),
  CategoryTheory.NatIso.unop (CategoryTheory.Iso.refl F) = CategoryTheory.Iso.refl F.unop
-- Aesop.Index
Aesop.instInhabitedIndex : {a : Type} → Inhabited (Aesop.Index a)
-- Mathlib.Order.Hom.Order
OrderHom.coe_iInf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {ι : Sort u_3} [inst_1 : CompleteLattice β] (f : ι → α →o β),
  ⇑(⨅ i, f i) = ⨅ i, ⇑(f i)
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the keys of a dependent hash map.
The iterator yields the keys in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.Raw.keysIter : {α : Type u} → {β : α → Type u} → Std.DHashMap.Raw α β → Std.Iter α
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedOrderHom β γ)
  (g : BoundedOrderHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- A submodule `S` of a module `M` is co-finitely generated (CoFG) if the quotient
space `M ⧸ S` is finitely generated.  -/
Submodule.CoFG : {R : Type u_1} →
  [inst : Ring R] → {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → Prop
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuousOn.upperHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  {s : Set α}, UpperHemicontinuousOn f s → x ∈ s → UpperHemicontinuousWithinAt f s x
-- Mathlib.Algebra.Order.Floor.Defs
_private.Mathlib.Algebra.Order.Floor.Defs.0.floorAux : {α : Type u_4} →
  [inst : Ring α] →
    [inst_1 : PartialOrder α] →
      [IsOrderedRing α] →
        [Nontrivial α] → {x : α} → (∃ n, ↑n ≤ x) → (∃ n, x ≤ ↑n) → { n // ↑n ≤ x ∧ ∀ (m : ℤ), ↑m ≤ x → m ≤ n }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_one_lt_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightStrictMono α] {a b c : α},
  1 < a → b < c → b < a * c
-- Mathlib.CategoryTheory.ObjectProperty.Shift
/-- `P : ObjectProperty C` is stable under the shift by `a : A` if
`P X` implies `P X⟦a⟧`.  -/
CategoryTheory.ObjectProperty.IsStableUnderShiftBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → {A : Type u_2} → [inst_1 : AddMonoid A] → [CategoryTheory.HasShift C A] → A → Prop
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_zero : ∀ {α : Type u_1} [inst : Zero α], ofColex 0 = 0
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.homEquiv_ofNatIsoLeft_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D C} (adj : F ⊣ H) (iso : F ≅ G) {X : C} {Y : D}
  (f : X ⟶ H.obj Y),
  ((adj.ofNatIsoLeft iso).homEquiv X Y).symm f =
    CategoryTheory.CategoryStruct.comp (iso.inv.app X) ((adj.homEquiv X Y).symm f)
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_iff_comp_right : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i]
  [inst_4 : ∀ (i : ι), M.HasHomology i] [hφ' : QuasiIso φ'],
  QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔ QuasiIso φ
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toMax : {α : Type u} → [self : Std.LinearOrderPackage α] → Max α
-- Mathlib.Algebra.Colimit.Module
/-- The canonical map from a component to the direct limit.  -/
AddCommGroup.DirectLimit.of : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        (f : (i j : ι) → i ≤ j → G i →+ G j) → [inst_2 : DecidableEq ι] → (i : ι) → G i →+ AddCommGroup.DirectLimit G f
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Iic : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderBot α]
  (a : Subtype p),
  (∀ ⦃a x : α⦄, x ≤ a → p a → p x) → Finset.map (Function.Embedding.subtype p) (Finset.Iic a) = Finset.Iic ↑a
-- Mathlib.Data.Nat.Cast.Basic
eq_natCast : ∀ {R : Type u_3} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : FunLike F ℕ R] [RingHomClass F ℕ R] (f : F)
  (n : ℕ), f n = ↑n
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_assoc : ∀ {B : Type u} [inst : Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  {g g' : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ g g')
  (h : CategoryTheory.FreeBicategory.Hom c d),
  CategoryTheory.FreeBicategory.Rel
    (CategoryTheory.FreeBicategory.Hom₂.whisker_right h (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η))
    ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp
      ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η)).vcomp
        (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g' h)))
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.coe_ofConeComb : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : Set E) (nonempty : C.Nonempty)
  (coneComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a : R), 0 ≤ a → ∀ (b : R), 0 ≤ b → a • x + b • y ∈ C),
  ↑(PointedCone.ofConeComb C nonempty coneComb) = C
-- Std.Do.WP.SimpLemmas
Std.Do.WP.get_MonadStateOf : ∀ {m : Type u → Type v} {σ : Type u} {n : Type u → Type u_1} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond σ ps}
  [inst : MonadStateOf σ m] [inst_1 : MonadLift m n] [inst_2 : Std.Do.WP n ps],
  (Std.Do.wp MonadStateOf.get).apply Q = (Std.Do.wp (MonadLift.monadLift MonadStateOf.get)).apply Q
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_intCast : ∀ {R : Type u} [inst : Ring R] (z : ℤ), (↑z).toFinsupp = ↑z
-- Mathlib.Computability.StateTransition
StateTransition.frespects_eq : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} {a₂ b₂ : σ₂},
  f₂ a₂ = f₂ b₂ → ∀ {b₁ : Option σ₁}, StateTransition.FRespects f₂ tr a₂ b₁ ↔ StateTransition.FRespects f₂ tr b₂ b₁
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_refl : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinForm.congr (LinearEquiv.refl R M) = LinearEquiv.refl R (LinearMap.BilinForm R M)
-- Lean.Declaration
Lean.instInhabitedDefinitionVal : Inhabited Lean.DefinitionVal
-- Mathlib.SetTheory.Ordinal.Basic
WellOrder.mk.injEq : ∀ (α : Type u) (r : α → α → Prop) (wo : IsWellOrder α r) (α_1 : Type u) (r_1 : α_1 → α_1 → Prop)
  (wo_1 : IsWellOrder α_1 r_1),
  ({ α := α, r := r, wo := wo } = { α := α_1, r := r_1, wo := wo_1 }) = (α = α_1 ∧ r ≍ r_1)
-- Init.Data.SInt.Basic
/-- Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on
overflow.

Examples:
 * `Nat.toInt16 127 = 127`
 * `Nat.toInt16 32767 = 32767`
 * `Nat.toInt16 32768 = -32768`
 * `Nat.toInt16 32770 = -32766`
 -/
Nat.toInt16 : ℕ → Int16
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_mul_cancel_left : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' (↑y * x) y = f x
-- Mathlib.Data.Set.Finite.Lattice
iSup_iInf_eq_of_finite : ∀ {α : Type u} {ι : Sort v} {κ : ι → Sort w} [inst : Order.Coframe α] [Finite ι] {f : (a : ι) → κ a → α},
  ⨆ a, ⨅ b, f a b = ⨅ g, ⨆ a, f a (g a)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augmentOfIsInitial_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsInitial T) (x : SimplexCategory), (X.augmentOfIsInitial hT).hom.app x = hT.to (X.obj x)
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.empty : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)},
  Std.Sat.AIG.RelabelNat.State.Inv2 decls 0 ∅
-- Mathlib.Data.Int.Init
/-- **Alias** of `Int.leInduction`.

---

See `Int.inductionOn'` for an induction in both directions.  -/
Int.le_induction : {m : ℤ} →
  {motive : (n : ℤ) → m ≤ n → Sort u_1} →
    motive m ⋯ → ((n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯) → (n : ℤ) → (hmn : m ≤ n) → motive n hmn
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
Echelon.Decomposition.isPivotedBy : ∀ {m : Type u_1} [inst : Fintype m] [inst_1 : LinearOrder m] {n : Type u_2} [inst_2 : LinearOrder n] {R : Type u_3}
  [inst_3 : CommRing R] {A : Matrix m n R} (self : Echelon.Decomposition A),
  (self.L * A.submatrix (⇑self.σ) id).IsPivotedBy self.pivot
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittSub.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], WittVector.wittSub p = wittStructureInt p (MvPolynomial.X 0 - MvPolynomial.X 1)
-- Qq.MetaM
/-- The result of `Qq.isDefEqQ`; `MaybeDefEq a b` is an optional version of `$a =Q $b`.  -/
Qq.MaybeDefEq : {u : Lean.Level} →
  {α :
      let u := u;
      Q(Sort u)} →
    Q(«$α») → Q(«$α») → Type
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (app : (a : B) → η.app a ⟶ θ.app a) →
              autoParam
                  (∀ {a b : B} (f : a ⟶ b),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
                        (θ.naturality f) =
                      CategoryTheory.CategoryStruct.comp (η.naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
                  CategoryTheory.Lax.OplaxTrans.Modification.naturality._autoParam →
                CategoryTheory.Lax.OplaxTrans.Modification η θ
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.infsep_zero_iff_subsingleton : ∀ {α : Type u_1} [inst : MetricSpace α] {s : Set α}, s.Finite → (s.infsep = 0 ↔ s.Subsingleton)
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNatLT : ∀ {n : ℕ} (h : n < UInt16.size), (UInt16.ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.isBlock_iff_disjoint_vadd_of_ne : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B ↔ ∀ ⦃g : G⦄, g +ᵥ B ≠ B → Disjoint (g +ᵥ B) B
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.sproj.injEq : ∀ (n offset : ℕ) (x : Lean.IR.VarId) (n_1 offset_1 : ℕ) (x_1 : Lean.IR.VarId),
  (Lean.IR.Expr.sproj n offset x = Lean.IR.Expr.sproj n_1 offset_1 x_1) = (n = n_1 ∧ offset = offset_1 ∧ x = x_1)
-- Mathlib.Topology.LocallyFinite
LocallyFinite.eventually_subset : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {s : ι → Set X},
  LocallyFinite s → (∀ (i : ι), IsClosed (s i)) → ∀ (x : X), ∀ᶠ (y : X) in nhds x, {i | y ∈ s i} ⊆ {i | x ∈ s i}
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_self_of_notMem`. -/
Set.insert_diff_self_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → insert a s \ {a} = s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabelPart.location? : Lean.Lsp.InlayHintLabelPart → Option Lean.Lsp.Location
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute : Type
-- Aesop.Options.Public
/-- If Aesop proves a goal and this option is `true`, Aesop prints a tactic proof
as a `Try this:` suggestion.
 -/
Aesop.Options.traceScript : Aesop.Options → Bool
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.encard_vadd_set : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] (a : G) (s : Set α),
  (a +ᵥ s).encard = s.encard
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.OptionT.bind.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Batteries.Control.AlternativeMonad
StateRefT'.instAlternativeMonad : {m : Type → Type} → {ω σ : Type} → [AlternativeMonad m] → AlternativeMonad (StateRefT' ω σ m)
-- Mathlib.Topology.UniformSpace.Defs
/-- Construct a `UniformSpace` from a `u : UniformSpace.Core` and a `TopologicalSpace` structure
that is equal to `u.toTopologicalSpace`.  -/
UniformSpace.ofCoreEq : {α : Type u} → (u : UniformSpace.Core α) → (t : TopologicalSpace α) → t = u.toTopologicalSpace → UniformSpace α
-- Mathlib.RingTheory.Valuation.Basic
/-- A valuation on a ring is nontrivial if there exists an element with valuation
not equal to `0` or `1`.  -/
Valuation.IsNontrivial : {R : Type u_3} →
  {Γ₀ : Type u_4} → [inst : Ring R] → [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → Valuation R Γ₀ → Prop
-- Mathlib.Data.Num.Bitwise
instCoeNzsNumSNum : Coe NzsNum SNum
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α}, f =o[l] g → ∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → (f ∘ k) =o[l'] (g ∘ k)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) {Z : ModuleCat k} (h : ModuleCat.of k ↥(groupHomology.cycles₁ C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.mapCycles₁ (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ))) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₁ g ψ) h)
-- Lean.Elab.Match
Lean.Elab.Term.elabNoMatch : Lean.Elab.Term.TermElab
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_formPerm_singleton : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (x y : α), [x].formPerm.toList y = []
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffOn_const : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {s : Set M} {n : WithTop ℕ∞}
  {c : M'}, ContMDiffOn I I' n (fun x => c) s
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
BoxIntegral.Prepartition.mem_splitCenter : ∀ {ι : Type u_1} [inst : Fintype ι] {I J : BoxIntegral.Box ι},
  J ∈ BoxIntegral.Prepartition.splitCenter I ↔ ∃ s, I.splitCenterBox s = J
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_filterMap_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)},
  (Std.ExtDHashMap.filterMap f m).size ≤ m.size
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongEpi.iff_of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g), CategoryTheory.StrongEpi f ↔ CategoryTheory.StrongEpi g
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_iff_of_monotone : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  (∀ (a : Ordinal.{u}), Monotone (op a)) →
    (∀ (a : Ordinal.{u}), Monotone (Function.swap op a)) → (Ordinal.IsPrincipal op o ↔ ∀ a < o, op a a < o)
-- Mathlib.Data.List.OfFn
List.ofFn_fin_repeat : ∀ {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ), List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten
-- Mathlib.Order.Bounds.Basic
bddBelow_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddBelow (Set.Ico a b)