mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_eq_zero : ∀ {b x : ℝ}, Real.logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.coe_centralizer : ∀ {M : Type u_1} (S : Set M) [inst : AddSemigroup M], ↑(AddSubsemigroup.centralizer S) = S.addCentralizer
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- A splitting on a short complex induces splittings on isomorphic short complexes.  -/
CategoryTheory.ShortComplex.Splitting.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → S₁.Splitting → (S₁ ≅ S₂) → S₂.Splitting
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft_obj_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {X Y : CategoryTheory.Functor D E} (α : X ⟶ Y),
  ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).map α = F.whiskerLeft α
-- Lean.Data.KVMap
Lean.mkBoolDataValueEx : Bool → Lean.DataValue
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite colimits, then `F.unop : C ⥤ D` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F.unop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.eq_1 : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Option (aig.RefVec w) → Sort u_1) (vec : aig.RefVec w)
  (h_1 : (vec : aig.RefVec w) → motive (some vec)) (h_2 : Unit → motive none),
  (match some vec with
    | some vec => h_1 vec
    | none => h_2 ()) =
    h_1 vec
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), IsClosed I.supportSet
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.neZero_count : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Nonempty α], NeZero MeasureTheory.Measure.count
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousAt_mul_const : ∀ {a b : ENNReal}, a ≠ ⊤ ∨ b ≠ 0 → ContinuousAt (fun x => x * a) b
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_self : ∀ {E : ℕ → Type u_1} (x : (n : ℕ) → E n), dist x x = 0
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.IsNormalMonoCategory D
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_eq_eRank : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.E ⊆ X → M.eRk X = M.eRank
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α} {k : α}, (m.insertManyIfNewUnit l)[k]? = if k ∈ m ∨ l.contains k = true then some () else none
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
AddMonoidAlgebra.antipode_single : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {G : Type u_3}
  [inst_3 : AddGroup G] (g : G) (a : A),
  (HopfAlgebraStruct.antipode R) (AddMonoidAlgebra.single g a) =
    AddMonoidAlgebra.single (-g) ((HopfAlgebraStruct.antipode R) a)
