mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.measurable_coe_ennreal_comp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X NNReal), Measurable fun x => ↑(f x)
-- Mathlib.Data.FP.Basic
FP.Float.instAdd : [C : FP.FloatCfg] → Add FP.Float
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.emphLike.noSpaceBefore : Char → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Topology.Order.LeftRightLim
rightLim_rightLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T3Space β] {f : α → β} {a : α},
  Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds (Function.rightLim f a)) →
    Function.rightLim (Function.rightLim f) a = Function.rightLim f a
-- Mathlib.Data.Set.Semiring
SetSemiring.imageHom_def : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (s : SetSemiring α),
  (SetSemiring.imageHom f) s = Set.up (⇑f '' SetSemiring.down s)
-- Mathlib.Topology.Constructible
/-- **Alias** of the reverse direction of `Topology.isConstructible_compl`. -/
Topology.IsConstructible.compl : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Topology.IsConstructible s → Topology.IsConstructible sᶜ
-- Mathlib.MeasureTheory.MeasurableSpace.Invariants
/-- Given a self-map `f : α → α`,
`invariants f` is the σ-algebra of measurable sets that are invariant under `f`.

A set `s` is `(invariants f)`-measurable
iff it is measurable w.r.t. the canonical σ-algebra on `α` and `f ⁻¹' s = s`.  -/
MeasurableSpace.invariants : {α : Type u_1} → [m : MeasurableSpace α] → (α → α) → MeasurableSpace α
-- Init.Data.UInt.Bitwise
UInt16.not_ne_self : ∀ {a : UInt16}, ~~~a ≠ a
-- Mathlib.Data.Num.Basic
instDecidableEqZNum.decEq : (x x_1 : ZNum) → Decidable (x = x_1)
-- Mathlib.Analysis.InnerProductSpace.PiL2
_private.Mathlib.Analysis.InnerProductSpace.PiL2.0.DirectSum.IsInternal.subordinateOrthonormalBasisIndexFiberEquiv : {ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              [inst_4 : FiniteDimensional 𝕜 E] →
                {n : ℕ} →
                  (hn : Module.finrank 𝕜 E = n) →
                    [inst_5 : DecidableEq ι] →
                      {V : ι → Submodule 𝕜 E} →
                        (hV : DirectSum.IsInternal V) →
                          (hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
                            (i : ι) →
                              { a // DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn hV a hV' = i } ≃
                                Fin (Module.finrank 𝕜 ↥(V i))
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subLeft.eq_1 : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  IsometryEquiv.subLeft c = { toEquiv := Equiv.subLeft c, isometry_toFun := ⋯ }
-- Mathlib.Order.SuccPred.Basic
Order.Ici_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), Set.Ici (Order.succ a) = Set.Ioi a
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.Monic.degree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).degree = p.degree + q.degree
-- Mathlib.Algebra.Algebra.Operations
/-- Sub-R-modules of an R-algebra A form a semiring.  -/
Submodule.instIdemCommSemiring : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → IdemCommSemiring (Submodule R A)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.ae_integrable_of_integrable_comp : ∀ {α : Type u_5} {β : Type u_6} {E : Type u_7} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : MeasureTheory.Measure α} {f : β → E},
  MeasureTheory.Integrable f (μ.bind ⇑κ) → ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable f (κ x)
-- Lean.Elab.Match
Lean.Elab.Term.GeneralizeResult.mk.injEq : ∀ (discrs : Array Lean.Elab.Term.Discr) (toClear : Array Lean.FVarId) (matchType : Lean.Expr)
  (altViews : Array Lean.Elab.Term.TermMatchAltView) (refined : Bool) (discrs_1 : Array Lean.Elab.Term.Discr)
  (toClear_1 : Array Lean.FVarId) (matchType_1 : Lean.Expr) (altViews_1 : Array Lean.Elab.Term.TermMatchAltView)
  (refined_1 : Bool),
  ({ discrs := discrs, toClear := toClear, matchType := matchType, altViews := altViews, refined := refined } =
      { discrs := discrs_1, toClear := toClear_1, matchType := matchType_1, altViews := altViews_1,
        refined := refined_1 }) =
    (discrs = discrs_1 ∧ toClear = toClear_1 ∧ matchType = matchType_1 ∧ altViews = altViews_1 ∧ refined = refined_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
OneHom.mulSingle_apply : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] (i : I) (x : f i),
  (OneHom.mulSingle f i) x = Pi.mulSingle i x
