mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.congr_simp : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (x x_1 : A),
  x = x_1 → Algebra.elemental R x = Algebra.elemental R x_1
-- Mathlib.Combinatorics.Additive.ETransform
/-- This statement is meant to be combined with
`le_or_lt_of_add_le_add` and similar lemmas.  -/
Finset.AddETransform.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).1.card + (Finset.addETransformLeft e x).2.card +
      ((Finset.addETransformRight e x).1.card + (Finset.addETransformRight e x).2.card) =
    x.1.card + x.2.card + (x.1.card + x.2.card)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance
/-- Homotopic maps of simplicial sets induce the same map on homology of the singular
chain complex (with coefficients in `R`).
 -/
SSet.Homotopy.congr_homologyMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasCoproducts C] {X Y : SSet} {f g : X ⟶ Y}
  [inst_3 : CategoryTheory.CategoryWithHomology C] (H : SSet.Homotopy f g) (R : C) (n : ℕ),
  SSet.homologyMap f R n = SSet.homologyMap g R n
-- Mathlib.Logic.Basic
not_and_not_right : ∀ {a b : Prop}, ¬(a ∧ ¬b) ↔ a → b
-- Mathlib.Order.Hom.WithTopBot
/-- A version of `WithBot.map` for order embeddings.  -/
OrderEmbedding.withBotMap : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → α ↪o β → WithBot α ↪o WithBot β
-- Aesop.Script.SpecificTactics
Aesop.unfoldManyStarS : Lean.MVarId → (Lean.Name → Option (Option Lean.Name)) → Aesop.ScriptM (Option Lean.MVarId)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsert : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {b : β a},
      (Std.DHashMap.Internal.toListModel (↑(m.containsThenInsert a b).2).buckets).Perm
        (Std.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.ofInjective_toFun : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.IsAlgebraic] {f : L.Hom M N} (hf : Function.Injective ⇑f) (a : M),
  (FirstOrder.Language.Embedding.ofInjective hf) a = f a
-- Init.Data.Array.Extract
Array.takeWhile_append : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  Array.takeWhile p (xs ++ ys) =
    if (Array.takeWhile p xs).size = xs.size then xs ++ Array.takeWhile p ys else Array.takeWhile p xs
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_univ : ∀ {G : Type u_1} [inst : Group G], Subgroup.closure Set.univ = ⊤
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MeasureTheory.integrable_comp_div_iff : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] (g : ℝ → F) {R : ℝ},
  R ≠ 0 →
    (MeasureTheory.Integrable (fun x => g (x / R)) MeasureTheory.volume ↔
      MeasureTheory.Integrable g MeasureTheory.volume)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformlyOn.inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F : ι → X → α} {f : X → α} {s : Set X} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s → TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l s
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Comonad.comparison L`
sending objects `X : C` to Eilenberg-Moore coalgebras for `L ⋙ R` with underlying object
`L.obj X`.
 -/
CategoryTheory.Comonad.comparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (h : L ⊣ R) → CategoryTheory.Functor C h.toComonad.Coalgebra
-- Mathlib.Topology.Separation.Lemmas
Set.Countable.totallySeparatedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T35Space X] {s : Set X}, s.Countable → TotallySeparatedSpace ↑s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMapLinearMap_apply : ∀ (S : Type u_1) (R : Type u_3) (M : Type u_4) {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Semiring S] [inst_6 : Module S N]
  [inst_7 : SMulCommClass S R N] [inst_8 : SMulCommClass R S N] (B : LinearMap.BilinMap R M N),
  (LinearMap.BilinMap.toQuadraticMapLinearMap S R M) B = B.toQuadraticMap
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.arg.inj : ∀ {a b : Lean.Expr} {i : ℕ} {eq : Lean.Expr} {source : Lean.Meta.Grind.SplitSource} {a_1 b_1 : Lean.Expr} {i_1 : ℕ}
  {eq_1 : Lean.Expr} {source_1 : Lean.Meta.Grind.SplitSource},
  Lean.Meta.Grind.SplitInfo.arg a b i eq source = Lean.Meta.Grind.SplitInfo.arg a_1 b_1 i_1 eq_1 source_1 →
    a = a_1 ∧ b = b_1 ∧ i = i_1 ∧ eq = eq_1 ∧ source = source_1
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- **Alias** of the forward direction of `lipschitzWith_iff_dist_le_mul`. -/
LipschitzWith.dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.ofNatTrans_app : ∀ {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} {A : CategoryTheory.Functor C (Type w)} (f : F ⟶ G) (X : C) (x : A.obj X),
  (CategoryTheory.Functor.HomObj.ofNatTrans f).app X x = f.app X
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_add_eq_map_add_linearDeriv_add : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommGroup (M₁ i)] [inst_2 : AddCommGroup M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (x h : (i : ι) → M₁ i), f (x + h) = f x + (f.linearDeriv x) h + ∑ s with 2 ≤ s.card, f (s.piecewise h x)
-- Mathlib.RingTheory.SimpleModule.Basic
Module.Finite.of_isComplemented_codomain : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M}
  (R₀ : Type u_6) (P : Type u_7) [inst_3 : Semiring R₀] [inst_4 : AddCommMonoid P] [inst_5 : Module R P]
  [inst_6 : Module R₀ M] [inst_7 : SMulCommClass R R₀ M] [inst_8 : SMul R₀ R] [inst_9 : IsScalarTower R₀ R M]
  [Module.Finite R₀ (P →ₗ[R] M)], IsComplemented m → Module.Finite R₀ (P →ₗ[R] ↥m)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instSimpAndAnd : ∀ (σs : List (Type u_1)) (P Q : Std.Do.SPred σs), Std.Do.SPred.Tactic.SimpAnd P Q spred(P ∧ Q)
-- Lean.Meta.Instances
Lean.Meta.getGlobalInstancesIndex : Lean.CoreM (Lean.Meta.DiscrTree Lean.Meta.InstanceEntry)
-- Mathlib.Order.Interval.Basic
/-- Binary pushforward of nonempty intervals.  -/
NonemptyInterval.map₂ : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            (f : α → β → γ) →
              (∀ (b : β), Monotone fun a => f a b) →
                (∀ (a : α), Monotone (f a)) → NonemptyInterval α → NonemptyInterval β → NonemptyInterval γ
-- Mathlib.Data.List.Rotate
List.rotate_rotate : ∀ {α : Type u} (l : List α) (n m : ℕ), (l.rotate n).rotate m = l.rotate (n + m)
-- Mathlib.Algebra.Free
Magma.AssocQuotient.lift.eq_1 : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β],
  Magma.AssocQuotient.lift =
    { toFun := fun f => { toFun := fun x => Quot.liftOn x ⇑f ⋯, map_mul' := ⋯ },
      invFun := fun f => f.comp Magma.AssocQuotient.of, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.val_toFin : ∀ {w : ℕ} (x : BitVec w), ↑x.toFin = x.toNat
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A convenience function for `ReflectsLimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
 -/
CategoryTheory.Limits.isLimitOfReflects : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cone K} →
                  CategoryTheory.Limits.IsLimit (F.mapCone c) →
                    [CategoryTheory.Limits.ReflectsLimit K F] → CategoryTheory.Limits.IsLimit c
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roc : ∀ {m n fallback : ℤ} {i : ℕ}, (m<...=n).toList.getD i fallback = if i < (n - m).toNat then m + 1 + ↑i else fallback
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.ReflexiveRelation.toJointlyMono₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.ReflexiveRelation p₁ p₂), CategoryTheory.JointlyMono₂ p₁ p₂
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBiprod_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : F.PreservesZeroMorphisms] [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F],
  (F.mapBiprod X Y).hom =
    CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.map_prime_of_equiv`. -/
map_prime_of_equiv : ∀ {T : Type u_4} [inst : CommRing T] [IsDedekindDomain T] {R : Type u_5} [inst_2 : CommRing R] [IsDedekindDomain R]
  (f : T ≃+* R) {I : Ideal T}, Prime I → I ≠ ⊥ → Prime (Ideal.map f I)
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.mk.inj : ∀ {hour : Std.Time.Hour.Ordinal} {minute : Std.Time.Minute.Ordinal} {second : Std.Time.Second.Ordinal true}
  {nanosecond : Std.Time.Nanosecond.Ordinal} {hour_1 : Std.Time.Hour.Ordinal} {minute_1 : Std.Time.Minute.Ordinal}
  {second_1 : Std.Time.Second.Ordinal true} {nanosecond_1 : Std.Time.Nanosecond.Ordinal},
  { hour := hour, minute := minute, second := second, nanosecond := nanosecond } =
      { hour := hour_1, minute := minute_1, second := second_1, nanosecond := nanosecond_1 } →
    hour = hour_1 ∧ minute = minute_1 ∧ second = second_1 ∧ nanosecond = nanosecond_1
-- Mathlib.Combinatorics.Matroid.Constructions
/-- The `Matroid α` with empty ground set.  -/
Matroid.emptyOn : (α : Type u_2) → Matroid α
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.instInitialCostructuredArrowCompPreOfRepresentablyCoflat : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (X : E) [CategoryTheory.RepresentablyCoflat F],
  (CategoryTheory.CostructuredArrow.pre F G X).Initial
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- **Alias** of `MeasureTheory.ae_finite_setOfPred_mem`.

---

One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a countable family of sets such that `∑' i, μ (s i)` is finite,
then a.e. all points belong to finitely many sets of the family.  -/
MeasureTheory.ae_finite_setOf_mem : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] [Countable ι] {μ : F} {s : ι → Set α},
  ∑' (i : ι), μ (s i) ≠ ⊤ → ∀ᵐ (x : α) ∂μ, {i | x ∈ s i}.Finite
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.startPos_ofSliceFrom : ∀ {s : String.Slice} {p : s.Pos} {st : String.Slice.Pattern.SearchStep (s.sliceFrom p)},
  st.ofSliceFrom.startPos = String.Slice.Pos.ofSliceFrom st.startPos
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- The 2-morphism underlying the oplax unity constraint.  -/
CategoryTheory.OplaxFunctor.mapId : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.OplaxFunctor B C) →
          (a : B) → self.map (CategoryTheory.CategoryStruct.id a) ⟶ CategoryTheory.CategoryStruct.id (self.obj a)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.instIsMulCommutative_adjoin : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S : Type u_1} [inst_8 : SetLike S A] [inst_9 : MulMemClass S A] [StarMemClass S A] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(NonUnitalStarAlgebra.adjoin R ↑s)
-- Mathlib.Topology.Gluing
TopCat.GlueData.mk.sizeOf_spec : ∀ (toGlueData : CategoryTheory.GlueData TopCat)
  (f_open : ∀ (i j : toGlueData.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (toGlueData.f i j))),
  sizeOf { toGlueData := toGlueData, f_open := f_open } = 1 + sizeOf toGlueData
-- Mathlib.Algebra.Algebra.Basic
int_algebra_subsingleton : ∀ {R : Type u_1} [inst : Ring R], Subsingleton (Algebra ℤ R)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDifferentiableWithinAt_univ : ∀ {𝕜 : 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} {x v : E},
  LineDifferentiableWithinAt 𝕜 f Set.univ x v ↔ LineDifferentiableAt 𝕜 f x v
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {A : Type u} [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K]
  (P : CategoryTheory.Functor Dᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf K P → CategoryTheory.Presheaf.IsSheaf J (F.op.comp P)
-- Mathlib.LinearAlgebra.UnitaryGroup
Unitary.tmul_mem : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : StarRing A] [inst_6 : StarRing B] [inst_7 : StarRing R]
  [inst_8 : StarModule R A] [inst_9 : StarModule R B] {U : A} {V : B},
  U ∈ unitary A → V ∈ unitary B → U ⊗ₜ[R] V ∈ unitary (TensorProduct R A B)
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The restriction of scalars functor `AlgCat S ⥤ AlgCat R` induced by a ring homomorphism
`R →+* S`.  -/
AlgCat.restrictScalars : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → CategoryTheory.Functor (AlgCat S) (AlgCat R)
-- Mathlib.Data.Set.Prod
Set.prod_mono_left : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, s₁ ⊆ s₂ → s₁ ×ˢ t ⊆ s₂ ×ˢ t
-- Init.Data.Nat.Lemmas
Nat.mod_succ_eq_iff_lt : ∀ {m n : ℕ}, m % n.succ = m ↔ m < n.succ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Differentiable.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ fun x => Real.arctan (f x)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Two non-unital subsemirings are equal if they have the same elements.  -/
NonUnitalSubsemiring.ext : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S T : NonUnitalSubsemiring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoi : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Roi α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α}, a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_neg_one_of_isEmpty : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  [IsEmpty n], Matrix.detp (-1) A = 0
-- Mathlib.Data.ENNReal.Inv
ENNReal.top_div : ∀ {a : ENNReal}, ⊤ / a = if a = ⊤ then 0 else ⊤
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_ofToSlice_iff : ∀ {s : String} {p : s.toSlice.Pos} {t₁ t₂ : String}, (String.Pos.ofToSlice p).Splits t₁ t₂ ↔ p.Splits t₁ t₂
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toContinuousMap : C(α, β))
  (map_bounded' : ∃ C, ∀ (x y : α), dist (toContinuousMap.toFun x) (toContinuousMap.toFun y) ≤ C),
  sizeOf { toContinuousMap := toContinuousMap, map_bounded' := map_bounded' } =
    1 + sizeOf toContinuousMap + sizeOf map_bounded'
-- Init.Data.List.Basic
/-- The first list is a suffix of the second.

`IsSuffix l₁ l₂`, written `l₁ <:+ l₂`, means that there exists some `t : List α` such that `l₂` has
the form `t ++ l₁`.

The function `List.isSuffixOf` is a Boolean equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+` in identifiers is `suffix` (not `isSuffix`). -/
List.IsSuffix : {α : Type u} → List α → List α → Prop
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.neBot : ∀ {α : Type u} (f : Ultrafilter α), (↑f).NeBot
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.id : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.End.invtSubmodule LinearMap.id = ⊤
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f),
  hf.map hf LinearMap.id LinearMap.id = LinearMap.id
-- Mathlib.Data.Ordmap.Ordnode
/-- **Internal use only**

O(1). Rebalance a tree which was previously balanced but has had one side change
by at most 1.  -/
Ordnode.balance : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.ModelTheory.Fraisse
/-- The age of a countable structure is essentially countable (has countably many isomorphism
classes).  -/
FirstOrder.Language.age.countable_quotient : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] [h : Countable M], (Quotient.mk' '' L.age M).Countable
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear
CategoryTheory.Abelian.Ext.comp_smul : ∀ {R : Type t} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.Linear R C] [inst_4 : CategoryTheory.HasExt C]
  {X Y Z : C} {a b : ℕ} (α : CategoryTheory.Abelian.Ext X Y a) (β : CategoryTheory.Abelian.Ext Y Z b) {c : ℕ}
  (h : a + b = c) (r : R), α.comp (r • β) h = r • α.comp β h
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.dirSupClosedOn_of_isClosed : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsClosed s → DirSupClosedOn D s
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalAddMonoidHom.eq_1 : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → AddZeroClass (f i)] (i : I),
  Pi.evalAddMonoidHom f i = { toFun := fun g => g i, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addCommMonoid : {R : Type u} → {M : Type v} → [AddCommMonoid R] → [AddCommMonoid M] → AddCommMonoid (TrivSqZeroExt R M)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is `π`, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_eq_pi : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑Real.pi → y ≠ 0
-- Lean.Data.Lsp.Utf16
/-- Gets the LSP range from a `Lean.Syntax.Range`.  -/
Lean.FileMap.utf8RangeToLspRange : Lean.FileMap → Lean.Syntax.Range → Lean.Lsp.Range
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.covering_mem_family : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) {p : X × Set X},
  p ∈ h.index → h.covering p ∈ v.setsAt p.1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.mk.injEq : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (toSlashInvariantForm : SlashInvariantForm Γ k)
  (holo' : MDiff ⇑toSlashInvariantForm)
  (bdd_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k)
  (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff ⇑toSlashInvariantForm_1)
  (bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm_1.toFun k),
  ({ toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := bdd_at_cusps' } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := bdd_at_cusps'_1 }) =
    (toSlashInvariantForm = toSlashInvariantForm_1)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_ofBijective : ∀ {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B]
  [inst_9 : StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f), ⇑(StarAlgEquiv.ofBijective f hf) = ⇑f
-- Mathlib.MeasureTheory.Measure.SubFinite
MeasureTheory.Measure.sub_le_iff_le_add : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν ξ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], μ - ν ≤ ξ ↔ μ ≤ ξ + ν
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Turn a morphism in `SemiNormedGrp₁` back into a norm-nonincreasing `NormedAddGroupHom`.  -/
SemiNormedGrp₁.Hom.hom : {M N : SemiNormedGrp₁} → M.Hom N → { f // f.NormNoninc }
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : SizeOf C] (toFunctor : CategoryTheory.Functor C C)
  (ε : toFunctor ⟶ CategoryTheory.Functor.id C) (δ : toFunctor ⟶ toFunctor.comp toFunctor)
  (coassoc :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (δ.app X)) =
          CategoryTheory.CategoryStruct.comp (δ.app X) (δ.app (toFunctor.obj X)))
      CategoryTheory.Comonad.coassoc._autoParam)
  (left_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (ε.app (toFunctor.obj X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.left_counit._autoParam)
  (right_counit :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (ε.app X)) =
          CategoryTheory.CategoryStruct.id (toFunctor.obj X))
      CategoryTheory.Comonad.right_counit._autoParam),
  sizeOf
      { toFunctor := toFunctor, ε := ε, δ := δ, coassoc := coassoc, left_counit := left_counit,
        right_counit := right_counit } =
    1 + sizeOf toFunctor + sizeOf ε + sizeOf δ