mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Lean.ContextInfo
/-- Embeds a `MetaM` action in `CommandElabM` by supplying the information stored in `info`.

Copy of `ContextInfo.runMetaM` that makes use of the `CommandElabM` context for:
* message logging (messages produced by the `CoreM` action are migrated back),
* metavariable generation,
* auxiliary declaration generation,
* local instances.
 -/
Lean.Elab.ContextInfo.runMetaMWithMessages : {α : Type} → Lean.Elab.ContextInfo → Lean.LocalContext → Lean.MetaM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_six : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 6 → M), ∑ i, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis.congr_simp : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone.expMapBasis = NumberField.mixedEmbedding.fundamentalCone.expMapBasis
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr : ∀ (m n : ℕ) (lhs : BitVec m) (rhs : BitVec n) (lhs' : BitVec m) (rhs' : BitVec n),
  lhs' = lhs → rhs' = rhs → lhs >>> rhs = lhs' >>> rhs'
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
/-- A modular form is a cusp form if and only if it vanishes at every cusp. This is the
general characterization valid for any subgroup.  -/
ModularForm.isCuspForm_iff : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] (f : ModularForm Γ k),
  f.IsCuspForm ↔ ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt (⇑f) k
-- Mathlib.Analysis.Complex.Trigonometric
Real.abs_cos_eq_sqrt_one_sub_sin_sq : ∀ (x : ℝ), |Real.cos x| = √(1 - Real.sin x ^ 2)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_univ_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndepOn R v Set.univ ↔ LinearIndependent R v
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- A stronger form of **Cramer's rule** that allows us to solve some instances of `A * x = b` even
if the determinant is not a unit. A sufficient (but still not necessary) condition is that `A.det`
divides `b`.  -/
Matrix.mulVec_cramer : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (b : n → α), A.mulVec (A.cramer b) = A.det • b
-- Mathlib.Algebra.Module.Torsion.Basic
Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (m : M), Ideal.torsionOf R M m = ⊥ ↔ m ≠ 0
-- Batteries.Data.List.Lemmas
List.isChain_iff_getElem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l ↔ ∀ (i : ℕ) (_hi : i + 1 < l.length), R l[i] l[i + 1]
-- Mathlib.Data.Nat.Init
Nat.two_mul_odd_div_two : ∀ {n : ℕ}, n % 2 = 1 → 2 * (n / 2) = n - 1
-- Init.Data.List.Pairwise
List.Pairwise.rel_of_mem_take_of_mem_drop : ∀ {α : Type u_1} {R : α → α → Prop} {i : ℕ} {x y : α} {l : List α},
  List.Pairwise R l → x ∈ List.take i l → y ∈ List.drop i l → R x y
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_functor_obj_right_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (F : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory) C) (X : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.functor.obj F).right.obj X =
    F.obj (CategoryTheory.WithInitial.incl.obj X)
-- Mathlib.Topology.Connected.Basic
IsConnected.eq_1 : ∀ {α : Type u} [inst : TopologicalSpace α] (s : Set α), IsConnected s = (s.Nonempty ∧ IsPreconnected s)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∈ m → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey! k = m.getKey! k
-- Mathlib.Order.Lattice.Nat
Nat.iSup_lt_succ' : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_digits_append_digits : ∀ {b m n : ℕ}, Nat.ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
-- Std.Data.TreeMap.Raw.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.TreeMap.Raw.valuesArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Array β
-- Lean.Elab.Do.Basic
/-- Pluggable builders for the `pure` / `bind` applications emitted by the `do` elaborator.  -/
Lean.Elab.Do.DoOps : Type
-- Std.Http.Data.Body.Stream
Std.Http.Body.Stream.NextChunk.mk : {m : Type → Type} → (Std.Http.Body.Stream → m (Option Std.Http.Chunk)) → Std.Http.Body.Stream.NextChunk m
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.AC.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.AC.EqCnstrProof → Sort u} →
    (t : Lean.Meta.Grind.AC.EqCnstr) →
      ((t : Lean.Meta.Grind.AC.EqCnstr) → t.below → motive_1 t) →
        ((t : Lean.Meta.Grind.AC.EqCnstrProof) → t.below → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ_w : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (q₁ q₂ : ℕ) (hq : q₁ ≤ q₂),
  CategoryTheory.CategoryStruct.comp (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₂)
      ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor✝ f n₀).map (CategoryTheory.homOfLE hq).op).hom.h =
    CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.midπ✝ f n₀ q₁