-- Init.Data.Array.MapIdx
List.mapFinIdx_toArray : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_split_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- A single step in evaluating a `LazyEntry`. Allow multiple different outcomes.  -/
Lean.Meta.RefinedDiscrTree.evalLazyEntry : Lean.Meta.RefinedDiscrTree.LazyEntry →
  Bool → Lean.MetaM (Option (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
MulOpposite.instIsUniformGroup : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], IsUniformGroup αᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↑(ProjectiveSpectrum.top 𝒜)) (hx : x ∈ ProjectiveSpectrum.basicOpen 𝒜 f),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection 𝒜 f)
      ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ (ProjectiveSpectrum.basicOpen 𝒜 f) x
        hx) =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
      (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_uIcc : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, (Finset.uIcc a b).Nonempty
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe : ∀ {V : Type u} (G : SimpleGraph V) (u v : V) (p : { p // p.length = 2 }),
  ↑((G.walkLengthTwoEquivCommonNeighbors u v) p) = (↑p).snd
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instStarOfContinuousStar : {α : Type u_1} →
  [inst : MeasurableSpace α] →
    {μ : MeasureTheory.Measure α} →
      {R : Type u_5} → [inst_1 : TopologicalSpace R] → [inst_2 : Star R] → [ContinuousStar R] → Star (α →ₘ[μ] R)
-- Mathlib.RingTheory.Localization.NumDen
/-- `f.den x` is the denominator of `x : f.codomain` as a reduced fraction.  -/
IsFractionRing.den : (A : Type u_1) →
  [inst : CommRing A] →
    [IsDomain A] →
      [UniqueFactorizationMonoid A] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra A K] → [IsFractionRing A K] → K → ↥(nonZeroDivisors A)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.lit.injEq : ∀ (v v_1 : Lean.IR.LitVal), (Lean.IR.Expr.lit v = Lean.IR.Expr.lit v_1) = (v = v_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k : α},
  m.WF → (k ∈ Std.DHashMap.Raw.filter (fun a x => f a) m ↔ ∃ (h : k ∈ m), f (m.getKey k h) = true)
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.map_ker_stabilizer_subtype : ∀ {A : Type u_3} {B : Type u_4} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] (G : Type u_6) [inst_4 : Group G] [inst_5 : MulSemiringAction G B]
  [inst_6 : SMulCommClass G A B],
  Subgroup.map (MulAction.stabilizer G P).subtype (Ideal.Quotient.stabilizerHom P p G).ker = Ideal.inertia G P
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The conversion from a Weierstrass curve to Jacobian coordinates.  -/
WeierstrassCurve.toJacobian : {R : Type r} → WeierstrassCurve R → WeierstrassCurve.Jacobian R
-- Std.Do.WP.SimpLemmas
Std.Do.WP.tryCatch_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {x : ExceptT ε m α} {h : ε → ExceptT ε m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (MonadExceptOf.tryCatch x h)).apply Q =
    (Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosMono.toMulPosReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α] [MulPosMono α], MulPosReflectLT α
-- Mathlib.Topology.UniformSpace.Uniformizable
UniformSpace.toCompletelyRegularSpace : ∀ {X : Type u_1} [inst : UniformSpace X], CompletelyRegularSpace X
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivWithinAt.eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E},
  IsSymmSndFDerivWithinAt 𝕜 f s x →
    ∀ (v w : E), ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.mk_lt_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M} (ha : a ≠ 0)
  {b : M} (hb : b ≠ 0),
  FiniteArchimedeanClass.mk a ha < FiniteArchimedeanClass.mk b hb ↔ ArchimedeanClass.mk a < ArchimedeanClass.mk b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_zero_of_add_nonneg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [AddLeftMono α] {a b : α},
  a ≤ 0 → b ≤ 0 → 0 ≤ a + b → a = 0
-- Init.Data.Array.Attach
Array.foldr_attachWith : ∀ {α : Type u_1} {β : Type u_2} {start : ℕ} {xs : Array α} {q : α → Prop} (H : ∀ a ∈ xs, q a) {f : { x // q x } → β → β}
  {b : β},
  start = xs.size → Array.foldr f b (xs.attachWith q H) start = Array.foldr (fun a acc => f ⟨↑a, ⋯⟩ acc) b xs.attach
-- Lean.ResolveName
/-- Given a name `id` try to find namespaces it may refer to. The resolution procedure works as follows

1- If `id` is in the scope of `namespace` commands the namespace `s_1. ... . s_n`,
then we include `s_1 . ... . s_i ++ n` in the result if it is the name of an existing namespace.
We search "backwards", and include at most one of the in the list of resulting namespaces.

2- If `id` is the exact name of an existing namespace, then include `id`

3- Finally, for each command `open N`, include in the result `N ++ n` if it is the name of an existing namespace.
We only consider simple `open` commands.  -/
Lean.ResolveName.resolveNamespace : Lean.Environment → Lean.Name → List Lean.OpenDecl → Lean.Name → List Lean.Name
-- Mathlib.Order.Filter.Partial
/-- The forward map of a filter under a partial function. Generalization of `Filter.map` to partial
functions.  -/
Filter.pmap : {α : Type u} → {β : Type v} → (α →. β) → Filter α → Filter β
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- Distance from the image of a point under inversion to the center. This formula accidentally
works for `x = c`.  -/
EuclideanGeometry.dist_inversion_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c x : P) (R : ℝ), dist (EuclideanGeometry.inversion c R x) c = R ^ 2 / dist x c
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.is3Clique_iff_exists_cycle_length_three : ∀ {α : Type u_1} {G : SimpleGraph α}, (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3
-- Mathlib.Algebra.Lie.SerreConstruction
CartanMatrix.Generators.H : {B : Type v} → B → CartanMatrix.Generators B
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeList.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (List α) × List α → Sort u_2) (xss : List (List α)) (rest : List α)
  (h_1 : (xss : List (List α)) → (rest : List α) → motive (xss, rest)),
  (match (xss, rest) with
    | (xss, rest) => h_1 xss rest) =
    h_1 xss rest
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.eqToHom_comp_lift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] {b' : 𝒳} (h : b = b'),
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp φ (CategoryTheory.eqToHom h))
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- Extension for the `positivity` tactic: `Real.log` of an integer is always nonnegative.  -/
Mathlib.Meta.Positivity.evalLogIntCast : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.ext_iff : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {f g : X →ₑ[φ] Y}, f = g ↔ ∀ (x : X), f x = g x
-- Mathlib.Data.NNRat.Defs
NNRat.divNat_mul_left : ∀ {a : ℕ}, a ≠ 0 → ∀ (n d : ℕ), NNRat.divNat (a * n) (a * d) = NNRat.divNat n d
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.div_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Div β]
  [inst_3 : ContinuousDiv β] (f g : C(α, β)) (x : α), (f / g) x = f x / g x
