mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_add : ∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M),
  ∑ i, f i = ∑ i, f (Fin.castAdd b i) + ∑ i, f (Fin.natAdd a i)
-- Mathlib.Analysis.Normed.Group.Defs
NormedCommGroup.ofMulDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : CommGroup E] [inst_2 : MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y),
  NormedCommGroup.ofMulDist' h₁ h₂ =
    { toNorm := (NormedGroup.ofMulDist' h₁ h₂).toNorm, toGroup := (NormedGroup.ofMulDist' h₁ h₂).toGroup, mul_comm := ⋯,
      toMetricSpace := (NormedGroup.ofMulDist' h₁ h₂).toMetricSpace, dist_eq := ⋯ }
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lsmul_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.IsTorsionFree R M] {x : R}, x ≠ 0 → Function.Injective ⇑((LinearMap.lsmul R M) x)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le : ∀ {α : Type u_1} {E' : Type u_3} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E') {t : Set α},
  MeasurableSet t →
    μ t ≠ ⊤ →
      ∫⁻ (a : α) in t, ↑‖↑↑↑((MeasureTheory.condExpL2 E' 𝕜 hm) (MeasureTheory.indicatorConstLp 2 hs hμs x)) a‖₊ ∂μ ≤
        μ (s ∩ t) * ↑‖x‖₊
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.instInhabitedState : Inhabited Aesop.RuleTac.ForwardM.State
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.map_comp_ι : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂),
  (CliffordAlgebra.map f).toLinearMap ∘ₗ CliffordAlgebra.ι Q₁ = CliffordAlgebra.ι Q₂ ∘ₗ f.toLinearMap
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.of.sizeOf_spec : ∀ (carrier : Type u) [str : TopologicalSpace carrier], sizeOf (TopCat.of carrier) = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.map₂_def₂ : ∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4}
  {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h)
  [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_6 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_7 : IsDirectedOrder ι]
  (ih : (i : ι) → F₁ i → F₂ i → F i)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (x : (i : ι) × F₁ i) (y : (i : ι) × F₂ i) (i : ι) (hxi : x.fst ≤ i) (hyi : y.fst ≤ i),
  DirectLimit.map₂ f₁ f₂ f ih compat ⟦x⟧ ⟦y⟧ = ⟦⟨i, ih i ((f₁ x.fst i hxi) x.snd) ((f₂ y.fst i hyi) y.snd)⟩⟧
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessage : Inhabited Lean.JsonRpc.Message
-- Init.Data.SInt.Bitwise
instCommutativeInt8HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Init.Data.Iterators.Combinators.FilterMap
/-- If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

If `f` is pure, then the simpler variant `it.filter` can be used instead.

**Marble diagram (without monadic effects):**

```text
it             ---a--b--c--d-e--⊥
it.filterM     ---a-----c-------⊥
```

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it`
isn't. In such cases, the termination proof needs to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.Iter.filterM : {α β : Type w} →
  [Std.Iterator α Id β] →
    {m : Type w → Type w'} →
      [inst : Monad m] → [inst_1 : MonadAttach m] → (f : β → m (ULift.{w, 0} Bool)) → Std.Iter β → Std.IterM m β
-- Init.Data.Int.Gcd
Int.dvd_mul_gcd_iff_dvd_mul : ∀ {k n m : ℤ}, k ∣ n * ↑(k.gcd m) ↔ k ∣ n * m
-- Mathlib.Data.Finset.Card
/-- a special case of `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` where `t` is `s.image f`  -/
Finset.exists_ne_map_eq_of_card_image_lt : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} [inst : DecidableEq β] {f : α → β},
  (Finset.image f s).card < s.card → ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
-- Std.Do.PostCond
_private.Std.Do.PostCond.0.Std.Do.ExceptConds.entails.match_1.eq_3 : ∀ (motive : (ps : Std.Do.PostShape) → Std.Do.ExceptConds ps → Std.Do.ExceptConds ps → Sort u_2) (ε : Type u_1)
  (ps : Std.Do.PostShape) (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps))
  (h_1 : (x y : Std.Do.ExceptConds Std.Do.PostShape.pure) → motive Std.Do.PostShape.pure x y)
  (h_2 :
    (σ : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps)) → motive (Std.Do.PostShape.arg σ ps) x y)
  (h_3 :
    (ε : Type u_1) →
      (ps : Std.Do.PostShape) →
        (x y : Std.Do.ExceptConds (Std.Do.PostShape.except ε ps)) → motive (Std.Do.PostShape.except ε ps) x y),
  (match Std.Do.PostShape.except ε ps, x, y with
    | Std.Do.PostShape.pure, x, y => h_1 x y
    | Std.Do.PostShape.arg σ ps, x, y => h_2 σ ps x y
    | Std.Do.PostShape.except ε ps, x, y => h_3 ε ps x y) =
    h_3 ε ps x y
-- Mathlib.GroupTheory.GroupAction.Primitive
/-- In a preprimitive action, any normal subgroup that acts nontrivially is pretransitive
(Wielandt, th. 7.1).  -/
MulAction.IsPreprimitive.isQuasiPreprimitive : ∀ {M : Type u_3} [inst : Group M] {α : Type u_4} [inst_1 : MulAction M α] [MulAction.IsPreprimitive M α],
  MulAction.IsQuasiPreprimitive M α
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a a' : α},
  ¬(SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₀ a')
-- Mathlib.RingTheory.KrullDimension.Basic
Ideal.isMaximal_iff_isPrime : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] {I : Ideal R}, I.IsMaximal ↔ I.IsPrime
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α} {h₁ : a ∈ m.insert k}, (m.insert k).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.get a ⋯
-- Lean.Meta.Basic
Lean.Meta.ExprConfigCacheKey.expr : Lean.Meta.ExprConfigCacheKey → Lean.Expr
-- Init.Data.SInt.IntToBitVec
Int16.toBitVec32_toISize : ∀ (n : Int16) (h : System.Platform.numBits = 32), n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₁.isPushout : CategoryTheory.IsPushout (SSet.stdSimplex.δ 0) (SSet.stdSimplex.δ 1) SSet.horn₂₁.ι₀₁ SSet.horn₂₁.ι₁₂
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateIsoEquiv_symm_apply_inv : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (β : R₁ ≅ R₂),
  ((CategoryTheory.conjugateIsoEquiv adj₁ adj₂).symm β).inv = (CategoryTheory.conjugateEquiv adj₂ adj₁).symm β.inv
-- Mathlib.NumberTheory.MulChar.Basic
/-- If `χ` is of odd order, then `χ(-1) = 1`  -/
MulChar.val_neg_one_eq_one_of_odd_order : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommMonoidWithZero R'] {χ : MulChar R R'} {n : ℕ},
  Odd n → χ ^ n = 1 → χ (-1) = 1
-- Init.Data.Array.Lemmas
Array.foldl_reverse : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : β → α → β} {b : β},
  Array.foldl f b xs.reverse = Array.foldr (fun x y => f y x) b xs
-- Mathlib.Analysis.Complex.Circle
/-- The coercion `Circle → ℂ` as a monoid homomorphism.  -/
Circle.coeHom : Circle →* ℂ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeWhisker.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconeWhisker =
    CategoryTheory.Limits.Cocone.extInv
      (CategoryTheory.Iso.refl (H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c)).pt) ⋯
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.of_toAddSubgroup_le : ∀ {R : Type u_1} [inst : Ring R] {S : Type u_2} [inst_1 : Ring S] {M : Type u_4} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module S M] {U : Submodule R M} {V : Submodule S M},
  U.toAddSubgroup ≤ V.toAddSubgroup → ∀ {x y : M}, x ≡ y [SMOD U] → x ≡ y [SMOD V]
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- An isomorphism of `PresheafedSpace`s is a homeomorphism of the underlying space, and a
natural transformation between the sheaves.
 -/
AlgebraicGeometry.PresheafedSpace.isoOfComponents : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : AlgebraicGeometry.PresheafedSpace C} →
      (H : ↑X ≅ ↑Y) → ((TopCat.Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf) → (X ≅ Y)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.nth.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (n : ℕ), T.nth (Int.ofNat n.succ) = T.right.nth n
-- Mathlib.RingTheory.Noetherian.Defs
/-- **Alias** of the reverse direction of `isNoetherian_iff'`. -/
isNoetherian_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  WellFoundedGT (Submodule R M) → IsNoetherian R M
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The "homotopic relative to boundary" relation between `GenLoop`s.  -/
GenLoop.Homotopic : {N : Type u_1} → {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → ↑(GenLoop N X x) → ↑(GenLoop N X x) → Prop
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.of_separableSpace : ∀ {α : Type u} [t : TopologicalSpace α] [h : TopologicalSpace.SeparableSpace α] (s : Set α),
  TopologicalSpace.IsSeparable s
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_mapComp_hom_toNatTrans_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {a b c : CategoryTheory.LocallyDiscrete Cᵒᵖ} (x : a ⟶ b) (x_1 : b ⟶ c)
  (X : CategoryTheory.Sheaf (J.over (Opposite.unop a.as)) A) (X_1 : (CategoryTheory.Over (Opposite.unop c.as))ᵒᵖ),
  (((J.pseudofunctorOver A).mapComp x x_1).hom.toNatTrans.app X).hom.app X_1 =
    X.obj.map ((CategoryTheory.Over.mapComp x_1.as.unop x.as.unop).inv.app (Opposite.unop X_1)).op
-- Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
QuadraticModuleCat.cliffordAlgebra_map : ∀ {R : Type u} [inst : CommRing R] {_M _N : QuadraticModuleCat R} (f : _M ⟶ _N),
  QuadraticModuleCat.cliffordAlgebra.map f = AlgCat.ofHom (CliffordAlgebra.map (QuadraticModuleCat.Hom.toIsometry f))
-- Lean.Meta.Offset
Lean.Meta.isDefEqOffset : Lean.Expr → Lean.Expr → Lean.MetaM Lean.LBool
-- Mathlib.Topology.Convenient.Category
/-- Use the abbreviation `TopCat.toContinuousGeneratedByCat` for the faithful
functor `TopCat ⥤ ContinuousGeneratedByCat X` which sends
a topological space `Y` to the same type `Y`, with the same topology, but
considered as an object of `ContinuousGeneratedByCat X`.  -/
ContinuousGeneratedByCat.instHasForget₂TopCatContinuousMapCarrierContinuousMapGeneratedByCarrier : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.HasForget₂ TopCat (ContinuousGeneratedByCat X)
-- Mathlib.Data.List.Permutation
List.length_permutationsAux : ∀ {α : Type u_1} (ts is : List α),
  (ts.permutationsAux is).length + is.length.factorial = (ts.length + is.length).factorial
-- Lean.Meta.Tactic.Grind.ProveEq
/-- If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,
and internalize the result.

This is an auxiliary function used at `proveEq?` and `proveHEq?`.
 -/
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.ensureInternalized : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- The support of `G.deleteIncidenceSet x` is a subset of the support of `G` set difference the
singleton set `{x}`.  -/
SimpleGraph.support_deleteIncidenceSet_subset : ∀ {V : Type u_1} (G : SimpleGraph V) (x : V), (G.deleteIncidenceSet x).support ⊆ G.support \ {x}
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E}
  {g : α → F} {l : Filter α},
  Asymptotics.IsBigOWith c l f g →
    ∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → Asymptotics.IsBigOWith c l' (f ∘ k) (g ∘ k)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxEntry_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.maxEntry he = t₂.maxEntry ⋯
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instOrdOrdinal : Ord Std.Time.Week.OfYear.Ordinal
-- Mathlib.Tactic.Ring.Common
/-- Evaluates an atom, an expression where `ring` can find no additional structure.

* `a = a ^ 1 * 1 + 0`
 -/
Mathlib.Tactic.Ring.Common.evalAtom : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            (e : Q(«$α»)) →
              Mathlib.Tactic.AtomM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) e)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableAt_atlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {e : OpenPartialHomeomorph M H} [IsManifold I 1 M],
  e ∈ atlas H M → ∀ {x : M}, x ∈ e.source → MDiffAt ↑e x
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.toInvariantForm_form : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic], P.toInvariantForm.form = P.RootForm
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instHasLimits : ∀ {X : AlgebraicGeometry.Scheme}, CategoryTheory.Limits.HasLimits X.Modules
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- Pullback of an `OuterMeasure`: `comap f μ s = μ (f '' s)`.  -/
MeasureTheory.OuterMeasure.comap : {α : Type u_1} → {β : Type u_3} → (α → β) → MeasureTheory.OuterMeasure β →ₗ[ENNReal] MeasureTheory.OuterMeasure α
-- Mathlib.Analysis.CStarAlgebra.Spectrum
StarAlgEquiv.isometry : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass F A B] (φ : F), Isometry ⇑φ
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instDistribSMul' : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : AddZeroClass M₀] → [DistribSMul G₀ M₀] → DistribSMul G₀ (Lex M₀)
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtDTreeMap.minEntry! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Inhabited ((a : α) × β a)] → Std.ExtDTreeMap α β cmp → (a : α) × β a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.exists_mem_pow_notMem_pow_succ : ∀ {A : Type u_2} [inst : CommRing A] [IsDedekindDomain A] (I : Ideal A),
  I ≠ ⊥ → I ≠ ⊤ → ∀ (e : ℕ), ∃ x ∈ I ^ e, x ∉ I ^ (e + 1)
