mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The centroid as an affine combination over a `Fintype`.  -/
Finset.centroid_eq_affineCombination_fintype : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_4 : Fintype ι] (p : ι → P),
  Finset.centroid k s p = (Finset.affineCombination k Finset.univ p) (Finset.centroidWeightsIndicator k s)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.isPositive_smul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → T ≠ 0 → ∀ {α : 𝕜}, (α • T).IsPositive ↔ 0 ≤ α
-- Batteries.Control.Nondet.Basic
/-- Filter and map a nondeterministic value using a monadic function which may return `none`.  -/
Nondet.filterMapM : {σ : Type} →
  {m : Type → Type} →
    [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → (α → m (Option β)) → Nondet m α → Nondet m β
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mk_coe : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (h : ∀ (m : R) (x : M), (↑f).toFun (m • x) = σ m • (↑f).toFun x),
  { toAddHom := ↑f, map_smul' := h } = f
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor_obj : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) (i : 𝒰.I₀), d.functor.obj i = (d.cocone i).pt.left
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdNatCoreE₂HomologicalNat : CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.HasFirstPageComputation
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
/-- Category instance on the indexing category.  -/
CategoryTheory.IndParallelPairPresentation.ℐ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} →
      {f g : A ⟶ B} → (self : CategoryTheory.IndParallelPairPresentation f g) → CategoryTheory.SmallCategory self.I
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- A linear ordered semiring is a locally convex space over itself.  -/
LinearOrderedSemiring.toLocallyConvexSpace : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Semiring R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  [OrderTopology R], LocallyConvexSpace R R
-- Mathlib.Topology.Algebra.Group.Defs
Continuous.fun_neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G}, Continuous f → Continuous fun i => -f i
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_zero_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.coeff 0 1 = 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_fac : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F) (j : J),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.PresheafedSpace.colimitCocone F).ι.app j)
      (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc F s) =
    s.ι.app j
-- Std.Data.HashMap.Lemmas
Std.HashMap.toList_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {f : α → β → γ},
  (Std.HashMap.map f m).toList.Perm (List.map (fun p => (p.1, f p.1 p.2)) m.toList)
-- Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
/-- Arithmetic subgroups of `GL(2, ℝ)` act properly discontinuously on `ℍ`.  -/
Subgroup.IsArithmetic.properlyDiscontinuous : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic], ProperlyDiscontinuousSMul (↥𝒢) UpperHalfPlane
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (Std.ExtDTreeMap.ofList l cmp).getKey! k' = k
-- Mathlib.Algebra.Polynomial.Div
Polynomial.map_mod_divByMonic : ∀ {R : Type u} {S : Type v} [inst : Ring R] {p q : Polynomial R} [inst_1 : Ring S] (f : R →+* S),
  q.Monic →
    Polynomial.map f (p /ₘ q) = Polynomial.map f p /ₘ Polynomial.map f q ∧
      Polynomial.map f (p %ₘ q) = Polynomial.map f p %ₘ Polynomial.map f q
