mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- Converse to the mean value inequality: if `f` is line differentiable at `x₀` and `C`-lipschitz
on a neighborhood of `x₀` then its line derivative at `x₀` in the direction `v` has norm
bounded by `C * ‖v‖`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a
neighborhood of `x`.  -/
HasLineDerivAt.le_of_lipschitzOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {v : E}
  {f : E → F} {f' : F} {x₀ : E},
  HasLineDerivAt 𝕜 f f' x₀ v → ∀ {s : Set E}, s ∈ nhds x₀ → ∀ {C : NNReal}, LipschitzOnWith C f s → ‖f'‖ ≤ ↑C * ‖v‖
-- Mathlib.RingTheory.Polynomial.GaussLemma
/-- If `K = Frac(R)` and `g : K[X]` divides a monic polynomial with coefficients in `R`, then
`g * (C g.leadingCoeff⁻¹)` has coefficients in `R`  -/
IsIntegrallyClosed.eq_map_mul_C_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsIntegrallyClosed R] {f : Polynomial R},
  f.Monic →
    ∀ {g : Polynomial K},
      g ∣ Polynomial.map (algebraMap R K) f → ∃ g', Polynomial.map (algebraMap R K) g' * Polynomial.C g.leadingCoeff = g
-- Mathlib.NumberTheory.Chebyshev
/-- `ψ - θ` is the sum of `Λ` over non-primes.  -/
Chebyshev.psi_sub_theta_eq_sum_not_prime : ∀ (x : ℝ),
  Chebyshev.psi x - Chebyshev.theta x = ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, ArithmeticFunction.vonMangoldt n
-- Batteries.Lean.EStateM
EStateM.run'_seqLeft : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ),
  (x <* y).run' s =
    match x.run s with
    | EStateM.Result.ok v s => Option.map (fun x => v) (y.run' s)
    | EStateM.Result.error a a_1 => none
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mk_smul : ∀ {K : Type u} [inst : CommRing K] {R : Type u_1} [inst_1 : IsDomain K] [inst_2 : Monoid R]
  [inst_3 : DistribMulAction R (Polynomial K)] [inst_4 : IsScalarTower R (Polynomial K) (Polynomial K)] (c : R)
  (p q : Polynomial K), RatFunc.mk (c • p) q = c • RatFunc.mk p q
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.eq_iff_aeval_minpoly_eq_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [IsDomain B] {C : Type u_3}
  [inst_4 : Ring C] [inst_5 : Algebra A C] [Nontrivial C] {b : B},
  IsIntegral A b → ∀ {c : C}, minpoly A b = minpoly A c ↔ (Polynomial.aeval c) (minpoly A b) = 0
-- Mathlib.Topology.Separation.Basic
Inseparable.of_nhds_neBot : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x y : X}, (nhds x ⊓ nhds y).NeBot → Inseparable x y
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_single_subset : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, (fun₀ | i => b).support ⊆ {i}
-- Mathlib.Order.Interval.Set.Defs
Set.Ioo_def : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), {x | a < x ∧ x < b} = Set.Ioo a b
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.LEquiv.onBoundedFormula_symm : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {α : Type u'} {n : ℕ} (φ : L ≃ᴸ L'),
  φ.onBoundedFormula.symm = φ.symm.onBoundedFormula
-- Mathlib.Data.Nat.Log
Nat.pow_lt_of_lt_clog : ∀ {b x y : ℕ}, y < Nat.clog b x → b ^ y < x
-- Init.Data.String.Pattern.Basic
/-- The subslice starting at `startPos` and ending at `endPos` did not match the pattern.
   -/
