mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Sylow
Sylow.isPGroup' : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (self : Sylow p G), IsPGroup p ↥↑self
-- Mathlib.Order.Filter.Pointwise
Filter.map_zero' : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] (f : α → β), Filter.map f 0 = pure (f 0)
-- Lean.Expr
Lean.ExprMap : Type → Type
-- Mathlib.Algebra.Ring.Parity
neg_one_pow_congr : ∀ {R : Type u_4} [inst : Monoid R] [inst_1 : HasDistribNeg R] {m n : ℕ}, (Even m ↔ Even n) → (-1) ^ m = (-1) ^ n
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_one : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  {π₁ : ContRepresentation R G V}, ContIntertwiningMap.toContinuousLinearMap 1 = 1
-- Mathlib.Order.Ideal
Order.Ideal.mk : {P : Type u_2} →
  [inst : LE P] →
    (toLowerSet : LowerSet P) →
      toLowerSet.carrier.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) toLowerSet.carrier → Order.Ideal P
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instSMulZeroClass : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : Zero M₀] → [SMulZeroClass G₀ M₀] → SMulZeroClass G₀ᵒᵈ M₀
-- Mathlib.Data.List.Chain
List.IsChain.rel_getLast_dropLast : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.IsChain R l → ∀ (hne : l.dropLast ≠ []), R (l.dropLast.getLast hne) (l.getLast ⋯)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D]
  (X : CategoryTheory.Functor C (CategoryTheory.CommMon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom.hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Mathlib.Order.Atoms
IsSimpleOrder.instIsCoatomic : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsSimpleOrder α], IsCoatomic α
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataParts.unsafe_impl_2 : System.FilePath → Array Lean.CompactedRegion → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Aesop.Saturate
_private.Aesop.Saturate.0.Aesop.saturateCore.runFirstRule : {α : Type} →
  Lean.MVarId →
    Aesop.UnorderedArraySet Lean.MVarId →
      Lean.Meta.SavedState → Array (Aesop.IndexMatchResult (Aesop.Rule α)) → Aesop.SaturateM (Option Aesop.GoalDiff)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_smul : ∀ {α : Type u_1} {mα : MeasurableSpace α} {R : Type u_3} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.Measure (MeasureTheory.Measure α)),
  (c • m).join = c • m.join
-- Mathlib.RingTheory.Jacobson.Radical
/-- The Jacobson radical of a ring `R` is the Jacobson radical of `R` as an `R`-module.  -/
Ring.jacobson : (R : Type u_1) → [inst : Ring R] → Ideal R
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
/-- The canonical morphism `mappingCone S.f ⟶ S.X₃` when `S` is a short complex
of cochain complexes.  -/
CochainComplex.mappingCone.descShortComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) → CochainComplex.mappingCone S.f ⟶ S.X₃
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.min : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ →
    MeasureTheory.IsStoppingTime f π → MeasureTheory.IsStoppingTime f fun ω => min (τ ω) (π ω)
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- `withSetOptionIn` currently breaks infotree searches, so we simply set `Bool` options
until this is fixed in [lean4#11313](https://github.com/leanprover/lean4/pull/11313).  -/
Mathlib.Linter.UnusedInstancesInType.withSetBoolOptionIn : Lean.Elab.Command.CommandElab → Lean.Elab.Command.CommandElab
-- Mathlib.RingTheory.Derivation.Basic
Derivation.liftOfRightInverse.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing M]
  [inst_3 : Algebra R A] [inst_4 : Algebra R M] {F : Type u_4} [inst_5 : FunLike F A M] [inst_6 : AlgHomClass F R A M]
  {f f_1 : F} (e_f : f = f_1) {f_inv f_inv_1 : M → A} (e_f_inv : f_inv = f_inv_1) (hf : Function.RightInverse f_inv ⇑f)
  ⦃d d_1 : Derivation R A A⦄ (e_d : d = d_1) (hd : ∀ (x : A), f x = 0 → f (d x) = 0),
  Derivation.liftOfRightInverse hf hd = Derivation.liftOfRightInverse ⋯ ⋯
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_dvd_false : ∀ {a b a' b' c : ℕ}, Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → b'.mod a' = c.succ → ¬a ∣ b
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `f = μ.rnDeriv ν`.

