mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.coe_symm_toAlgEquiv : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B] (f : A ≃⋆ₐ[R] B),
  ⇑f.toAlgEquiv.symm = ⇑f.symm
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.zero : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι], Matrix.Represents b 0 0
-- Mathlib.FieldTheory.Perfect
Polynomial.roots_expand_pow_map_iterateFrobenius_le : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (p n : ℕ) [inst_2 : ExpChar R p] (f : Polynomial R),
  Multiset.map (⇑(iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots ≤ p ^ n • f.roots
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.singleton_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a},
  {p} = ∅.insert p.fst p.snd
-- Lean.MetavarContext
/-- Set the metavariable user facing name.
 -/
Lean.MetavarContext.setMVarUserName : Lean.MetavarContext → Lean.MVarId → Lean.Name → Lean.MetavarContext
-- Mathlib.Topology.Algebra.Module.Equiv
MulOpposite.opContinuousLinearEquiv_apply : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (a : M), (MulOpposite.opContinuousLinearEquiv R) a = MulOpposite.op a
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  (TopologicalSpace.Opens.map hU.fromSpec.base).obj U = ⊤
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.associator_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.X Y.X Z.X).hom
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : SupHom α β)
  (hf : ∀ (a b : α), f.toFun (a ⊓ b) = f.toFun a ⊓ f.toFun b), ⇑{ toSupHom := f, map_inf' := hf } = ⇑f
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState : Type
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_one : ∀ (f : (a : Ordinal.{u_3}) → a < 1 → Ordinal.{max u_3 u_4}), Ordinal.bsup 1 f = f 0 ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_le_functorPushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.map F S ≤ CategoryTheory.Presieve.functorPushforward F S
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_inf : ∀ {M : Type u_2} [inst : AddZeroClass M] (S₁ S₂ : AddSubmonoid M), (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Given an orthogonal basis with respect to a bilinear map, the bilinear map is right-separating
if the basis has no elements which are self-orthogonal.  -/
LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self : ∀ {n : Type u_19} {R : Type u_20} {M : Type u_21} {M₁ : Type u_22} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [IsDomain R] [Module.IsTorsionFree R M₁]
  {B : M →ₗ[R] M →ₗ[R] M₁} (v : Module.Basis n R M),
  B.IsOrthoᵢ ⇑v → (∀ (i : n), (B (v i)) (v i) ≠ 0) → B.SeparatingRight
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.FractionRing.frobeniusRingHom.congr_simp : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_1) [inst_1 : CommRing k] [inst_2 : CharP k p]
  [inst_3 : PerfectRing k p],
  WittVector.FractionRing.frobeniusRingHom p k = WittVector.FractionRing.frobeniusRingHom p k
-- Mathlib.Topology.Bornology.Basic
/-- **Alias** of the reverse direction of `Bornology.isBounded_compl_iff`. -/
Bornology.IsCobounded.compl : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded s → Bornology.IsBounded sᶜ
-- Init.Prelude
/-- The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. -/
LE.le : {α : Type u} → [self : LE α] → α → α → Prop
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.coconeMorphism.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] (j : J),
  MonCat.FilteredColimits.coconeMorphism F j =
    MonCat.ofHom
      {
        toFun :=
          ⇑(CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.Types.TypeMax.colimitCocone (F.comp (CategoryTheory.forget MonCat))).ι.app j)),
        map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Order.Hom.Basic