String.Slice.Pattern.SearchStep.rejected : {s : String.Slice} → s.Pos → s.Pos → String.Slice.Pattern.SearchStep s
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.mk.sizeOf_spec : ∀ {α : Type u_4} {β : Type u_5} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toEquiv : α ≃ β) (uniformContinuous_toFun : UniformContinuous toEquiv.toFun)
  (uniformContinuous_invFun : UniformContinuous toEquiv.invFun),
  sizeOf
      { toEquiv := toEquiv, uniformContinuous_toFun := uniformContinuous_toFun,
        uniformContinuous_invFun := uniformContinuous_invFun } =
    1 + sizeOf toEquiv
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : EInt} (f : X ⟶ Y) (j : C),
  ((t.eTriangleLTGE.map f).app j).hom₁ = (t.eTruncLT.map f).app j
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instCoeSortType : (P : TopCat → Prop) → CoeSort (CompHausLike P) (Type u)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- Extension for the `positivity` tactic: `UpperHalfPlane.im`.  -/
Mathlib.Meta.Positivity.evalUpperHalfPlaneIm : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.Basic
Pi.instHImp : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → HImp (π i)] → HImp ((i : ι) → π i)
-- Mathlib.LinearAlgebra.Dual.Defs
Submodule.mem_dualAnnihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {W : Submodule R M} (φ : Module.Dual R M), φ ∈ W.dualAnnihilator ↔ ∀ w ∈ W, φ w = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Dense.borel_eq_generateFrom_Ico_mem_aux : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α},
  Dense s →
    (∀ (x : α), IsBot x → x ∈ s) →
      (∀ (x y : α), x < y → Set.Ioo x y = ∅ → y ∈ s) →
        borel α = MeasurableSpace.generateFrom {S | ∃ l ∈ s, ∃ u ∈ s, l < u ∧ Set.Ico l u = S}
-- Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties
CategoryTheory.injective_iff_rlp_monomorphisms_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {I Z : C}
  (p : I ⟶ Z),
  CategoryTheory.Limits.IsZero Z →
    (CategoryTheory.Injective I ↔ (CategoryTheory.MorphismProperty.monomorphisms C).rlp p)
