mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv_symm : ∀ {ι' : Type u_2} {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12}
  [inst_1 : Semiring R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M']
  (b' : Module.Basis ι' R M') (e : ι ≃ ι'), (b.equiv b' e).symm = b'.equiv b e.symm
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.isEmbedding_subtype : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), Topology.IsEmbedding ⇑p.subtype
-- Std.Data.DHashMap.Raw
/-- Returns the number of buckets in the internal representation of the hash map. This function may be
useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.DHashMap.Raw.Internal.numBuckets : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → ℕ
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
/-- A presheaf `F` of types is (strongly) separated for a pre-`1`-hypercover if `F` is separated for
both the `0` and the `1`-components.  -/
CategoryTheory.PreOneHypercover.IsStronglySeparatedFor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : C} → CategoryTheory.PreOneHypercover X → CategoryTheory.Functor Cᵒᵖ (Type u_3) → Prop
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_map_comp_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {ι : Type u_2}
  (f : R →+* S₁) (h : ι → MvPolynomial σ S₁) (p : MvPolynomial ι R),
  MvPolynomial.eval₂ ((MvPolynomial.map f).comp MvPolynomial.C) h p =
    MvPolynomial.eval₂ MvPolynomial.C h ((MvPolynomial.map f) p)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso_inv_comp_image_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.compIso f g).inv (CategoryTheory.Limits.image.ι f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp f g))
      (CategoryTheory.inv g)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLT?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyLT? k = t₂.getKeyLT? k
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The image of a simplex by a morphism of simplicial sets.  -/
SSet.S.map : {X Y : SSet} → (X ⟶ Y) → X.S → Y.S
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : PseudoEpimorphism α β),
  (PseudoEpimorphism.id β).comp f = f
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_verschiebung_iterate_frobenius : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) (n : ℕ),
  (⇑WittVector.verschiebung)^[n] ((⇑WittVector.frobenius)^[n] x) = x * ↑p ^ n
-- Lean.Data.Trie
Lean.Data.Trie.leaf : {α : Type} → Option α → Lean.Data.Trie α
-- Mathlib.Topology.OmegaCompletePartialOrder
Scott.isOpen_sUnion : ∀ (α : Type u) [inst : OmegaCompletePartialOrder α] (s : Set (Set α)),
  (∀ t ∈ s, Scott.IsOpen α t) → Scott.IsOpen α (⋃₀ s)
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mem_toAddSubmonoid : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (x : M), x ∈ p.toAddSubmonoid ↔ x ∈ p
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.get_EStateM : ∀ {σ ε : Type} (post : σ → σ → Prop) (epost : ε → σ → Prop), ⦃ fun s => post s s ⦄ MonadStateOf.get ⦃ post; epost ⦄
-- Mathlib.Order.CompleteBooleanAlgebra
himp_eq_sSup : ∀ {α : Type u} [inst : Order.Frame α] {a b : α}, a ⇨ b = sSup {w | w ⊓ a ≤ b}
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.refl_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c), (HomotopyEquiv.refl C).inv = CategoryTheory.CategoryStruct.id C
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.instDecidableEqLabel : DecidableEq Lean.Meta.NormCast.Label
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_eq_getD_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  m.getD a fallback = (m.get? a).getD fallback
-- Mathlib.Algebra.CharP.Two
CharTwo.two_eq_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharP R 2], 2 = 0
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.mgf_le : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ᵐ (ω' : Ω) ∂μ.trim hm,
      ∀ (t : ℝ), ProbabilityTheory.mgf X ((ProbabilityTheory.condExpKernel μ m) ω') t ≤ Real.exp (↑c * t ^ 2 / 2)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkRingHom_apply : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonAssocSemiring R] [inst_2 : IsTopologicalSemiring R] (a : R),
  SeparationQuotient.mkRingHom a = SeparationQuotient.mk a
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.total : ∀ {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α}, ChainClosure r c₁ → ChainClosure r c₂ → c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
-- Init.Data.Fin.Lemmas
Fin.cast_castSucc : ∀ {n n' : ℕ} {h : n + 1 = n' + 1} {i : Fin n}, Fin.cast h i.castSucc = (Fin.cast ⋯ i).castSucc
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.instMonoι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), CategoryTheory.Mono (CategoryTheory.kernelCokernelCompSequence.ι f g)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inr_coprodIsoPushout_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y]
  {Z : C} (h : X ⨿ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y))
      (CategoryTheory.CategoryStruct.comp (coprodIsoPushout X Y).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- **Alias** of `CategoryTheory.ObjectProperty.FullSubcategory.concreteCategory`. -/
CategoryTheory.FullSubcategory.concreteCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_2} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [CategoryTheory.ConcreteCategory C FC] →
            (P : CategoryTheory.ObjectProperty C) →
              CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
