mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyData.mapCyclesIso_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (hl : S.LeftHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasLeftHomology]
  [inst_6 : F.PreservesLeftHomologyOf S], S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.isCompact_closure_image_of_isVonNBounded : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁]
  [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module 𝕜₁ M₁] [inst_7 : Module 𝕜₂ M₂]
  [ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
  IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsVonNBounded 𝕜₁ S → IsCompact (closure (⇑f '' S))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.diff_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)
-- Mathlib.Algebra.BigOperators.Field
Finset.dens_biUnion : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] {s : Finset α} {t : α → Finset β} [inst_1 : DecidableEq β],
  (↑s).PairwiseDisjoint t → (s.biUnion t).dens = ∑ u ∈ s, (t u).dens
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_X₃ : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).X₃ = F.comp CategoryTheory.ShortComplex.π₃
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_singleton_right : ∀ {α : Type u_2} {s : Finset α} {a : α}, Disjoint s {a} ↔ a ∉ s
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.const_mul : ∀ {𝕜 : Type u_1} {α : Type u_3} {p : ENNReal} [inst : NormedRing 𝕜] {f : α → 𝕜},
  Memℓp f p → ∀ (c : 𝕜), Memℓp (fun x => c * f x) p
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.OLeanEntry.category.injEq : ∀ (catName declName : Lean.Name) (behavior : Lean.Parser.LeadingIdentBehavior) (catName_1 declName_1 : Lean.Name)
  (behavior_1 : Lean.Parser.LeadingIdentBehavior),
  (Lean.Parser.ParserExtension.OLeanEntry.category catName declName behavior =
      Lean.Parser.ParserExtension.OLeanEntry.category catName_1 declName_1 behavior_1) =
    (catName = catName_1 ∧ declName = declName_1 ∧ behavior = behavior_1)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintParams : Lean.FromJson Lean.Lsp.InlayHintParams
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.empty_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering}, ∅.toList = []
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.CoverPreserving.cover_preserve : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D},
  CategoryTheory.CoverPreserving J K G →
    ∀ {U : C} {S : CategoryTheory.Sieve U}, S ∈ J U → CategoryTheory.Sieve.functorPushforward G S ∈ K (G.obj U)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.isoMk_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreZeroHypercover.isoMk._auto_1)
  (i : E.I₀), (CategoryTheory.PreZeroHypercover.isoMk s₀ h₀ w₀).hom.h₀ i = (h₀ i).hom
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The union of all the relations as a subset of the free Lie algebra.  -/
CartanMatrix.Relations.toSet : (R : Type u) →
  {B : Type v} →
    [inst : CommRing R] → Matrix B B ℤ → [DecidableEq B] → Set (FreeLieAlgebra R (CartanMatrix.Generators B))
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (γ : A ⟶ S.homology),
  ∃ A' π,
    ∃ (_ : CategoryTheory.Epi π),
      ∃ z,
        ∃ (hz : CategoryTheory.CategoryStruct.comp z S.g = 0),
          CategoryTheory.CategoryStruct.comp π γ = CategoryTheory.CategoryStruct.comp (S.liftCycles z hz) S.homologyπ
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.isAddUnit_iff : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a : α}, IsAddUnit a ↔ a ≠ ⊤
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.tendsto_measure_Iic_atTop : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : Preorder α] [Filter.atTop.IsCountablyGenerated]
  (μ : MeasureTheory.Measure α), Filter.Tendsto (fun x => μ (Set.Iic x)) Filter.atTop (nhds (μ Set.univ))
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformInvCLM_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)),
  (Real.Lp.fourierTransformInvCLM V E) f = Real.Lp.fourierTransformInv f
