mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
apply_le_nnnorm_cfc_nnreal : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄,
  x ∈ spectrum NNReal a →
    autoParam (ContinuousOn f (spectrum NNReal a)) apply_le_nnnorm_cfc_nnreal._auto_1 →
      autoParam (0 ≤ a) apply_le_nnnorm_cfc_nnreal._auto_3 → f x ≤ ‖cfc f a‖₊
-- Mathlib.Algebra.Group.End
Equiv.neg_addRight : ∀ {α : Type u_4} [inst : AddGroup α] (a : α), (Equiv.addRight a)⁻¹ = Equiv.addRight (-a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_eq_fallback : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {a : α} {fallback : β}, a ∉ t → Std.DTreeMap.Internal.Impl.Const.getD t a fallback = fallback
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- A `ForIn'` instance for iterators. Its generic membership relation is not easy to use,
so this is not marked as `instance`. This way, more convenient instances can be built on top of it
or future library improvements will make it more comfortable.
 -/
Std.IterM.instForIn' : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    {α β : Type w} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m n] →
          [Monad n] →
            [MonadLiftT m n] → ForIn' n (Std.IterM m β) β { mem := fun it out => it.IsPlausibleIndirectOutput out }
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_le_iff_le_comap : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S} {s : Subsemiring R}
  {t : Subsemiring S}, Subsemiring.map f s ≤ t ↔ s ≤ Subsemiring.comap f t
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.elim_some : ∀ {X : Type u_1} {Y : Type u_2} (y : Y) (f : X → Y) (x : X), (↑x).elim y f = f x
-- Mathlib.Algebra.Lie.Quotient
/-- The first isomorphism theorem for morphisms of Lie algebras.  -/
LieHom.quotKerEquivRange : {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'] → (f : L →ₗ⁅R⁆ L') → (L ⧸ f.ker) ≃ₗ⁅R⁆ ↥f.range
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `s` is closed, being locally integrable on `s` w.r.t. `μ` is equivalent to being locally
integrable with respect to `μ.restrict s`. For the one-way implication without assuming `s` closed,
see `locallyIntegrableOn_of_locallyIntegrable_restrict`.  -/
MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X],
  IsClosed s → (MeasureTheory.LocallyIntegrableOn f s μ ↔ MeasureTheory.LocallyIntegrable f (μ.restrict s))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLE!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited ((a : α) × β a)],
          Std.DTreeMap.Internal.Impl.getEntryLE! k t₁ = Std.DTreeMap.Internal.Impl.getEntryLE! k t₂
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperSemicontinuousOn_iff_frequently`. -/
UpperSemicontinuousOn.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  UpperSemicontinuousOn f s → ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- Given `C^n` manifolds `M` and `N`, `Sum.inl : M → M ⊕ N` is a `C^n` embedding.  -/
Manifold.IsSmoothEmbedding.sumInl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] {H : Type u_6} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_14}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'],
  Manifold.IsSmoothEmbedding I I n Sum.inl
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.IsLimit.lift.congr_simp : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.WeightedCone W F}
  (hc hc_1 : c.IsLimit),
  hc = hc_1 →
    ∀ {Z : C} (π π_1 : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j)) (e_π : π = π_1)
      (hπ :
        ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
          CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)),
      hc.lift π hπ = hc_1.lift π_1 ⋯
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The isomorphism from `Matrix.SpecialLinearGroup n R`
to the special linear group of a module associated with a basis of that module.  -/
Matrix.SpecialLinearGroup.toLin_equiv : {R : Type u_1} →
  {V : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] →
          {n : Type u_3} →
            [inst_3 : Fintype n] →
              [inst_4 : DecidableEq n] → Module.Basis n R V → Matrix.SpecialLinearGroup n R ≃* SpecialLinearGroup R V
-- Mathlib.Dynamics.Flow
/-- A set `s ⊆ α` is invariant under `ϕ : τ → α → α` if `ϕ t s ⊆ s` for all `t` in `τ`.  -/
IsInvariant : {τ : Type u_1} → {α : Type u_2} → (τ → α → α) → Set α → Prop
-- Mathlib.RingTheory.Localization.Integral
_private.Mathlib.RingTheory.Localization.Integral.0.IsLocalization.exists_integer_polynomial_multiple_and_support_subset : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] (p : Polynomial S),
  ∃ b ∈ M, ∃ q, Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_shiftLeft_of_lt : ∀ (a b : UInt32), b < 32 → (a <<< b).toUInt64 = a.toUInt64 <<< b.toUInt64 % 4294967296
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (φ : G ≃ₜ* G),
  MeasureTheory.mulEquivHaarChar φ =
    MeasureTheory.Measure.haar.haarScalarFactor (MeasureTheory.Measure.map (⇑φ) MeasureTheory.Measure.haar)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.sub` -/
