mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
HasContDiffBump.mk : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  Nonempty (ContDiffBumpBase E) → HasContDiffBump E
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.abs_truncation_le_bound : ∀ {α : Type u_1} (f : α → ℝ) (A : ℝ) (x : α), |ProbabilityTheory.truncation f A x| ≤ |A|
-- Mathlib.Data.List.Sublists
/-- Auxiliary helper function for `sublists`  -/
List.sublistsAux : {α : Type u} → α → List (List α) → List (List α)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushout.desc.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  {arrows : (j : J) → B ⟶ objs j} [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] {X : C} (f f_1 : B ⟶ X)
  (e_f : f = f_1) (fs fs_1 : (j : J) → objs j ⟶ X) (e_fs : fs = fs_1)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (arrows j) (fs j) = f),
  CategoryTheory.Limits.WidePushout.desc f fs w = CategoryTheory.Limits.WidePushout.desc f_1 fs_1 ⋯
-- Lean.Server.InfoUtils
_private.Lean.Server.InfoUtils.0.Lean.Elab.InfoTree.visitM.go : {m : Type → Type u_1} →
  {α : Type} →
    [Monad m] →
      (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → m Bool) →
        (Lean.Elab.ContextInfo → Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List (Option α) → m α) →
          Option Lean.Elab.ContextInfo → Lean.Elab.InfoTree → m (Option α)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α} {b : β a}, (m.insert a b).getKey! a = a
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If `f` is a split epi, the pushforward-pullback adjunction on sieves is reflective.  -/
CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      (f : Y ⟶ X) →
        [CategoryTheory.IsSplitEpi f] →
          GaloisInsertion (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_zero : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ), c • 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.pow_rpow_inv_natCast : ∀ {n : ℕ}, n ≠ 0 → ∀ (x : ENNReal), (x ^ n) ^ (↑n)⁻¹ = x
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.inheritDocStringExt : Lean.MapDeclarationExtension Lean.Name
-- Mathlib.Algebra.Order.Star.Pi
Pi.instStarOrderedRing : ∀ {ι : Type u_1} [Finite ι] {A : ι → Type u_2} [inst : (i : ι) → PartialOrder (A i)]
  [inst_1 : (i : ι) → NonUnitalSemiring (A i)] [inst_2 : (i : ι) → StarRing (A i)] [∀ (i : ι), StarOrderedRing (A i)],
  StarOrderedRing ((i : ι) → A i)