-- Mathlib.Topology.Closure
Filter.HasBasis.lift'_closure_eq_self : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort v} {l : Filter X} {p : ι → Prop} {s : ι → Set X},
  l.HasBasis p s → (∀ (i : ι), p i → IsClosed (s i)) → l.lift' closure = l
-- Mathlib.Data.List.Triplewise
List.triplewise_pair : ∀ {α : Type u_1} (a b : α) (p : α → α → α → Prop), List.Triplewise p [a, b]
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.fderivWithin_congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s t : Set E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F],
  DifferentiableWithinAt 𝕜 f s x →
    Set.EqOn f₁ f t → f₁ x = f x → UniqueDiffWithinAt 𝕜 t x → t ⊆ s → fderivWithin 𝕜 f₁ t x = fderivWithin 𝕜 f s x
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.subset`.

---

Set notation form of `LT.lt.le` -/
HasSSubset.SSubset.subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → a ⊆ b
-- Mathlib.GroupTheory.GroupAction.Iwasawa
MulAction.IwasawaStructure.mk.injEq : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] (T : α → Subgroup M)
  (is_comm : ∀ (x : α), IsMulCommutative ↥(T x)) (is_conj : ∀ (g : M) (x : α), T (g • x) = MulAut.conj g • T x)
  (is_generator : iSup T = ⊤) (T_1 : α → Subgroup M) (is_comm_1 : ∀ (x : α), IsMulCommutative ↥(T_1 x))
  (is_conj_1 : ∀ (g : M) (x : α), T_1 (g • x) = MulAut.conj g • T_1 x) (is_generator_1 : iSup T_1 = ⊤),
  ({ T := T, is_comm := is_comm, is_conj := is_conj, is_generator := is_generator } =
      { T := T_1, is_comm := is_comm_1, is_conj := is_conj_1, is_generator := is_generator_1 }) =
    (T = T_1)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `neg_le_neg_iff`. -/
le_of_neg_le_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α} [AddRightMono α], -a ≤ -b → b ≤ a
-- Mathlib.MeasureTheory.Integral.Marginal
MeasureTheory.lintegral_eq_lmarginal_univ : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] {μ : (i : δ) → MeasureTheory.Measure (X i)}
  [inst_1 : DecidableEq δ] [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] [inst_3 : Fintype δ]
  {f : ((i : δ) → X i) → ENNReal} (x : (i : δ) → X i),
  ∫⁻ (x : (i : δ) → X i), f x ∂MeasureTheory.Measure.pi μ = (∫⋯∫⁻_Finset.univ, f ∂μ) x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonFullyFaithful.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddMonFullyFaithful =
    {
      preimage := fun {M N} α =>
        { hom := (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op M.X))) (CategoryTheory.CategoryStruct.id M.X),
          isAddMonHom_hom := ⋯ },
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_iff_tendsto : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r ↔ Filter.Germ.Tendsto x (nhds r)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.map_zero_mem_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), ↑(Topology.RelCWComplex.map n i) 0 ∈ Topology.RelCWComplex.openCell n i
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.treeMap : {α : Type u} → [inst : Ord α] → Std.DTreeMap.Internal.Unit.RciSliceData α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.Topology.Neighborhoods
interior_eq_nhds' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = {x | s ∈ nhds x}
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsLE : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iic a)) (nhdsWithin a⁻¹ (Set.Ici a⁻¹))
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- The map from the quotient of `M` by a submodule `p` to `M₂` induced by a linear map `f : M → M₂`
vanishing on `p`, as a linear map.  -/
Submodule.liftQ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p : Submodule R M) →
            {R₂ : Type u_3} →
              {M₂ : Type u_4} →
                [inst_3 : Ring R₂] →
                  [inst_4 : AddCommGroup M₂] →
                    [inst_5 : Module R₂ M₂] → {τ₁₂ : R →+* R₂} → (f : M →ₛₗ[τ₁₂] M₂) → p ≤ f.ker → M ⧸ p →ₛₗ[τ₁₂] M₂
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.continuousAt_log_iff : ∀ {x : ℝ}, ContinuousAt Real.log x ↔ x ≠ 0
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- Sufficient conditions to show that the `p`-adic valuation of `q` is less than or equal to the
`p`-adic valuation of `q + r`.  -/
padicValRat.le_padicValRat_add_of_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  q + r ≠ 0 → padicValRat p q ≤ padicValRat p r → padicValRat p q ≤ padicValRat p (q + r)
-- Init.Data.SInt.Lemmas
Int64.lt_or_eq_of_le : ∀ {a b : Int64}, a ≤ b → a < b ∨ a = b
-- Mathlib.Topology.Order.LeftRightNhds
orderTopology_of_nhds_mabs : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α],
  (∀ (a : α), nhds a = ⨅ r, ⨅ (_ : r > 1), Filter.principal {b | |a / b|ₘ < r}) → OrderTopology α
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.get? : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → Option β
-- Std.Time.Format.Modifier
/-- `ZoneName` represents different zone name formats based on the number of pattern letters and
whether daylight saving time is considered.
 -/
Std.Time.ZoneName : Type
-- Init.Prelude
/-- This function does not have special support for macro scopes.
See `Name.append`.
 -/
Lean.Name.appendCore : Lean.Name → Lean.Name → Lean.Name
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiable.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'] {f : M → E'}, MDiff f → MDiff (-f)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.eps_pos : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {P : Finpartition Finset.univ} {ε : ℝ},
  100 ≤ 4 ^ P.parts.card * ε ^ 5 → 0 < ε
-- Mathlib.Analysis.Normed.MulAction
nnnorm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
  [inst_2 : SMulZeroClass α β] [IsBoundedSMul α β] (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊
-- Mathlib.Order.Filter.Lift
Filter.mem_lift'_sets : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β},
  Monotone h → ∀ {s : Set β}, s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), ⨆ i, AlgebraicGeometry.Scheme.Hom.opensRange (𝒰.f i) = ⊤
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter : ∀ {α : Type u_1} {M : Matroid α} {C K : Set α}, M.IsCircuit C → M.IsCocircuit K → Disjoint C K ∨ (C ∩ K).Nontrivial
-- Mathlib.Topology.Constructible
_private.Mathlib.Topology.Constructible.0.infClosed_isRetrocompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X], InfClosed {s | IsRetrocompact s}
-- Mathlib.NumberTheory.MulChar.Basic
/-- The commutative group structure on `MulChar R R'`.  -/
MulChar.commGroup : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → CommGroup (MulChar R R')
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.atEnd : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → (it.atEnd = true ↔ r = [])
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.fvar.inj : ∀ {fvarId : Lean.FVarId} {nargs : ℕ} {fvarId_1 : Lean.FVarId} {nargs_1 : ℕ},
  Lean.Meta.RefinedDiscrTree.Key.fvar fvarId nargs = Lean.Meta.RefinedDiscrTree.Key.fvar fvarId_1 nargs_1 →
    fvarId = fvarId_1 ∧ nargs = nargs_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℂ n f x → ContDiffAt ℂ n (fun x => Complex.cos (f x)) x
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.mkNameFromParserSyntax.appendCatName : Lean.Name → String → String
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The comparison morphism for the coproduct of `f`. This is an iso iff `G` preserves the coproduct
of `f`, see `PreservesCoproduct.ofIsoComparison`.  -/
CategoryTheory.Limits.sigmaComparison : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (G : CategoryTheory.Functor C D) →
            (f : β → C) →
              [inst_2 : CategoryTheory.Limits.HasCoproduct f] →
                [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)] →
                  (∐ fun b => G.obj (f b)) ⟶ G.obj (∐ f)