This theorem provides the uniqueness of the `rnDeriv` in the Lebesgue decomposition
theorem, while `MeasureTheory.Measure.eq_singularPart` provides the uniqueness of the
`singularPart`. Here, the uniqueness is given in terms of the measures, while the uniqueness in
terms of the functions is given in `eq_rnDeriv`.  -/
MeasureTheory.Measure.eq_withDensity_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν s : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} (c : F), deriv (fun y => f y - c) x = deriv f x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} (h : t.WF)
  {h' : k ∈ Std.DTreeMap.Raw.map f t},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.map f t) k h' = f k (Std.DTreeMap.Raw.Const.get t k ⋯)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.inv_hom_apply : ∀ {M N : CommMonCat} (e : M ≅ N) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Algebra.GroupWithZero.Divisibility
eq_of_forall_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ],
  (∀ (c : α), a ∣ c ↔ b ∣ c) → a = b
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist is antitone with respect to inclusion.  -/
Metric.infEDist_anti : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α}, s ⊆ t → Metric.infEDist x t ≤ Metric.infEDist x s
-- Mathlib.Algebra.Order.Ring.Defs
IsStrictOrderedRing.toNoMaxOrder : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R], NoMaxOrder R
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.instDecidableEqOfNormalOfFintypeAlgEquiv : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → [Normal K L] → [DecidableEq L] → [Fintype Gal(L/K)] → DecidableEq (ConjRootClass K L)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.vcomp_left : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b}
  (η₁ η₂ : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel η₁ η₂ → CategoryTheory.FreeBicategory.Rel (η₁.vcomp θ) (η₂.vcomp θ)
-- Mathlib.Analysis.Real.Pi.Chudnovsky
/-- The denominator of the nth term in Chudnovsky's series  -/
chudnovskyDenom : ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeUnop_map : ∀ (J : Type w) {X Y : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.widePullbackShapeUnop J).map f =
    (CategoryTheory.Limits.widePullbackShapeOpMap J (Opposite.unop Y) (Opposite.unop X) f.unop).unop
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.integral_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] {f : β × γ → E},
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    ∫ (z : β × γ), f z ∂(κ.compProd η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findM?_pure : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id m] [inst_3 : Std.IteratorLoop α Id Id] [LawfulMonad m] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id m] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → ULift.{w, 0} Bool},
  (it.findM? fun x => pure (f x)) = pure (it.find? fun x => (f x).down)
-- Aesop.EMap
Aesop.EMap.mk : {α : Type u_1} → Lean.PArray (Option (Lean.Expr × α)) → Lean.Meta.DiscrTree ℕ → Aesop.EMap α
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.himp_def : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : TopologicalSpace.Opens α},
  U ⇨ V = TopologicalSpace.Opens.interior (↑U ⇨ ↑V)
-- Init.GrindInstances.Ring.UInt
USize.intCast_neg : ∀ (x : ℤ), ↑(-x) = -↑x
-- Mathlib.Analysis.Normed.Group.Completion
UniformSpace.Completion.nnnorm_coe : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (x : E), ‖↑x‖₊ = ‖x‖₊
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffOn_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (E : Type uE) [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι] (i : ι) (s : Set (ι → E)),
  ContDiffOn 𝕜 n (fun f => f i) s
-- Mathlib.Order.BooleanAlgebra.Defs
/-- `x \ y` is equal to `x ⊓ yᶜ`  -/
BooleanAlgebra.sdiff_eq : ∀ {α : Type u} [self : BooleanAlgebra α] (x y : α), x \ y = x ⊓ yᶜ
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddMonoid.equivWithZeroFreeAddSemigroup.eq_1 : ∀ {α : Type u_1},
  FreeAddMonoid.equivWithZeroFreeAddSemigroup =
    { toFun := ⇑(FreeAddMonoid.lift fun x => ↑(FreeAddSemigroup.of x)),
      invFun := ⇑(WithZero.lift FreeAddSemigroup.toFreeAddMonoid), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Init.Data.Array.Find
Array.findIdx_eq_size_of_false : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, (∀ x ∈ xs, p x = false) → Array.findIdx p xs = xs.size
-- Mathlib.Algebra.GradedMonoid
SetLike.coe_gOne : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : One R] [inst_2 : Zero ι] (A : ι → S)
  [inst_3 : SetLike.GradedOne A], ↑GradedMonoid.GOne.one = 1
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℂ fun n => ↑n + 1) 0 1
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.instLocallySmallElements : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  (F : CategoryTheory.Functor C (Type w)), CategoryTheory.LocallySmall.{w, v, max u w} F.Elements
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.mk : {R : Type v} →
  [inst : NonAssocSemiring R] →
    [inst_1 : Star R] →
      (toSubsemiring : Subsemiring R) →
        (∀ {a : R}, a ∈ toSubsemiring.carrier → star a ∈ toSubsemiring.carrier) → StarSubsemiring R
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → Array α → Sort u_2) (n : ℕ) (xs : Array α) (h_1 : (xs : Array α) → motive 0 xs)
  (h_2 : (n : ℕ) → (xs : Array α) → motive n.succ xs),
  (match n.succ, xs with
    | 0, xs => h_1 xs
    | n.succ, xs => h_2 n xs) =
    h_2 n xs
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.below.trivial : ∀ {F : PFunctor.{uA, uB}} {motive : (a : ℕ) → (a_1 a_2 : F.M) → PFunctor.M.Agree' a a_1 a_2 → Prop} (x y : F.M),
  PFunctor.M.Agree'.below ⋯
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α}, t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.Order.Fin.Tuple
/-- Order isomorphism between tuples of length `n + 1` and pairs of an element and a tuple of length
`n` given by separating out the `p`-th element of the tuple.