-- Init.Data.Nat.Basic
Nat.lt_trichotomy : ∀ (a b : ℕ), a < b ∨ a = b ∨ b < a
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- Mapping an edge to a finite set produces a finset of size `2`.  -/
SimpleGraph.card_toFinset_mem_edgeFinset : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet] [inst_1 : DecidableEq V] (e : ↥G.edgeFinset),
  (↑e).toFinset.card = 2
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.sheafedSpace_hasPullback_of_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f], CategoryTheory.Limits.HasPullback f g
-- Aesop.Stats.Basic
Aesop.enableStats : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → m Bool
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.BisimO.match_1.splitter : {α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) →
    (x x_1 : Option (Stream'.Seq1 α)) →
      (Unit → motive none none) →
        ((a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s'))) →
          ((x x_2 : Option (Stream'.Seq1 α)) →
              (x = none → x_2 = none → False) →
                (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α),
                    x = some (a, s) → x_2 = some (a', s') → False) →
                  motive x x_2) →
            motive x x_1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.primeIdealOf.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  hU.primeIdealOf x = hU.isoSpec.hom x
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.equivAddSubgroupOrbits.eq_1 : ∀ {G : Type u} (X : Type v) [inst : AddGroup G] [inst_1 : AddAction G X] (H : AddSubgroup G),
  AddAction.equivAddSubgroupOrbits X H =
    (Setoid.sigmaQuotientEquivOfLe ⋯).symm.trans
      (Equiv.sigmaCongrRight fun ω => (AddAction.equivAddSubgroupOrbitsSetoidComap H ω).symm)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidChangeTextDocumentParams.toJson : Lean.Lsp.DidChangeTextDocumentParams → Lean.Json
-- Init.Data.List.Attach
/-- If we fold over `l.attach` with a function that ignores the membership predicate,
we get the same results as folding over `l` directly.

This is useful when we need to use `attach` to show termination.

Unfortunately this can't be applied by `simp` because of the higher order unification problem,
and even when rewriting we need to specify the function explicitly.
See however `foldl_subtype` below.
 -/
List.foldl_attach : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {b : β},
  List.foldl (fun acc t => f acc ↑t) b l.attach = List.foldl f b l
-- Mathlib.Computability.Reduce
/-- Computable and injective mapping of predicates to sets of natural numbers.
 -/
toNat : {α : Type u} → [Primcodable α] → [Inhabited α] → Set α → Set ℕ
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ico_disjoint_Ico : ∀ {α : Type v} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  Disjoint (Set.Ico a₁ a₂) (Set.Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
-- Batteries.Tactic.Case
/-- The body of a `case ... : ...` tactic.  -/
Batteries.Tactic.casePattBody : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_pos : ∀ {b o : Ordinal.{u_1}}, 1 < b → o ≠ 0 → b ≤ o → 0 < Ordinal.log b o
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_ofNatLT : ∀ {n : ℕ} (h : n < UInt8.size), (UInt8.ofNatLT n h).toUInt16 = UInt16.ofNatLT n ⋯
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.valuation_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], PadicInt.valuation 0 = 0
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddHom.eq_of_eqOn_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f g : M →ₙ+ N}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isSome_get?_eq_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, (Std.DHashMap.Const.get? m a).isSome = m.contains a
-- Mathlib.Algebra.Group.TypeTags.Basic
toMul_zero : ∀ {α : Type u} [inst : One α], Additive.toMul 0 = 1
-- Mathlib.Topology.Sheaves.Points
Opens.instSmallPointOpensGrothendieckTopologyPointsGrothendieckTopology : ∀ (X : Type u_1) [inst : TopologicalSpace X],
  CategoryTheory.ObjectProperty.Small.{u_1, u_1, u_1 + 1} (Opens.pointsGrothendieckTopology X)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelComparison.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)],
  CategoryTheory.Limits.cokernelComparison f G = CategoryTheory.Limits.cokernelComparison f G
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instAddAction : {M : Type u_1} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction Mᵒᵈ α
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGT? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Mathlib.Order.Minimal
/-- **Alias** of `image_monotone_setOfPred_minimal`. -/
image_monotone_setOf_minimal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) →
    f '' {x | Minimal P x} = {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_eq_extract_left : ∀ {a : ByteArray} {i i' j : ℕ}, a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i'
-- Mathlib.CategoryTheory.Action.Limits
Action.instHasColimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasColimits V], CategoryTheory.Limits.HasColimits (Action V G)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.add_apply : ∀ {A : Type u_2} {ι : Type u_3} {E : ι → Type u_4} (x y : WithCStarModule A ((i : ι) → E i)) (i : ι)
  [inst : (i : ι) → AddCommGroup (E i)], (x + y) i = x i + y i
-- Mathlib.Algebra.Group.Basic
add_sub_one_nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ}, n ≠ 0 → ∀ (a : M), (n - 1) • a + a = n • a
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_ediv_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → (a / b).natAbs = a.natAbs / b.natAbs
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_counitIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : D),
  (e.changeFunctor iso).counitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (e.counitIso.inv.app X) (iso.hom.app (e.inverse.obj X))
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_inv_app_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).inv.app X).1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inl_ A A').associator (CategoryTheory.Sum.inl_ (A ⊕ A') T) X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inlCompInverseAssociator A A' T).inv X)
        ((CategoryTheory.Sum.inl_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).hom)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- A commutative group object is a commutative group object in the category of group objects.  -/
CategoryTheory.Grp.instIsCommMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.IsCommMonObj H
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_lt_toColex : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α},
  toColex s < toColex t ↔ s ≠ t ∧ ∀ ⦃a : α⦄, a ∈ s → a ∉ t → ∃ b ∈ t, b ∉ s ∧ a ≤ b
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The fifth simplicial identity  -/
CategoryTheory.SimplicialObject.σ_comp_σ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i j : Fin (n + 1)},
  i ≤ j →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n + 1 + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.σ i.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.σ i) (CategoryTheory.CategoryStruct.comp (X.σ j.succ) h)
