mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.comp_h_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  {X_1 Y_1 Z : CategoryTheory.Factorisation f} (f_1 : X_1 ⟶ Y_1) (g : Y_1 ⟶ Z) {Z_1 : C} (h : Z.mid ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f_1 g).h h =
    CategoryTheory.CategoryStruct.comp f_1.h (CategoryTheory.CategoryStruct.comp g.h h)
-- Mathlib.Algebra.Module.NatInt
AddCommGroup.intIsScalarTower : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M], IsScalarTower ℤ R M
-- Mathlib.Computability.StateTransition
StateTransition.tr_eval_rev : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {f₁ : σ₁ → Option σ₁} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂ → Prop},
  StateTransition.Respects f₁ f₂ tr →
    ∀ {a₁ : σ₁} {b₂ a₂ : σ₂},
      tr a₁ a₂ → b₂ ∈ StateTransition.eval f₂ a₂ → ∃ b₁, tr b₁ b₂ ∧ b₁ ∈ StateTransition.eval f₁ a₁
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.ext_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A},
  S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T
-- Mathlib.Data.Set.Sups
Set.infs_assoc : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t u : Set α), s ⊼ t ⊼ u = s ⊼ (t ⊼ u)
-- Mathlib.Order.Filter.Cocardinal
Filter.cocardinal_aleph0_eq_cofinite : ∀ {α : Type u}, Filter.cocardinal α Cardinal.isRegular_aleph0 = Filter.cofinite
-- Mathlib.Analysis.Convex.Between
Sbtw.left_ne_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y z : P}, Sbtw R x y z → x ≠ z
-- Batteries.Lean.LawfulMonad
instLawfulMonadTacticM_batteries : LawfulMonad Lean.Elab.Tactic.TacticM
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback fallback' : α}, t.getD (t.minD fallback) fallback' = t.minD fallback
-- Mathlib.Algebra.Group.Units.Defs
/-- Constructs a `CommGroup` structure on a `CommMonoid` consisting only of units.  -/
commGroupOfIsUnit : {M : Type u_1} → [hM : CommMonoid M] → (∀ (a : M), IsUnit a) → CommGroup M
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_comp_obj' : ∀ {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Set ↑Z) (p : IsOpen U),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g)).obj { carrier := U, is_open' := p } =
    (TopologicalSpace.Opens.map f).obj ((TopologicalSpace.Opens.map g).obj { carrier := U, is_open' := p })
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft_base : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} (φ : CategoryTheory.Limits.CatCospanTransform F G F' G')
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (α : ψ ⟶ ψ'),
  (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft φ α).base = φ.base.whiskerLeft α.base
-- Init.Data.BitVec.Lemmas
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xhi` when `start` is outside `xlo`.
 -/
BitVec.extractLsb'_append_eq_of_le : ∀ {v w : ℕ} {xhi : BitVec v} {xlo : BitVec w} {start len : ℕ},
  w ≤ start → BitVec.extractLsb' start len (xhi ++ xlo) = BitVec.extractLsb' (start - w) len xhi
-- Init.Data.UInt.Bitwise
UInt16.toUSize_shiftLeft : ∀ (a b : UInt16), (a <<< b).toUSize = a.toUSize <<< (b % 16).toUSize % 65536
-- Mathlib.Algebra.Group.EvenFunction
/-- A function `f` is _even_ if it satisfies `f (-x) = f x` for all `x`.  -/
Function.Even : {α : Type u_1} → {β : Type u_2} → [Neg α] → (α → β) → Prop
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.to_isRat : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n d : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a n d → Mathlib.Meta.NormNum.IsRat a (Int.ofNat n) d
-- Aesop.Options.Public
/-- (aesop) Only for use by Aesop developers. Generates a script even if none was requested.
 -/
Aesop.aesop.dev.generateScript : Lean.Option Bool
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.completeSpace : ∀ (α : Type u_1) [inst : UniformSpace α], CompleteSpace (UniformSpace.Completion α)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.unop_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (h : g.op.MulStruct f.op fg.op i) {j : Fin n} (hij : autoParam (i.rev = j) SSet.PtSimplex.MulStruct.unop._auto_1),
  (h.unop hij).map = SSet.yonedaEquiv.symm (SSet.opObjEquiv (SSet.yonedaEquiv h.map))
-- Mathlib.Data.PEquiv
/-- If the domain of a `PEquiv` is `α` except a point, its forward direction is injective.  -/
PEquiv.injective_of_forall_ne_isSome : ∀ {α : Type u} {β : Type v} (f : α ≃. β) (a₂ : α), (∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true) → Function.Injective ⇑f
-- Mathlib.Data.Sum.Interval
Sum.Ioo_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (b₁ b₂ : β),
  Finset.Ioo (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Ioo b₁ b₂)
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Reinterpret an `AffineIsometryEquiv` as an `AffineIsometry`.  -/
AffineIsometryEquiv.toAffineIsometry : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P →ᵃⁱ[𝕜] P₂
-- Lean.Elab.Tactic.Basic
/-- Use position of `=> $body` for error messages.
If there is a line break before `body`, the message will be displayed on `=>` only,
but the "full range" for the info view will still include `body`.  -/
Lean.Elab.Tactic.withCaseRef : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadRef m] → Lean.Syntax → Lean.Syntax → m α → m α
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The semilinear map constructed by applying a semilinear map to all the entries of the matrix.  -/
CStarMatrix.mapₗ : {m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_3} →
      {S : Type u_4} →
        {A : Type u_5} →
          {B : Type u_6} →
            [inst : Semiring R] →
              [inst_1 : Semiring S] →
                {σ : R →+* S} →
                  [inst_2 : AddCommMonoid A] →
                    [inst_3 : AddCommMonoid B] →
                      [inst_4 : Module R A] →
                        [inst_5 : Module S B] → (A →ₛₗ[σ] B) → CStarMatrix m n A →ₛₗ[σ] CStarMatrix m n B
-- Init.Data.List.SplitOn.Lemmas
_private.Init.Data.List.SplitOn.Lemmas.0.List.splitOnPPrepend.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (x : List α) (a : α) (t : List α),
  List.splitOnPPrepend p (a :: t) x =
    if p a = true then x.reverse :: List.splitOnPPrepend p t [] else List.splitOnPPrepend p t (a :: x)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {f' : F}
  {s t : Set E} {x v : E}, HasLineDerivWithinAt 𝕜 f f' s x v → t ⊆ s → HasLineDerivWithinAt 𝕜 f f' t x v
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The colimit of `F` represents the functor taking `W` to
the set of cocones on `F` with cone point `W`.  -/
CategoryTheory.Limits.IsColimit.natIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t →
              ((CategoryTheory.coyoneda.obj (Opposite.op t.pt)).comp CategoryTheory.uliftFunctor.{u₁, v₃} ≅ F.cocones)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.State.mk.injEq : ∀ (varMap : Lean.Meta.KExprMap ℕ) (vars : Array Lean.Expr) (varMap_1 : Lean.Meta.KExprMap ℕ) (vars_1 : Array Lean.Expr),
  ({ varMap := varMap, vars := vars } = { varMap := varMap_1, vars := vars_1 }) = (varMap = varMap_1 ∧ vars = vars_1)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtype_apply_coe : ∀ {α : Type u_9} {p q : α → Prop} (h : ∀ {x : α}, q x → p x) (a : { x // q ↑x }),
  ↑((Equiv.subtypeSubtypeEquivSubtype h) a) = ↑↑a
-- Mathlib.Data.Subtype
Subtype.val_prop : ∀ {α : Type u_1} {S : Set α} (a : { a // a ∈ S }), ↑a ∈ S
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given `P : ObjectProperty C` and `X : C`, this is the map which
sends `i : StructuredArrow P.ι X` to `i.right.obj : C`. The product
of this family is the target of the morphism `P.productTo X`.  -/
CategoryTheory.ObjectProperty.productToFamily : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) → (X : C) → CategoryTheory.StructuredArrow X P.ι → C
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).π = π
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsRevMatch.exists_isLongestRevMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos → ∃ pos', String.Slice.Pattern.Model.IsLongestRevMatch pat pos'
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Conjugation induces an equivariant map between the SubMulAction of
the stabilizer of a point and that of its translate.  -/
SubMulAction.ofStabilizer.conjMap : {G : Type u_1} →
  [inst : Group G] →
    {α : Type u_2} →
      [inst_1 : MulAction G α] →
        {g : G} →
          {a b : α} →
            (hg : b = g • a) →
              ↥(SubMulAction.ofStabilizer G a) →ₑ[⇑(MulAction.stabilizerEquivStabilizer hg)]
                ↥(SubMulAction.ofStabilizer G b)
-- Mathlib.Algebra.Order.Field.Basic
inv_lt_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a⁻¹ < b ↔ b⁻¹ < a)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Composition of a square between right adjoints with a conjugate square.  -/
CategoryTheory.Bicategory.rightAdjointSquareConjugate.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {g : a ⟶ c} →
        {h : b ⟶ d} →
          {r₁ : b ⟶ a} →
            {r₂ r₃ : d ⟶ c} →
              (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂) →
                (r₂ ⟶ r₃) → (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₃)
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.nonneg_toAddSubmonoid : ∀ {H : Type u_1} [inst : AddCommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedAddMonoid H],
  (AddGroupCone.nonneg H).toAddSubmonoid = AddSubmonoid.nonneg H
-- Mathlib.Tactic.WithoutCDot
_private.Mathlib.Tactic.WithoutCDot.0.Lean.Elab.Term.withoutCDotContents.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Ioo : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a b : R},
  Int.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉
-- Mathlib.Order.Filter.Basic
Filter.filter_eq_iff : ∀ {α : Type u} {f g : Filter α}, f = g ↔ f.sets = g.sets
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_nonneg_of_tendsto : ∀ {x : ℝ*} {r : ℝ}, Filter.Germ.Tendsto x (nhds r) → 0 ≤ ArchimedeanClass.mk x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The sign of a `Real.Angle` is `0` if the angle is `0` or `π`, `1` if the angle is strictly
between `0` and `π` and `-1` is the angle is strictly between `-π` and `0`. It is defined as the
sign of the sine of the angle.  -/
Real.Angle.sign : Real.Angle → SignType
-- Mathlib.Topology.Algebra.ConstMulAction
continuousOn_const_smul_iff₀ : ∀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀]
  [inst_2 : MulAction G₀ α] [ContinuousConstSMul G₀ α] [inst_4 : TopologicalSpace β] {f : β → α} {c : G₀} {s : Set β},
  c ≠ 0 → (ContinuousOn (fun x => c • f x) s ↔ ContinuousOn f s)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.eq_rnDeriv_measure : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η ξ : ProbabilityTheory.Kernel α γ}
  {f : α → γ → ENNReal} [inst : ProbabilityTheory.IsFiniteKernel η],
  κ = η.withDensity f + ξ →
    Measurable (Function.uncurry f) → ∀ (a : α), (ξ a).MutuallySingular (η a) → f a =ᵐ[η a] (κ a).rnDeriv (η a)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The comap of a cone `F` under a surjective linear map is a face of the
comap of another cone `F` if and only if `F` is a face of `C`.  -/
PointedCone.isFaceOf_comap_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {f : N →ₗ[R] M},
  Function.Surjective ⇑f → ((PointedCone.comap f F).IsFaceOf (PointedCone.comap f C) ↔ F.IsFaceOf C)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommRingOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → CommRing (DirectLimit G f)
-- Mathlib.Analysis.Normed.Group.Defs
NormedGroup.toGroup : {E : Type u_8} → [self : NormedGroup E] → Group E
-- Mathlib.Algebra.Polynomial.Derivation
/-- A form of the chain rule: if `f` is a polynomial over `R`
and `d : A → M` is an `R`-derivation then for all `a : A` we have
$$ d(f(a)) = f' (a) d a. $$
The equation is in the `R[X]`-module `Module.AEval R M a`.
For the same equation in `M`, see `Derivation.compAEval_eq`.
 -/
Derivation.compAEval_eq : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [inst_6 : IsScalarTower R A M] (a : A)
  (d : Derivation R A M) (f : Polynomial R), (d.compAEval a) f = Polynomial.derivative f • (Module.AEval.of R M a) (d a)
-- Mathlib.Analysis.ODE.PicardLindelof
IsPicardLindelof.mk : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  (∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)) →
    (∀ x ∈ Metric.closedBall x₀ ↑a, ContinuousOn (fun x_1 => f x_1 x) (Set.Icc tmin tmax)) →
      (∀ t ∈ Set.Icc tmin tmax, ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f t x‖ ≤ ↑L) →
        ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r → IsPicardLindelof f t₀ x₀ a r L K
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_le_card : ∀ (o : Ordinal.{u_1}), o.cof ≤ o.card
-- Mathlib.Algebra.Category.CommBialgCat
instIsMonHomOppositeCommAlgCatOpOfHomToAlgHom : ∀ {R : Type u} [inst : CommRing R] {A B : Type u} [inst_1 : CommRing A] [inst_2 : Bialgebra R A] [inst_3 : CommRing B]
  [inst_4 : Bialgebra R B] (f : A →ₐc[R] B), CategoryTheory.IsMonHom (CommAlgCat.ofHom ↑f).op
-- Init.Data.BitVec.Lemmas
BitVec.clzAuxRec_eq_clzAuxRec_of_le : ∀ {w n : ℕ} {x : BitVec w}, w - 1 ≤ n → x.clzAuxRec n = x.clzAuxRec (w - 1)
-- Aesop.Search.ExpandSafePrefix
_private.Aesop.Search.ExpandSafePrefix.0.Aesop.expandFirstPrefixRapp : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.RappRef → Aesop.SafeExpansionM Q Unit
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atTop_pure : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : OrderTop α] (f : α → β),
  Filter.Tendsto f Filter.atTop (pure (f ⊤))
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.var : Lean.FVarId → Lean.Meta.Match.Example
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.property : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (self : I.sections) (r : J.R),
  (CategoryTheory.ConcreteCategory.hom (I.fst r)) (self.val (J.fst r)) =
    (CategoryTheory.ConcreteCategory.hom (I.snd r)) (self.val (J.snd r))
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coe_coePNatMonoidHom : ⇑PrimeMultiset.coePNatMonoidHom = PrimeMultiset.toPNatMultiset
-- Init.MetaTypes
/-- When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
a `Decidable p` instance and reducing it.
 -/
Lean.Meta.DSimp.Config.decide : Lean.Meta.DSimp.Config → Bool
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and itself are linearly disjoint, if `M` is flat,
if any two elements of `M` are commutative, then the rank of `M` is at most one.  -/
Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M : Submodule R S},
  M.LinearDisjoint M → ∀ [Module.Flat R ↥M], (∀ (m n : ↥M), Commute ↑m ↑n) → Module.rank R ↥M ≤ 1
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.prod.eq_1 : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F₁ : Type u_2} [inst_1 : TopologicalSpace F₁] {E₁ : B → Type u_3}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_4} [inst_3 : TopologicalSpace F₂]
  {E₂ : B → Type u_5} [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [inst_5 : (x : B) → Zero (E₁ x)] [inst_6 : (x : B) → Zero (E₂ x)],
  e₁.prod e₂ =
    { toFun := Bundle.Trivialization.Prod.toFun' e₁ e₂, invFun := Bundle.Trivialization.Prod.invFun' e₁ e₂,
      source := Bundle.TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet), target := (e₁.baseSet ∩ e₂.baseSet) ×ˢ Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, continuousOn_toFun := ⋯,
      continuousOn_invFun := ⋯, open_source := ⋯, open_target := ⋯, baseSet := e₁.baseSet ∩ e₂.baseSet,
      open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.fstₗ_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : Semiring 𝕜] [inst_1 : AddCommGroup α]
  [inst_2 : AddCommGroup β] [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β] (x : WithLp p (α × β)),
  (WithLp.fstₗ p 𝕜 α β) x = x.fst
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftComp_hom_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : CategoryTheory.Comma L₃ R),
  ((CategoryTheory.Comma.mapLeftComp R l l').hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.instMulAction : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → {d : HNNExtension.NormalWord.TransversalPair G A B} → MulAction G (HNNExtension.NormalWord d)
-- Mathlib.Topology.Compactness.Lindelof
/-- X is a Lindelöf space iff every open cover has a countable subcover.  -/
LindelofSpace : (X : Type u_2) → [TopologicalSpace X] → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.diagramIsoReflexivePair F).hom.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
    | CategoryTheory.Limits.WalkingReflexivePair.one =>
      CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingReflexivePair.one)
-- Mathlib.Topology.Constructions.SumProd
Topology.IsEmbedding.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Y} {g : Z → W},
  Topology.IsEmbedding f → Topology.IsEmbedding g → Topology.IsEmbedding (Prod.map f g)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_ite_index : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (p : Prop) [inst_1 : Decidable p] (s t : Finset ι) (f : ι → M),
  ∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivWithinAt.const_sub : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x → ∀ (c : F), HasFDerivWithinAt (fun x => c - f x) (-f') s x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.size_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.partSize_pos : ∀ {n : ℕ} (self : OrderedFinpartition n) (m : Fin self.length), 0 < self.partSize m