-- Mathlib.Tactic.Simproc.Divisors
/-- The dsimproc `Nat.properDivisors_ofNat` computes the finset `Nat.properDivisors n` when
`n` is a numeral. For instance, this simplifies `Nat.properDivisors 12` to `{1, 2, 3, 4, 6}`.  -/
Nat.properDivisors_ofNat : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.π₂_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  {X Y : CategoryTheory.Limits.CategoricalPullback F G} (f : X ⟶ Y),
  (CategoryTheory.Limits.CategoricalPullback.π₂ F G).map f = f.snd
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  (Std.DTreeMap.Raw.Const.toList t).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The cone points of two limit cones for naturally isomorphic functors
are themselves isomorphic.
 -/
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cone F} →
            {t : CategoryTheory.Limits.Cone G} →
              CategoryTheory.Limits.IsLimit s → CategoryTheory.Limits.IsLimit t → (F ≅ G) → (s.pt ≅ t.pt)
-- Mathlib.Data.List.Map2
List.zipLeft_eq_zipLeft' : ∀ {α : Type u} {β : Type v} (as : List α) (bs : List β), as.zipLeft bs = (as.zipLeft' bs).1
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instLocallyOfFiniteTypeMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.LocallyOfFiniteType (f ∣_ V)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an isomorphism in `P.Under Q X` from an isomorphism in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Under.isoMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      {X : T} →
        [inst_1 : Q.IsMultiplicative] →
          [Q.RespectsIso] →
            {A B : P.Under Q X} →
              (f : A.right ≅ B.right) →
                autoParam (CategoryTheory.CategoryStruct.comp A.hom f.hom = B.hom)
                    CategoryTheory.MorphismProperty.Under.isoMk._auto_1 →
                  (A ≅ B)
-- Init.Data.Fin.Iterate
_private.Init.Data.Fin.Iterate.0.Fin.hIterateFrom_elim : ∀ {P : ℕ → Sort u_1} (Q : (i : ℕ) → P i → Prop) {n : ℕ} (f : (i : Fin n) → P ↑i → P (↑i + 1)) {i : ℕ} (ubnd : i ≤ n)
  (s : P i), Q i s → (∀ (k : Fin n) (s : P ↑k), Q (↑k) s → Q (↑k + 1) (f k s)) → Q n (Fin.hIterateFrom P f i ubnd s)
-- Batteries.Tactic.Trans
/-- Expression for transitive relation.  -/
Batteries.Tactic.TransRelation.app : Lean.Expr → Batteries.Tactic.TransRelation
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.type : Lean.Meta.SynthInstanceCacheKey → Lean.Expr
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.instMul : {α : Type u_2} → {x : NonAssocSemiring α} → Mul (α →+* α)
-- Mathlib.Algebra.Homology.LocalCohomology
/-- `localCohomology J i` is `i`-th the local cohomology module of a module `M` over
a commutative ring `R` with support in the ideal `J` of `R`, defined as the direct limit
of `Ext^i(R/J^t, M)` over all powers `t : ℕ`.  -/
localCohomology : {R : Type u} → [inst : CommRing R] → Ideal R → ℕ → CategoryTheory.Functor (ModuleCat R) (ModuleCat R)
-- Mathlib.Data.FunLike.Basic
/-- The class `DFunLike F α β` expresses that terms of type `F` have an
injective coercion to (dependent) functions from `α` to `β`.

For non-dependent functions you can also use the abbreviation `FunLike`.

This typeclass is used in the definition of the homomorphism typeclasses,
such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, ....
 -/
DFunLike : Sort u_1 → (α : outParam (Sort u_2)) → outParam (α → Sort u_3) → Sort (max (max (max 1 u_1) u_2) u_3)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_add_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_add_sdiff._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_add_sdiff._auto_3 → μ.real s + μ.real (t \ s) = μ.real (s ∪ t)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Iso.homCongr_eq_arrowCongr : ∀ {S : Type u} [inst : CommRing S] {X Y X' Y' : ModuleCat S} (i : X ≅ X') (j : Y ≅ Y') (f : X ⟶ Y),
  (i.homCongr j) f = { hom' := (i.toLinearEquiv.arrowCongr j.toLinearEquiv) (ModuleCat.Hom.hom f) }
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.inv Z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)
-- Init.Data.List.Find
List.getLast_flatten : ∀ {α : Type u_1} {L : List (List α)} (h : ∃ l ∈ L, l ≠ []),
  L.flatten.getLast ⋯ = (List.findSome? List.getLast? L.reverse).get ⋯