-- Mathlib.Order.SuccPred.Basic
Order.succ_pred : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] [NoMinOrder α] (a : α),
  Order.succ (Order.pred a) = a
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pi_congrRight : ∀ {ι : Type u} {f g : ι → Type v},
  (∀ (i : ι), Cardinal.mk (f i) = Cardinal.mk (g i)) → Cardinal.mk ((i : ι) → f i) = Cardinal.mk ((i : ι) → g i)
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.nanosecond : Std.Time.PlainDateTime → Std.Time.Nanosecond.Ordinal
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
ContinuousMapZero.UniqueHom.mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : NonUnitalRing A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Module R A] [inst_9 : IsScalarTower R A A] [inst_10 : SMulCommClass R A A],
  (∀ (s : Set R) [CompactSpace ↑s] [inst_12 : Fact (0 ∈ s)] (φ ψ : ContinuousMapZero (↑s) R →⋆ₙₐ[R] A),
      Continuous ⇑φ → Continuous ⇑ψ → φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s) → φ = ψ) →
    ContinuousMapZero.UniqueHom R A
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Convert the tree to a list in ascending order.  -/
RBTree.RBSet.toList : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → List α
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.mk.injEq : ∀ {σ : Type} (ref : Lean.Syntax) (var? : Option Lean.Elab.Term.Do.Var) (funName : Lean.Syntax)
  (pvars : Array Lean.Syntax) (rhs : σ) (ref_1 : Lean.Syntax) (var?_1 : Option Lean.Elab.Term.Do.Var)
  (funName_1 : Lean.Syntax) (pvars_1 : Array Lean.Syntax) (rhs_1 : σ),
  ({ ref := ref, var? := var?, funName := funName, pvars := pvars, rhs := rhs } =
      { ref := ref_1, var? := var?_1, funName := funName_1, pvars := pvars_1, rhs := rhs_1 }) =
    (ref = ref_1 ∧ var? = var?_1 ∧ funName = funName_1 ∧ pvars = pvars_1 ∧ rhs = rhs_1)
-- Mathlib.Algebra.GroupWithZero.Invertible
invOf_div : ∀ {α : Type u} [inst : GroupWithZero α] (a b : α) [Invertible a] [Invertible b] [inst_3 : Invertible (a / b)],
  ⅟(a / b) = b / a
-- Init.Core
true_eq_false_of_false : False → True = False
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) (h : n < UInt64.size), UInt64.ofNatLT n h = UInt64.ofNatLT n_1 ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.innerFibration_pullbackObjObjπ : ∀ {X₁ Y₁ E B : SSet} {i : X₁ ⟶ Y₁} {p : E ⟶ B} [CategoryTheory.Mono i] [SSet.InnerFibration p]
  (sq₁₃ : CategoryTheory.MonoidalClosed.internalHom.PullbackObjObj i p), SSet.InnerFibration sq₁₃.π
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → LowerSemicontinuousWithinAt f s x → Antitone g → UpperSemicontinuousWithinAt (g ∘ f) s x
-- Mathlib.Analysis.Normed.Operator.CompleteCodomain
ContinuousLinearMap.smulRightL.eq_1 : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ],
  ContinuousLinearMap.smulRightL 𝕜 E Fₗ =
    { toFun := ContinuousLinearMap.smulRightₗ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous₂ 1 ⋯
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).tdiv (Int.negSucc n) = -Int.ofNat (m / n.succ)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddSubgroup.noncommPiCoprod_apply : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} {H : ι → AddSubgroup G} [inst_1 : Fintype ι]
  (comm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → AddCommute x y) (u : (i : ι) → ↥(H i)),
  (AddSubgroup.noncommPiCoprod comm) u = Finset.univ.noncommSum (fun i => ↑(u i)) ⋯