-- Lean.Elab.PreDefinition.Structural.IndPred
/-- Calculates the `.brecOn` motive corresponding to one structural recursive function.
The `value` is the function with (only) the fixed parameters moved into the context.
 -/
Lean.Elab.Structural.mkIndPredBRecOnMotive : Lean.Elab.Structural.RecArgInfo → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- Every well-order has a cofinal subset of order type `(cof α).ord`.  -/
Ordinal.exists_ord_cof_eq : ∀ (α : Type u) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  ∃ s, IsCofinal s ∧ (Ordinal.type fun x1 x2 => x1 < x2) = (Order.cof α).ord
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric_nnreal_smul : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : ENNReal → ENNReal) {c : NNReal},
  c ≠ 0 → MeasureTheory.OuterMeasure.mkMetric (c • m) = c • MeasureTheory.OuterMeasure.mkMetric m
-- Batteries.Control.Nondet.Basic
/-- The empty nondeterministic value.  -/
Nondet.nil : {σ : Type} → {m : Type → Type} → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- **Alias** of `MeasureTheory.all_ae_norm_ofReal_F_le_bound`. -/
MeasureTheory.all_ae_ofReal_F_le_bound : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {bound : α → ℝ},
  (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
    ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), ↑(Finset.Ici a) = Set.Ici a
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_apply_eq_self : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} {a : α},
  s.mulIndicator f a = f a ↔ a ∉ s → f a = 1