-- Mathlib.LinearAlgebra.Dimension.Localization
IsBaseChange.rank_eq_of_le_nonZeroDivisors : ∀ {R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N)
  [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R →
    ∀ [Module.Free S N] [StrongRankCondition S] {T : Type uT} [inst_13 : CommRing T] [inst_14 : Algebra R T],
      Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T →
        ∀ [StrongRankCondition (TensorProduct R S T)] {P : Type uM} [inst_16 : AddCommGroup P] [inst_17 : Module R P]
          [inst_18 : Module T P] [inst_19 : IsScalarTower R T P] {g : M →ₗ[R] P},
          IsBaseChange T g → Module.rank T P = Module.rank R M
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.intCast_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (n : ℤ), (↑n).toProd.2 = ↑n
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.optionEquivLeft_symm_X : ∀ (R : Type u) (S₁ : Type v) [inst : CommSemiring R],
  (MvPolynomial.optionEquivLeft R S₁).symm Polynomial.X = MvPolynomial.X none
-- Init.Grind.Ring.Basic
Lean.Grind.PowIdentity.mk : ∀ {α : Type u} [inst : Lean.Grind.CommSemiring α] {p : outParam ℕ}, (∀ (x : α), x ^ p = x) → Lean.Grind.PowIdentity α p
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_hom_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g),
  CategoryTheory.CategoryStruct.comp (F.map₂ η.hom) (F.map₂ η.inv) = CategoryTheory.CategoryStruct.id (F.map f)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint_mem_affineSpan : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)), s.touchpoint signs i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relations_G : ∀ (R : Type u) [inst : CommRing R] (ι : Type u_4) [inst_1 : DecidableEq ι] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], (exteriorPower.presentation.relations R ι M).G = (ι → M)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.instPowInt : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → Pow (C ≌ C) ℤ
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Runs the Simplex Algorithm inside the `SimplexAlgorithmM`. It always terminates, finding solution if
such exists.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.runSimplexAlgorithm : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Unit
-- Aesop.Stats.Extension
Aesop.StatsExtensionEntry.position? : Aesop.StatsExtensionEntry → Option Lean.Position
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- **Alias** of `MeasureTheory.AEStronglyMeasurable.fun_const_vadd`.

---

Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.const_vadd` -/
MeasureTheory.AEStronglyMeasurable.const_vadd' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {𝕜 : Type u_5} [inst_1 : VAdd 𝕜 β] [ContinuousConstVAdd 𝕜 β],
  MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (fun i => c +ᵥ f i) μ
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factors_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y),
  P.Factors f ↔ (CategoryTheory.Subobject.representative.obj P).Factors f
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.foldM_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α m n] [inst_11 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o] [inst_14 : MonadLiftT m n] [inst_15 : MonadLiftT n o]
  [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → o δ} {init : δ}
  {it : Std.IterM m β} {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← liftM (f b).run
          g d c)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.IterM.mapWithPostcondition f it) ⦃ Q; eQ ⦄
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the left by a nonnegative element preserves antitonicity.  -/
Antitone.const_smul : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → β}, Antitone f → 0 ≤ a → Antitone fun x => a • f x
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LocalizedModule.map.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_3} [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  LocalizedModule.map S =
    IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
      (Localization S)
-- Mathlib.Topology.Constructions.SumProd
continuous_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Continuous Prod.fst
-- Mathlib.Analysis.Convex.Approximation
LowerSemicontinuousOn.isClosed_re_epigraph : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E],
  IsClosed s → LowerSemicontinuousOn φ s → IsClosed {p | p.1 ∈ s ∧ φ p.1 ≤ RCLike.re p.2}
-- Mathlib.Topology.Specialization
/-- `toEquiv` is the "identity" function to the `Specialization` of a type.  -/
Specialization.toEquiv : {α : Type u_1} → α ≃ Specialization α
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The `addGroupFilterBasis` induced by the filter basis `Seminorm.basisSets`.  -/
SeminormFamily.addGroupFilterBasis : {R : Type u_1} →
  {E : Type u_6} →
    {ι : Type u_9} →
      [inst : SeminormedRing R] →
        [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → SeminormFamily R E ι → AddGroupFilterBasis E
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.const abv (x * y) = CauSeq.const abv x * CauSeq.const abv y
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.χ_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type (max u v))} (m : F ⟶ G) [inst_1 : CategoryTheory.Mono m],
  (CategoryTheory.Sheaf.χ m).hom = CategoryTheory.Subfunctor.lift (CategoryTheory.Presheaf.χ m.hom) ⋯
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.isConstructible_toSet : ∀ {R : Type u_1} [inst : CommSemiring R] (S : PrimeSpectrum.ConstructibleSetData R), Topology.IsConstructible S.toSet
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mk_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A : C} (f : A ⟶ X) [hf : CategoryTheory.Mono f],
  (CategoryTheory.MonoOver.mk f).obj = CategoryTheory.Over.mk f
-- Mathlib.Analysis.Normed.Module.Basic
nnnorm_algebraMap : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  (x : 𝕜), ‖(algebraMap 𝕜 𝕜') x‖₊ = ‖x‖₊ * ‖1‖₊
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_swap : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {x y : α}, x ≠ y → (Equiv.swap x y).support = {x, y}
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.hasNoetherianRange_iff_quotient_ker : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Ring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasNoetherianRange ↔ IsNoetherian K (V ⧸ f.ker)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul : ∀ {ι : Type u_1} [inst : DecidableEq ι] {G : ι → Type u_4} [inst_1 : (i : ι) → Group (G i)]
  [inst_2 : (i : ι) → DecidableEq (G i)] {i : ι} (w : Monoid.CoprodI.Word G),
  ((Monoid.CoprodI.Word.equivPair i) w).tail = (Monoid.CoprodI.of ((Monoid.CoprodI.Word.equivPair i) w).head)⁻¹ • w
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.id_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.Hom.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
/-- The kernel of a homological functor `F : C ⥤ A` is the strictly full
triangulated subcategory consisting of objects `X` such that
for all `n : ℤ`, `F.obj (X⟦n⟧)` is zero.  -/
CategoryTheory.Functor.homologicalKernel : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.HasShift C ℤ] →
        [inst_2 : CategoryTheory.Category.{v_3, u_3} A] → CategoryTheory.Functor C A → CategoryTheory.ObjectProperty C
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁.union m₂},
  Std.DHashMap.Const.get (m₁.union m₂) k h' = Std.DHashMap.Const.get m₂ k ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
Fin.succFunctor_map : ∀ (n : ℕ) {x x_1 : Fin n} (hij : x ⟶ x_1), (Fin.succFunctor n).map hij = CategoryTheory.homOfLE ⋯
-- Mathlib.Topology.Algebra.Order.Group
ContinuousAt.mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {x : X},
  ContinuousAt f x → ContinuousAt (fun x => |f x|ₘ) x
-- Mathlib.CategoryTheory.Sums.Products
/-- Composing the forward direction of `functorEquiv` with the second projection is the same as
precomposition with `inr_ A A'`.  -/
CategoryTheory.Sum.functorEquivFunctorCompSndIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (CategoryTheory.Sum.functorEquiv A A' B).functor.comp
                (CategoryTheory.Prod.snd (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)) ≅
              (CategoryTheory.Functor.whiskeringLeft A' (A ⊕ A') B).obj (CategoryTheory.Sum.inr_ A A')
-- Mathlib.Data.Set.Image
Set.prod_quotient_preimage_eq_image : ∀ {α : Type u_1} {β : Type u_2} [s : Setoid α] (g : Quotient s → β) {h : α → β},
  h = g ∘ Quotient.mk'' →
    ∀ (r : Set (β × β)), {x | (g x.1, g x.2) ∈ r} = (fun a => (⟦a.1⟧, ⟦a.2⟧)) '' (fun a => (h a.1, h a.2)) ⁻¹' r
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.CommMon C} (f : X ⟶ Y)
  (x : CategoryTheory.Discrete PUnit.{u + 1}),
  ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C).map f).hom.hom.app x = f.hom.hom
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.distribSMul' : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {S : Type u_3} →
            [inst_3 : SMul S R] →
              [inst_4 : DistribSMul S M] → [IsScalarTower S R M] → (P : Submodule R M) → DistribSMul S (M ⧸ P)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instCoeSortType : CoeSort RingCat (Type u)
-- Lean.Compiler.IR.Basic
Lean.IR.Param.mk.inj : ∀ {x : Lean.IR.VarId} {borrow : Bool} {ty : Lean.IR.IRType} {x_1 : Lean.IR.VarId} {borrow_1 : Bool}
  {ty_1 : Lean.IR.IRType},
  { x := x, borrow := borrow, ty := ty } = { x := x_1, borrow := borrow_1, ty := ty_1 } →
    x = x_1 ∧ borrow = borrow_1 ∧ ty = ty_1
-- Mathlib.Analysis.PSeries
NNReal.summable_rpow_inv : ∀ {p : ℝ}, (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Composition of affine maps acts as applying the two functions.  -/
AffineMap.coe_comp : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_himp_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∈ s ⇨ t ↔ a ∈ s → a ∈ t
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
        U)
      (smoothSheafCommRing.forgetStalk IM I M R x).inv =
    TypeCat.ofHom
      ⇑(CommRingCat.Hom.hom
          (CategoryTheory.Limits.colimit.ι
            ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
-- Lean.Parser.Command
Lean.Parser.Command.init_quot.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Environment
Lean.instHashableModuleIdx : Hashable Lean.ModuleIdx
-- Mathlib.Topology.Sion
/-- Disjointness criterion for two `sublevelLeft` at different values of the parameter  -/
_private.Mathlib.Topology.Sion.0.Sion.disjoint_sublevelLeft : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β} {a : E}
  {b : β} {y y' : ↑Y},
  (∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')) →
    b < max (f a ↑y) (f a ↑y') → Disjoint (Sion.sublevelLeft✝ X f b ↑y) (Sion.sublevelLeft✝ X f b ↑y')
-- Mathlib.Data.List.Rotate
List.rotate_append_length_eq : ∀ {α : Type u} (l l' : List α), (l ++ l').rotate l.length = l' ++ l
-- Mathlib.GroupTheory.Congruence.Hom
/-- An `AddMonoid` homomorphism `f` induces an injective homomorphism on the quotient
by `f`'s kernel.  -/
AddCon.kerLift_injective : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P),
  Function.Injective ⇑(AddCon.kerLift f)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Oplax.StrongTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- If `X` and `Y` are closed then `X ⊗ Y` is.
This isn't an instance because it's not usually how we want to construct internal homs,
we'll usually prove all objects are closed uniformly.
 -/
CategoryTheory.tensorClosed : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        CategoryTheory.Closed X →
          CategoryTheory.Closed Y → CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.ite_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x₁ : M) (x₂ : N) (P : Prop)
  [inst_5 : Decidable P], (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)) (size : ℕ) (k' : α) (v' : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
    match compare k k' with
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k (some (k', v')) r
    | x => Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best l
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.extend_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f₁ : MeasureTheory.SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ)
  (x : α), (f₁.extend g hg f₂) (g x) = f₁ x
-- Init.Data.UInt.Bitwise
USize.and_self : ∀ {a : USize}, a &&& a = a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRcoSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Rco.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RcoSlice α β)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- `I` is a sub-dp-ideal of itself.  -/
DividedPowers.SubDPIdeal.instTop : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → Top hI.SubDPIdeal