mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum.congr_simp : ∀ {α : Type u_1} (M M_1 : Matroid α) (e_M : M = M_1) (N N_1 : Matroid α) (e_N : N = N_1) (h : Disjoint M.E N.E),
  M.disjointSum N h = M_1.disjointSum N_1 ⋯
-- Mathlib.Analysis.Normed.Order.UpperLower
dist_mono_left_pi : ∀ {ι : Type u_2} [inst : Fintype ι] {y : ι → ℝ}, MonotoneOn (fun x => dist x y) (Set.Ici y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
`2 * cosh θ` to the value `2 * cosh (n * θ)`.  -/
Polynomial.Chebyshev.C_two_mul_complex_cosh : ∀ (θ : ℂ) (n : ℤ), Polynomial.eval (2 * Complex.cosh θ) (Polynomial.Chebyshev.C ℂ n) = 2 * Complex.cosh (↑n * θ)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Reinterpret an ordered monoid homomorphism as an order homomorphism.  -/
OrderMonoidHom.toOrderHom : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] → [inst_2 : MulOneClass α] → [inst_3 : MulOneClass β] → (α →*o β) → α →o β
-- Mathlib.Algebra.Order.Kleene
KleeneAlgebra.toIdemSemiring : {α : Type u_5} → [self : KleeneAlgebra α] → IdemSemiring α
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Core.transform.visit.visitPost : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.CoreM m] →
      [MonadControlT Lean.CoreM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            (x : STWorld IO.RealWorld m) →
              MonadLiftT (ST IO.RealWorld) m → Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapAddGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapAddGrp =
    { functor := e.functor.mapAddGrp, inverse := e.inverse.mapAddGrp,
      unitIso :=
        CategoryTheory.Functor.mapAddGrpIdIso.symm ≪≫
          CategoryTheory.Functor.mapAddGrpNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapAddGrpCompIso,
      counitIso :=
        CategoryTheory.Functor.mapAddGrpCompIso.symm ≪≫
          CategoryTheory.Functor.mapAddGrpNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapAddGrpIdIso,
      functor_unitIso_comp := ⋯ }
-- Aesop.Search.Main
Aesop.nextActiveGoal : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM Q Aesop.GoalRef
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
BoundedContinuousFunction.toLp.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_3)
  [inst_5 : Fact (1 ≤ p)] [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E],
  BoundedContinuousFunction.toLp p μ 𝕜 = BoundedContinuousFunction.toLp p μ 𝕜
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Methods.toMethodsRefImpl : Lean.Meta.Sym.Simp.Methods → Lean.Meta.Sym.Simp.MethodsRef
-- Mathlib.Order.Partition.Finpartition
Finpartition.atomise.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (F : Finset (Finset α)),
  Finpartition.atomise s F =
    Finpartition.ofErase (Finset.image (fun Q => {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset) ⋯ ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp t.maxKey! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of_inj : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsHausdorff I M] {a b : M}, (AdicCompletion.of I M) a = (AdicCompletion.of I M) b ↔ a = b
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.reflection_inv : ∀ {ι : 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) (i : ι),
  (RootPairing.Equiv.reflection P i)⁻¹ = RootPairing.Equiv.reflection P i
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise_of_maps_to : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ}
  [inst_1 : DecidableEq κ] {g : ι → κ},
  (∀ i ∈ s, g i ∈ t) → ∀ (f : ι → M), ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_insertMany_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) {t₂ : Std.DTreeMap.Internal.Impl α β},
  (↑(t₁.insertMany t₂ ⋯)).toListModel.Perm (Std.Internal.List.insertList t₁.toListModel t₂.toListModel)
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {X Y : HopfAlgCat R} {f g : X ⟶ Y},
  f = g ↔ HopfAlgCat.Hom.toBialgHom f = HopfAlgCat.Hom.toBialgHom g
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.get.match_1.eq_1 : ∀ (motive : Substring.Raw → String.Pos.Raw → Sort u_1) (s : String) (b stopPos p : String.Pos.Raw)
  (h_1 : (s : String) → (b stopPos p : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos } p),
  (match { str := s, startPos := b, stopPos := stopPos }, p with
    | { str := s, startPos := b, stopPos := stopPos }, p => h_1 s b stopPos p) =
    h_1 s b stopPos p
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.sup : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {f g : E → β} [inst_4 : SemilatticeSup β],
  QuasiconvexOn 𝕜 s f → QuasiconvexOn 𝕜 s g → QuasiconvexOn 𝕜 s (f ⊔ g)
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`).  -/
GroupSeminorm.toSeminormedGroup : {E : Type u_5} → [inst : Group E] → GroupSeminorm E → SeminormedGroup E
-- Mathlib.Order.Interval.Set.OrderEmbedding
OrderEmbedding.preimage_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] (e : α ↪o β) (x y : α),
  ⇑e ⁻¹' Set.uIcc (e x) (e y) = Set.uIcc x y
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.nontrivial : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V}, G.IsBridge e → Nontrivial V
-- Lean.Elab.Tactic.Try
/-- A user-defined generator that proposes tactics for `try?` to attempt.
Takes the goal MVarId and collected info, returns array of tactics to try.  -/
Lean.Elab.Tactic.Try.TrySuggestionGenerator : Type
-- Std.Async.TCP
/-- Connects the client socket to the given address.
 -/
Std.Async.TCP.Socket.Client.connect : Std.Async.TCP.Socket.Client → Std.Net.SocketAddress → Std.Async.Async Unit
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_eq_get! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α} {h : a ∈ m},
  Std.DHashMap.Const.get m a h = Std.DHashMap.Const.get! m a
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instBEqKey : BEq Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.left_mem_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a ∈ Set.uIcc a b
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_counitIso_inv_app : ∀ (R : Type u) [inst : CommRing R] (X : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ),
  (commBialgCatEquivComonCommAlgCat R).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is clopen in the valuative topology.  -/
Valuation.isClopen_ball : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsClopen {x | v.restrict x < r}
-- Mathlib.Data.Set.Subsingleton
Set.subsingleton_univ : ∀ {α : Type u} [Subsingleton α], Set.univ.Subsingleton
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instZeroHomClass : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R], ZeroHomClass (ContinuousMapZero X R) X R
-- Mathlib.Order.Filter.Extr
IsMaxFilter.inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {l : Filter α},
  IsMaxFilter f l a → IsMaxFilter g l a → IsMaxFilter (fun x => f x ⊓ g x) l a
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_empty`.