-- Mathlib.NumberTheory.Height.NumberField
NumberField.totalWeight_eq_sum_mult : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Height.totalWeight K = ∑ v, v.mult
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [inst_3 : Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKey! k = ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).get!
-- Mathlib.Algebra.Lie.Prod
LieHom.coe_inr : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], ⇑(LieHom.inr R L₁ L₂) = Prod.mk 0
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (F.map f) (app b) ≅
                      CategoryTheory.CategoryStruct.comp (app a) (G.map f)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
                        (naturality g).hom =
                      CategoryTheory.CategoryStruct.comp (naturality f).hom
                        (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
                  CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.id a)).hom
                          (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a).hom) =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Bicategory.whiskerRight (F.mapId a).hom (app a))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
                            (CategoryTheory.Bicategory.rightUnitor (app a)).inv))
                    CategoryTheory.Pseudofunctor.StrongTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp (naturality (CategoryTheory.CategoryStruct.comp f g)).hom
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g).hom) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (app c))
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g).hom)
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.whiskerRight (naturality f).hom (G.map g))
                                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom)))))
                      CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp._autoParam →
                    F.StrongTrans G
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instSumScheme : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S} {𝒱 : CategoryTheory.PreZeroHypercover S}
  [AlgebraicGeometry.QuasiCompactCover 𝒰], AlgebraicGeometry.QuasiCompactCover (𝒰.sum 𝒱)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.ret.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf Λ] [inst_3 : SizeOf σ] (a : Turing.TM2.Stmt Γ Λ σ), sizeOf (Turing.TM2to1.Λ'.ret a) = 1 + sizeOf a
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Coe (Matrix.SpecialLinearGroup n R) (GL n R)
-- Lean.Parser.Command
Lean.Parser.Command.import : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- See `eLpNorm_smul_measure_of_ne_top'` for a version with scalar multiplication by `ℝ≥0∞`.  -/
MeasureTheory.eLpNorm_smul_measure_of_ne_top' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  p ≠ ⊤ → ∀ (c : NNReal) (f : α → ε), MeasureTheory.eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.eLpNorm f p μ
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.norm_one : ∀ {α : Type u_1} [inst : DecidableEq α], FreeGroup.norm 1 = 0
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyPToId.eq_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (x : ℕ),
  AlgebraicTopology.DoldKan.homotopyPToId X x =
    match x with
    | 0 => Homotopy.refl (AlgebraicTopology.DoldKan.P 0)
    | q.succ =>
      (Homotopy.ofEq ⋯).trans
        (((AlgebraicTopology.DoldKan.homotopyPToId X q).add
              ((AlgebraicTopology.DoldKan.homotopyHσToZero q).compLeft (AlgebraicTopology.DoldKan.P q))).trans
          (Homotopy.ofEq ⋯))
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.doubleDualEmb_inj : ∀ {α : Type u_1} [inst : AddCommGroup α] {a b : α} [Finite α], AddChar.doubleDualEmb a = AddChar.doubleDualEmb b ↔ a = b
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.fromNormalizedChainComplex_f_toNormalizedChainComplex_f_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ) {Z : C} (h : (X.normalizedChainComplex R).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.fromNormalizedChainComplex R).f n)
      (CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) h) =
    h
-- Init.Core
Subtype.instBEq : {α : Type u} → {p : α → Prop} → [BEq α] → BEq { x // p x }
-- Mathlib.Order.Minimal
exists_maximalFor_of_wellFoundedGT : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [WellFoundedGT α] (P : ι → Prop) (f : ι → α),
  (∃ i, P i) → ∃ i, MaximalFor P f i
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.ext : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {A B : HomologicalComplex V c}
  {x y : A.Hom B}, x.f = y.f → x = y
-- Mathlib.FieldTheory.LinearDisjoint
/-- If there exists an `F`-basis of `A` which remains linearly independent over `L`, then
`A` and `L` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_basis_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E]
  {ι : Type u_1} (a : Module.Basis ι F ↥A), LinearIndependent L (⇑A.val ∘ ⇑a) → A.LinearDisjoint L
