mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Module.End.baseChangeHom_apply_apply : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (a : Module.End R M) (a_1 : TensorProduct R A M),
  ((Module.End.baseChangeHom R A M) a) a_1 =
    (TensorProduct.liftAux
        (↑R { toFun := fun h => h ∘ₗ a, map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
          ↑R (TensorProduct.AlgebraTensorModule.mk R A A M)))
      a_1
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addRightReflectLE : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] [AddRightReflectLE M],
  AddRightReflectLE { x // 0 < x }
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- We can turn any limit cone over a discrete collection of objects into a bicone.  -/
CategoryTheory.Limits.Bicone.ofLimitCone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : J → C} →
          {t : CategoryTheory.Limits.Cone (CategoryTheory.Discrete.functor f)} →
            CategoryTheory.Limits.IsLimit t → CategoryTheory.Limits.Bicone f
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.continuous_extend : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T3Space γ] {f : α → γ} (di : IsDenseInducing i),
  (∀ (b : β), ∃ c, Filter.Tendsto f (Filter.comap i (nhds b)) (nhds c)) → Continuous (di.extend f)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given a diagram
```
a --φ--> b        b'
|        |        |
v        v        v
R --f--> S --g--> S'
```
such that `φ` is strongly co-Cartesian, and morphisms `ψ ψ' : b ⟶ b'` such that
`g ≫ ψ = φ' = g ≫ ψ'`. Then we have that `ψ = ψ'`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.ext : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮}
  {b' : 𝒳} (g : S ⟶ S') {ψ ψ' : b ⟶ b'} [p.IsHomLift g ψ] [p.IsHomLift g ψ'],
  CategoryTheory.CategoryStruct.comp φ ψ = CategoryTheory.CategoryStruct.comp φ ψ' → ψ = ψ'
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_append : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) {s1 s2 : Stream'.WSeq α} {t1 t2 : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s1 t1 → Stream'.WSeq.LiftRel R s2 t2 → Stream'.WSeq.LiftRel R (s1.append s2) (t1.append t2)
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- The same-universe version of `Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`.  -/
Field.insepDegree_mul_insepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  Field.insepDegree F E * Field.insepDegree E K = Field.insepDegree F K
-- Lean.Language.Basic
_private.Lean.Language.Basic.0.Lean.Language.Snapshot.Diagnostics.mk.sizeOf_spec : ∀ (msgLog : Lean.MessageLog) (interactiveDiagsRef? : Option (IO.Ref (Option Dynamic))),
  sizeOf { msgLog := msgLog, interactiveDiagsRef? := interactiveDiagsRef? } =
    1 + sizeOf msgLog + sizeOf interactiveDiagsRef?
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The functor `pullback f : Over X ⥤ Over Y` is naturally isomorphic to
`toOver : Over X ⥤ Over (Over.mk f)` post-composed with the
iterated slice equivalence `Over (Over.mk f) ⥤ Over Y`.  -/
CategoryTheory.toOverIteratedSliceForwardIsoPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.ChosenPullbacks C] →
      {X Y : C} →
        (f : Y ⟶ X) →
          (CategoryTheory.toOver (CategoryTheory.Over.mk f)).comp (CategoryTheory.Over.mk f).iteratedSliceForward ≅
            CategoryTheory.ChosenPullbacksAlong.pullback f
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.renameInaccessibleFVars : Lean.MVarId → Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsDiscreteValuationRing.not_krullDimLE_zero : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R], ¬Ring.KrullDimLE 0 R
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addXYZ_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R),
  W'.addXYZ P Q 2 = WeierstrassCurve.Jacobian.addZ P Q