-- Mathlib.Analysis.Convex.PathConnected
/-- A nonempty convex set is path connected.  -/
Convex.isPathConnected : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E] {s : Set E}, Convex ℝ s → s.Nonempty → IsPathConnected s
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Ico_left : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₁ ≤ a₂ → Set.Ico a₂ b ⊆ Set.Ico a₁ b
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
StarOrderedRing.nonneg_iff_spectrum_nonneg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (a : A), autoParam (p a) StarOrderedRing.nonneg_iff_spectrum_nonneg._auto_1 → (0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x)
-- Init.Data.Vector.InsertIdx
Vector.mem_insertIdx : ∀ {α : Type u} {a : α} {n i : ℕ} {b : α} {xs : Vector α n} {h : i ≤ n}, a ∈ xs.insertIdx i b h ↔ a = b ∨ a ∈ xs
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_alter_eq_sub_one : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  k ∈ m → (f (Std.ExtDHashMap.Const.get? m k)).isNone = true → (Std.ExtDHashMap.Const.alter m k f).size = m.size - 1
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (a : δ) (k : α) (v : β k) (t : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.forInStep.go✝ f (Std.DHashMap.Internal.AssocList.cons k v t) a = do
    let __do_lift ← f k v a
    match __do_lift with
      | ForInStep.done d => pure (ForInStep.done d)
      | ForInStep.yield d => Std.DHashMap.Internal.AssocList.forInStep.go✝ f t d
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurveAt.comp_mul_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {t₀ : ℝ},
  IsMIntegralCurveAt γ v t₀ → ∀ {a : ℝ}, a ≠ 0 → IsMIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
-- Mathlib.RingTheory.MatrixAlgebra
/-- (Implementation detail).
The function underlying `(A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A`,
as an `R`-bilinear map.
 -/
MatrixEquivTensor.toFunBilinear : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A →ₗ[R] Matrix n n R →ₗ[R] Matrix n n A
-- Mathlib.Data.ENNReal.Real
ENNReal.ofNat_lt_ofReal : ∀ {n : ℕ} [inst : n.AtLeastTwo] {r : ℝ}, OfNat.ofNat n < ENNReal.ofReal r ↔ OfNat.ofNat n < r
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` and `G'` are finite Galois groups for `B/A`, then `G` is isomorphic to `G'`.  -/
IsGaloisGroup.mulEquivCongr : (G : Type u_1) →
  (G' : Type u_2) →
    [inst : Group G] →
      [inst_1 : Group G'] →
        (A : Type u_5) →
          (B : Type u_6) →
            [inst_2 : CommRing A] →
              [inst_3 : CommRing B] →
                [IsDomain B] →
                  [inst_5 : Algebra A B] →
                    [FaithfulSMul A B] →
                      [inst_7 : MulSemiringAction G B] →
                        [inst_8 : MulSemiringAction G' B] →
                          [IsGaloisGroup G A B] → [IsGaloisGroup G' A B] → [Finite G] → [Finite G'] → G ≃* G'
-- Mathlib.Topology.Closure
sdiff_subset_closure_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, s \ t ⊆ closure t ↔ s ⊆ closure t
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.HasPullbacksAgainst P'` states that for any morphism `f` satisfying `P'`,
`P` has pullbacks along `f`.  -/
CategoryTheory.MorphismProperty.HasPullbacksAgainst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Group.Defs
/-- **Alias** of `div_eq_mul_inv`.

---

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of `DivInvMonoid.div_eq_mul_inv` ensuring that the types unfold better.
 -/
division_def : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
-- Lean.Data.Lsp.Basic
/-- A batch of `TextEdit`s to perform on a versioned text document.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocumentEdit)  -/
Lean.Lsp.TextDocumentEdit : Type
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- In a normed vector space, the subtraction of a measurable function and a strongly measurable
function is measurable. Note that this is not true without further second-countability assumptions
for the subtraction of two measurable functions.  -/
Measurable.sub_stronglyMeasurable : ∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E]
  [inst_2 : MeasurableSpace E] [BorelSpace E] [ContinuousAdd E] [ContinuousNeg E]
  [TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E},
  Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g - f)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.IsContinuous.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D},
  (∀ (G : CategoryTheory.Sheaf K (Type (max u₁ v₁ u₂ v₂))), CategoryTheory.Presieve.IsSheaf J (F.op.comp G.obj)) →
    F.IsContinuous J K
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.rTensor_comp_δ : ∀ {G : Type v} [inst : Monoid G] {X Y : Action (Type w) G} (Z : Action (Type w) G) {k : Type u}
  [inst_1 : CommSemiring k] (f : X ⟶ Y),
  (Representation.IntertwiningMap.rTensor (Representation.linearize k G Z) (Representation.linearizeMap f)).comp
      (Representation.LinearizeMonoidal.δ X Z) =
    (Representation.LinearizeMonoidal.δ Y Z).comp
      (Representation.linearizeMap (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_ciSup : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] [Nonempty ι] (e : α ≃o β) {f : ι → α},
  BddAbove (Set.range f) → e (⨆ i, f i) = ⨆ i, e (f i)