-- Mathlib.Data.Sign.Basic
_private.Mathlib.Data.Sign.Basic.0.exists_signed_sum_aux : ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α) (f : α → ℤ),
  ∃ β t sgn g,
    (∀ (b : β), g b ∈ s) ∧ t.card = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b ∈ t, if g b = a then ↑(sgn b) else 0) = f a
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, a, ...as]` is split at `a`, the first element is `xs`,
assuming no element in `xs` is equal to `a`.  -/
List.splitOn_append_cons_self_of_not_mem : ∀ {α : Type u_1} {xs : List α} [inst : BEq α] [LawfulBEq α] {a : α},
  a ∉ xs → ∀ (as : List α), List.splitOn a (xs ++ a :: as) = xs :: List.splitOn a as
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.decompose : ∀ {d x y : ℤ}, { re := x, im := y } = ↑x + Zsqrtd.sqrtd * ↑y
-- Mathlib.FieldTheory.AlgebraicClosure
/-- The normal closure in `E/F` of the algebraic closure of `F` in `E` is equal to itself.  -/
algebraicClosure.normalClosure_eq_self : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IntermediateField.normalClosure F (↥(algebraicClosure F E)) E = algebraicClosure F E
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Pos.Raw.utf8GetAux.match_1.eq_1 : ∀ (motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) (x x_1 : String.Pos.Raw)
  (h_1 : (x x_2 : String.Pos.Raw) → motive [] x x_2)
  (h_2 : (c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p),
  (match [], x, x_1 with
    | [], x, x_2 => h_1 x x_2
    | c :: cs, i, p => h_2 c cs i p) =
    h_1 x x_1
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.numbering : Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Monovary
antivary_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → (Antivary f⁻¹ g ↔ Monovary f g)
-- Mathlib.Logic.Encodable.Basic
/-- Lowers an `a : α` into `ULower α`.  -/
ULower.down : {α : Type u_1} → [inst : Encodable α] → α → ULower α
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
MonoidAlgebra.nonUnitalAlgHom_ext' : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Mul M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A},
  φ₁.toMulHom.comp (MonoidAlgebra.ofMagma R M) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma R M) → φ₁ = φ₂
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.instInhabited : {α : Type u_3} → Inhabited (MeasurableSpace.DynkinSystem α)
-- Mathlib.Data.Finset.Option
Finset.eraseNone_image_some : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset α), Finset.eraseNone (Finset.image some s) = s
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} {h : P.I ⟶ Y}
  {h₀ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h = f) HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam}
  {h₁ :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h = g) HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam}
  {h_1 : P.I ⟶ Y}
  {h₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₀ h_1 = f)
      HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀._autoParam}
  {h₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp P.i₁ h_1 = g)
      HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁._autoParam},
  { h := h, h₀ := h₀, h₁ := h₁ } = { h := h_1, h₀ := h₀_1, h₁ := h₁_1 } → h = h_1
-- Mathlib.Data.List.Pi
List.pi_nil : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Type u_2} (t : (i : ι) → List (α i)), [].pi t = [List.Pi.nil α]
-- Init.System.FilePath
/-- The character that separates directories.

On platforms that support multiple separators, `System.FilePath.pathSeparator` is the “ideal” one expected by users
on the platform. `System.FilePath.pathSeparators` lists all supported separators.
 -/
System.FilePath.pathSeparator : Char
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_none_none : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α], edist none none = 0
-- Mathlib.Tactic.Translate.Core
/-- Elaboration of the configuration options for a translation attribute. It is assumed that
- `stx[0]` is the attribute (e.g. `to_additive`)
- `stx[1]` is the optional tracing `?`
- `stx[2]` is the remaining `attrArgs`

TODO: Currently, we don't deduce any `dont_translate` arguments based on the type of `declName`.
In the future we would like that the presence of `MonoidAlgebra k G` will automatically
flag `k` as a type to not be translated.  -/
Mathlib.Tactic.Translate.elabTranslationAttr : Lean.Name → Lean.Syntax → Lean.CoreM Mathlib.Tactic.Translate.Config
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Methods.mk : Lean.Meta.Grind.Propagator → Lean.Meta.Grind.Propagator → Lean.Meta.Grind.EvalTactic → Lean.Meta.Grind.Methods
-- Mathlib.Analysis.Complex.Basic
ContinuousLinearMap.restrictScalars.congr_simp : ∀ {A : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} (R : Type u_4) [inst : Semiring A] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module A M₁] [inst_4 : Module R M₁] [inst_5 : TopologicalSpace M₁]
  [inst_6 : AddCommMonoid M₂] [inst_7 : Module A M₂] [inst_8 : Module R M₂] [inst_9 : TopologicalSpace M₂]
  [inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A] (f f_1 : M₁ →L[A] M₂),
  f = f_1 → ContinuousLinearMap.restrictScalars R f = ContinuousLinearMap.restrictScalars R f_1
-- Mathlib.Tactic.Linarith.Frontend
Mathlib.Tactic.Linarith.LinarithConfig.mk.inj : ∀ {discharger : Lean.Elab.Tactic.TacticM Unit} {exfalso : Bool} {transparency : Lean.Meta.TransparencyMode}
  {splitHypotheses splitNe minimize : Bool} {preprocessors : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor}
  {oracle : Mathlib.Tactic.Linarith.CertificateOracle} {discharger_1 : Lean.Elab.Tactic.TacticM Unit} {exfalso_1 : Bool}
  {transparency_1 : Lean.Meta.TransparencyMode} {splitHypotheses_1 splitNe_1 minimize_1 : Bool}
  {preprocessors_1 : List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor}
  {oracle_1 : Mathlib.Tactic.Linarith.CertificateOracle},
  { discharger := discharger, exfalso := exfalso, transparency := transparency, splitHypotheses := splitHypotheses,
        splitNe := splitNe, minimize := minimize, preprocessors := preprocessors, oracle := oracle } =
      { discharger := discharger_1, exfalso := exfalso_1, transparency := transparency_1,
        splitHypotheses := splitHypotheses_1, splitNe := splitNe_1, minimize := minimize_1,
        preprocessors := preprocessors_1, oracle := oracle_1 } →
    discharger = discharger_1 ∧
      exfalso = exfalso_1 ∧
        transparency = transparency_1 ∧
          splitHypotheses = splitHypotheses_1 ∧
            splitNe = splitNe_1 ∧ minimize = minimize_1 ∧ preprocessors = preprocessors_1 ∧ oracle = oracle_1
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_mono : ∀ {α : Type u_1} {β : Type u_2} {m₁ m₂ : MeasurableSpace α} {f : α → β},
  m₁ ≤ m₂ → MeasurableSpace.map f m₁ ≤ MeasurableSpace.map f m₂
-- Mathlib.Algebra.Order.SuccPred
Order.add_one_inj : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α] [NoMaxOrder α],
  x + 1 = y + 1 ↔ x = y
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `lia` by identifying places where it does not yet supersede `omega`.  -/
linter.tacticAnalysis.regressions.omegaToLia : Lean.Option Bool
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
NNReal.nndist_eq : ∀ (a b : NNReal), nndist a b = max (a - b) (b - a)
-- Mathlib.FieldTheory.Galois.Basic
/-- A subgroup is isomorphic to the Galois group of its fixed field.
 -/
IntermediateField.subgroupEquivAlgEquiv : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [FiniteDimensional F E] → (H : Subgroup Gal(E/F)) → ↥H ≃* Gal(E/↥(IntermediateField.fixedField H))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- the data of sections of `M` over `X i` which generate `M.over (X i)`  -/
SheafOfModules.LocalGeneratorsData.generators : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        {M : SheafOfModules R} →
          [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
            [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
              (self : M.LocalGeneratorsData) → (i : self.I) → (M.over (self.X i)).GeneratingSections
-- Mathlib.Data.PNat.Interval
PNat.card_fintype_Ico : ∀ (a b : ℕ+), Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
-- Lean.Message
Lean.BaseMessage.endPos : {α : Type u} → Lean.BaseMessage α → Option Lean.Position
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_attach_univ : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] (f : ↥Finset.univ → M),
  ∑ i ∈ Finset.univ.attach, f i = ∑ i, f ⟨i, ⋯⟩
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.hasSum_inr : ∀ {α : Type u_1} {R : Type u_3} (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid R] [inst_3 : AddCommMonoid M] {f : α → M} {a : M},
  HasSum f a → HasSum (fun x => TrivSqZeroExt.inr (f x)) (TrivSqZeroExt.inr a)
-- Mathlib.Analysis.Complex.AbsMax
/-- If `f` is a function differentiable on the open unit ball, and there exists an `r < 1` such that
any value of `‖f‖` on the open ball is bounded above by some value on the closed ball of radius `r`,
then `f` is constant.  -/
Complex.eq_const_of_exists_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [StrictConvexSpace ℝ F] [ProperSpace E] {f : E → F} {r b : ℝ},
  DifferentiableOn ℂ f (Metric.ball 0 b) →
    0 ≤ r →
      r < b →
        (∀ z ∈ Metric.ball 0 b, ∃ w ∈ Metric.closedBall 0 r, ‖f z‖ ≤ ‖f w‖) →
          Set.EqOn f (Function.const E (f 0)) (Metric.ball 0 b)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  X.σ₀Iter 0 ⋯ = CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Lean.Data.RArray
Lean.RArray.size.eq_1 : ∀ {α : Type u} (x : α), (Lean.RArray.leaf x).size = 1
-- Std.Tactic.BVDecide.LRAT.Parser
/-- Serialize `proof` into the non-binary LRAT format as a `String`.
 -/
Std.Tactic.BVDecide.LRAT.lratProofToString : Array Std.Tactic.BVDecide.LRAT.IntAction → String
-- Mathlib.Topology.Instances.Matrix
Topology.IsInducing.matrix_map : ∀ {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [inst : TopologicalSpace R]
  [inst_1 : TopologicalSpace S] {f : R → S}, Topology.IsInducing f → Topology.IsInducing fun x => x.map f
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_of_nonneg : ∀ (x : NNReal) {y z : ℝ}, 0 ≤ y → 0 ≤ z → x ^ (y + z) = x ^ y * x ^ z
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_toInt : ∀ (x : Int64), Int64.ofIntLE x.toInt ⋯ ⋯ = x
-- Mathlib.Order.Preorder.Chain
IsChain.preimage : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β),
  Function.Injective f → (∀ (x y : α), s (f x) (f y) → r x y) → ∀ {c : Set β}, IsChain s c → IsChain r (f ⁻¹' c)
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The subsemiring of continuous maps `α → β`.  -/
continuousSubsemiring : (α : Type u_1) →
  (R : Type u_2) →
    [TopologicalSpace α] →
      [inst : TopologicalSpace R] → [inst_1 : NonAssocSemiring R] → [IsTopologicalSemiring R] → Subsemiring (α → R)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.one_mul : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel.below ⋯
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.StructuredArrow.projectSubobject.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} [inst_2 : CategoryTheory.Limits.HasFiniteLimits C]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteLimits T] {A : CategoryTheory.StructuredArrow S T}
  (a a_1 : CategoryTheory.Subobject A),
  a = a_1 → CategoryTheory.StructuredArrow.projectSubobject a = CategoryTheory.StructuredArrow.projectSubobject a_1
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s` in a complete space, so is its derivative.  -/
AnalyticOnNhd.deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F],
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (deriv f) s
-- Mathlib.RingTheory.NormalClosure
Ring.instIsScalarTowerNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S], IsScalarTower R S (Ring.NormalClosure R S)
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePair R) (I : Ideal S),
  I ^ 2 = ⊥ → ∀ (x : S), P.HasMap ((Ideal.Quotient.mk I) x) → ∃! ε, ε ∈ I ∧ P.HasMap (x + ε)