-- Mathlib.Geometry.Manifold.Submersion
/-- A linear equivalence `E ≃L[𝕜] (E'' × F)` which belongs to the data of a submersion `f` at `x`:
the particular equivalence is arbitrary, but this choice matches the witnesses given by
`h.domChart` and `h.codChart`.  -/
Manifold.IsSubmersionAt.equiv : {𝕜 : Type u_1} →
  {E'' : Type u_3} →
    {H : Type u_7} →
      {G : Type u_9} →
        {E : Type u} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup E''] →
                  [inst_4 : NormedSpace 𝕜 E''] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 E'' G} →
                            {M : Type u_11} →
                              {N : Type u_13} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              (h : Manifold.IsSubmersionAt I J n f x) → E ≃L[𝕜] E'' × h.complement
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- An integral domain that is module-finite as an algebra over a field is a field.  -/
fieldOfFiniteDimensional : (F : Type u_1) →
  (K : Type u_2) →
    [inst : Field F] → [h : CommRing K] → [IsDomain K] → [inst_2 : Algebra F K] → [FiniteDimensional F K] → Field K
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instToStringOffset : ToString Std.Time.Millisecond.Offset
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- **Alias** of `MeasureTheory.nullSingletonClass_withDensity`. -/
MeasureTheory.noAtoms_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  (f : α → ENNReal), MeasureTheory.NullSingletonClass (μ.withDensity f)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.id.sizeOf_spec : ∀ (e : Lean.Expr) (f : Mathlib.Tactic.BicategoryLike.Mor₁),
  sizeOf (Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f) = 1 + sizeOf e + sizeOf f
-- Mathlib.Order.SuccPred.Relation
/-- `(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ pred i` and
`pred i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_pred_of_refl : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α}
  [Std.Refl r],
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → Relation.TransGen r n m
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The weight space representation of endomorphisms  -/
RootPairing.Hom.weightHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.End →* Module.End R M
-- Mathlib.Algebra.Module.Injective
Module.Baer.extensionOfMaxAdjoin.eq_1 : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) (y : N),
  Module.Baer.extensionOfMaxAdjoin i f h y =
    { domain := Module.Baer.supExtensionOfMaxSingleton i f y,
      toFun := { toFun := Module.Baer.ExtensionOfMaxAdjoin.extensionToFun i f h, map_add' := ⋯, map_smul' := ⋯ },
      le := ⋯, is_extension := ⋯ }
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.of : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃x y : R⦄, r x y → RingQuot.Rel r x y
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃` is the pushout `X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃)`.  -/
CategoryTheory.Limits.pushoutAssocIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout
                        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₁ g₂)
                          (CategoryTheory.Limits.pushout.inl
                            (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄))
                        (CategoryTheory.Limits.pushout.desc
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
                            (CategoryTheory.Limits.pushout.inl
                              (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄))
                          (CategoryTheory.Limits.pushout.inr
                            (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
                          ⋯)
                        ⋯)
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Partially-applied version of `FractionalIdeal.ext`.  -/
FractionalIdeal.coe_ext : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, ↑I = ↑J → I = J
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.funMap_quotient_mk' : ∀ {L : FirstOrder.Language} {M : Type u_1} (s : Setoid M) [ps : L.Prestructure s] {n : ℕ} (f : L.Functions n)
  (x : Fin n → M), (FirstOrder.Language.Structure.funMap f fun i => ⟦x i⟧) = ⟦FirstOrder.Language.Structure.funMap f x⟧
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValNat.prime_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), padicValNat p (p ^ n) = n
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- If a morphism `g : V ⟶ U.unop` belongs to the sieve `imageSieve f s g`, then
this is choice of a preimage of `G.map g.op s` in `F.obj (op V)`, see
`app_localPreimage`.  -/
CategoryTheory.Presheaf.localPreimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} A] →
        {FA : A → A → Type u_1} →
          {CA : A → Type w'} →
            [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
              [inst_3 : CategoryTheory.ConcreteCategory A FA] →
                {F G : CategoryTheory.Functor Cᵒᵖ A} →
                  (f : F ⟶ G) →
                    {U : Cᵒᵖ} →
                      (s : CategoryTheory.ToType (G.obj U)) →
                        {V : C} →
                          (g : V ⟶ Opposite.unop U) →
                            (CategoryTheory.Presheaf.imageSieve f s).arrows g →
                              CategoryTheory.ToType (F.obj (Opposite.op V))
-- Std.Internal.Do.Triple.SpecLemmas
/-- An invariant combinator for loops with early return, for the new `do` elaborator which
uses `Prod` for the state tuple: `onContinue` is the invariant while iterating, `onReturn`
holds once the loop returned early with a value.  -/
Std.Internal.Do.Invariant.withEarlyReturnNewDo : {α : Type u₁} →
  {xs : List α} →
    {β γ : Type u₂} →
      (Pred : Type (max u₁ u₂)) →
        [Std.Internal.Do.Assertion Pred] →
          (xs.Cursor → β → Pred) → (γ → β → Pred) → Std.Internal.Do.Invariant xs (Option γ × β) Pred
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_symm_apply_add_right : ∀ {n : ℕ} (i : ℕ), (finSumNatEquiv n).symm (n + i) = Sum.inr i
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.support_mul_subset_right : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] (f g : ι → M₀),
  (Function.support fun x => f x * g x) ⊆ Function.support g
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_mul_right_left_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime (x - z * y) y ↔ IsCoprime x y
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed
set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e.  points
to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected
value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also
`ConvexOn.map_centerMass_le` for a finite sum version of this lemma.  -/
ConvexOn.map_integral_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ],
  ConvexOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ → g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