-- Mathlib.Topology.Closure
mem_interior_iff_notMem_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {x : X}, x ∈ s → (x ∈ interior s ↔ x ∉ frontier s)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.refl_toLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], (CoalgEquiv.refl R A).toLinearEquiv = LinearEquiv.refl R A
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- The `BoxIntegral.IntegrationParams` corresponding to the Riemann integral. In the
corresponding filter, we require that the diameters of all boxes `J` of a tagged partition are
bounded from above by a constant upper estimate that may not depend on the geometry of `J`, and each
tag belongs to the corresponding closed box.  -/
BoxIntegral.IntegrationParams.Riemann : BoxIntegral.IntegrationParams
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- A `MulEquiv` `φ` between two semigroups `M` and `N` induces a `MulEquiv` between
a subsemigroup `S ≤ M` and the subsemigroup `φ(S) ≤ N`.
See `MulHom.subsemigroupMap` for a variant for `MulHom`s.  -/
MulEquiv.subsemigroupMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (e : M ≃* N) → (S : Subsemigroup M) → ↥S ≃* ↥(Subsemigroup.map (↑e) S)
-- Mathlib.Data.Vector.Basic
List.Vector.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (l : List α) (h : l.length = n),
  List.Vector.map f ⟨l, h⟩ = ⟨List.map f l, ⋯⟩