-- Mathlib.GroupTheory.ResiduallyFinite
Group.residuallyFinite_def : ∀ {G : Type u_1} [inst : Group G], Group.ResiduallyFinite G ↔ ⨅ H, H.toSubgroup = ⊥
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balLeft.match_1.congr_eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (r : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (b : RBTree.RBNode α) →
          (z : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c))
  (h_3 : (r : RBTree.RBNode α) → motive r) (a : RBTree.RBNode α) (y : α) (b : RBTree.RBNode α) (z : α)
  (c : RBTree.RBNode α),
  r = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c →
    (match r with
      | RBTree.RBNode.node RBTree.RBColor.black a y b => h_1 a y b
      | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.black a y b) z c => h_2 a y b z c
      | r => h_3 r) ≍
      h_2 a y b z c
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- Notation for the identity prefunctor on a quiver.  -/
Prefunctor.«term𝟭q» : Lean.ParserDescr
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_right : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} (c : M), a ≡ b [PMOD p] → a + c ≡ b + c [PMOD p]
-- Mathlib.Topology.Neighborhoods
interior_setOfPred_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD_parent : ∀ (self : Batteries.UnionFind) (x : ℕ), self.rootD (self.parent x) = self.rootD x
-- Mathlib.Order.Hom.Bounded
TopHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] (f : TopHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.empty_mem_generateMeasurableRec : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}), ∅ ∈ MeasurableSpace.generateMeasurableRec s i
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Quotients of `X`-generated spaces are `X`-generated.  -/
Quotient.isGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [Topology.IsGeneratedBy X Y] {s : Setoid Y}, Topology.IsGeneratedBy X (Quotient s)
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y} (H : CategoryTheory.SimplicialObject.Homotopy f g) (p : ℕ),
  CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H p (p + 1) = -∑ k, (-1) ^ ↑k • H.h k
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.registerAttr : Lean.Name → autoParam Lean.Name Lean.Meta.Grind.registerAttr._auto_1 → IO Lean.Meta.Grind.Extension
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_inv_id : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R]
  (a : Aˣ), autoParam (p ↑a) cfc_inv_id._auto_1 → cfc (fun x => x⁻¹) ↑a = ↑a⁻¹
-- Lean.Parser.Extra
Lean.Parser.adaptCacheableContext.parenthesizer : (Lean.Parser.CacheableParserContext → Lean.Parser.CacheableParserContext) →
  Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_le_apply : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ {a b : Ordinal.{u}}, Ordinal.nfp f a ≤ f b ↔ Ordinal.nfp f a ≤ b
-- Mathlib.Algebra.Category.CommHopfAlgCat
/-- The category of commutative `R`-Hopf algebras and their morphisms.  -/
CommHopfAlgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.mem_chart_target_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p : H × E)
  (q : TangentBundle I M), p ∈ (chartAt (ModelProd H E) q).target ↔ p.1 ∈ (chartAt H q.proj).target
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- A tensor product analogue of `mul_right_comm`.  -/
TensorProduct.rightComm : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (N : Type u_6) →
        (P : Type u_7) →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      TensorProduct R (TensorProduct R M N) P ≃ₗ[R] TensorProduct R (TensorProduct R M P) N
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddZeroClassOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass Mᵃᵒᵖ], DomAddAct.instAddZeroClassOfAddOpposite = inst
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = true → t[a]? = some (t.getD a fallback)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_mul_comm : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R), x * y =ᵥ y * x
-- Mathlib.Tactic.ITauto
/-- * `ak = .and`: `(p: A ∧ B) ⊢ B`
* `ak = .iff`: `(p: A ↔ B) ⊢ B → A`
* `ak = .eq`: `(p: A = B) ⊢ B → A`
 -/
Mathlib.Tactic.ITauto.Proof.andRight : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- **Alias** of the forward direction of `EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection`. -/
EuclideanGeometry.Sphere.IsTangent.isTangentAt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} [inst_4 : Nonempty ↥as]
  [inst_5 : as.direction.HasOrthogonalProjection],
  s.IsTangent as → s.IsTangentAt (↑((EuclideanGeometry.orthogonalProjection as) s.center)) as
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.length_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Init.Data.Int.DivMod.Basic
Int.fdiv.eq_6 : ∀ (m n : ℕ), (Int.negSucc m).fdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_real : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ),
  NumberField.mixedEmbedding.norm (fun x => c, fun x => ↑c) = |c| ^ Module.finrank ℚ K