-- Mathlib.Computability.Primrec.Basic
Primrec.encode : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Encodable.encode
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instMaxOfSeparatelyContinuousAdd : {G : Type u} →
  [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → [SeparatelyContinuousAdd G] → Max (OpenNormalAddSubgroup G)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- If `𝔖` covers `α`, the natural map `UniformOnFun.toFun` from `α →ᵤ[𝔖] β` to `α → β` is
uniformly continuous.

In other words, if `𝔖` covers `α`, then the uniform structure of `𝔖`-convergence is finer than
that of pointwise convergence.  -/
UniformOnFun.uniformContinuous_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
  ⋃₀ 𝔖 = Set.univ → UniformContinuous ⇑(UniformOnFun.toFun 𝔖)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := false })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := false }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_1 h'
-- Mathlib.Order.Interval.Set.Basic
/-- **Alias** of `Set.Iic_sdiff_right`. -/
Set.Iic_diff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iic a \ {a} = Set.Iio a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_swap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {Z : C} (h : Y ⨯ B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id B)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map g (CategoryTheory.CategoryStruct.id A))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id Y) f) h)
-- Std.Time.Duration
Std.Time.instToStringDuration : ToString Std.Time.Duration
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_le_expGrowthSup : ∀ {u : ℕ → ENNReal}, ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthSup u
-- Init.Core
decide_true : ∀ (h : Decidable True), decide True = true
-- Init.MetaTypes
/-- When `false` (default: `true`), then disables zeta reduction of `have` expressions.
If `zeta` is `false`, then this option has no effect.
Unused `have`s are still removed if `zeta` or `zetaUnused` are true.
 -/
Lean.Meta.Simp.Config.zetaHave : Lean.Meta.Simp.Config → Bool
-- Mathlib.Data.DFinsupp.FiniteInfinite
/-- See `DFinsupp.infinite_of_right` for this in instance form, with the drawback that
it needs all `π i` to be infinite.  -/
DFinsupp.infinite_of_exists_right : ∀ {ι : Type u_1} {π : ι → Type u_2} (i : ι) [Infinite (π i)] [inst : (i : ι) → Zero (π i)], Infinite (Π₀ (i : ι), π i)
-- Init.Data.Nat.Basic
Nat.succ_lt_succ : ∀ {n m : ℕ}, n < m → n.succ < m.succ
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Tensor product of identity maps is the identity: `𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (X₁ ⊗ X₂)`  -/
CategoryTheory.MonoidalCategory.id_tensorHom_id : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₁)
      (CategoryTheory.CategoryStruct.id X₂) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, IsIdempotentElem T → (T.IsSymmetric ↔ T.rangeᗮ = T.ker)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_iff : ∀ {o : Ordinal.{u_4}}, Order.IsSuccLimit o ↔ o ≠ 0 ∧ Order.IsSuccPrelimit o