TendstoUniformly.fun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l →
    TendstoUniformly f' g' l → TendstoUniformly (fun i i_1 => f i i_1 - f' i i_1) (fun i => g i - g' i) l
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_unitIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.Preadditive.commGrpEquivalence.unitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : C ⥤ᵣ D) (X : D ⥤ᵣ E),
  (((CategoryTheory.RightExactFunctor.whiskeringLeft C D E).obj F).obj X).obj = F.obj.comp X.obj
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X} (k : f ⟶ g)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left k.hom)
      (CategoryTheory.CategoryStruct.comp g.arrow h) =
    CategoryTheory.CategoryStruct.comp f.arrow h
-- Mathlib.Data.Num.Bitwise
/-- The opposite of a `SNum`.  -/
SNum.neg : SNum → SNum
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.M : Type → Type
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_le_powerset : ∀ {α : Type u_1} (n : ℕ) (s : Multiset α), Multiset.powersetCard n s ≤ s.powerset
-- Mathlib.Analysis.Normed.Ring.Lemmas
SeparationQuotient.instNonUnitalNormedRing : {α : Type u_1} → [inst : NonUnitalSeminormedRing α] → NonUnitalNormedRing (SeparationQuotient α)
-- Mathlib.Data.Nat.Prime.Defs
Nat.irreducible_iff_prime : ∀ {p : ℕ}, Irreducible p ↔ Prime p
-- Lean.Meta.Sym.Pattern
/-- `isDefEqMain` implementation.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isDefEqMainImpl : Lean.Expr → Lean.Expr → Lean.Meta.Sym.DefEqM✝ Bool
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
/-- For presheaves valued in a concrete category, whose forgetful functor reflects isomorphisms and
preserves limits, the sheaf condition in terms of unique gluings is equivalent to the usual one.
 -/
TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Presheaf C X), F.IsSheaf ↔ F.IsSheafUniqueGluing
-- Init.Data.SInt.Lemmas
Int16.toInt_ofIntClamp : ∀ {x : ℤ}, Int16.minValue.toInt ≤ x → x ≤ Int16.maxValue.toInt → (Int16.ofIntClamp x).toInt = x
-- Mathlib.RepresentationTheory.Basic
Representation.ofMulDistribMulAction_apply_apply : ∀ (M : Type u_1) (G : Type u_2) [inst : Monoid M] [inst_1 : CommGroup G] [inst_2 : MulDistribMulAction M G] (g : M)
  (a : Additive G), ((Representation.ofMulDistribMulAction M G) g) a = Additive.ofMul (g • Additive.toMul a)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Embedding of a submodule `p` to the ambient space `M`.  -/
SubAddAction.subtype : {R : Type u} → {M : Type v} → [inst : VAdd R M] → (p : SubAddAction R M) → ↥p →ₑ[id] M
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.instStarHomClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Star A] [inst_3 : Star B],
  StarHomClass (A ≃⋆* B) A B
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
HomotopicalAlgebra.ModelCategory.cm3b : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.End.equivMulOpposite_symm_apply_apply : ∀ {M : Type u_2} [inst : Monoid M] (m : Mᵐᵒᵖ) (x : M),
  (MulActionHom.End.equivMulOpposite.symm m) x = x * MulOpposite.unop m
