mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) →
              (unit : CategoryTheory.Functor.id C ⟶ F.comp G) →
                (counit : G.comp F ⟶ CategoryTheory.Functor.id D) →
                  autoParam
                      (∀ {X : C} {Y : D} {f : F.obj X ⟶ Y},
                        (homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (unit.app X) (G.map f))
                      CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_unit._autoParam →
                    autoParam
                        (∀ {X : C} {Y : D} {g : X ⟶ G.obj Y},
                          (homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (counit.app Y))
                        CategoryTheory.Adjunction.CoreHomEquivUnitCounit.homEquiv_counit._autoParam →
                      CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G
-- Mathlib.Data.Set.Image
Set.image_sdiff_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β}, f '' (s \ f ⁻¹' t) = f '' s \ t
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Disjoint.ndunion_eq : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, Disjoint s t → s.ndunion t = s.dedup + t
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct an isomorphism of monoid objects by giving an isomorphism between the underlying
objects and checking compatibility with unit and multiplication only in the forward direction.  -/
CategoryTheory.Mon.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Mon C} →
        (e : M.X ≅ N.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
              CategoryTheory.Mon.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.MonObj.mul)
                CategoryTheory.Mon.mkIso._auto_3 →
              (M ≅ N)
-- Mathlib.Tactic.FunProp.FunctionData
/-- Of the form `⇑f x y ...` i.e. additional applied arguments `y ...`.  -/
Mathlib.Meta.FunProp.MorApplication.overApplied : Mathlib.Meta.FunProp.MorApplication
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmop_inj_iff : ∀ {C : Type u₁} (x y : Cᴹᵒᵖ), x.unmop = y.unmop ↔ x = y
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (discr : aig.Ref)
  (lhs rhs : aig.RefVec w),
  Std.Sat.AIG.RefVec.ite aig { discr := discr, lhs := lhs, rhs := rhs } =
    Std.Sat.AIG.RefVec.ite.go aig 0 ⋯ discr lhs rhs (Std.Sat.AIG.RefVec.emptyWithCapacity w)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.match_1.congr_eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ) (n_1 : ℕ),
  n = n_1.succ →
    (match n with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_2 n_1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_top_eq_enat_card : ∀ {V : Type u}, ⊤.chromaticNumber = ENat.card V
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- Given an action of a monoidal category `C` on a category `D`,
an action of an additive monoid object `M` in `C` on an object `X` in `D` is the data of a
map `vadd : M ⊙ₗ X ⟶ X` that satisfies zero-additivity and associativity with addition.

See `AddAction` for the non-categorical version.  -/
CategoryTheory.AddModObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (M : C) → [CategoryTheory.AddMonObj M] → D → Type v₂
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Flip the second and third arguments in a trifunctor.
 -/
CategoryTheory.Functor.flip₂₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) →
                  CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ (CategoryTheory.Functor C₂ E))
-- Mathlib.Data.Set.Image
Set.image_id_eq : ∀ {α : Type u_1}, Set.image id = id
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- `MeasureTheory.Lp.compMeasurePreserving` as a linear isometry.  -/
MeasureTheory.Lp.compMeasurePreservingₗᵢ : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            {β : Type u_7} →
              [inst_1 : MeasurableSpace β] →
                {μb : MeasureTheory.Measure β} →
                  (𝕜 : Type u_8) →
                    [inst_2 : NormedRing 𝕜] →
                      [inst_3 : Module 𝕜 E] →
                        [inst_4 : IsBoundedSMul 𝕜 E] →
                          [inst_5 : Fact (1 ≤ p)] →
                            (f : α → β) →
                              MeasureTheory.MeasurePreserving f μ μb →
                                ↥(MeasureTheory.Lp E p μb) →ₗᵢ[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.le_bsup : ∀ {o : Ordinal.{u_3}} (f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}) (i : Ordinal.{u_3}) (h : i < o),
  f i h ≤ o.bsup f
-- Init.Control.MonadAttach
LawfulMonadAttach.toWeaklyLawfulMonadAttach : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadAttach m} [self : LawfulMonadAttach m],
  WeaklyLawfulMonadAttach m
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_apply : ∀ (k : ℂ) (F : UpperHalfPlane → ℂ) (z : UpperHalfPlane),
  Derivative.serreDerivative k F z = Derivative.normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z
-- Std.Sync.CancellationToken
Std.CancellationReason.custom.inj : ∀ {msg msg_1 : String}, Std.CancellationReason.custom msg = Std.CancellationReason.custom msg_1 → msg = msg_1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.lit.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (value value_1 : Lean.Compiler.LCNF.LitValue),
  (Lean.Compiler.LCNF.LetValue.lit value = Lean.Compiler.LCNF.LetValue.lit value_1) = (value = value_1)
-- Batteries.Data.List.Lemmas
List.disjoint_of_subset_right : ∀ {α : Type u_1} {l₂ l l₁ : List α}, l₂ ⊆ l → l₁.Disjoint l → l₁.Disjoint l₂
-- Mathlib.Topology.Bases
TopologicalSpace.isTopologicalBasis_of_cover : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} {U : ι → Set α},
  (∀ (i : ι), IsOpen (U i)) →
    ⋃ i, U i = Set.univ →
      ∀ {b : (i : ι) → Set (Set ↑(U i))},
        (∀ (i : ι), TopologicalSpace.IsTopologicalBasis (b i)) →
          TopologicalSpace.IsTopologicalBasis (⋃ i, Set.image Subtype.val '' b i)
-- Mathlib.Data.EReal.Basic
instInfSetEReal : InfSet EReal
-- Mathlib.Topology.Inseparable
SeparationQuotient.exists : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : SeparationQuotient X → Prop},
  (∃ x, P x) ↔ ∃ x, P (SeparationQuotient.mk x)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_iInter_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : Set α) (t : ι → Set α), s - ⋂ i, t i ⊆ ⋂ i, s - t i
-- Mathlib.LinearAlgebra.Pi
Submodule.iSup_map_single_le : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {I : Set ι} {p : (i : ι) → Submodule R (φ i)} [inst_3 : DecidableEq ι],
  ⨆ i, Submodule.map (LinearMap.single R φ i) (p i) ≤ Submodule.pi I p
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachStateTOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [WeaklyLawfulMonadAttach m], WeaklyLawfulMonadAttach (StateT σ m)
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.Context : Type
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitz.prodMk_left : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (a : α),
  LocallyLipschitz (Prod.mk a)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Given an internal direct sum decomposition of a module `M`, and an orthonormal basis for each