-- Batteries.Data.String.Lemmas
String.Pos.Raw.Valid.exists : ∀ {s : String} {p : String.Pos.Raw},
  String.Pos.Raw.Valid s p → ∃ cs cs', String.ofList (cs ++ cs') = s ∧ p = { byteIdx := String.utf8Len cs }
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert_eq_insertₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {h : l.Balanced},
  (Std.DTreeMap.Internal.Impl.insert k v l h).impl = Std.DTreeMap.Internal.Impl.insertₘ k v l h
-- Mathlib.Topology.DiscreteQuotient
/-- A helper lemma to prove that `finsetClopens X` is injective, see `finsetClopens_inj`.  -/
DiscreteQuotient.comp_finsetClopens : ∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : CompactSpace X],
  ((Set.image fun t => t.carrier) ∘ SetLike.coe) ∘ DiscreteQuotient.finsetClopens X = fun x =>
    match x with
    | { toSetoid := f, isOpen_setOfPred_rel := isOpen_setOfPred_rel } => f.classes
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequenceδ_comp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁),
      CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) = 0
-- Init.Data.Rat.Lemmas
Rat.neg_den : ∀ (a : ℚ), (-a).den = a.den
-- Lean.Elab.Tactic.SolveByElim
/-- Parse the lemma argument of a call to `solve_by_elim`.
The first component should be true if `*` appears at least once.
The second component should contain each term `t`in the arguments.
The third component should contain `t` for each `-t` in the arguments.
 -/