-- Mathlib.Order.LiminfLimsup
Filter.liminf_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α] (u : β → α) (v : γ → β)
  (f : Filter γ), Filter.liminf (u ∘ v) f = Filter.liminf u (Filter.map v f)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.le_posPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  {a : A}, autoParam (IsSelfAdjoint a) CFC.le_posPart._auto_1 → a ≤ a⁺
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.comap_id : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α),
  BooleanSubalgebra.comap (BoundedLatticeHom.id α) L = L
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_mul_inv_iff_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, 1 < a * b⁻¹ ↔ b < a
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.instInhabitedForwardRuleMatches.default : Aesop.ForwardRuleMatches
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  [inst_1 : SizeOf C] {k k' : ℕ} (hk : k < n) (hk' : k' < n) (j : (X k hk).fst) (j' : (X k' hk').fst)
  (a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j'),
  sizeOf (CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq✝ hk hk' j j' a a_1) =
    1 + sizeOf k + sizeOf k' + sizeOf hk + sizeOf hk' + sizeOf j + sizeOf j' + sizeOf a + sizeOf a_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- If the support of the simple graph `G` is a subset of the set `s`, then the induced subgraph of
`s` has the same number of edges as `G`.  -/
SimpleGraph.card_edgeFinset_induce_of_support_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj], G.support ⊆ s → (SimpleGraph.induce s G).edgeFinset.card = G.edgeFinset.card
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
  (f : ↑(X.presheaf.obj (Opposite.op U))), IsNilpotent f → X.toRingedSpace.basicOpen f = ⊥
-- Mathlib.GroupTheory.Perm.Sign
_private.Mathlib.GroupTheory.Perm.Sign.0.Equiv.Perm.signAux2.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Equiv.Perm α → Sort u_2) (x : α) (l : List α) (f : Equiv.Perm α)
  (h_1 : (x : Equiv.Perm α) → motive [] x) (h_2 : (x : α) → (l : List α) → (f : Equiv.Perm α) → motive (x :: l) f),
  (match x :: l, f with
    | [], x => h_1 x
    | x :: l, f => h_2 x l f) =
    h_2 x l f
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_ndunion : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s₁ s₂ : Multiset α), (s₁.ndunion s₂).lcm = lcm s₁.lcm s₂.lcm
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly.eq_1 : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L), φ.polyCharpoly b = φ.polyCharpolyAux b (Module.Free.chooseBasis R M)
-- Mathlib.LinearAlgebra.Multilinear.Curry
LinearMap.curryMid_uncurryMid : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (i : Fin (n + 1))
  (f : M i →ₗ[R] MultilinearMap R (fun j => M (i.succAbove j)) M₂),
  MultilinearMap.curryMid i (LinearMap.uncurryMid i f) = f
-- Std.Data.DHashMap.Lemmas
/-- Internal implementation detail of the hash map.  -/
Std.DHashMap.isSetoid : (α : Type u_1) → (β : α → Type u_2) → [inst : BEq α] → [inst_1 : Hashable α] → Setoid (Std.DHashMap α β)
-- Mathlib.Order.Fin.Basic
Fin.castSuccOrderEmb_toEmbedding : ∀ {n : ℕ}, Fin.castSuccOrderEmb.toEmbedding = { toFun := Fin.castSucc, inj' := ⋯ }
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.Aesop.tactic_clause.quot : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_zero : ∀ (L : PeriodPair) (l₀ : ℂ), L.weierstrassPExcept l₀ 0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_union_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₂ = false →
    Std.DTreeMap.Internal.Impl.Const.get? (m₁.union m₂ ⋯ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.RepresentationTheory.Semisimple
Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V),
  ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule (MonoidAlgebra k G) ρ.asModule
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instLE : {M : Type u_2} →
  [inst : AddCommMonoid M] → [inst_1 : LinearOrder M] → [IsOrderedCancelAddMonoid M] → LE (DivisibleHull M)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendIso_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X),
  (s.extendIso f).hom.hom = f.hom
-- Mathlib.Data.Finset.Sups
/-- `sᶜˢ` is the finset of elements of the form `aᶜ` where `a ∈ s`.  -/
FinsetFamily.«term_ᶜˢ» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.mk : {R : Type u_2} →
  [inst : NonUnitalNonAssocRing R] →
    (toAddGroupSeminorm : AddGroupSeminorm R) →
      (∀ (x y : R), toAddGroupSeminorm.toFun (x * y) ≤ toAddGroupSeminorm.toFun x * toAddGroupSeminorm.toFun y) →
        RingSeminorm R
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.nextCoeff.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
  p.nextCoeff = if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.comp_mem_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (i : X ⟶ Y) (f : Y ⟶ Z) [CategoryTheory.IsIso i]
  (S : CategoryTheory.Sieve Z), S.arrows (CategoryTheory.CategoryStruct.comp i f) ↔ S.arrows f