-- Init.Data.String.Lemmas.StringOrder
String.instLawfulOrderLT : Std.LawfulOrderLT String
-- Init.Data.Nat.Basic
Nat.sub_sub : ∀ (n m k : ℕ), n - m - k = n - (m + k)
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_neg : ∀ {M : Type u_10} {F : Type u_11} [inst : AddGroup M] [inst_1 : FunLike F M M] [AddMonoidHomClass F M M] (f : F) (n : ℕ)
  (x : M), (⇑f)^[n] (-x) = -(⇑f)^[n] x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.cocone_naturality : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (AddMonCat.FilteredColimits.coconeMorphism F j') =
    AddMonCat.FilteredColimits.coconeMorphism F j
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.cuspFunction_neg`. -/
ModularFormClass.cuspFunction_neg : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : F) [ModularFormClass F Γ k], UpperHalfPlane.cuspFunction h (-⇑f) = -UpperHalfPlane.cuspFunction h ⇑f
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.eq_top : ∀ {G : Type u_1} [inst : Group G] [Group.IsNilpotent G] {a b : ℕ},
  a ≠ b → Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b → Subgroup.upperCentralSeries G a = ⊤
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.isOrtho_smul_right : ∀ {R₄ : Type u_7} {M₄ : Type u_8} [inst : CommRing R₄] [IsDomain R₄] [inst_2 : AddCommGroup M₄] [inst_3 : Module R₄ M₄]
  {G : LinearMap.BilinForm R₄ M₄} {x y : M₄} {a : R₄}, a ≠ 0 → (G.IsOrtho x (a • y) ↔ G.IsOrtho x y)
-- Mathlib.GroupTheory.Exponent
Group.exponent_dvd_nat_card : ∀ {G : Type u} [inst : Group G], Monoid.exponent G ∣ Nat.card G
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuous_tsum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_4} {f : ι → α → ENNReal},
  (∀ (i : ι), LowerSemicontinuous (f i)) → LowerSemicontinuous fun x' => ∑' (i : ι), f i x'
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivWithinAt.neg : ∀ {𝕜 : 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' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'} {f' : TangentSpace I z →L[𝕜] E'} {s : Set M},
  HasMFDerivAt[s] f z f' → HasMFDerivAt[s] (-f) z (-f')
-- Mathlib.Order.SuccPred.Basic
Order.succ_lt_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a < b → Order.succ a < Order.succ b
-- Mathlib.Analysis.Convex.Uniform
/-- A *uniformly convex space* is a real normed space where the triangle inequality is strict with a
uniform bound. Namely, over the `x` and `y` of norm `1`, `‖x + y‖` is uniformly bounded above
by a constant `< 2` when `‖x - y‖` is uniformly bounded below by a positive constant.  -/
UniformConvexSpace : (E : Type u_1) → [SeminormedAddCommGroup E] → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comp_h₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂),
  (h.comp h').h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₁ h'.h₀
-- Mathlib.Algebra.Ring.Defs
CommRing.toNonAssocCommRing : {α : Type u} → [CommRing α] → NonAssocCommRing α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.toArray_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.toArray = t₂.toArray
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.eval_udiv : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVBinOp.udiv.eval = fun x1 x2 => x1 / x2
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck_fold_formula_eq : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)),
      have performRatCheck_fold_res :=
        Array.foldl (fun x ratHint => if x.2 = true then x.1.performRatCheck p ratHint else (x.1, false)) (f, true)
          ratHints;
      performRatCheck_fold_res.1 = f
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeqSet.congr_simp : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {f f_1 : ι → α → β} (e_f : f = f_1) {μ μ_1 : MeasureTheory.Measure α} (e_μ : μ = μ_1)
  (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p p_1 : α → (ι → β) → Prop),
  p = p_1 → ∀ (a a_1 : α), a = a_1 → aeSeqSet hf p a = aeSeqSet ⋯ p_1 a_1
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a
`C^{k+1}` section, the result `∇_X σ` is a `C^k` section.
This is a class so typeclass inference can deduce this automatically.
We will prove in a later file that any `C^(k+1)` covariant derivative is `C^k`.
 -/
CovariantDerivative.ContMDiffCovariantDerivative : {𝕜 : 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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)] →
                                        [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] →
                                          [inst_14 : FiberBundle F V] →
                                            [IsManifold I 1 M] →
                                              [VectorBundle 𝕜 F V] → CovariantDerivative I F V → WithTop ℕ∞ → Prop
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.le_of_pow_le : ∀ {R : Type u} [inst : CommSemiring R] {I P : Ideal R} [hP : P.IsPrime] {n : ℕ}, I ^ n ≤ P → I ≤ P
-- Mathlib.Algebra.Order.Group.Finset
/-- Also see `Finset.add_sup''` that works for canonically ordered monoids.  -/
Finset.add_sup' : ∀ {ι : Type u_1} {G : Type u_4} [inst : AddGroup G] [inst_1 : LinearOrder G] [AddLeftMono G] (s : Finset ι) (f : ι → G)
  (a : G) (hs : s.Nonempty), a + s.sup' hs f = s.sup' hs fun i => a + f i
-- Mathlib.Data.Finset.Defs
Finset.mem_of_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
CStarAlgebra.directedOn_nonneg_ball : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  DirectedOn (fun x1 x2 => x1 ≤ x2) ({x | 0 ≤ x} ∩ Metric.ball 0 1)
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_ge`. -/
LE.le.compRel_symm : ∀ {α : Type u_1} {a b : α} [inst : LE α], b ≤ a → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {l : List α} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.unitOfList l) k = ()
-- Mathlib.Order.Booleanisation
Booleanisation.lift_bot : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α], Booleanisation.lift ⊥ = ⊥
-- Mathlib.Analysis.Analytic.Constructions
ContinuousMultilinearMap.restrictScalars.congr_simp : ∀ (R : Type u) {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂] {A : Type u_1}
  [inst_7 : Semiring A] [inst_8 : SMul R A] [inst_9 : (i : ι) → Module A (M₁ i)] [inst_10 : Module A M₂]
  [inst_11 : ∀ (i : ι), IsScalarTower R A (M₁ i)] [inst_12 : IsScalarTower R A M₂]
  (f f_1 : ContinuousMultilinearMap A M₁ M₂),
  f = f_1 → ContinuousMultilinearMap.restrictScalars R f = ContinuousMultilinearMap.restrictScalars R f_1
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_set_eq_zero_iff : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s = 0 ↔ s = ∅
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMul.eq_1 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M],
  ContinuousMap.instSMul = { smul := fun r f => { toFun := r • ⇑f, continuous_toFun := ⋯ } }
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.lift_mapComp : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  {a b c : CategoryTheory.FreeBicategory B} (x : a ⟶ b) (x_1 : b ⟶ c),
  (CategoryTheory.FreeBicategory.lift F).mapComp x x_1 =
    CategoryTheory.Iso.refl (CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.comp x x_1))