Lean.Elab.Tactic.SolveByElim.parseArgs : Option (Lean.TSyntax `Lean.Parser.Tactic.SolveByElim.args) → Bool × List Lean.Term × List Lean.Term
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.const.sizeOf_spec : ∀ {e : Q(ℕ)} (value : Mathlib.Tactic.Ring.Common.btℕ e),
  sizeOf (Mathlib.Tactic.Ring.Common.ExProdNat.const value) = 1 + sizeOf e + sizeOf value
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup.eq_def : ∀ (s : Lean.Grind.AC.Seq),
  s.eraseDup =
    match s with
    | Lean.Grind.AC.Seq.var x => Lean.Grind.AC.Seq.var x
    | Lean.Grind.AC.Seq.cons x s =>
      have s' := s.eraseDup;
      match s' with
      | Lean.Grind.AC.Seq.var y =>
        if Nat.beq x y = true then Lean.Grind.AC.Seq.var x else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)
      | Lean.Grind.AC.Seq.cons y s' =>
        if Nat.beq x y = true then Lean.Grind.AC.Seq.cons y s'
        else Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s')
-- Mathlib.GroupTheory.Exponent
Monoid.exp_eq_one_iff : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent G = 1 ↔ Subsingleton G
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.mk.inj : ∀ {openDecls : List Lean.OpenDecl} {currNamespace : Lean.Name} {openDecls_1 : List Lean.OpenDecl}
  {currNamespace_1 : Lean.Name},
  { openDecls := openDecls, currNamespace := currNamespace } =
      { openDecls := openDecls_1, currNamespace := currNamespace_1 } →
    openDecls = openDecls_1 ∧ currNamespace = currNamespace_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.support_updateRIn : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] {r : ℝ} (hr : r ∈ Set.Ioo 0 f.rOut),
  Function.support ↑(f.updateRIn r hr) = Function.support ↑f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_finset_le_card : ∀ (α : Type u_1) (n : ℕ), ↑n ≤ Cardinal.mk α → ∃ s, n ≤ s.card