---

The diameter of the empty set vanishes  -/
EMetric.diam_empty : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X], Metric.ediam ∅ = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sum_of_pos : ∀ {ι : Type u_1} {a : ℝ}, 0 < a → ∀ (f : ι → ℝ) (s : Finset ι), a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x
-- Mathlib.Topology.VectorBundle.Basic
/-- A version of `Bundle.Trivialization.coordChangeL_apply` that fully unfolds `coordChange`. The
right-hand side is ugly, but has good definitional properties for specifically defined
trivializations.  -/
Bundle.Trivialization.coordChangeL_apply' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (y : F), (Bundle.Trivialization.coordChangeL R e e' b) y = (↑e' (↑e.symm (b, y))).2
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.EssentiallySmall.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} Q],
  P ≤ Q → CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The constant factor occurring in the conclusion of `lintegral_pow_le_pow_lintegral_fderiv`.
It only depends on `E`, `μ` and `p`.
It is determined by the ratio of the measures on `E` and `ℝⁿ` and
the operator norm of a chosen equivalence `E ≃ ℝⁿ` (raised to suitable powers involving `p`).  -/
MeasureTheory.lintegralPowLePowLIntegralFDerivConst : {E : Type u_5} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      [inst_2 : MeasurableSpace E] →
        [BorelSpace E] → [FiniteDimensional ℝ E] → (μ : MeasureTheory.Measure E) → [μ.IsAddHaarMeasure] → ℝ → NNReal
-- Mathlib.Analysis.Normed.Affine.AsymptoticCone
/-- In a finite dimensional normed affine space over `ℝ`, a set is unbounded if and only if its
asymptotic cone contains a nonzero vector.  -/
not_bounded_iff_exists_ne_zero_mem_asymptoticCone : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Set P},
  ¬Bornology.IsBounded s ↔ ∃ v, v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Reinterpret a `Subalgebra` as a `Subsemiring`.  -/