-- Mathlib.RingTheory.WittVector.Compare
TruncatedWittVector.zmodEquivTrunc_apply : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {x : ZMod (p ^ n)},
  (TruncatedWittVector.zmodEquivTrunc p n) x = (ZMod.castHom ⋯ (TruncatedWittVector p n (ZMod p))) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k : α},
  k ∈ Std.DHashMap.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') (Std.DHashMap.Const.get m k h') = true
-- Mathlib.RingTheory.Valuation.AlgebraInstances
ValuationSubring.isIntegral_of_mem_ringOfIntegers : ∀ {K : Type u_1} [inst : Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) (L : Type u_2) [inst_1 : Field L]
  [inst_2 : Algebra K L] {x : L} (hx : x ∈ integralClosure (↥v.valuationSubring) L),
  IsIntegral ↥v.valuationSubring ⟨x, hx⟩
-- Mathlib.RingTheory.IsAdjoinRoot
/-- `IsAdjoinRootMonic S f` states that the ring `S` can be constructed by adjoining a specified
root of the monic polynomial `f : R[X]` to `R`.

As long as `f` is monic, there is a well-defined representation of elements of `S` as polynomials
in `R[X]` of degree lower than `deg f` (see `modByMonicHom` and `coeff`). In particular,
we have `IsAdjoinRootMonic.powerBasis`.

Bundling `Monic` into this structure is very useful when working with explicit `f`s such as
`X^2 - C a * X - C b` since it saves you carrying around the proofs of monicity.
 -/
IsAdjoinRootMonic : {R : Type u} →
  (S : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring S] → [Algebra R S] → Polynomial R → Type (max u v)
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.expectedType? : Lean.Elab.PartialTermInfo → Option Lean.Expr
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
MeasureTheory.exp_llr_of_ac' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  ν.AbsolutelyContinuous μ → (fun x => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => (μ.rnDeriv ν x).toReal
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
/-- The set of all cylinders based on closed compact sets. Note that such a set is closed, but
not compact in general (for instance, the whole space is always a closed compact cylinder).  -/
MeasureTheory.closedCompactCylinders : {ι : Type u_1} → (X : ι → Type u_2) → [(i : ι) → TopologicalSpace (X i)] → Set (Set ((i : ι) → X i))
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_irrefl' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {f' : α → E'} {l : Filter α},
  (∃ᶠ (x : α) in l, ‖f' x‖ ≠ 0) → ¬f' =o[l] f'
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.boundedSpace : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [inst_1 : ∀ (n : ℕ), DiscreteTopology (E n)],
  BoundedSpace ((n : ℕ) → E n)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_of_le_ge_cert.eq_1 : ∀ (p₁ p₂ : Lean.Grind.Linarith.Poly), Lean.Grind.Linarith.eq_of_le_ge_cert p₁ p₂ = (p₂ == p₁.mul (-1))
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFiniteType f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FiniteType
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubalgebra R L → Submodule R L
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
EuclideanGeometry.angle_pointReflection_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = Real.pi - EuclideanGeometry.angle p₁ p₂ p₃
-- Init.Data.BitVec.BasicAux
/-- Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction
modulo `2^n`. Usually accessed via the `-` operator.

 -/
BitVec.sub : {n : ℕ} → BitVec n → BitVec n → BitVec n
-- Mathlib.Algebra.Algebra.Hom
AlgHom.congr_arg : ∀ {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] (φ : A →ₐ[R] B) {x y : A}, x = y → φ x = φ y
-- Lean.Meta.Injective
Lean.Meta.mkInjectiveTheorems : Lean.Name → Lean.MetaM Unit
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toLinearMap₁₂_apply : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (L : E →SL[σ₁₃] F →SL[σ₂₃] G),
  ContinuousLinearMap.toLinearMap₁₂ L = ContinuousLinearMap.coeLMₛₗ σ₂₃ ∘ₛₗ ↑L
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasCoequalizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasCoequalizers C
-- Mathlib.Data.Real.Sign
Real.inv_sign : ∀ (r : ℝ), r.sign⁻¹ = r.sign