-- Mathlib.Algebra.Field.Rat
Rat.instDivisionRing : DivisionRing ℚ
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.contDiff : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {Y : Type u_2} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] [inst_4 : NormedAddCommGroup Y] [inst_5 : NormedSpace ℝ Y]
  [inst_6 : DiffeologicalSpace Y] [Diffeology.IsContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y},
  Diffeology.DSmooth f → ContDiff ℝ (↑⊤) f
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluate the product of two normalized expressions in `R` using `ring`.  -/
Mathlib.Tactic.Algebra.RingCompute.neg : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Algebra.Cache sR →
              {a : Q(«$A»)} →
                (_rA : Q(CommRing «$A»)) →
                  Mathlib.Tactic.Algebra.BaseType sAlg a →
                    Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.BaseType sAlg) q(-«$a»))
-- Mathlib.Data.Set.Disjoint
/-- **Alias** of the forward direction of `Set.disjoint_left`. -/
Disjoint.notMem_of_mem_left : ∀ {α : Type u} {s t : Set α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_iff_exists_edge_coe : ∀ {V : Type u} {G : SimpleGraph V} {a b : V}, G.Adj a b ↔ ∃ e, ↑e = s(a, b)
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeLinearEquiv_apply_coe : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (i : ι) (x : ↥(ℳ i)),
  (DirectSum.decomposeLinearEquiv ℳ) ↑x = (DirectSum.lof R ι (fun i => ↥(ℳ i)) i) x
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂ : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a b : ℕ),
  (ProbabilityTheory.Kernel.partialTraj κ a (b + 1)).map (Preorder.frestrictLe₂ ⋯) =
    ProbabilityTheory.Kernel.partialTraj κ a b
-- Mathlib.Data.Rat.Init
NNRatCast.toCoeHTCT : {K : Type u_1} → [NNRatCast K] → CoeHTCT ℚ≥0 K
-- Mathlib.Data.Int.Interval
Int.Icc_eq_finset_map : ∀ (a b : ℤ), Finset.Icc a b = Finset.map (Nat.castEmbedding.trans (addLeftEmbedding a)) (Finset.range (b + 1 - a).toNat)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.upper : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RxoIterator α β → α
-- Mathlib.GroupTheory.Sylow
/-- If `G` has a normal Sylow `p`-subgroup, then it is the only Sylow `p`-subgroup.  -/
Sylow.unique_of_normal : {G : Type u} →
  [inst : Group G] →
    {p : ℕ} → [Fact (Nat.Prime p)] → [Finite (Sylow p G)] → (P : Sylow p G) → (↑P).Normal → Unique (Sylow p G)
-- Mathlib.Algebra.Group.Subgroup.Map
AddMonoidHom.addSubgroupComap.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G') (H' : AddSubgroup G'),
  f.addSubgroupComap H' = f.addSubmonoidComap H'.toAddSubmonoid
-- Init.Control.Lawful.Basic
seq_eq_bind_map : ∀ {m : Type u → Type u_1} {α β : Type u} [inst : Monad m] [LawfulMonad m] (f : m (α → β)) (x : m α),
  f <*> x = do
    let x_1 ← f
    x_1 <$> x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A], NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
-- Mathlib.Topology.NhdsSet
nhdsSet_eq_principal_iff : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, nhdsSet s = Filter.principal s ↔ IsOpen s
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.graph.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (f : G →+ H),
  f.graph = { toAddSubmonoid := f.mgraph, neg_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a normed ring is also a normed ring, with the restriction of the norm.  -/
Subalgebra.normedRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} → [inst_1 : NormedRing E] → [inst_2 : Algebra 𝕜 E] → (s : Subalgebra 𝕜 E) → NormedRing ↥s
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mop_hom_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).hom.mop = (β_ { unmop := Y } { unmop := X }).hom
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.centralAlgebraMul_apply : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V) {z : MonoidAlgebra A G}
  (hz : z ∈ Submonoid.center (MonoidAlgebra A G)) (v : V),
  (Representation.IntertwiningMap.centralAlgebraMul ρ hz) v = (ρ.asAlgebraHom z) v
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eraseKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getValue? k (Std.Internal.List.eraseKey k l) = none
-- Init.Data.List.MinMaxIdx
List.minIdxOn_cons : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α}
  {f : α → β},
  List.minIdxOn f (x :: xs) ⋯ =
    if h : xs = [] then 0 else if f x ≤ f (List.minOn f xs h) then 0 else List.minIdxOn f xs h + 1