Subalgebra.toSubsemiring : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A → Subsemiring A
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.match_1.eq_2 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {n : Type u_1 → Type u_3} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (upperBound : α)
  (f :
    (b : α) →
      { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
        (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next, upperBound := upperBound } } f)
  (h_2 :
    (upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := none, upperBound := upperBound } } f),
  (match { internalState := { next := none, upperBound := upperBound } }, f with
    | { internalState := { next := some next, upperBound := upperBound } }, f => h_1 next upperBound f
    | { internalState := { next := none, upperBound := upperBound } }, f => h_2 upperBound f) =
    h_2 upperBound f
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
/-- The linear map from the top exterior power of `M × N` to `M` induced by the cofactor
expansion along the `M`-summand.  -/
_private.Mathlib.Algebra.Module.StablyFree.FreeOfInvertible.0.exteriorPower.cofactorToLeft : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → {n : ℕ} → Module.Basis (Fin n) R N → ↥(⋀[R]^(n + 1) (M × N)) →ₗ[R] M
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f i))
          (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Iterates over the whole iterator, applying the monadic effects of each step, discarding all
emitted values.
 -/
Std.IterM.drain : {α : Type w} →
  {m : Type w → Type w'} →
    [Monad m] → {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM m β → [Std.IteratorLoop α m m] → m PUnit.{w + 1}
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_one_eq_lift : ∀ {o : Ordinal.{u}}, Ordinal.omega 1 = Ordinal.lift.{v, u} o ↔ Ordinal.omega 1 = o
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Monotone.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} [MulRightMono α],
  Monotone f → ∀ (a : α), Monotone fun x => f x * a
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- `ContinuousAlternatingMap.restrictScalars` as a `LinearIsometry`.  -/
ContinuousAlternatingMap.restrictScalarsLI : {𝕜 : Type u} →
  {E : Type wE} →
    {F : Type wF} →
      {ι : Type v} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : NormedSpace 𝕜 F] →
                  [inst_5 : Fintype ι] →
                    (𝕜' : Type u_1) →
                      [inst_6 : NontriviallyNormedField 𝕜'] →
                        [inst_7 : NormedAlgebra 𝕜' 𝕜] →
                          [inst_8 : NormedSpace 𝕜' F] →
                            [inst_9 : IsScalarTower 𝕜' 𝕜 F] →
                              [inst_10 : NormedSpace 𝕜' E] →
                                [IsScalarTower 𝕜' 𝕜 E] → E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜'] E [⋀^ι]→L[𝕜'] F
-- Mathlib.Algebra.Group.Pi.Basic
Pi.leftCancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → LeftCancelMonoid (f i)] → LeftCancelMonoid ((i : I) → f i)
-- Lean.Parser.Do
Lean.Parser.Term.doPatDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.WHNF
/-- Unfold definition using "smart unfolding" if possible.
If `ignoreTransparency = true`, then the definition is unfolded even if the transparency setting does not allow it.
 -/
Lean.Meta.unfoldDefinition? : Lean.Expr → optParam Bool false → Lean.MetaM (Option Lean.Expr)
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.addTrailingParserAux : Lean.Parser.PrattParsingTables → Lean.Parser.TrailingParser → ℕ → Lean.Parser.PrattParsingTables
-- Aesop.Forward.State
Aesop.instHashablePatSubstSource.hash : Aesop.PatSubstSource → UInt64
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.liftInner.eq_1 : ∀ {α : Type u_1} {m : Type w → Type w'} (n : Type w → Type w'') [inst : MonadLiftT m n] (x : Std.Iterators.HetT m α),
  Std.Iterators.HetT.liftInner n x = { Property := x.Property, small := ⋯, operation := liftM x.operation }
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
The natural transformation given by the algebra structure maps, used to construct a cocone `c` with
point `colimit (D ⋙ forget T)`.
 -/
CategoryTheory.Monad.ForgetCreatesColimits.γ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} → (D.comp T.forget).comp T.toFunctor ⟶ D.comp T.forget
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.of_mapCocone : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F}
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G]
  [CategoryTheory.Limits.ReflectsColimitsOfShape J G],
  CategoryTheory.IsUniversalColimit (G.mapCocone c) → CategoryTheory.IsUniversalColimit c
-- Mathlib.Topology.Order.OrderClosed
frontier_ge_subset_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {g f : β → α}
  [inst_3 : TopologicalSpace β], Continuous g → Continuous f → frontier {b | g b ≤ f b} ⊆ {b | f b = g b}
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_def'_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (e : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_def'_cert x e p = p.beq' (Int.Internal.Linear.Poly.add (-1) x e.norm)
-- Plausible.Arbitrary
Plausible.Unit.Arbitrary : Plausible.Arbitrary Unit
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `#clear_deprecations "YYYY₁-MM₁-DD₁" "YYYY₂-MM₂-DD₂" really` computes the declarations that have
the `@[deprecated]` attribute and the `since` field satisfies
`YYYY₁-MM₁-DD₁ ≤ since ≤ YYYY₂-MM₂-DD₂`.
For each one of them, it retrieves the command that generated it and removes it.
It also verbosely logs various steps of the computation.

Running `#clear_deprecations "YYYY₁-MM₁-DD₁" "YYYY₂-MM₂-DD₂"`, without the trailing `really` skips
the removal, but still emits the same verbose output.

This function is intended for automated use by the `remove_deprecations` automation.
 -/
Mathlib.Tactic.«command#clear_deprecations___Really» : Lean.ParserDescr
-- Mathlib.Data.Stream.Init
Stream'.get_enum : ∀ {α : Type u} (s : Stream' α) (n : ℕ), s.enum.get n = (n, s.get n)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, (s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Init.Grind.ToInt
Lean.Grind.IntInterval.mem_io : ∀ (hi x : ℤ), x ∈ Lean.Grind.IntInterval.io hi ↔ x < hi
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.alterₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [Hashable α] →
        [LawfulBEq α] →
          Std.DHashMap.Internal.Raw₀ α β → (a : α) → (Option (β a) → Option (β a)) → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_mem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∉ s → y ∈ s → (ProbabilityTheory.bernoulliMeasure x y p).real s = 1 - ↑p
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.extend_val_inr : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} (P : Algebra.Generators R S ι) (b : ι' → S) (i : ι'), (P.extend b).val (Sum.inr i) = b i
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Core function that delaborates a natural number (an `OfNat.ofNat` literal).
 -/
Lean.PrettyPrinter.Delaborator.delabOfNatCore : optParam Bool false → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Data.Nat.Factors
Nat.le_of_mem_primeFactorsList : ∀ {n p : ℕ}, p ∈ n.primeFactorsList → p ≤ n
-- Mathlib.Topology.Instances.EReal.Lemmas
ContinuousAt.ereal_toENNReal : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f : α → EReal} {x : α},
  ContinuousAt f x → ContinuousAt (fun x => (f x).toENNReal) x
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.mk.sizeOf_spec : ∀ (privateConstInfo exportedConstInfo : Lean.ConstantInfo) (exts : Array Lean.EnvExtensionState)
  (nestedConsts : Lean.VisibilityMap✝ Lean.AsyncConsts✝),
  sizeOf
      { privateConstInfo := privateConstInfo, exportedConstInfo := exportedConstInfo, exts := exts,
        nestedConsts := nestedConsts } =
    1 + sizeOf privateConstInfo + sizeOf exportedConstInfo + sizeOf exts + sizeOf nestedConsts
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.mul : ∀ {R : Type u_1} [inst : CommSemigroup R] [inst_1 : StarMul R] {x y : R},
  IsSelfAdjoint x → IsSelfAdjoint y → IsSelfAdjoint (x * y)
-- Mathlib.Topology.Compactness.SigmaCompact
compactCovering.eq_1 : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X], compactCovering X = Set.accumulate ⋯.choose
-- Init.Data.Nat.Lemmas
Nat.mul_pos_iff_of_pos_right : ∀ {a b : ℕ}, 0 < b → (0 < a * b ↔ 0 < a)