mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_eq_setToL1SCLM : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (f : ↥(α →₁ₛ[μ] E)), (MeasureTheory.L1.setToL1 hT) ↑f = (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f
-- Init.Data.Option.Basic
Option.any_some : ∀ {α : Type u_1} {p : α → Bool} {x : α}, Option.any p (some x) = p x
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.toNorm : {E : Type u_2} → [Norm E] → Norm (Multiplicative E)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_sSup : ∀ {M : Type u_1} [inst : MulOneClass M] {f : Set (Submonoid M)}, (sSup f).saturation = ⨆ s ∈ f, s.saturation
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M} {g : N →+* M},
  c.comap g = RingCon.ker (c.mk'.comp g)
-- Init.GetElem
List.none_eq_getElem?_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, none = l[i]? ↔ l.length ≤ i
-- Lean.Elab.App
/-- When named arguments are provided and explicit arguments occurring before them are missing,
the elaborator eta-expands the declaration. For example,
```
def f (x y : Nat) := x + y
#check f (y := 5)
-- fun x => f x 5
```
`etaArgs` stores the fresh free variables for implementing the eta-expansion.
Each pair records the name to use for the binding and the fvar for the argument.

When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`.
When there are named arguments that depend on a missing argument, the missing arguments
are treated as `_` as well.
 -/
Lean.Elab.Term.ElabAppArgs.State.etaArgs : Lean.Elab.Term.ElabAppArgs.State → Array (Lean.Name × Lean.Expr)
-- Mathlib.Topology.Algebra.LinearTopology
IsLinearTopology.hasBasis_open_ideal : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : TopologicalSpace R] [ContinuousAdd R] [IsLinearTopology R R],
  (nhds 0).HasBasis (fun I => IsOpen ↑I) fun I => ↑I
-- Lean.HeadIndex
Lean.instBEqHeadIndex.beq : Lean.HeadIndex → Lean.HeadIndex → Bool
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_bot_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.IsComplement' ⊥ ↔ H = ⊤
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toLocallyRingedSpace_obj : ∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.Spec.toLocallyRingedSpace.obj R = AlgebraicGeometry.Spec.locallyRingedSpaceObj (Opposite.unop R)
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instEquivLike.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N],
  AddEquiv.instEquivLike =
    { coe := fun f => f.toFun, inv := fun f => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insertC.go.induct_unfolding : ∀ (m : Lean.Grind.CommRing.Mon) (c : ℕ) (k : ℤ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num k_1))) →
    (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        m.grevlex m_1 = Ordering.eq →
          have k'' := (k + k_1) % ↑c;
          (k'' == 0) = true → motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) p) →
      (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          m.grevlex m_1 = Ordering.eq →
            have k'' := (k + k_1) % ↑c;
            (k'' == 0) = false →
              motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) (Lean.Grind.CommRing.Poly.add k'' m p)) →
        (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
            m.grevlex m_1 = Ordering.gt →
              motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
                (Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.add k_1 m_1 p))) →
          (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
              m.grevlex m_1 = Ordering.lt →
                motive p (Lean.Grind.CommRing.Poly.insertC.go m c k p) →
                  motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
                    (Lean.Grind.CommRing.Poly.add k_1 m_1 (Lean.Grind.CommRing.Poly.insertC.go m c k p))) →
            ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.insertC.go m c k a)
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
TopCat.toSSetObjEdgeEquiv_symm_apply : ∀ {X : TopCat} {x y : ↑X} (p : X.Path x y),
  TopCat.toSSetObjEdgeEquiv.symm p = SSet.Edge.mk (TopCat.toSSetObj₁Equiv.symm p.hom) ⋯ ⋯
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.hasDetector_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.HasDetector Cᵒᵖ ↔ CategoryTheory.HasCodetector C
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk.injEq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] (toMulHom : M →ₙ* N)
  (isLocalizationMap : S.IsLocalizationMap toMulHom.toFun) (toMulHom_1 : M →ₙ* N)
  (isLocalizationMap_1 : S.IsLocalizationMap toMulHom_1.toFun),
  ({ toMulHom := toMulHom, isLocalizationMap := isLocalizationMap } =
      { toMulHom := toMulHom_1, isLocalizationMap := isLocalizationMap_1 }) =
    (toMulHom = toMulHom_1)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sum_sq_le_of_mem_box : ∀ {n d : ℕ} {x : Fin n → ℕ}, x ∈ Behrend.box n d → ∑ i, x i ^ 2 ≤ n * (d - 1) ^ 2
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mono_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.MonoOver X),
  CategoryTheory.Mono S.obj.hom
-- Mathlib.Data.List.Cycle
Cycle.length_reverse : ∀ {α : Type u_1} (s : Cycle α), s.reverse.length = s.length
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstHSubNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.ComonObj A]
  (X : C),
  (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj A X
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α),
  ∏' (x : ↑Set.univ), f ↑x = ∏' (x : β), f x
-- Init.Data.String.Search
String.findAux : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
-- Lean.Data.SSet
Lean.instReprSSet : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → [Repr α] → Repr (Lean.SSet α)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_zero_of_subsingleton : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  Module.rankAtStalk M = 0
-- Init.Data.UInt.Bitwise
UInt8.and_comm : ∀ (a b : UInt8), a &&& b = b &&& a
-- Lean.Data.Json.Basic
Lean.Json.brecOn_5.go : {motive_1 : Lean.Json → Sort u} →
  {motive_2 : Array Lean.Json → Sort u} →
    {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} →
      {motive_4 : List Lean.Json → Sort u} →
        {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u} →
          {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} →
            (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
              ((t : Lean.Json) → t.below → motive_1 t) →
                ((t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t) →
                  ((t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t) →
                    ((t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t) →
                      ((t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t) →
                        ((t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) →
                            Lean.Json.below_5 t → motive_6 t) →
                          motive_6 t ×' Lean.Json.below_5 t
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.add_congr : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] {a b : α} {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' →
    Lean.Grind.IntModule.OfNatModule.toQ b = b' → Lean.Grind.IntModule.OfNatModule.toQ (a + b) = a' + b'
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToStringRequestID : ToString Lean.JsonRpc.RequestID
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_4 : Nat.Partrec.Code.right.encodeCode = 3
-- Init.Data.SInt.Lemmas
Int16.toInt32_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
-- Mathlib.Data.LawfulXor.Basic
xor_left_involutive : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α] (a : α), Function.Involutive fun x => x ^^^ a
-- Mathlib.Data.List.Cycle
Cycle.instDecidableMemOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (x : α) → (s : Cycle α) → Decidable (x ∈ s)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- **Alias** of the reverse direction of `LinearMap.IsStarProjection.ext_iff`.

---

Star projection operators are equal iff their range are.  -/
LinearMap.IsStarProjection.ext : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {S T : E →ₗ[𝕜] E},
  IsStarProjection S → IsStarProjection T → S.range = T.range → S = T
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_lt_bddAbove : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
  a < b → BddAbove {n | MeasureTheory.upperCrossingTime a b f N n ω < N}
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instOrderBot : {α : Type u_4} →
  {β : Type u_5} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → OrderBot (ProbabilityTheory.Kernel α β)
-- Init.Data.String.Lemmas.Slice
String.Slice.beq_list_eq_decide : ∀ {l l' : List String.Slice}, (l == l') = decide (List.map String.Slice.copy l = List.map String.Slice.copy l')
-- Mathlib.Logic.Function.Basic
Function.instIsStrictOrderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsStrictOrder α r], IsStrictOrder α (Function.swap r)
-- Mathlib.Data.Set.Basic
Set.bot_eq_empty : ∀ {α : Type u}, ⊥ = ∅
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
HomotopicalAlgebra.rightHomotopyClassToHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {H : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] {X Y : C}
  (a a_1 : HomotopicalAlgebra.RightHomotopyClass X Y),
  a = a_1 → HomotopicalAlgebra.rightHomotopyClassToHom L a = HomotopicalAlgebra.rightHomotopyClassToHom L a_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.mul.eq_1 : ∀ (t1 t2 : Tactic.ComputeAsymptotics.Monomial), t1.mul t2 = { coef := t1.coef * t2.coef, unit := t1.unit.mul t2.unit }
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.enorm_compContinuousLinearMap_le : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [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] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F)
  (n : ℕ), ‖p.compContinuousLinearMap u n‖ₑ ≤ ‖p n‖ₑ * ‖u‖ₑ ^ n
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_erase : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : DecidableEq α] (b : α),
  (Finset.Iic b).erase b = Finset.Iio b
-- Mathlib.GroupTheory.SemidirectProduct
/-- Define an isomorphism from `N₁ ⋊[φ₁] G₁` to `N₂ ⋊[φ₂] G₂` given isomorphisms `N₁ ≃* N₂` and
`G₁ ≃* G₂` that satisfy a commutativity condition `∀ n g, fn (φ₁ g n) = φ₂ (fg g) (fn n)`.  -/
SemidirectProduct.congr : {N₁ : Type u_4} →
  {G₁ : Type u_5} →
    {N₂ : Type u_6} →
      {G₂ : Type u_7} →
        [inst : Group N₁] →
          [inst_1 : Group G₁] →
            [inst_2 : Group N₂] →
              [inst_3 : Group G₂] →
                {φ₁ : G₁ →* MulAut N₁} →
                  {φ₂ : G₂ →* MulAut N₂} →
                    (fn : N₁ ≃* N₂) →
                      (fg : G₁ ≃* G₂) →
                        (∀ (g : G₁), MulEquiv.trans (φ₁ g) fn = fn.trans (φ₂ (fg g))) → N₁ ⋊[φ₁] G₁ ≃* N₂ ⋊[φ₂] G₂
-- Mathlib.Algebra.Lie.Solvable
/-- The derived length of a Lie algebra is the derived length of its 'top' Lie ideal.

See also `LieAlgebra.derivedLength_eq_derivedLengthOfIdeal`.  -/
LieAlgebra.derivedLength : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → ℕ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {l : List α} {k : α}, (Std.HashMap.Raw.unitOfList l)[k]! = ()
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerLeft_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G H K : CategoryTheory.Functor D E} (α : G ⟶ H) (β : H ⟶ K) {Z : CategoryTheory.Functor C E} (h : F.comp K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.whiskerLeft (CategoryTheory.CategoryStruct.comp α β)) h =
    CategoryTheory.CategoryStruct.comp (F.whiskerLeft α) (CategoryTheory.CategoryStruct.comp (F.whiskerLeft β) h)
-- Init.Data.UInt.Lemmas
UInt8.toUSize_le : ∀ {a b : UInt8}, a.toUSize ≤ b.toUSize ↔ a ≤ b
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.add : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f g : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ →
    MeasureTheory.UnifTight g p μ →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
        (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (g i) μ) → MeasureTheory.UnifTight (f + g) p μ
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mulRight_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.GrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  (CategoryTheory.GrpObj.mulRight f).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
          (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv)))
      CategoryTheory.MonObj.mul
-- Mathlib.Analysis.Calculus.Deriv.Pow
derivWithin_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    ∀ (n : ℕ), derivWithin (f ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_nsmul_add_sum : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} {b : M},
  s.card • b + ∑ a ∈ s, f a = ∑ a ∈ s, (b + f a)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.HasCoeffs.relation_mem_range_map : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [P.HasCoeffs R₀] (x : σ),
  P.relation x ∈ Set.range ⇑(MvPolynomial.map (algebraMap R₀ R))
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_sup_eq : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (H K : Subgroup N),
  Function.Surjective ⇑f → Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.comap f (H ⊔ K)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (Std.DTreeMap.Raw.Const.get? t a).isSome = t.contains a
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.HasBasis.totallyBounded_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α},
  (uniformity α).HasBasis p U →
    ∀ {s : Set α}, TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ}
  (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (k : Rˣ) (z₂ : CochainComplex.HomComplex.Cochain G K n₂)
  (h : n₁ + n₂ = n₁₂), z₁.comp (k • z₂) h = k • z₁.comp z₂ h
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.succ.inj : ∀ {q q_1 : Turing.PartrecToTM2.Λ'}, q.succ = q_1.succ → q = q_1
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_three : catalan 3 = 5
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.sq_hasLift_of_hasLiftingProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) {f : A ⟶ X}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) [hip : CategoryTheory.HasLiftingProperty i p], sq.HasLift
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.OLeanEntry.mk.inj : ∀ {key : Lean.KeyedDeclsAttribute.Key} {declName : Lean.Name} {key_1 : Lean.KeyedDeclsAttribute.Key}
  {declName_1 : Lean.Name},
  { key := key, declName := declName } = { key := key_1, declName := declName_1 } → key = key_1 ∧ declName = declName_1
-- Lean.ReducibilityAttrs
/-- Return `true` if the given declaration has been marked as `[reducible]`.  -/
Lean.isReducible : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_trans_aeeq_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F)
  (γab : Path a b) (γbc : Path b c),
  curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc 0 (1 / 2))] fun t =>
    2 • curveIntegralFun ω γab (2 * t)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.ext_iff : ∀ {A : Type u_1} {σ : Type u_2} {inst : CommRing A} {inst_1 : SetLike σ A} {inst_2 : AddSubmonoidClass σ A} {𝒜 : ℕ → σ}
  {inst_3 : GradedRing 𝒜} {x y : ProjectiveSpectrum 𝒜}, x = y ↔ x.asHomogeneousIdeal = y.asHomogeneousIdeal
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.isoCoequalizer.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right],
  CategoryTheory.Limits.Multicoequalizer.isoCoequalizer I =
    CategoryTheory.Limits.colimit.isoColimitCocone
      {
        cocone :=
          I.multicoforkEquivSigmaCofork.inverse.obj
            (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair I.fstSigmaMap I.sndSigmaMap)),
        isColimit :=
          CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial I.multicoforkEquivSigmaCofork.inverse
            (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair I.fstSigmaMap I.sndSigmaMap)) }
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The identity for the `V`-enrichment of the category `J ⥤ C`.  -/
CategoryTheory.Enriched.FunctorCategory.enrichedId : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] →
                (F₁ : CategoryTheory.Functor J C) →
                  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁] →
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                      CategoryTheory.Enriched.FunctorCategory.enrichedHom V F₁ F₁
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_two_two_eq_four : ∀ (n : ℕ), hyperoperation (n + 1) 2 2 = 4
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.Equivalent.trans : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {N : Type u_9} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R N] {Q₁ : QuadraticMap R M₁ N}
  {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N}, Q₁.Equivalent Q₂ → Q₂.Equivalent Q₃ → Q₁.Equivalent Q₃
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.getKey? (t.maxKey he) = some (t.maxKey he)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∈ m₂ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.t2Space_iff_sInter_subset : ∀ {G : Type u} [inst : AddGroup G] [t : TopologicalSpace G] (F : AddGroupFilterBasis G),
  F.topology = t → (T2Space G ↔ ⋂₀ F.sets ⊆ {0})
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (property : [].length = 0),
  List.MergeSort.Internal.mergeSortTR₂.run✝ le ⟨[], property⟩ = []
-- Mathlib.RepresentationTheory.Coinduced
Rep.coindFunctor_obj : ∀ (k : Type u) {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (A : Rep.{t, u, v} k G), (Rep.coindFunctor k φ).obj A = Rep.coind.{u, v, w, t} φ A
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.toFunctor : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Monad C → CategoryTheory.Functor C C
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fundamentalSequence.match_3.splitter : (motive : Option ONote ⊕ (ℕ → ONote) → Sort u_1) →
  (x : Option ONote ⊕ (ℕ → ONote)) →
    ((f : ℕ → ONote) → motive (Sum.inr f)) →
      ((b' : ONote) → motive (Sum.inl (some b'))) → (Unit → motive (Sum.inl none)) → motive x