of the components of the direct sum, the disjoint union of these orthonormal bases is an
orthonormal basis for `M`.  -/
DirectSum.IsInternal.collectedOrthonormalBasis : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {A : ι → Submodule 𝕜 E} →
                (OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ) →
                  [inst_4 : DecidableEq ι] →
                    (DirectSum.IsInternal fun i => A i) →
                      {α : ι → Type u_7} →
                        [inst_5 : (i : ι) → Fintype (α i)] →
                          ((i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) → OrthonormalBasis ((i : ι) × α i) 𝕜 E
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `𝒜` be a graded ring, finitely generated (as an algebra) over `𝒜₀` by `{ vᵢ }`,
where `vᵢ` has degree `dvᵢ`.
If `f : A` has degree `d`, then `𝒜_(f)` is generated (as an algebra) over `𝒜₀` by
elements of the form `(∏ i, vᵢ ^ aᵢ) / fᵃ` such that `∑ aᵢ • dvᵢ = a • d` and `∀ i, aᵢ ≤ d`.
 -/
HomogeneousLocalization.Away.adjoin_mk_prod_pow_eq_top : ∀ {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} {d : ℕ} (hf : f ∈ 𝒜 d) (ι' : Type u_4) [inst_4 : Fintype ι'] (v : ι' → A),
  Algebra.adjoin (↥(𝒜 0)) (Set.range v) = ⊤ →
    ∀ (dv : ι' → ℕ) (hxd : ∀ (i : ι'), v i ∈ 𝒜 (dv i)),
      Algebra.adjoin ↥(𝒜 0)
          {x |
            ∃ a ai,
              ∃ (hai : ∑ i, ai i • dv i = a • d) (_ : ∀ (i : ι'), ai i ≤ d),
                HomogeneousLocalization.Away.mk 𝒜 hf a (∏ i, v i ^ ai i) ⋯ = x} =
        ⊤
-- Mathlib.Order.Filter.Pointwise
/-- `0 : Filter α` is defined as the filter of sets containing `0 : α` in scope `Pointwise`.  -/
Filter.instZero : {α : Type u_2} → [Zero α] → Zero (Filter α)
-- Mathlib.Data.Finmap
/-- The quotient map from `AList` to `Finmap`.  -/
AList.toFinmap : {α : Type u} → {β : α → Type v} → AList β → Finmap β
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.continuousOn_smul`

---

If `g` is continuous on the circle `sphere c |R|` and `f` is circle integrable, then `g • f` is
circle integrable.
 -/
CircleIntegrable.fun_continuousOn_smul : ∀ {c : ℂ} {R : ℝ} {𝕜 : Type u_3} {F : Type u_4} [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] {f : ℂ → F} {g : ℂ → 𝕜},
  CircleIntegrable f c R → ContinuousOn g (Metric.sphere c |R|) → CircleIntegrable (fun i => g i • f i) c R
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.lsub_pos : ∀ {ι : Type u_3} [h : Nonempty ι] (f : ι → Ordinal.{max u_4 u_3}), 0 < Ordinal.lsub f
-- Mathlib.CategoryTheory.FintypeCat
/-- The "standard" skeleton for `FintypeCat`. This is the full subcategory of `FintypeCat`
spanned by objects of the form `ULift (Fin n)` for `n : ℕ`. We parameterize the objects
of `FintypeCat.Skeleton` directly as `ULift ℕ`, as the type `ULift (Fin m) ≃ ULift (Fin n)`
is nonempty if and only if `n = m`. Specifying universes, `Skeleton : Type u` is a small
skeletal category equivalent to `FintypeCat.{u}`.
 -/
FintypeCat.Skeleton : Type u
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.get?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] (m : Std.DHashMap.Raw α β)
  (a : α), m.get? a = if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.get? ⟨m, h⟩ a else none
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
SSet.notNonempty_iff_hasDimensionLT_zero : ∀ (X : SSet), ¬X.Nonempty ↔ X.HasDimensionLT 0
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (f : ContinuousMultilinearMap 𝕜 E₁ G) (g dg : (i : ι) → E i →L[𝕜] E₁ i) (v : (i : ι) → E i),
  ((f.fderivCompContinuousLinearMap g) dg) v = ∑ i, f fun j => (Function.update g i (dg i) j) (v j)
-- Mathlib.CategoryTheory.EssentialImage
/-- The induced functor of a full functor is full.  -/
CategoryTheory.Functor.Full.toEssImage : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full], F.toEssImage.Full
-- Mathlib.Logic.ExistsUnique
existsUnique_prop : ∀ {p q : Prop}, (∃! x, q) ↔ p ∧ q
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk''.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero f = CategoryTheory.AddMonObj.zero)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
        CategoryTheory.AddMonObj.add),
  CategoryTheory.AddGrp.homMk'' f one_f mul_f = CategoryTheory.AddGrp.homMk f
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.le_sub : ∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : Ring S] [inst_2 : PartialOrder S] [IsOrderedRing S]
  (abv : AbsoluteValue R S) (a b : R), abv a - abv b ≤ abv (a - b)
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- The functor from sets to light condensed sets given by locally constant maps into the set.  -/
LightCondSet.LocallyConstant.functor : CategoryTheory.Functor (Type u) LightCondSet
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.option : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e →
    ∀ [inst_1 : Fintype I] (x : R),
      IsIdempotentElem x → x * ∑ i, e i = 0 → (∑ i, e i) * x = 0 → OrthogonalIdempotents fun x_1 => x_1.elim x e
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
/-- **Lebesgue dominated convergence theorem** provides sufficient conditions under which almost
everywhere convergence of a sequence of functions implies the convergence of their integrals.
We could weaken the condition `bound_integrable` to require `HasFiniteIntegral bound μ` instead
(i.e. not requiring that `bound` is measurable), but in all applications proving integrability
is easier.  -/
MeasureTheory.tendsto_integral_of_dominated_convergence : ∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {F : ℕ → α → G} {f : α → G} (bound : α → ℝ),
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) →
    MeasureTheory.Integrable bound μ →
      (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
        (∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
          Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_symm_zero : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D), (adj.homEquiv X Y).symm 0 = 0
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_transpose : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R), Matrix.detp s A.transpose = Matrix.detp s A
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.top_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B), ⊤.Factors f
-- Init.Data.Nat.Gcd
Nat.gcd_gcd_self_left_right : ∀ (m n : ℕ), (n.gcd m).gcd m = n.gcd m
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  LinearIndependent ℤ
      (Profinite.NobelingProof.GoodProducts.eval
        (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ↔
    LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.smaller C o)) => ↑p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.Equiv.beq_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : BEq β]
  [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Std.DHashMap α fun x => β},
  m₁.Equiv m₃ → m₂.Equiv m₄ → Std.DHashMap.Const.beq m₁ m₂ = Std.DHashMap.Const.beq m₃ m₄
-- Init.Data.SInt.Lemmas
Int32.lt_trans : ∀ {a b c : Int32}, a < b → b < c → a < c
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax left unity.  -/
CategoryTheory.LaxFunctor.map₂_leftUnitor_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(self.obj a)) {Z : ↑(self.obj b)}
  (h : (self.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv).toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((self.map f).toFunctor.map ((self.mapId a).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X) h)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_le_of_ae_enorm_bound : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε}
  {C : ENNReal}, (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C) → MeasureTheory.eLpNormEssSup f μ ≤ C
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.isSymm_degMatrix : ∀ {V : Type u_1} (R : Type u_2) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : AddMonoidWithOne R], (SimpleGraph.degMatrix R G).IsSymm
-- Mathlib.Algebra.GCDMonoid.Nat
Int.natAbs_lcm : ∀ (i j : ℤ), (lcm i j).natAbs = i.lcm j
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity follows from scaled extended distance. Backward direction of
`similar_iff_exists_edist_eq`.  -/
Similar.of_exists_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)) → Similar v₁ v₂
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G} {m : (i : ι) → E i} {C : ℝ} {b : ι → ℝ},
  ‖f‖ ≤ C → (∀ (i : ι), ‖m i‖ ≤ b i) → ‖f m‖ ≤ C * ∏ i, b i
-- Mathlib.Algebra.Order.Round
abs_sub_round_eq_min : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α),
  |x - ↑(round x)| = min (Int.fract x) (1 - Int.fract x)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.domRestrict_comp_rangeSRestrict : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (g : S →+* T) (f : R →+* S), (g.domRestrict f.rangeS).comp f.rangeSRestrict = g.comp f
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.dvd_gcd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The identity structured arrow is initial.  -/
CategoryTheory.StructuredArrow.mkIdInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {Y : C} →
          {T : CategoryTheory.Functor C D} →
            [T.Full] →
              [T.Faithful] →
                CategoryTheory.Limits.IsInitial
                  (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (T.obj Y)))
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.monotone_stabilizes : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Convergence in Lp implies uniform integrability.  -/
MeasureTheory.unifIntegrable_of_tendsto_Lp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {f : ℕ → α → β} {g : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        MeasureTheory.MemLp g p μ →
          Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0) →
            MeasureTheory.UnifIntegrable f p μ
-- Mathlib.Topology.Constructions
ContinuousAt.matrixVecCons : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {n : ℕ} {f : X → Z}
  {g : X → Fin n → Z} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => Matrix.vecCons (f a) (g a)) x
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgEquiv_comp : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (C : Type u_3) [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C),
  (Polynomial.mapAlgEquiv f).trans (Polynomial.mapAlgEquiv g) = Polynomial.mapAlgEquiv (f.trans g)
-- Mathlib.RingTheory.MatrixAlgebra
matrixEquivTensor_apply : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (M : Matrix n n A),
  (matrixEquivTensor n R A) M = ∑ p, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1