-- Mathlib.Topology.ContinuousMap.Algebra
/-- A set of continuous maps "separates points strongly"
if for each pair of distinct points there is a function with specified values on them.

We give a slightly unusual formulation, where the specified values are given by some
function `v`, and we ask `f x = v x ∧ f y = v y`. This avoids needing a hypothesis `x ≠ y`.

In fact, this definition would work perfectly well for a set of non-continuous functions,
but as the only current use case is in the Stone-Weierstrass theorem,
writing it this way avoids having to deal with casts inside the set.
(This may need to change if we do Stone-Weierstrass on non-compact spaces,
where the functions would be continuous functions vanishing at infinity.)
 -/
Set.SeparatesPointsStrongly : {α : Type u_1} → [inst : TopologicalSpace α] → {𝕜 : Type u_5} → [inst_1 : TopologicalSpace 𝕜] → Set C(α, 𝕜) → Prop
-- Mathlib.Algebra.Group.Action.End
/-- The permutation group of `α` acts transitively on `α`.  -/
Equiv.Perm.instIsPretransitive : ∀ {α : Type u_5}, MulAction.IsPretransitive (Equiv.Perm α) α
-- Mathlib.Tactic.Ring.Common
/-- Multiplies two monomials `va, vb` together to get a normalized result monomial.

* `x * y = (x * y)` (for `x`, `y` coefficients)
* `x * (b₁ * b₂) = b₁ * (b₂ * x)` (for `x` coefficient)
* `(a₁ * a₂) * y = a₁ * (a₂ * y)` (for `y` coefficient)
* `(x ^ ea * a₂) * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)`
  (if `ea` and `eb` are identical except coefficient)
* `(a₁ * a₂) * (b₁ * b₂) = a₁ * (a₂ * (b₁ * b₂))` (if `a₁.lt b₁`)
* `(a₁ * a₂) * (b₁ * b₂) = b₁ * ((a₁ * a₂) * b₂)` (if not `a₁.lt b₁`)
 -/
Mathlib.Tactic.Ring.Common.evalMulProd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExProd bt sα a →
                Mathlib.Tactic.Ring.Common.ExProd bt sα b →
                  Lean.MetaM
                    (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) q(«$a» * «$b»))
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.sup_of_right : ∀ {α : Type u_1} {β : Type u_2} {mα mα' : MeasurableSpace α} {x : MeasurableSpace β} {f : α → β},
  Measurable f → Measurable f
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.rank_mul_eq_right_of_isUpperTriangular : ∀ {m : Type um} {n : Type un} [inst : Fintype n] {R : Type u_1} [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype m]
  [inst_4 : LinearOrder m] (A : Matrix m m R) (B : Matrix m n R),
  A.IsUpperTriangular → (∀ (i : m), A.diag i ≠ 0) → (A * B).rank = B.rank
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_injective : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y],
  Function.Injective fun x => ⇑x