-- Mathlib.Tactic.Clean
/-- List of names removed by the `clean` tactic.
All of these names must resolve to functions defeq `id`.  -/
Lean.Expr.cleanConsts : List Lean.Name
-- Mathlib.Topology.MetricSpace.Similarity
Similar.comp_right : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {F : Type u_6}
  [inst_3 : FunLike F P₂ P₃] [DilationClass F P₂ P₃] (f : F), Similar v₁ v₂ → Similar v₁ (⇑f ∘ v₂)
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Constant functions are Lipschitz (with any constant).  -/
LipschitzWith.const : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
  LipschitzWith 0 fun x => b
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- `χ m` is the only map `X ⟶ Ω` which forms the appropriate pullback square for any `χ₀'`.  -/
CategoryTheory.Subobject.Classifier.uniq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Subobject.Classifier C) {U X : C}
  (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ self.Ω₀} {χ' : X ⟶ self.Ω},
  CategoryTheory.IsPullback m χ₀' χ' self.truth → χ' = self.χ m
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk'_toAddSubgroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s), (NonUnitalSubring.mk' s sm sa hm ha).toAddSubgroup = sa
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpFunctor.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D],
  CategoryTheory.Functor.mapAddGrpFunctor =
    { obj := fun F => F.obj.mapAddGrp,
      map := fun {F G} α => { app := fun A => CategoryTheory.AddGrp.homMk'' (α.hom.app A.X) ⋯ ⋯, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Init.Grind.Offset
Lean.Grind.Nat.of_ro_eq_false : ∀ (u v k : ℕ), (u ≤ v + k) = False → v + (k + 1) ≤ u
-- Mathlib.Algebra.Group.Action.End
/-- The tautological action by `Function.End α` on `α`.

This is generalized to bundled endomorphisms by:
* `Equiv.Perm.applyMulAction`
* `AddMonoid.End.applyDistribMulAction`
* `AddMonoid.End.applyModule`
* `AddAut.applyDistribMulAction`
* `MulAut.applyMulDistribMulAction`
* `LinearEquiv.applyDistribMulAction`
* `LinearMap.applyModule`
* `RingHom.applyMulSemiringAction`
* `RingAut.applyMulSemiringAction`
* `AlgEquiv.applyMulSemiringAction`
* `RelHom.applyMulAction`
* `RelEmbedding.applyMulAction`
* `RelIso.applyMulAction`
 -/
Function.End.applyMulAction : {α : Type u_5} → MulAction (Function.End α) α
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.zero_rpow_of_pos : ∀ {y : ℝ}, 0 < y → 0 ^ y = 0
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mk.sizeOf_spec : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [inst_3 : SizeOf R]
  [inst_4 : SizeOf L] (toSubmodule : Submodule R L)
  (lie_mem' : ∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier),
  sizeOf { toSubmodule := toSubmodule, lie_mem' := lie_mem' } = 1 + sizeOf toSubmodule
-- Mathlib.Topology.ContinuousOn
ContinuousOn.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β × γ} {s : Set α}, ContinuousOn f s → ContinuousOn (fun x => (f x).1) s
-- Aesop.Builder.NormSimp
Aesop.RuleBuilder.simp : Aesop.RuleBuilder
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.isLeft.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((val : α) → motive (Sum.inl val)) → ((val : β) → motive (Sum.inr val)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsIndepSet.card_le_indepNum : ∀ {α : Type u_3} {G : SimpleGraph α} [Finite α] {t : Finset α}, G.IsIndepSet ↑t → t.card ≤ G.indepNum
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (cmp (t.insert k).min! k).isLE = true
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.norm_le_one : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] (x : ↥(Valued.integer K)), ‖x‖ ≤ 1
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.ext₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (h₀ : f.obj' 0 _proof_297✝ = g.obj' 0 _proof_297✝) (h₁ : f.obj' 1 _proof_298✝ = g.obj' 1 _proof_298✝)
  (h₂ : f.obj' 2 _proof_299✝ = g.obj' 2 _proof_299✝) (h₃ : f.obj' 3 _proof_300✝ = g.obj' 3 _proof_300✝),
  f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝ =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₀)
        (CategoryTheory.CategoryStruct.comp (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
          (CategoryTheory.eqToHom ⋯)) →
    f.map' 1 2 _proof_246✝ _proof_299✝ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₁)
          (CategoryTheory.CategoryStruct.comp (g.map' 1 2 _proof_246✝ _proof_299✝) (CategoryTheory.eqToHom ⋯)) →
      f.map' 2 3 _proof_299✝ _proof_300✝ =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h₂)
            (CategoryTheory.CategoryStruct.comp (g.map' 2 3 _proof_299✝ _proof_300✝) (CategoryTheory.eqToHom ⋯)) →
        f = g
-- Mathlib.LinearAlgebra.Finsupp.Span
/-- `Submodule.exists_finset_of_mem_iSup` as an `iff`  -/
Submodule.mem_iSup_iff_exists_finset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  {p : ι → Submodule R M} {m : M}, m ∈ ⨆ i, p i ↔ ∃ s, m ∈ ⨆ i ∈ s, p i
-- Mathlib.GroupTheory.PushoutI
/-- The relation we quotient by to form the pushout  -/
Monoid.PushoutI.con : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] →
        [inst_1 : Monoid H] → ((i : ι) → H →* G i) → Con (Monoid.Coprod (Monoid.CoprodI G) H)
-- Std.Internal.UV.System
/-- Retrieves resource usage statistics.
 -/
Std.Internal.UV.System.getrusage : IO Std.Internal.UV.System.RUsage
-- Mathlib.Algebra.Ring.Commute
neg_one_sq : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R], (-1) ^ 2 = 1
-- Mathlib.Dynamics.Ergodic.Conservative
/-- We say that a non-singular (`MeasureTheory.QuasiMeasurePreserving`) self-map is
*conservative* if for any measurable set `s` of positive measure there exists `x ∈ s` such that `x`
returns back to `s` under some iteration of `f`.  -/
MeasureTheory.Conservative : {α : Type u_1} → [inst : MeasurableSpace α] → (α → α) → MeasureTheory.Measure α → Prop
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.isDense_iff_nonempty_isPointwiseLeftKanExtension : ∀ {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.IsDense ↔
    Nonempty
      (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D)
          F.rightUnitor.inv).IsPointwiseLeftKanExtension
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.subgraphInhabited_default : ∀ {V : Type u} {G : SimpleGraph V}, default = ⊥
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.neg : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup β] {l : Filter α} {f : α → β},
  l.BoundedAtFilter f → l.BoundedAtFilter (-f)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∉ t → l.contains k = false → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey! k = default
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The adjunction `Hom_{CRing}(Fun(n, R), S) ≃ Fun(n, Hom_{CRing}(R, S))`.  -/
CommRingCat.coyonedaAdj : (R : CommRingCat) → (CommRingCat.coyoneda.flip.obj R).rightOp ⊣ CategoryTheory.yoneda.obj R
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_mul_intCast : ∀ (x : ENNReal) (y : ℝ) (n : ℤ), x ^ (y * ↑n) = (x ^ y) ^ n