This is `Fin.insertNth` as an `OrderIso`.  -/
Fin.insertNthOrderIso : {n : ℕ} →
  (α : Fin (n + 1) → Type u_2) →
    [inst : (i : Fin (n + 1)) → LE (α i)] →
      (p : Fin (n + 1)) → α p × ((i : Fin n) → α (p.succAbove i)) ≃o ((i : Fin (n + 1)) → α i)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_mono_ae : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  s ≤ᵐ[μ] t → μ.restrict s ≤ μ.restrict t
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.FibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.FibrantObject.homRel C f g ↔ HomotopicalAlgebra.LeftHomotopyRel f.hom g.hom
-- Mathlib.Data.Set.Semiring
/-- Since addition on `SetSemiring` is commutative (it is set union), there is no need
to also have the instance `AddRightMono (SetSemiring α)`.  -/
SetSemiring.addLeftMono : ∀ {α : Type u_1}, AddLeftMono (SetSemiring α)
-- Mathlib.Algebra.Group.Action.Basic
IsUnit.smul_bijective : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] {m : α},
  IsUnit m → Function.Bijective fun a => m • a
-- Mathlib.Geometry.Manifold.StructureGroupoid
closedUnderRestriction' : ∀ {H : Type u_1} [inst : TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G]
  {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ {s : Set H}, IsOpen s → e.restr s ∈ G
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.instPartialOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α], MulOpposite.instPartialOrder = PartialOrder.lift MulOpposite.unop ⋯
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- A matrix is Hadamard iff its negation is.  -/
Matrix.IsHadamard.neg_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Ring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, (-A).IsHadamard ↔ A.IsHadamard
-- Mathlib.AlgebraicGeometry.Limits
/-- The open cover of the coproduct of two schemes.  -/
AlgebraicGeometry.coprodOpenCover : (X Y : AlgebraicGeometry.Scheme) → (X ⨿ Y).OpenCover
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.mapExtendScalars.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S S_1 : Submonoid R) (e_S : S = S_1) {M : Type u_2} {M' : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M']
  (f f_1 : M →ₗ[R] M') (e_f : f = f_1) [inst_5 : IsLocalizedModule S f] {N : Type u_4} {N' : Type u_5}
  [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N] [inst_9 : Module R N']
  (g g_1 : N →ₗ[R] N') (e_g : g = g_1) [inst_10 : IsLocalizedModule S g] (Rₛ : Type u_6) [inst_11 : CommSemiring Rₛ]
  [inst_12 : Algebra R Rₛ] [inst_13 : Module Rₛ M'] [inst_14 : Module Rₛ N'] [inst_15 : IsScalarTower R Rₛ M']
  [inst_16 : IsScalarTower R Rₛ N'] [inst_17 : IsLocalization S Rₛ],
  IsLocalizedModule.mapExtendScalars S f g Rₛ = IsLocalizedModule.mapExtendScalars S_1 f_1 g_1 Rₛ
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital seminormed commutative ring is a non-unital commutative ring endowed with a
seminorm which satisfies the inequality `‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
NonUnitalSeminormedCommRing : Type u_5 → Type u_5
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
Polynomial.idealX_span : ∀ (K : Type u_1) [inst : Field K], (Polynomial.idealX K).asIdeal = Ideal.span {Polynomial.X}
-- Mathlib.Analysis.Normed.Group.Continuity
/-- In a normed additive group, the pullback under the norm of `𝓝[>] 0` is the punctured
neighborhood of `0`.  -/
comap_norm_nhdsGT_zero : ∀ (E : Type u_4) [inst : NormedAddGroup E], Filter.comap norm (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 0 {0}ᶜ
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.instCoeFunNonlinearRightInverseForall : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] → (f : E →SL[σ] F) → CoeFun f.NonlinearRightInverse fun x => F → E
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_2 : ∀ {α : Type u_1}, RegularExpression.epsilon.matches' = 1
-- Init.Control.StateRef
StateRefT'.instAlternativeOfMonad : {ω σ : Type} → {m : Type → Type} → [Alternative m] → [Monad m] → Alternative (StateRefT' ω σ m)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso_hom_app_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addUnitIso C).hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj X_1)
-- Mathlib.Order.CompleteBooleanAlgebra
CompleteBooleanAlgebra.toSDiff : {α : Type u_1} → [self : CompleteBooleanAlgebra α] → SDiff α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insert! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a k : α} {v : β},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insert! k v t) a =
        if compare k a = Ordering.eq then some v else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat),
  (CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence F).unitIso =
    CategoryTheory.Iso.refl
      (CategoryTheory.Functor.id (CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)))
-- Mathlib.Data.Nat.Cast.Order.Ring
Nat.neg_cast_eq_cast : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {m n : ℕ}, -↑m = ↑n ↔ m = 0 ∧ n = 0
-- Mathlib.Algebra.Ring.Units
IsUnit.sub_iff : ∀ {α : Type u} [inst : Ring α] {x y : α}, IsUnit (x - y) ↔ IsUnit (y - x)
-- Batteries.Data.List.Basic
List.fillNones.eq_2 : ∀ {α : Type u_1} (x : List α) (a : α) (as : List (Option α)), (some a :: as).fillNones x = a :: as.fillNones x
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The connecting homomorphism `δ : L₀.X₃ ⟶ L₃.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.δ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.L₀.X₃ ⟶ S.L₃.X₁
-- Mathlib.Data.Finset.Basic
Finset.disjoint_filter_filter' : ∀ {α : Type u_1} (s t : Finset α) {p q : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  Disjoint p q → Disjoint (Finset.filter p s) (Finset.filter q t)
-- Mathlib.RingTheory.Polynomial.GaussNorm
/-- If `v` is a nonnegative function with `v 0 = 0` and `c` is nonnegative, there exists a minimal
index `i` such that the Gauss norm of `p` at `c` is attained at `i`.  -/
Polynomial.exists_min_eq_gaussNorm : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} [ZeroHomClass F R ℝ]
  [NonnegHomClass F R ℝ] (p : Polynomial R),
  0 ≤ c →
    ∃ i,
      Polynomial.gaussNorm v c p = v (p.coeff i) * c ^ i ∧ ∀ j < i, v (p.coeff j) * c ^ j < Polynomial.gaussNorm v c p
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddMonoid : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddMonoid M] → [ContinuousAdd M] → AddMonoid (SeparationQuotient M)
-- Init.Data.Hashable
instHashableInt : Hashable ℤ
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.lowerCrossingTime_lt_of_lt_upcrossingsBefore : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  0 < N → a < b → n < MeasureTheory.upcrossingsBefore a b f N ω → MeasureTheory.lowerCrossingTime a b f N n ω < N
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_vadd_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k),
  (AffineMap.lineMap v₁ v₂) c +ᵥ (AffineMap.lineMap p₁ p₂) c = (AffineMap.lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂)) c