-- Std.Sync.Channel
/-- Producers that are blocked on a consumer taking their value as there was no buffer space
available when they tried to enqueue.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.producers : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → Std.Queue (IO.Promise Bool)
-- Mathlib.Order.Minimal
image_antitone_setOfPred_maximal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ x ≤ y)) →
    f '' {x | Maximal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ f '' s) x}
-- Init.Data.UInt.Basic
/-- Bitwise or for 8-bit unsigned integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.lor : UInt8 → UInt8 → UInt8
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.isoSum_inv_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (A ⊕ B) C) (a : A),
  F.isoSum.inv.app (Sum.inl a) = CategoryTheory.CategoryStruct.id (F.obj (Sum.inl a))
-- Mathlib.NumberTheory.AlmostPrime
Nat.IsAlmostPrime.eq_1 : ∀ (k n : ℕ), k.IsAlmostPrime n = (n ≠ 0 ∧ ArithmeticFunction.cardFactors n = k)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_sub : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] (x y : AddMonoidAlgebra R M), (x - y).coeff = x.coeff - y.coeff
-- Mathlib.Algebra.Group.Action.Defs
/-- This cannot be an instance because it can cause infinite loops whenever the `SMul` arguments
are still metavariables.  -/
SMul.comp.smulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul β α]
  [SMulCommClass M β α] (g : N → M), SMulCommClass N β α
-- Mathlib.Data.Set.Lattice.Image
Set.bijOn_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [hi : Nonempty ι] {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.InjOn f (⋃ i, s i) → Set.BijOn f (⋂ i, s i) (⋂ i, t i)
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonUnitalNonAssocCommSemiring.toNonUnitalNonAssocSemiring R)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.ModelCategory.over : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (S : C) → [HomotopicalAlgebra.ModelCategory C] → HomotopicalAlgebra.ModelCategory (CategoryTheory.Over S)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.setoid.eq_1 : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r),
  h.setoid = { r := fun x1 x2 => ¬G.Adj x1 x2, iseqv := ⋯ }
