mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Unramified.LocalRing
/-- [Stacks Tag 00UW](https://stacks.math.columbia.edu/tag/00UW) ((2)) -/
Algebra.instFiniteResidueFieldOfFormallyUnramified : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [inst_5 : IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S]
  [Algebra.FormallyUnramified R S], Module.Finite (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.Algebra.Order.SuccPred
/-- A typeclass for `succ x = x + 1`.  -/
SuccAddOrder : (α : Type u_1) → [Preorder α] → [Add α] → [One α] → Type u_1
-- Mathlib.CategoryTheory.Sites.Continuous
/-- Given a 1-hypercover `E : J.OneHypercover X` of an object of `C`, a functor `F : C ⥤ D`
such that `E.IsPreservedBy F K` for a Grothendieck topology `K` on `D`, this is
the image of `E` by `F`, as a 1-hypercover of `F.obj X` for `K`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {X : C} →
            (E : J.OneHypercover X) →
              (F : CategoryTheory.Functor C D) →
                (K : CategoryTheory.GrothendieckTopology D) → [E.IsPreservedBy F K] → K.OneHypercover (F.obj X)
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
/-- **Inclusion-exclusion principle**, indicator version over a finite union of sets.  -/
Finset.indicator_biUnion_eq_sum_powerset : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddCommGroup G] (s : Finset ι) (S : ι → Set α) (f : α → G)
  (a : α),
  (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (t.card + 1) • (⋂ i ∈ t, S i).indicator f a
-- Mathlib.Control.Monad.Writer
/-- Lift an `M` to a `WriterT ω M`, using the given `empty` as the monoid unit.  -/
WriterT.liftTell : {M : Type u → Type v} → {ω : Type u} → [Monad M] → ω → MonadLift M (WriterT ω M)
-- Mathlib.Data.Multiset.Bind
Multiset.sum_bind : ∀ {α : Type u_1} {β : Type v} [inst : AddCommMonoid β] (s : Multiset α) (t : α → Multiset β),
  (s.bind t).sum = (Multiset.map (fun a => (t a).sum) s).sum
-- Mathlib.Algebra.Group.Units.Defs
Units.instDecidableEq.eq_1 : ∀ {α : Type u} [inst : Monoid α] [inst_1 : DecidableEq α] (x x_1 : αˣ),
  x.instDecidableEq x_1 = decidable_of_iff' (↑x = ↑x_1) ⋯
-- Mathlib.Topology.Order
isOpen_singleton_true : IsOpen {True}
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.comap_f : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} {M : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
  [inst_7 : IsManifold I k M] [inst_8 : CompactSpace M] [inst_9 : BoundarylessManifold I M] (s : SingularManifold X k I)
  {φ : M → s.M} (hφ : Continuous φ), (s.comap hφ).f = s.f ∘ φ
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {a : α} {b : β}, a +ᵥ {b} = {a +ᵥ b}
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_inv : ∀ {R : Type u_1} [inst : GroupWithZero R] [inst_1 : StarMul R] (U : ↥(unitary R)), ↑U⁻¹ = (↑U)⁻¹
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson.isMaximal : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [H : I.IsMaximal], I.jacobson.IsMaximal
-- Mathlib.Topology.Order.SuccPred
SuccOrder.nhds_of_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α}, IsMin a → nhds a = pure a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv_def : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Inv G] (μ : MeasureTheory.Measure G),
  μ.inv = MeasureTheory.Measure.map Inv.inv μ
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The canonical linear map `M →ₗ[R] DividedPowerAlgebra R M`.  -/
DividedPowerAlgebra.embed : (R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] DividedPowerAlgebra R M
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.conjugate_embedding_mem_mixedEmbeddingsOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K},
  ∀ w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v,
    NumberField.ComplexEmbedding.conjugate w.embedding ∈ NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.ancestralRel_iff : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s t : h.ι),
  h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t)
-- Mathlib.Topology.Sheaves.Abelian
TopCat.Presheaf.stalkFunctor.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (x x_1 : ↑X), x = x_1 → TopCat.Presheaf.stalkFunctor C x = TopCat.Presheaf.stalkFunctor C x_1
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
apply_eq_dotProduct_toMatrix₂_mulVec : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂]
  {σ₁ σ₂ : R →+* R} [inst_5 : Fintype n] [inst_6 : Fintype m] [inst_7 : DecidableEq m] [inst_8 : DecidableEq n]
  (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂) (B : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] R) (x : M₁) (y : M₂),
  (B x) y = ⇑σ₁ ∘ ⇑(b₁.repr x) ⬝ᵥ ((LinearMap.toMatrix₂ b₁ b₂) B).mulVec (⇑σ₂ ∘ ⇑(b₂.repr y))
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.mutuallySingular_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s t : MeasureTheory.SignedMeasure α),
  MeasureTheory.VectorMeasure.MutuallySingular s t ↔ s.totalVariation.MutuallySingular t.totalVariation
-- Mathlib.Analysis.Convex.Side
Function.Injective.sOppSide_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : CommRing R]
  [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V]
  [inst_5 : AddTorsor V P] [inst_6 : AddCommGroup V'] [inst_7 : Module R V'] [inst_8 : AddTorsor V' P']
  {s : AffineSubspace R P} {x y : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → ((AffineSubspace.map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.toMatrix_symm`. -/
BilinForm.toMatrix_symm : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁),
  (LinearMap.BilinForm.toMatrix b).symm = Matrix.toBilin b
-- Mathlib.LinearAlgebra.TensorProduct.Opposite
Algebra.TensorProduct.opAlgEquiv_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (a : A) (b : B),
  (Algebra.TensorProduct.opAlgEquiv R S A B).symm (MulOpposite.op (a ⊗ₜ[R] b)) = MulOpposite.op a ⊗ₜ[R] MulOpposite.op b
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.instBicategoryMonoidalSingleObj : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Bicategory (CategoryTheory.MonoidalSingleObj C)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skipWhile_eq_self : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, ¬String.Slice.Pattern.Model.MatchesAt pat pos → pos.skipWhile pat = pos
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux.mk : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {V : (AlgebraicGeometry.Spec R).Opens},
  (∀ (f : ↑R) (hf : PrimeSpectrum.basicOpen f ≤ V) (s : ↑(M.presheaf.obj (Opposite.op (PrimeSpectrum.basicOpen f)))),
      ∃ n t, (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) t = f ^ n • s) →
    (∀ (f : ↑R) (hf : PrimeSpectrum.basicOpen f ≤ V) (t : ↑(M.presheaf.obj (Opposite.op V))),
        (CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE hf).op)) t = 0 →
          ∃ n, f ^ n • t = 0) →
      AlgebraicGeometry.QuasicoherentTilde.Aux✝ M V
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).get k' h' = cast ⋯ v
-- Mathlib.Algebra.Group.Invertible.Defs
/-- An element in a Dedekind-finite monoid is invertible if it has a right inverse.  -/
invertibleOfRightInverse : {α : Type u} → [inst : Monoid α] → [IsDedekindFiniteMonoid α] → (a b : α) → a * b = 1 → Invertible a
-- Mathlib.Algebra.Star.SelfAdjoint
isSelfAdjoint_map : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : Star R] [inst_1 : Star S] [inst_2 : FunLike F R S]
  [StarHomClass F R S] [TrivialStar R] (f : F) (x : R), IsSelfAdjoint (f x)
-- Mathlib.Combinatorics.Digraph.Basic
/-- The infimum of two digraphs `x ⊓ y` has edges where both `x` and `y` have edges.  -/
Digraph.instMin : {V : Type u_2} → Min (Digraph V)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousLinearMap.coe_toContinuousAffineMap : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] [inst_6 : TopologicalSpace W]
  (f : V →L[R] W), ⇑f.toContinuousAffineMap = ⇑f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g h : G) (a : ↑A),
  ((fun₀ | (g, 1) => (A.ρ g) a) - fun₀ | (1, h) => a) ∈ groupHomology.boundaries₂ A
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.toList_uLift : ∀ {α β : Type u} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id],
  it.uLift.toList = List.map ULift.up it.toList
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.swap B C).mapId x).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1))
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.mk.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app : (a : B) → η.app a ⟶ θ.app a)
  (naturality :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)))
      CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam)
  (app_1 : (a : B) → η.app a ⟶ θ.app a)
  (naturality_1 :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app_1 b))
            (θ.naturality f).hom =
          CategoryTheory.CategoryStruct.comp (η.naturality f).hom
            (CategoryTheory.Bicategory.whiskerRight (app_1 a) (G.map f)))
      CategoryTheory.Oplax.StrongTrans.Modification.naturality._autoParam),
  ({ app := app, naturality := naturality } = { app := app_1, naturality := naturality_1 }) = (app = app_1)
-- Init.Data.Int.Linear
Int.Internal.Linear.emod_le_cert.eq_1 : ∀ (y n : ℤ), Int.Internal.Linear.emod_le_cert y n = (y != 0 && n == 1 - ↑y.natAbs)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.left : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} (self : CategoryTheory.SimplicialThickening.Path i j), i ∈ self.I
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_univ : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F}, HasGradientWithinAt f f' Set.univ x ↔ HasGradientAt f f' x
-- Mathlib.Data.Set.Function
Set.MapsTo.inter : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s t₁ → Set.MapsTo f s t₂ → Set.MapsTo f s (t₁ ∩ t₂)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- Pull an additive subsemigroup back to an opposite subsemigroup
along `AddOpposite.unop`  -/
AddSubsemigroup.op : {M : Type u_2} → [inst : Add M] → AddSubsemigroup M → AddSubsemigroup Mᵃᵒᵖ
-- Init.Guard
/-- Tactic to check that the target agrees with a given expression.
* `guard_target = e` checks that the target is defeq at reducible transparency to `e`.
* `guard_target =~ e` checks that the target is defeq at default transparency to `e`.
* `guard_target =ₛ e` checks that the target is syntactically equal to `e`.
* `guard_target =ₐ e` checks that the target is alpha-equivalent to `e`.

The term `e` is elaborated with the type of the goal as the expected type, which is mostly
useful within `conv` mode.
 -/
Lean.Parser.Tactic.guardTargetConv : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_union_of_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- If a span is the pullback span over the terminal object, then it is a binary product.  -/
isBinaryProductOfIsTerminalIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
      (c : CategoryTheory.Limits.Cone F) →
        {X : C} →
          (hX : CategoryTheory.Limits.IsTerminal X) →
            (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ X) →
              (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ X) →
                CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.PullbackCone.mk (c.π.app { as := CategoryTheory.Limits.WalkingPair.left })
                      (c.π.app { as := CategoryTheory.Limits.WalkingPair.right }) ⋯) →
                  CategoryTheory.Limits.IsLimit c
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hf_modif_FE : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (x : ℝ),
  0 < x → P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x
-- Init.Data.SInt.Bitwise
USize.toISize_or : ∀ (a b : USize), (a ||| b).toISize = a.toISize ||| b.toISize
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The left homotopy relation is reflexive.
 -/
SSet.Truncated.HomotopicL.refl : ∀ {X : SSet.Truncated 2}
  {x y : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })}
  {f : SSet.Truncated.Edge x y}, SSet.Truncated.HomotopicL f f
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α), Filter.Tendsto (f a) Filter.atBot (nhds 0)
-- Mathlib.Data.List.ModifyLast
List.modifyLast_concat : ∀ {α : Type u_1} (f : α → α) (a : α) (l : List α), List.modifyLast f (l ++ [a]) = l ++ [f a]
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.rank_vonNeumann : ∀ (o : Ordinal.{u_1}), (ZFSet.vonNeumann o).rank = o
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false →
    ¬cmp k (t.minKeyD fallback) = Ordering.eq → (t.erase k).minKeyD fallback = t.minKeyD fallback
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.max?.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  x.max? =
    match x with
    | RBTree.RBNode.nil => none
    | RBTree.RBNode.node c l v RBTree.RBNode.nil => some v
    | RBTree.RBNode.node c l v r => r.max?
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.mk.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (app app_1 : (a : B) → η.app a ⟶ θ.app a) (e_app : app = app_1)
  (naturality :
    ∀ {a b : B} (f : a ⟶ b),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (app a) (G.map f)) (θ.naturality f) =
        CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b))),
  { app := app, naturality := naturality } = { app := app_1, naturality := ⋯ }
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.mul_one : ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a * Nat.rawCast 1 = a
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- A version of `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary` that works for bases with
different index types.  -/
OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : Fintype ι']
  (a : OrthonormalBasis ι' 𝕜 E) (b : OrthonormalBasis ι 𝕜 E),
  (a.toBasis.toMatrix ⇑b).conjTranspose * a.toBasis.toMatrix ⇑b = 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.rocIterator : {α : Type u_1} → {β : α → Type u_2} → [inst : Ord α] → Std.DTreeMap.Internal.Impl α β → α → α → Std.Iter ((a : α) × β a)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The signs which appear in the vertical differential of the total complex.  -/
ComplexShape.ε : {I : Type u_7} → [inst : AddMonoid I] → (c : ComplexShape I) → [c.TensorSigns] → I → ℤˣ
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.congr_fun : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (η η' : ApplicativeTransformation F G),
  η = η' → ∀ {α : Type u} (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.natTransPInfty_f_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℕ)
  (X : CategoryTheory.SimplicialObject C),
  (AlgebraicTopology.DoldKan.natTransPInfty_f C n).app X = AlgebraicTopology.DoldKan.PInfty.f n
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `smul_apply`. -/
CuspForm.IsGLPos.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.memLp_two_of_variance_ne_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ → ProbabilityTheory.variance X μ ≠ 0 → MeasureTheory.MemLp X 2 μ
-- Mathlib.Analysis.Normed.Ring.Units
/-- The function
`fun t ↦ Ring.inverse (x + t) - (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹`
is `O(t ^ n)` as `t → 0`.  -/
NormedRing.inverse_add_norm_diff_nth_order : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ) (n : ℕ),
  (fun t => Ring.inverse (↑x + t) - (∑ i ∈ Finset.range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[nhds 0] fun t => ‖t‖ ^ n
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- Signs alternate in the forward direction of the complex shape.  -/
ComplexShape.χ_next : ∀ {ι : Type u_1} (c : ComplexShape ι) [inst : c.EulerCharSigns] {i j : ι}, c.Rel i j → c.χ j = -c.χ i
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.unique : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    HasFPowerSeriesWithinOnBall g p s x r → Set.EqOn f g (insert x s ∩ Metric.eball x r)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_le_pi_mul_log' : ∀ (x : ℝ), Chebyshev.theta x ≤ ↑⌊x⌋₊.primeCounting * Real.log x
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
thickening_cthickening : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ},
  0 < ε → 0 ≤ δ → ∀ (s : Set E), Metric.thickening ε (Metric.cthickening δ s) = Metric.thickening (ε + δ) s
-- Lean.ImportingFlag
/-- By default the `initialize` code is not executed when importing .olean files.
When this flag is set to `true`, the initializers are executed.
This method is meant to be used by the Lean frontend only.
Remark: it is not safe to run `initialize` code when using multiple threads.
Remark: Any loaded native Lean code must match its imported version. In particular,
  no two versions of the same module may be loaded when this flag is set.
  No native code may be loaded after its module has been imported.
Remark: Compacted module regions must not be freed when using this flag as the
  cached initializer results may reference objects in them.
Remark: The Lean frontend executes this method at startup time.
 -/
Lean.enableInitializersExecution : BaseIO Unit
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_norm_norm`. -/
Asymptotics.IsBigOWith.of_norm_norm : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {c : ℝ} {f' : α → E'} {g' : α → F'} {l : Filter α},
  (Asymptotics.IsBigOWith c l (fun x => ‖f' x‖) fun x => ‖g' x‖) → Asymptotics.IsBigOWith c l f' g'
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.lt_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder R]
  (a b : Lex (HahnSeries Γ R)),
  a < b ↔ ∃ i, (∀ j < i, (ofLex a).coeff j = (ofLex b).coeff j) ∧ (ofLex a).coeff i < (ofLex b).coeff i
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The obvious isomorphism `(R/I)/J' → (R/J)/I'`  -/
DoubleQuot.quotQuotEquivComm : {R : Type u} →
  [inst : CommRing R] →
    (I J : Ideal R) → (R ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J ≃+* (R ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mk J) I
-- Mathlib.Order.Filter.Finite
Pairwise.exists_mem_filter_of_disjoint : ∀ {α : Type u} {ι : Type u_2} [Finite ι] {l : ι → Filter α},
  Pairwise (Function.onFun Disjoint l) → ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Function.onFun Disjoint s)
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
ringKrullDim_le_spanFinrank_maximalIdeal : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R],
  ringKrullDim R ≤ ↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R))