-- Mathlib.NumberTheory.NumberField.Ideal.Basic
/-- For `I` an integral ideal of `K`, the group morphism from the torsion of `K` to `(𝓞 K ⧸ I)ˣ`.
 -/
Ideal.torsionMapQuot : {K : Type u_1} →
  [inst : Field K] →
    (I : Ideal (NumberField.RingOfIntegers K)) → ↥(NumberField.Units.torsion K) →* (NumberField.RingOfIntegers K ⧸ I)ˣ
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_const : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] {c : ε} {s : Set α},
  MeasurableSet s → p ≠ 0 → p ≠ ⊤ → MeasureTheory.eLpNorm (s.indicator fun x => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_inv_ι_app : ∀ {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))
  (U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.colimit F)) (j : J),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit F U).inv
      ((CategoryTheory.Limits.colimit.ι F j).c.app (Opposite.op U)) =
    CategoryTheory.Limits.limit.π (AlgebraicGeometry.PresheafedSpace.componentwiseDiagram F U) (Opposite.op j)
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.scalingConstantOf.congr_simp : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ μ_1 : MeasureTheory.Measure α)
  (e_μ : μ = μ_1) [inst_2 : IsUnifLocDoublingMeasure μ] (K K_1 : ℝ),
  K = K_1 → IsUnifLocDoublingMeasure.scalingConstantOf μ K = IsUnifLocDoublingMeasure.scalingConstantOf μ_1 K_1
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instNontrivial : ∀ {R : Type u_1} {a b : R} [Nontrivial R], Nontrivial (QuadraticAlgebra R a b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_minKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {fallback : α} {he : Std.Internal.List.containsKey (Std.Internal.List.minKeyD l fallback) l = true},
      Std.Internal.List.getKey (Std.Internal.List.minKeyD l fallback) l he = Std.Internal.List.minKeyD l fallback
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_mul : ∀ (a b : UInt32), (a * b).toUInt64 = a.toUInt64 * b.toUInt64 % 4294967296