-- Init.Grind.AC
Lean.Grind.AC.instReflBEqSeq : ReflBEq Lean.Grind.AC.Seq
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (e : E) (x : 𝕜), MeromorphicAt (fun x => e) x
-- Mathlib.Data.Fintype.Card
Prop.instWellFoundedLT : WellFoundedLT Prop
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.getKey! a = (m.getKey? a).get!
-- Mathlib.Order.RelSeries
/-- If `a₀ -r→ a₁ -r→ ... -r→ aₙ` is an `r`-series and `a` is such that
`aᵢ -r→ a -r→ a_ᵢ₊₁`, then
`a₀ -r→ a₁ -r→ ... -r→ aᵢ -r→ a -r→ aᵢ₊₁ -r→ ... -r→ aₙ`
is another `r`-series
 -/
RelSeries.insertNth : {α : Type u_1} →
  {r : SetRel α α} →
    (p : RelSeries r) →
      (i : Fin p.length) → (a : α) → (p.toFun i.castSucc, a) ∈ r → (a, p.toFun i.succ) ∈ r → RelSeries r
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.fromLoop_trans_toLoop : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] {i : N}
  {p q : ↑(GenLoop N X x)},
  GenLoop.fromLoop i (Path.trans (GenLoop.toLoop i p) (GenLoop.toLoop i q)) = GenLoop.transAt i p q
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on `s` and `a : X → A` is continuous on `t : Set X`,
and `a x` is nonnegative for all `x ∈ t` and `s` is a common neighborhood of the
spectra of `a x` for all `x ∈ t`, then `fun x ↦ cfc f (a x)` is continuous on `t`.

This is weaker than `ContinuousOn.cfc_nnreal` since it requires `f` to be continuous on a
*neighborhood* of the spectra, but in practice it is often easier to apply because `s` is not
required to be compact, nor does it require an indexed family of compact sets. This is proven using
`ContinuousOn.cfc_nnreal` and `upperHemicontinuous_spectrum_nnreal` to produce the necessary family
of compact sets.  -/
ContinuousOn.cfc_nnreal_of_mem_nhdsSet : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [CompleteSpace A] [inst_11 : TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X},
  s ∈ nhdsSet (⋃ x ∈ t, spectrum NNReal (a x)) →
    ContinuousOn a t →
      autoParam (∀ x ∈ t, 0 ≤ a x) ContinuousOn.cfc_nnreal_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) ContinuousOn.cfc_nnreal_of_mem_nhdsSet._auto_3 →
          ContinuousOn (fun x => cfc f (a x)) t
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
/-- **Alias** of the reverse direction of `Matrix.nondegenerate_iff_separatingLeft`. -/
Matrix.SeparatingLeft.nondegenerate : ∀ {n : Type u_1} {A : Type u_4} [inst : CommRing A] [IsDomain A] {M : Matrix n n A} [inst_2 : Finite n],
  M.SeparatingLeft → M.Nondegenerate
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.symm = { toMulEquiv := f.symm, map_le_map_iff' := ⋯ }
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioc_right : ∀ {α : Type v} [inst : Preorder α] (a : α), ⋃ b, Set.Ioc a b = Set.Ioi a
-- Mathlib.Order.Bounds.Basic
bbdBelow_range_inf : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeInf α] {f g : ι → α},
  BddBelow (Set.range f) → BddBelow (Set.range g) → BddBelow (Set.range fun x => f x ⊓ g x)
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.instFiniteDimensionalROfFinite : ∀ (σ K : Type u) [inst : Fintype K] [inst_1 : Field K] [Finite σ], FiniteDimensional K (MvPolynomial.R σ K)
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_add_left_lt : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LT α] [DenselyOrdered α] [AddRightStrictMono α] {a b c : α},
  a + b < c → ∃ a' > a, a' + b < c