-- Batteries.Data.List.Basic
/-- Inner loop for `insertP`. Tail recursive.  -/
List.insertP.loop : {α : Type u_1} → (α → Bool) → α → List α → List α → List α
-- Init.Data.UInt.Lemmas
USize.toNat_toUInt8 : ∀ (x : USize), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_ihom_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C) {Y Y' : C}
  [inst_2 : CategoryTheory.Closed A] (g : Y ⟶ Y'),
  CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.ihom A).map g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app Y) g
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instSMul : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {α : Type u_5} →
      [inst : Preorder α] →
        [LocallyFiniteOrder α] →
          [inst_2 : AddCommMonoid 𝕜] →
            [inst_3 : AddCommMonoid 𝕝] → [SMul 𝕜 𝕝] → SMul (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderivWithin 𝕜 f s x (k x)` is smooth at `x₀` within `s`.  -/
ContDiffWithinAt.fderivWithin_right_apply : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {m n : WithTop ℕ∞} {f : F → G}
  {k : F → F} {s : Set F} {x₀ : F},
  ContDiffWithinAt 𝕜 n f s x₀ →
    ContDiffWithinAt 𝕜 m k s x₀ →
      UniqueDiffOn 𝕜 s → m + 1 ≤ n → x₀ ∈ s → ContDiffWithinAt 𝕜 m (fun x => (fderivWithin 𝕜 f s x) (k x)) s x₀
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivWithinAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {s : Set E}
  {x v : E} {f' : F} {c : 𝕜},
  c ≠ 0 → (HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) ↔ HasLineDerivWithinAt 𝕜 f f' s x v)
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_add_apply : ∀ (R : Type u_1) (p m n : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (iterateFrobeniusEquiv R p (m + n)) x = (iterateFrobeniusEquiv R p m) ((iterateFrobeniusEquiv R p n) x)
-- Mathlib.Data.Finsupp.Defs
_private.Mathlib.Data.Finsupp.Defs.0.Finsupp.embDomain.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.mk : ∀ {S : Type u_3} {M : outParam (Type u_4)} [inst : AddZeroClass M] [inst_1 : SetLike S M]
  [toAddMemClass : AddMemClass S M] [toZeroMemClass : ZeroMemClass S M], AddSubmonoidClass S M
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_comp_map' : ∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : α → C} {g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g] (p : α → β)
  (q : (a : α) → f a ⟶ g (p a)) (a : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f a) (CategoryTheory.Limits.Sigma.map' p q) =
    CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.Limits.Sigma.ι g (p a))
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.X_X : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i j : σ},
  MvPowerSeries.HasSubst ![MvPowerSeries.X i, MvPowerSeries.X j]
-- Mathlib.Algebra.Order.Monovary
antivary_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Antivary (-f) g ↔ Monovary f g
-- Mathlib.Data.List.Dedup
List.dedup_append : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
-- Mathlib.Algebra.Order.ToIntervalMod
/-- The unique integer such that this multiple of `p`, subtracted from `b`, is in `Ioc a (a + p)`.  -/
toIocDiv : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → [hα : Archimedean α] → {p : α} → 0 < p → α → α → ℤ
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.instQuasiCompactιSchemeOfQuasiSeparatedSpaceCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} [QuasiSeparatedSpace ↥Y] (f g : X ⟶ Y),
  AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.equalizer.ι f g)
-- Init.Data.Nat.Lcm
/-- The least common multiple of `m` and `n` is the smallest natural number that's evenly divisible by
both `m` and `n`. Returns `0` if either `m` or `n` is `0`.

Examples:
 * `Nat.lcm 9 6 = 18`
 * `Nat.lcm 9 3 = 9`
 * `Nat.lcm 0 3 = 0`
 * `Nat.lcm 3 0 = 0`
 -/
Nat.lcm : ℕ → ℕ → ℕ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {km : α}, t.min! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Analysis.Matrix.PosDef
/-- A Hermitian matrix is positive semi-definite if and only if its eigenvalues are non-negative.  -/
Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), A.PosSemidef ↔ 0 ≤ hA.eigenvalues
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The `AddHom` underlying an `AddEquiv`.  -/
AddEquiv.toAddHom : {A : Type u_9} → {B : Type u_10} → [inst : Add A] → [inst_1 : Add B] → A ≃+ B → A →ₙ+ B
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (-g) h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp f g) h