-- Mathlib.Algebra.Group.Ext
AddGroup.toSubNegAddMonoid_injective : ∀ {G : Type u_1}, Function.Injective (@AddGroup.toSubNegMonoid G)
-- Mathlib.Analysis.Meromorphic.Basic
meromorphicAt_mul_iff_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → (MeromorphicAt (g * f) x ↔ MeromorphicAt f x)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuous.mul_const' : ∀ {R : Type u_1} {β : Type u_2} [inst : Ring R] [inst_1 : UniformSpace R] [inst_2 : UniformSpace β]
  [UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R}, UniformContinuous f → ∀ (a : R), UniformContinuous fun x => f x * a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.productTriangle_mor₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  (T : J → CategoryTheory.Pretriangulated.Triangle C) [inst_2 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₁]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₂]
  [inst_4 : CategoryTheory.Limits.HasProduct fun j => (T j).obj₃]
  [inst_5 : CategoryTheory.Limits.HasProduct fun j => (CategoryTheory.shiftFunctor C 1).obj (T j).obj₁],
  (CategoryTheory.Pretriangulated.productTriangle T).mor₂ = CategoryTheory.Limits.Pi.map fun j => (T j).mor₂
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffOn.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => Real.sinh (f x)) s
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.sheafComposeIso_hom_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J A]
  [inst_4 : CategoryTheory.HasWeakSheafify J B] [inst_5 : J.HasSheafCompose F] [inst_6 : J.PreservesSheafification F]
  (P : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J (P.comp F))
      (CategoryTheory.sheafifyComposeIso J F P).hom =
    CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J P) F
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add_f_some : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S) (i : E.I₀), (E.add f).f (some i) = E.f i
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_nsmul : ∀ {α : Type u_1} (n : ℕ) (f : α → ℝ), Complex.ofReal ∘ (n • f) = n • Complex.ofReal ∘ f
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearEquiv.alternatingMapCongrRight_symm_apply_apply : ∀ {ι : Type u_7} {R' : Type u_10} {M'' : Type u_11} {N'' : Type u_13} {N₂'' : Type u_14} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid M''] [inst_2 : AddCommMonoid N''] [inst_3 : AddCommMonoid N₂''] [inst_4 : Module R' M'']
  [inst_5 : Module R' N''] [inst_6 : Module R' N₂''] (e : N'' ≃ₗ[R'] N₂'') (f : M'' [⋀^ι]→ₗ[R'] N₂'')
  (a : (i : ι) → (fun x => M'') i), (e.alternatingMapCongrRight.symm f) a = e.symm (f a)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ici_add_one_eq_Ioi_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a : α},
  ¬IsMax a → Set.Ici (a + 1) = Set.Ioi a
-- Mathlib.Order.RelSeries
RelSeries.append.congr_simp : ∀ {α : Type u_1} {r : SetRel α α} (p p_1 : RelSeries r) (e_p : p = p_1) (q q_1 : RelSeries r) (e_q : q = q_1)
  (connect : (p.last, q.head) ∈ r), p.append q connect = p_1.append q_1 ⋯
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.mor.inj : ∀ {thm thm_1 : Mathlib.Meta.FunProp.GeneralTheorem},
  Mathlib.Meta.FunProp.Theorem.mor thm = Mathlib.Meta.FunProp.Theorem.mor thm_1 → thm = thm_1
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.isDotCompletionMethod : Lean.Name → Lean.ConstantInfo → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
/-- **Alias** of `AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective`. -/
AlgebraicGeometry.Scheme.Hom.stalkMap_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.SurjectiveOnStalks f] (x : ↥X),
  Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  (χ : MulChar R R') (f : R' →+* R'') (a : R), (χ.ringHomComp f) a = f (χ a)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_smul_of_tower : ∀ {M₁ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁] {M₂ : Type u_6}
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] {R : Type u_9} {S : Type u_10} [inst_4 : Semiring S]
  [inst_5 : SMul R M₁] [inst_6 : Module S M₁] [inst_7 : SMul R M₂] [inst_8 : Module S M₂]
  [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁), f (c • x) = c • f x
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le_self' : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M},
  (∀ x ∉ s, 0 ≤ f x) → s.indicator f ≤ f
-- Mathlib.SetTheory.Ordinal.Arithmetic
Cardinal.noMaxOrder : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → NoMaxOrder c.ord.ToType