-- Mathlib.Computability.TuringMachine.Config
/-- The set of configurations of the machine:

* `halt v`: The machine is about to stop and `v : List ℕ` is the result.
* `ret k v`: The machine is about to pass `v : List ℕ` to continuation `k : Cont`.

We don't have a state corresponding to normal evaluation because these are evaluated immediately
to a `ret` "in zero steps" using the `stepNormal` function.  -/
Turing.ToPartrec.Cfg : Type
-- Init.Data.BEq
PartialEquivBEq.mk : ∀ {α : Type u_1} [inst : BEq α],
  (∀ {a b : α}, (a == b) = true → (b == a) = true) →
    (∀ {a b c : α}, (a == b) = true → (b == c) = true → (a == c) = true) → PartialEquivBEq α
-- Mathlib.Algebra.GroupWithZero.Action.Basic
IsUnit.smul_sub_iff_sub_inv_smul : ∀ {G : Type u_1} {R : Type u_7} [inst : Group G] [inst_1 : Monoid R] [inst_2 : AddGroup R]
  [inst_3 : DistribMulAction G R] [IsScalarTower G R R] [SMulCommClass G R R] (r : G) (a : R),
  IsUnit (r • 1 - a) ↔ IsUnit (1 - r⁻¹ • a)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.compl₁₂_inj : ∀ {R₁ : Type u_3} {R₂ : Type u_4} [inst : Semiring R₁] [inst_1 : Semiring R₂] {Mₗ : Type u_6} {N : Type u_7}
  {Pₗ : Type u_9} {Qₗ : Type u_10} {Qₗ' : Type u_11} [inst_2 : AddCommMonoid Mₗ] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid Pₗ] [inst_5 : AddCommMonoid Qₗ] [inst_6 : AddCommMonoid Qₗ'] [inst_7 : Module R₁ Mₗ]
  [inst_8 : Module R₂ N] [inst_9 : Module R₂ Pₗ] [inst_10 : Module R₁ Pₗ] [inst_11 : Module R₁ Qₗ]
  [inst_12 : Module R₂ Qₗ'] [inst_13 : SMulCommClass R₂ R₁ Pₗ] {f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ} {g : Qₗ →ₗ[R₁] Mₗ}
  {g' : Qₗ' →ₗ[R₂] N}, Function.Surjective ⇑g → Function.Surjective ⇑g' → (f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂)
-- Mathlib.CategoryTheory.Category.Preorder
OrderIso.equivalence_counitIso : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (e : X ≃o Y),
  e.equivalence.counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.mem_addFundamentalInterior : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {x : α},
  x ∈ MeasureTheory.addFundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 0 → x ∉ g +ᵥ s
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Construct an isomorphism from a homeomorphism.  -/
CompHausLike.isoOfHomeo : {P : TopCat → Prop} → {X Y : CompHausLike P} → ↑X.toTop ≃ₜ ↑Y.toTop → (X ≅ Y)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_undef : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ¬μ.Integrable f → ∫ᵛ (x : X), f x ∂[B; μ] = 0
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.Smooth.finitePresentation : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, f.Smooth → f.FinitePresentation
-- Mathlib.Order.PrimeSeparator
/-- **Alias** of `Lattice.mem_ideal_sup_principal`. -/
DistribLattice.mem_ideal_sup_principal : ∀ {α : Type u_1} [inst : Lattice α] (a b : α) (J : Order.Ideal α), b ∈ J ⊔ Order.Ideal.principal a ↔ ∃ j ∈ J, b ≤ j ⊔ a
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient of a second countable space by a group action is second countable.  -/
ContinuousConstSMul.secondCountableTopology : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
  [SecondCountableTopology T] [ContinuousConstSMul Γ T], SecondCountableTopology (Quotient (MulAction.orbitRel Γ T))