OrderIso.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {f : α ≃o β}, f.toFun = ⇑f
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- `Prod.snd` as a `ContinuousLinearMap`.  -/
ContinuousLinearMap.snd : (R : Type u_1) →
  [inst : Semiring R] →
    (M₁ : Type u_2) →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] →
          [inst_3 : Module R M₁] →
            (M₂ : Type u_3) →
              [inst_4 : TopologicalSpace M₂] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → M₁ × M₂ →L[R] M₂
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- commutation with `p`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.commp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (self : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.CategoryStruct.comp h₁.p self.φQ = CategoryTheory.CategoryStruct.comp φ.τ₂ h₂.p
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkXorCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkXorCached input).aig.decls.size},
  (aig.mkXorCached input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Z₂(G, A) ⟶ Z₂(H, B)`.  -/
groupHomology.mapCycles₂ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) →
              (A ⟶ Rep.res f B) →
                (ModuleCat.of k ↥(groupHomology.cycles₂ A) ⟶ ModuleCat.of k ↥(groupHomology.cycles₂ B))
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.sigma_pt : ∀ {C : Type u} (F : C → Type v), (CategoryTheory.Limits.CofanTypes.sigma F).pt = ((i : C) × F i)
-- Init.Data.List.Basic
List.range.loop : ℕ → List ℕ → List ℕ
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.map_snd : ∀ {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] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L),
  (d.map F).snd i = F.map (d.snd i)
-- Mathlib.Data.Complex.Basic
Complex.ofReal_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.isEmpty_toType_zero : IsEmpty (Ordinal.ToType 0)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instReflectsIsomorphismsSheafedSpaceCommRingCatForgetToSheafedSpace : AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.ReflectsIsomorphisms
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ Std.TreeMap.Raw.unitOfList l cmp},
  (Std.TreeMap.Raw.unitOfList l cmp)[k] = ()
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The object level part of the backward direction of `Comon (Mon C) ≌ Mon (Comon C)`  -/
CategoryTheory.Bimon.ofMonComonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Mon (CategoryTheory.Comon C) → CategoryTheory.Bimon C
-- Mathlib.Order.RelSeries
FiniteDimensionalOrder.ofUnique : ∀ (γ : Type u_3) [inst : Preorder γ] [Unique γ], FiniteDimensionalOrder γ
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.image_frontier : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
  ⇑h '' frontier s = frontier (⇑h '' s)
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.swap : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {a b : R},
  RingTheory.Sequence.IsWeaklyRegular M [a, b] →
    (Submodule.torsionBy R M b = a • Submodule.torsionBy R M b → Submodule.torsionBy R M b = ⊥) →
      RingTheory.Sequence.IsWeaklyRegular M [b, a]
-- Init.Data.Fin.Lemmas
Fin.cast_last : ∀ {n n' : ℕ} {h : n + 1 = n' + 1}, Fin.cast h (Fin.last n) = Fin.last n'
-- Mathlib.CategoryTheory.Sites.Canonical
/-- The yoneda embedding into the presheaf category factors through the one
to the sheaf category.
 -/
CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] → J.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type v)) ≅ CategoryTheory.yoneda
-- Lean.MetavarContext
Lean.LevelMetavarDecl.mk : ℕ → ℕ → Lean.LevelMetavarDecl
-- Mathlib.Order.SuccPred.WithBot
WithTop.pred_lt_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] {x y : WithTop α} [NoMinOrder α],
  x < y → x.pred < y.pred
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.mk.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (source : X.Opens) (dense_source : Dense ↑source) (target : Y.Opens)
  (dense_target : Dense ↑target) (iso iso_1 : ↑source ≅ ↑target),
  iso = iso_1 →
    { source := source, dense_source := dense_source, target := target, dense_target := dense_target, iso := iso } =
      { source := source, dense_source := dense_source, target := target, dense_target := dense_target, iso := iso_1 }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.IsProbabilityMeasure_comap_equiv : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] (f : β ≃ᵐ α),
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap (⇑f) μ)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `f` is integrable, then for any `c > 0` the set `{x | f x ≥ c}` has finite
measure.  -/
MeasureTheory.Integrable.measure_ge_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β],
  MeasureTheory.Integrable f μ → ∀ {ε : β}, 0 < ε → μ {a | ε ≤ f a} < ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.degenerate_zero : ∀ (X : SSet), X.degenerate 0 = ∅
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdxD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → ℕ → (a : α) × β a → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : ℕ) →
          (x_2 : (a : α) × β a) →
            ((x : ℕ) → (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf x fallback) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l r : Std.DTreeMap.Internal.Impl α β) →
                        (n : ℕ) →
                          (fallback : (a : α) × β a) →
                            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback) →
                motive x x_1 x_2
-- Mathlib.Tactic.CongrExclamation
/-- Pop the next pattern from the current state.  -/
CongrMetaM.nextPattern : CongrMetaM (Option (Lean.TSyntax `rintroPat))
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- The bialgebra morphism underlying a bialgebra equivalence.  -/
BialgEquiv.toBialgHom : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₐc[R] B) → A →ₐc[R] B
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.instInhabitedKleisliCatId : Inhabited (CategoryTheory.KleisliCat id)
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.instFunLike : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] → [inst_7 : LieRingModule L N] → FunLike (M →ₗ⁅R,L⁆ N) M N
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
tendsto_logDeriv_euler_cot_sub : ∀ {x : ℂ},
  x ∈ Complex.integerComplement →
    Filter.Tendsto (fun n => ∑ j ∈ Finset.range n, cotTerm x j) Filter.atTop
      (nhds (↑Real.pi * (↑Real.pi * x).cot - 1 / x))
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_of_nat : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : Norm α] [inst_1 : Norm β] (n : ℕ),
  p = ↑n → ∀ (f : WithLp p (α × β)), ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / ↑n)
-- Mathlib.Algebra.Group.Submonoid.Support
isPointed_iff_support_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G}, M.IsPointed ↔ M.support = ⊥
-- Init.Data.Nat.Basic
Nat.sub_one_ne_self : ∀ {a : ℕ}, a ≠ 0 → a - 1 ≠ a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.EssImageSubcategory.tensor_obj : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Full] [inst_5 : F.Faithful]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteProducts F] (X Y : F.EssImageSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.obj Y.obj
-- Mathlib.LinearAlgebra.Matrix.WithConv
instCommMonoidWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [CommMonoid α] → CommMonoid (WithConv (Matrix m n α))
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactors_prod_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  (s : Multiset α),
  (∀ a ∈ s, Irreducible a) → UniqueFactorizationMonoid.normalizedFactors s.prod = Multiset.map normalize s
-- Aesop.Forward.Substitution
Aesop.Substitution.instOrd : Ord Aesop.Substitution
-- Mathlib.Order.Category.Preord
Preord.hom_ext_iff : ∀ {X Y : Preord} {f g : X ⟶ Y}, f = g ↔ Preord.Hom.hom f = Preord.Hom.hom g
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instSMulCommClass : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {S : Type u_4}
  {T : Type u_5} [inst_7 : Monoid S] [inst_8 : DistribMulAction S M] [inst_9 : SMulCommClass R S M]
  [inst_10 : LieDerivation.SMulBracketCommClass S L M] [inst_11 : Monoid T] [inst_12 : DistribMulAction T M]
  [inst_13 : SMulCommClass R T M] [inst_14 : LieDerivation.SMulBracketCommClass T L M] [SMulCommClass S T M],
  SMulCommClass S T (LieDerivation R L M)
-- Mathlib.Geometry.Manifold.HasGroupoid
Topology.IsOpenEmbedding.singleton_hasGroupoid : ∀ {H : Type u} [inst : TopologicalSpace H] {α : Type u_5} [inst_1 : TopologicalSpace α] [inst_2 : Nonempty α]
  {f : α → H} (h : Topology.IsOpenEmbedding f) (G : StructureGroupoid H) [ClosedUnderRestriction G], HasGroupoid α G
-- Mathlib.CategoryTheory.Limits.Fubini
Trans.simple.eq_1 : ∀ {α : Sort u_1} {a b c : α} {r : α → α → Sort u_2} [inst : Trans r r r], Trans.simple = Trans.trans
-- Mathlib.Data.Set.Function
Set.surjOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.SurjOn f s ∅
-- Mathlib.Analysis.Normed.Group.Constructions
Additive.normedAddCommGroup : {E : Type u_2} → [NormedCommGroup E] → NormedAddCommGroup (Additive E)
-- Mathlib.Data.Finset.Image
Finset.filterMap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f f_1 : α → Option β) (e_f : f = f_1) (s s_1 : Finset α),
  s = s_1 →
    ∀ (f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'), Finset.filterMap f s f_inj = Finset.filterMap f_1 s_1 ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_measure_zero_of_neg : ∀ {α : Type u_1} {q : ℝ} {ε : Type u_7} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  [inst_2 : MeasurableSpace α] {f : α → ε}, q < 0 → MeasureTheory.eLpNorm' f q 0 = ⊤
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.g_shortComplexTruncLEX₃ToTruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.g_shortComplexTruncLEX₃ToTruncGE._auto_1),
  CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE n₀).g (K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h) =
    K.πTruncGE n₁
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.find?.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] (s : String.Slice) (pat : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pat σ],
  s.find? pat =
    (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s).findSome? fun x =>
      match x with
      | String.Slice.Pattern.SearchStep.matched startPos endPos => some startPos
      | String.Slice.Pattern.SearchStep.rejected startPos endPos => none
-- Mathlib.LinearAlgebra.Span.Basic
/-- If two linear maps are equal on a set `s`, then they are equal on `Submodule.span s`.

This version uses `Set.EqOn`, and the hidden argument will expand to `h : x ∈ (span R s : Set M)`.
See `LinearMap.eqOn_span` for a version that takes `h : x ∈ span R s` as an argument.  -/
LinearMap.eqOn_span' : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Submodule.span R s)
-- Init.Data.UInt.Lemmas
USize.ofInt_mul : ∀ (x y : ℤ), USize.ofInt (x * y) = USize.ofInt x * USize.ofInt y
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_zero_right : ∀ (p : ℕ), p.maxPowDvdDiv 0 = (0, 0)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_algebraMap : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] {S : Type u_5} [inst_4 : CommSemiring S] [inst_5 : Module S E] [inst_6 : SMulCommClass 𝕜₁ S E]
  [inst_7 : SMul S 𝕜₁] [inst_8 : IsScalarTower S 𝕜₁ E] [inst_9 : ContinuousConstSMul S E]
  [inst_10 : IsTopologicalAddGroup E] (c : S),
  ContinuousLinearMapWOT.ofCLM ((algebraMap S (E →L[𝕜₁] E)) c) = (algebraMap S (E →WOT[𝕜₁] E)) c
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_symm : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p],
  (IsPerfectClosure.equiv i j p).symm = IsPerfectClosure.equiv j i p
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.insert_sdiff_of_mem`. -/
Set.insert_diff_of_mem : ∀ {α : Type u_1} {t : Set α} {a : α} (s : Set α), a ∈ t → insert a s \ t = s \ t
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_and : ∀ {w k : ℕ} {x y : BitVec w}, BitVec.setWidth k (x &&& y) = BitVec.setWidth k x &&& BitVec.setWidth k y
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject.map (HomotopicalAlgebra.BifibrantObject.toHoCat.map f) =
    HomotopicalAlgebra.FibrantObject.toHoCat.map (HomotopicalAlgebra.FibrantObject.homMk f.hom)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
/-- `slope f a c` is an affine combination of `slope f a b` and `slope f b c`. This version uses
`lineMap` to express this property.  -/
lineMap_slope_slope_sub_div_sub : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b c : k),
  a ≠ c → (AffineMap.lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_one : ↑1 = 1
-- Lean.Parser.Term
/-- `letRecDecls` matches `letRecDecl,+`, a comma-separated list of let-rec declarations (see `letRecDecl`).  -/
Lean.Parser.Term.letRecDecls : Lean.Parser.Parser
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapArrowIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {F' G' : HomologicalComplex C c} (φ' : F' ⟶ G')
  [inst_4 : HomologicalComplex.HasHomotopyCofiber φ'] (H : ∀ (j : ι), ∃ i, c.Rel i j)
  (α : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'),
  (HomologicalComplex.homotopyCofiber.mapArrowIso φ φ' H α).hom =
    HomologicalComplex.homotopyCofiber.mapArrowHom φ φ' H α.hom
-- Mathlib.RingTheory.Congruence.Basic
/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
containing the supremum of the set's image under the map to the underlying binary relation.  -/
RingCon.sSup_def : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)), sSup S = ringConGen (sSup (DFunLike.coe '' S))
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonPublishDiagnosticsParams.toJson : Lean.Lsp.PublishDiagnosticsParams → Lean.Json
-- Std.Data.String.ToInt
String.isInt_of_toInt?_eq_some : ∀ {a : ℤ} {s : String}, s.toInt? = some a → s.isInt = true
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.mk.sizeOf_spec : ∀ (name type : String) (doc? : Option String),
  sizeOf { name := name, type := type, doc? := doc? } = 1 + sizeOf name + sizeOf type + sizeOf doc?
-- Mathlib.RingTheory.Ideal.Prime
Ideal.not_isPrime_iff : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, ¬I.IsPrime ↔ I = ⊤ ∨ ∃ x, ∃ (_ : x ∉ I), ∃ y, ∃ (_ : y ∉ I), x * y ∈ I