-- Mathlib.Logic.Equiv.Fin.Basic
/-- Equivalence between `Fin n ⊕ ℕ` and `ℕ` that sends `inl (a : Fin n)` to
`(a : ℕ)` and `inr a` to `n + a`.  -/
finSumNatEquiv : (n : ℕ) → Fin n ⊕ ℕ ≃ ℕ
-- Mathlib.Analysis.Convex.Combination
affineCombination_mem_convexHull : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Finset ι} {v : ι → E} {w : ι → R},
  (∀ i ∈ s, 0 ≤ w i) → s.sum w = 1 → (Finset.affineCombination R s v) w ∈ (convexHull R) (Set.range v)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.generateFrom_inter_toPlots : ∀ {X : Type u_1} (d₁ d₂ : DiffeologicalSpace X), DiffeologicalSpace.generateFrom (d₁.toPlots ∩ d₂.toPlots) = d₁ ⊓ d₂
-- Mathlib.Combinatorics.Configuration
Configuration.instFintypeDual : (P : Type u_1) → [h : Fintype P] → Fintype (Configuration.Dual P)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Monotone.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [inst_2 : ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ},
  Monotone u → IntervalIntegrable u μ a b
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrHyp.mk.sizeOf_spec : ∀ (lhsIdx rhsIdx hypIdx : ℕ) (hypsPos : List (Option ℕ)) (isContra : Bool),
  sizeOf { lhsIdx := lhsIdx, rhsIdx := rhsIdx, hypIdx := hypIdx, hypsPos := hypsPos, isContra := isContra } =
    1 + sizeOf lhsIdx + sizeOf rhsIdx + sizeOf hypIdx + sizeOf hypsPos + sizeOf isContra
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Typecheck a `MonoidHom` as a morphism in `CommMonCat`.  -/
CommMonCat.ofHom : {X Y : Type u} → [inst : CommMonoid X] → [inst_1 : CommMonoid Y] → (X →* Y) → (CommMonCat.of X ⟶ CommMonCat.of Y)
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toAddGroup : {R : Type u} → [self : AddGroupWithOne R] → AddGroup R
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.SectionKind.hyp : Mathlib.Tactic.ClickSuggestions.SectionKind
-- Mathlib.Algebra.Order.Ring.Basic
add_sq_le : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} [ExistsAddOfLE R],
  (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
_private.Mathlib.Algebra.Algebra.Subalgebra.Lattice.0.Algebra.delabAdjoinNotation.delabInsertArray : Lean.PrettyPrinter.Delaborator.DelabM (List Lean.Term)
-- Mathlib.Order.Disjoint
Complementeds.instMax : {α : Type u_1} → [inst : DistribLattice α] → [inst_1 : BoundedOrder α] → Max (Complementeds α)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prod_comp : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M₂ →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄)
  (h : M →ₗ[R] M₂), f.prod g ∘ₗ h = (f ∘ₗ h).prod (g ∘ₗ h)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSignatureHelpParams.toJson : Lean.Lsp.SignatureHelpParams → Lean.Json
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_add_iff_left : ∀ {a b c : ℕ}, a ∣ c → (a.Coprime (b + c) ↔ a.Coprime b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.map_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a}, Std.ExtDTreeMap.map f t = ∅ ↔ t = ∅
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.hasLimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (J : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} J]
  [CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.HasLimitsOfShape J (CategoryTheory.AsSmall C)
-- Mathlib.Order.Partition.Finpartition
Finpartition.exists_le_of_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a b : α} {P Q : Finpartition a},
  P ≤ Q → b ∈ Q.parts → ∃ c ∈ P.parts, c ≤ b
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.le_vanishingIdeal_zeroLocus : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), I ≤ PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstFields.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Defs
CommMagma.to_isCommutative : ∀ {G : Type u_1} [inst : CommMagma G], IsMulCommutative G
-- Mathlib.Data.Num.Bitwise
/-- Add a bit at the end of a `NzsNum`.  -/
NzsNum.«term_::_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.mk : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} →
      (pt : Type w₁) →
        (ι : (j : J) → F.obj j → pt) →
          autoParam (∀ {j j' : J} (f : j ⟶ j'), ι j' ∘ ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) = ι j)
              CategoryTheory.Functor.CoconeTypes.ι_naturality._autoParam →
            F.CoconeTypes
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.eqToIso_inv : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ = S₂), (SSet.Subcomplex.eqToIso h).inv = SSet.Subcomplex.homOfLE ⋯
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.induce_eq_top : ∀ {α : Type u_1} {G : SimpleGraph α} {s : Set α}, SimpleGraph.induce s G = ⊤ ↔ G.IsClique s