mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAlgEquiv_trans_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R]
  [inst_1 : Fintype n] [inst_2 : Fintype m] [inst_3 : Fintype o] [inst_4 : DecidableEq m] [inst_5 : DecidableEq n]
  [inst_6 : DecidableEq o] [inst_7 : Semiring A] [inst_8 : Algebra R A] (e : m ≃ n) (e' : n ≃ o),
  (Matrix.reindexAlgEquiv R A e).trans (Matrix.reindexAlgEquiv R A e') = Matrix.reindexAlgEquiv R A (e.trans e')
-- Init.Data.Rat.Lemmas
Rat.neg_lt_iff : ∀ {a b : ℚ}, -a < b ↔ -b < a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.map_neg : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Projective R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).neg (⇑f ∘ P) = ⇑f ∘ W'.neg P
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given two finite disjoint sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` equals
the sum of `f i` over `i ∈ s` plus the sum of `f i` over `i ∈ t`.  -/
finsum_mem_union : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  Disjoint s t →
    s.Finite → t.Finite → ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Algebra.Module.Projective
Module.Projective.tensorProduct : ∀ {R : Type u} [inst : Semiring R] {R₀ : Type u_2} {M : Type u_1} {N : Type u_3} [inst_1 : CommSemiring R₀]
  [inst_2 : Algebra R₀ R] [inst_3 : AddCommMonoid M] [inst_4 : Module R₀ M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R₀ R M] [inst_7 : AddCommMonoid N] [inst_8 : Module R₀ N] [hM : Module.Projective R M]
  [hN : Module.Projective R₀ N], Module.Projective R (TensorProduct R₀ M N)
-- Mathlib.Order.Booleanisation
/-- The order on `Booleanisation α` is as follows: For `a b : α`,
* `a < b` iff `a < b` in `α`
* `a < bᶜ` iff `a` and `b` are disjoint in `α`
* `aᶜ < bᶜ` iff `b < a` in `α`
* `¬ aᶜ < b`  -/
Booleanisation.LT : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Booleanisation α → Booleanisation α → Prop
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `swap_dist`.  -/
swap_hammingDist : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)],
  Function.swap hammingDist = hammingDist
-- Mathlib.Algebra.Category.BoolRing
BoolRing.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} BoolRing
-- Mathlib.Tactic.Positivity.Core
/-- Given an expression `e`, use the core method of the `positivity` tactic to prove it nonnegative.
 -/
Mathlib.Meta.Positivity.proveNonneg : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Notation
Lean.guardMsgsSpecElt : Lean.ParserDescr
-- Mathlib.Data.Seq.Defs
/-- a relation is bisimilar if it meets the `BisimO` test  -/
Stream'.Seq.IsBisimulation : {α : Type u} → (Stream'.Seq α → Stream'.Seq α → Prop) → Prop
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C}
  (h : S₂.L₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f₁ (CategoryTheory.CategoryStruct.comp S₂.v₁₂ h) =
    CategoryTheory.CategoryStruct.comp S₁.v₁₂ (CategoryTheory.CategoryStruct.comp self.f₂ h)
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.edge_mem : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.edge ∈ G.edgeSet
-- Mathlib.Analysis.Seminorm
Seminorm.le_finset_sup_apply : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : ι → Seminorm 𝕜 E} {s : Finset ι} {x : E} {i : ι}, i ∈ s → (p i) x ≤ (s.sup p) x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
card_addOrderOf_eq_totient_aux₂ : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | n • a = 0}.card ≤ n) →
    ∀ {d : ℕ}, d ∣ Fintype.card α → {a | addOrderOf a = d}.card = d.totient
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.right_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P}, s.IsDiameter p₁ p₂ → p₂ ∈ s
-- Lean.Meta.Tactic.Util
Lean.Meta.exactlyOne : List Lean.MVarId →
  optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals") →
    Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.star_eq_conjTranspose : ∀ {n : Type u_2} {A : Type u_5} [inst : Star A] {M : CStarMatrix n n A}, star M = M.conjTranspose
-- Mathlib.Data.Finset.Fold
Finset.fold_min_lt : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  Finset.fold min b f s < c ↔ b < c ∨ ∃ x ∈ s, f x < c
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the exponentiation to power `s : ℤ` of (± `y`) (here taking the specified signs) is ± `y ^ s`;
return this proof and the computed sign.  -/
Mathlib.Tactic.FieldSimp.Sign.zpow : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (y : Q(«$M»)) →
        (g : Mathlib.Tactic.FieldSimp.Sign M) →
          (s : ℤ) →
            Lean.MetaM
              ((G : Mathlib.Tactic.FieldSimp.Sign M) ×
                have a := G.expr q(«$y» ^ «$s»);
                have a_1 := g.expr y;
                Q(«$a_1» ^ «$s» = «$a»))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_union_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (mem : k ∈ t₂), (t₁ ∪ t₂)[k] = t₂[k]
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.leftAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : R.IsRightAdjoint], R.leftAdjoint = ⋯.choose
-- Lean.Elab.Do.Switch
Lean.Elab.Term.expandTermUnless : Lean.Macro
-- Init.Grind.Ring.Field
/-- The (n+1)-st power of any element is the element multiplied by the n-th power.  -/
Lean.Grind.Field.zpow_succ : ∀ {α : Type u} [self : Lean.Grind.Field α] (a : α) (n : ℕ), a ^ (↑n + 1) = a ^ ↑n * a
-- Mathlib.Algebra.Algebra.Equiv
/-- An equivalence of algebras commutes with the action of scalars.  -/
AlgEquivClass.commutes : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : EquivLike F A B}
  [self : AlgEquivClass F R A B] (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The σ-algebra of cylinder events on `Δ`. It is the smallest σ-algebra making the projections
on the `i`-th coordinate measurable for all `i ∈ Δ`.  -/
MeasureTheory.cylinderEvents : {ι : Type u_2} → {X : ι → Type u_3} → [m : (i : ι) → MeasurableSpace (X i)] → Set ι → MeasurableSpace ((i : ι) → X i)
-- Init.Data.Vector.Basic
Vector.drop_eq_cast_extract : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ), xs.drop i = Vector.cast ⋯ (xs.extract i)
-- Mathlib.RingTheory.Polynomial.Quotient
/-- Split off from `quotientEquivQuotientMvPolynomial` for speed.  -/
MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] (I : Ideal R),
  Function.RightInverse
    (MvPolynomial.eval₂ (Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯)
      fun i => (Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i))
    ⇑(Ideal.Quotient.lift (Ideal.map MvPolynomial.C I)
        (MvPolynomial.eval₂Hom (MvPolynomial.C.comp (Ideal.Quotient.mk I)) MvPolynomial.X) ⋯)
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.handle : Lean.Server.StatefulRequestHandler →
  Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.isWeierstrassFactorizationAt_iff : ∀ {A : Type u_1} [inst : CommRing A] (g : PowerSeries A) (f : Polynomial A) (h : PowerSeries A) (I : Ideal A),
  g.IsWeierstrassFactorizationAt f h I ↔ f.IsDistinguishedAt I ∧ IsUnit h ∧ g = ↑f * h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.data : Lean.Lsp.SemanticTokens → Array ℕ
-- Mathlib.GroupTheory.DivisibleHull
/-- Coercion from `M` to `DivisibleHull M` defined as `m ↦ m / 1`.  -/
DivisibleHull.instCoe : {M : Type u_1} → [inst : AddCommMonoid M] → Coe M (DivisibleHull M)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.coe_taylorEquiv : ∀ {R : Type u_1} [inst : CommRing R] (r : R), ↑↑(Polynomial.taylorEquiv r) = Polynomial.taylor r
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.isoSheafify.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P : CategoryTheory.Functor Cᵒᵖ D} (hP : CategoryTheory.Presheaf.IsSheaf J P),
  CategoryTheory.isoSheafify J hP = CategoryTheory.isoSheafify J hP
-- Std.Time.Format.Modifier
Std.Time.DayPeriod.pm.sizeOf_spec : sizeOf Std.Time.DayPeriod.pm = 1
-- Mathlib.GroupTheory.Congruence.Defs
/-- A congruence relation on a type with a multiplication is an equivalence relation which
preserves multiplication.  -/
Con : (M : Type u_1) → [Mul M] → Type u_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivAt.sin : ∀ {f : ℝ → ℝ} {f' x : ℝ}, HasDerivAt f f' x → HasDerivAt (fun x => Real.sin (f x)) (Real.cos (f x) * f') x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalClosure_empty : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.normalClosure ∅ = ⊥
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_comp_tensorComm : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Invertible 2]
  (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂),
  QuadraticMap.comp (Q₂.tmul Q₁) ↑(TensorProduct.comm R M₁ M₂) = Q₁.tmul Q₂
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smulInvariantMeasure_map : ∀ {M : Type uM} {α : Type uα} {β : Type uβ} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : SMul M α]
  [inst_3 : SMul M β] [MeasurableConstSMul M β] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ]
  (f : α → β),
  (∀ (m : M) (a : α), f (m • a) = m • f a) →
    Measurable f → MeasureTheory.SMulInvariantMeasure M β (MeasureTheory.Measure.map f μ)
-- Mathlib.Order.BoundedOrder.Basic
dite_ne_top : ∀ {α : Type u} [inst : Top α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α},
  (∀ (h : p), a h ≠ ⊤) → (∀ (h : ¬p), b h ≠ ⊤) → (if h : p then a h else b h) ≠ ⊤
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι},
  ProbabilityTheory.iCondIndepSets m' hm' π μ →
    a ∉ S → ProbabilityTheory.CondIndepSets m' hm' (piiUnionInter π ↑S) (π a) μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_map : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.biprod.map f g) =
    CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr
-- Lean.Parser.Extra
Lean.Parser.withCache.parenthesizer : Lean.Name → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_eq_iff_eq : ∀ {a b : Real.Angle}, a.sign ≠ 0 → a.sign = b.sign → (2 • a = 2 • b ↔ a = b)
-- Mathlib.Topology.Spectral.Hom
SpectralMap.instSpectralMapClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  SpectralMapClass (SpectralMap α β) α β
-- Mathlib.Order.Heyting.Hom
CoheytingHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (f : CoheytingHom α β)
  (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.mk.injEq : ∀ (goal : Lean.MVarId) (mvars : Std.HashSet Lean.MVarId) (goal_1 : Lean.MVarId) (mvars_1 : Std.HashSet Lean.MVarId),
  ({ goal := goal, mvars := mvars } = { goal := goal_1, mvars := mvars_1 }) = (goal = goal_1 ∧ mvars = mvars_1)
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The left inclusion `K.X i ⟶ K.cylinder.X j` when `c.Rel j i`.  -/
HomologicalComplex.cylinder.inlX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → (i j : ι) → c.Rel j i → (K.X i ⟶ K.cylinder.X j)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.instCommRingColimitType : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → CommRing (CommRingCat.Colimits.ColimitType F)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The cosine of an angle in a right-angled triangle as a ratio of sides.  -/
Orientation.cos_oangle_add_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y = ↑(Real.pi / 2) → (o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldlM_eq_foldlM_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.TreeMap.foldlM (fun d a x => f d a) init t = Array.foldlM f init t.keysArray
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskerLeft_app_fst : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ : CategoryTheory.Functor J C) {F₂ F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft F₁ g).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂'.obj j)) =
    CategoryTheory.SemiCartesianMonoidalCategory.fst (F₁.obj j) (F₂.obj j)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α),
  r.toList = (Std.Roo.Internal.iter r).toList
-- Mathlib.Algebra.Opposites
AddOpposite.instOne : {α : Type u_1} → [One α] → One αᵃᵒᵖ
-- Mathlib.Computability.RE
Partrec.dom_re : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α →. β},
  Partrec f → REPred fun a => (f a).Dom
-- Std.Http.Data.Body.Stream
/-- Creates a selector that resolves when a producer is waiting (or the channel closes).
 -/
Std.Http.Body.Stream.recvSelector : Std.Http.Body.Stream → Std.Async.Selector (Option Std.Http.Chunk)
-- Mathlib.LinearAlgebra.Contraction
homTensorHomEquiv_apply : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  [inst_9 : Module.Projective R M] [inst_10 : Module.Finite R M] [inst_11 : Module.Projective R N]
  [inst_12 : Module.Finite R N] (x : TensorProduct R (M →ₗ[R] P) (N →ₗ[R] Q)),
  (homTensorHomEquiv R M N P Q) x = (TensorProduct.homTensorHomMap (RingHom.id R) M N P Q) x
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
compact space converging pointwise to a continuous function `f`, then `F n` converges uniformly
to `f`.  -/
Antitone.tendstoUniformly_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} [CompactSpace α],
  (∀ (i : ι), Continuous (F i)) →
    Antitone F →
      Continuous f →
        (∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) → TendstoUniformly F f Filter.atTop
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldl_eq_foldl_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.TreeMap.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If one controls the norm of every `f x`, then one controls the norm of `f`.  -/
ContinuousMultilinearMap.opNorm_le_bound : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  {f : ContinuousMultilinearMap 𝕜 E G} {M : ℝ}, 0 ≤ M → (∀ (m : (i : ι) → E i), ‖f m‖ ≤ M * ∏ i, ‖m i‖) → ‖f‖ ≤ M
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_mul : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : Group M] [MulLeftMono M] [MulRightMono M]
  {s t : Set M}, s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (s * t) = sInf s * sInf t
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The action of the Galois group on infinite places.  -/
NumberField.InfinitePlace.instMulActionAlgEquiv : {k : Type u_1} →
  [inst : Field k] →
    {K : Type u_2} → [inst_1 : Field K] → [inst_2 : Algebra k K] → MulAction Gal(K/k) (NumberField.InfinitePlace K)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.instEmptyCollection : {α : Type u_1} → EmptyCollection (Multiset α)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.mk : Lean.Meta.Grind.Arith.CommRing.Semiring →
  ℕ → Lean.Expr → Option (Option Lean.Expr) → Option Lean.Expr → Lean.Meta.Grind.Arith.CommRing.CommSemiring
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- For any `I : RingCon R`, when we view it as an ideal, `I.subtype` is the injective `R`-linear map
`I → R`.
 -/
TwoSidedIdeal.subtype : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → ↥I →ₗ[R] R
-- Mathlib.Algebra.Algebra.Basic
PUnit.algebra : {R : Type u_1} → [inst : CommSemiring R] → Algebra R PUnit.{v + 1}
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
sInf_eq_argmin_on : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [inst_1 : WellFoundedLT α] (hs : s.Nonempty),
  sInf s = Function.argminOn id s hs
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_id' : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ⇑(ContinuousLinearMap.id R₁ M₁) = id
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex : ∀ {K : Type u_1} [inst : Field K] [NumberField K] (s : Subgroup (NumberField.RingOfIntegers K)ˣ),
  s.FiniteIndex ↔ (s ⊔ NumberField.Units.torsion K).FiniteIndex
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_apply_of_not_predicate : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R} (a : A),
  ¬p a → cfcₙ f a = 0
-- Mathlib.Algebra.Order.Hom.Ring
/-- Turn an element of a type `F` satisfying `OrderHomClass F α β` and `RingHomClass F α β`
into an actual `OrderRingHom`.
This is declared as the default coercion from `F` to `α →+*o β`.  -/
OrderRingHomClass.toOrderRingHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : NonAssocSemiring α] →
          [inst_2 : Preorder α] →
            [inst_3 : NonAssocSemiring β] →
              [inst_4 : Preorder β] → [OrderHomClass F α β] → [RingHomClass F α β] → F → α →+*o β
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_ne_top : ∀ {a b : ENNReal}, a ≠ ⊤ → a - b ≠ ⊤
-- Mathlib.Order.Hom.Bounded
BotHom.instLattice : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [inst_1 : Lattice β] → [inst_2 : OrderBot β] → Lattice (BotHom α β)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.ofNonUnitalStarAlgHom_symm_apply : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂) (a : A₂),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂).symm a = g a
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_iInter' : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_3} {s : ι → Set α} [∀ (i : ι), (s i).OrdConnected],
  (⋂ i, s i).OrdConnected
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
/-- If $((X_{i,j})_{j \in \kappa_i})_{i \in \iota}$ are jointly Gaussian, then they are independent
if for all $i_1 \ne i_2 \in \iota$ and for all $j_1 \in \kappa_{i_1}, j_2 \in \kappa_{i_2}$,
$\mathrm{Cov}(X_{i_1, j_1}, X_{i_2, j_2}) = 0$.  -/
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eval : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {κ : ι → Type u_4}
  [∀ (i : ι), Finite (κ i)] {X : (i : ι) → κ i → Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω i j => X i j ω) P →
    (∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), ProbabilityTheory.covariance (X i k) (X j l) P = 0) →
      ProbabilityTheory.iIndepFun (fun i ω j => X i j ω) P
-- Mathlib.Order.Compare
cmpLE_swap : ∀ {α : Type u_3} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (x y : α),
  (cmpLE x y).swap = cmpLE y x
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.one_def : ∀ {X : Type u_1} [inst : TopologicalSpace X], 1 = Homeomorph.refl X
-- Mathlib.Order.Max
instNoBotOrderOfNoMinOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α], NoBotOrder α