-- Mathlib.Data.Set.Order
Set.strictMonoOn_iff_strictMono : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMonoOn f s ↔ StrictMono fun a => f ↑a
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
/-- The `SeparationQuotient.outCLM K E` map is a topological embedding.  -/
SeparationQuotient.isEmbedding_outCLM : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E],
  Topology.IsEmbedding ⇑(SeparationQuotient.outCLM K E)
-- Mathlib.LinearAlgebra.Semisimple
/-- The minimal polynomial of a semisimple endomorphism is square free  -/
Module.End.IsSemisimple.minpoly_squarefree : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  [FiniteDimensional K M], f.IsSemisimple → Squarefree (minpoly K f)
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_dirac : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {f : X → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} [inst_6 : MeasurableSpace X]
  [MeasurableSingletonClass X] [CompleteSpace G] {a : X} {v : F} {s : Set X},
  MeasurableSet s →
    ∀ [inst_9 : Decidable (a ∈ s)],
      ∫ᵛ (x : X) in s, f x ∂[B; MeasureTheory.VectorMeasure.dirac a v] = if a ∈ s then (B (f a)) v else 0
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- See also the lemma `W_isInvertedBy_presheafFiber` in the file
`Mathlib/CategoryTheory/Sites/Point/Basic.lean` which may apply
in more cases.  -/
CategoryTheory.GrothendieckTopology.Point.W_isInvertedBy_presheafFiber' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {FC : A → A → Type u_1} {CC : A → Type w'}
  [inst_3 : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)] [inst_4 : CategoryTheory.ConcreteCategory A FC]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', w', u', w' + 1} (CategoryTheory.forget A)]
  [CategoryTheory.LocallySmall.{w, v, u} C] [J.WEqualsLocallyBijective A]
  [(CategoryTheory.forget A).ReflectsIsomorphisms], J.W.IsInvertedBy Φ.presheafFiber
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_boole_mul' : ∀ {ι : Type u_1} {K : Type u_3} [inst : Semifield K] [inst_1 : CharZero K] [inst_2 : Fintype ι] [Nonempty ι]
  [inst_4 : DecidableEq ι] (f : ι → K) (i : ι),
  (Finset.univ.expect fun j => (if j = i then ↑(Fintype.card ι) else 0) * f j) = f i
-- Mathlib.Data.Set.Image
Set.range_quotient_mk' : ∀ {α : Type u_1} {s : Setoid α}, Set.range Quotient.mk' = Set.univ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_ae_eq_condExpL1CLM : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (hm : m ≤ m₀)
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)] (hf : MeasureTheory.Integrable f μ),
  μ[f | m] =ᵐ[μ] ↑↑((MeasureTheory.condExpL1CLM E hm μ) (MeasureTheory.Integrable.toL1 f hf))
-- Lean.Declaration
Lean.Constructor : Type
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- Pushforwards along equal morphisms of sheaves of rings are isomorphic.  -/
SheafOfModules.pushforwardCongr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    {φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R} →
                      φ = ψ → (SheafOfModules.pushforward φ ≅ SheafOfModules.pushforward ψ)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α},
  k ∈ Std.DHashMap.filterMap f m ↔ ∃ (h : k ∈ m), (f k (m.get k h)).isSome = true
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Data.Holor
/-- The 1-dimensional "unit" holor with 1 in the `j`th position.  -/
Holor.unitVec : {α : Type} → [Monoid α] → [AddMonoid α] → (d : ℕ) → ℕ → Holor α [d]
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.DefEqM : Type → Type
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.m : Lean.Elab.Term.ExtractMonadResult → Lean.Expr
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.pos : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < p