mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (I : C) (i₀ i₁ : A ⟶ I) (π : I ⟶ A)
  (i₀_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₀ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam)
  (i₁_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₁ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam)
  (I_1 : C) (i₀_1 i₁_1 : A ⟶ I_1) (π_1 : I_1 ⟶ A)
  (i₀_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₀_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam)
  (i₁_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₁_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam),
  ({ I := I, i₀ := i₀, i₁ := i₁, π := π, i₀_π := i₀_π, i₁_π := i₁_π } =
      { I := I_1, i₀ := i₀_1, i₁ := i₁_1, π := π_1, i₀_π := i₀_π_1, i₁_π := i₁_π_1 }) =
    (I = I_1 ∧ i₀ ≍ i₀_1 ∧ i₁ ≍ i₁_1 ∧ π ≍ π_1)
-- Mathlib.Algebra.Group.Basic
mul_div_cancel_left : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * b / a = b
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap_app_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (δ : CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶ CategoryTheory.MonoidalCategory.curriedTensorPre F)
  (X X_1 X_2 : C),
  (((CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap δ).app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X X_1 X_2).hom)
      (CategoryTheory.CategoryStruct.comp ((δ.app X).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1 X_2))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) ((δ.app X_1).app X_2)))
-- Mathlib.Analysis.Complex.Trigonometric
Real.sinh_sq : ∀ (x : ℝ), Real.sinh x ^ 2 = Real.cosh x ^ 2 - 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.add_nonpos`.  -/
Left.add_nonpos : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [hP : P.IsStableUnderBaseChange], P.universally = P
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category for a comonad creates any limit
which the comonad itself preserves.
 -/
CategoryTheory.comonadicCreatesLimitOfPreservesLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} J] →
            (R : CategoryTheory.Functor D C) →
              (K : CategoryTheory.Functor J D) →
                [inst_3 : CategoryTheory.ComonadicLeftAdjoint R] →
                  [CategoryTheory.Limits.PreservesLimit (K.comp R) ((CategoryTheory.comonadicRightAdjoint R).comp R)] →
                    [CategoryTheory.Limits.PreservesLimit
                          ((K.comp R).comp ((CategoryTheory.comonadicRightAdjoint R).comp R))
                          ((CategoryTheory.comonadicRightAdjoint R).comp R)] →
                      CategoryTheory.CreatesLimit K R
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- If the `p`-adic norms of `q` and `r` are different, then the norm of `q + r` is equal to the max
of the norms of `q` and `r`.  -/
padicNorm.add_eq_max_of_ne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ},
  padicNorm p q ≠ padicNorm p r → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, (k == k') = true → m.getKey? k = m.getKey? k'
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁_D₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂) {Z : C} (h : K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂' i₁₂'') h) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (K.D₂ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'')) h
-- Mathlib.Topology.NhdsWithin
/-- Two functions agree on a neighborhood of `x` if they agree at `x` and in a punctured
neighborhood.  -/
eventuallyEq_nhds_of_eventuallyEq_nhdsNE : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f g : α → β} {a : α},
  f =ᶠ[nhdsWithin a {a}ᶜ] g → f a = g a → f =ᶠ[nhds a] g
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinderEvents_univ : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)],
  MeasureTheory.cylinderEvents Set.univ = MeasurableSpace.pi
-- Init.Data.Vector.MapIdx
Vector.mapFinIdxM.map.eq_def : ∀ {n : ℕ} {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (xs : Vector α n)
  (f : (i : ℕ) → α → i < n → m β) (i j : ℕ) (inv : i + j = n) (ys : Vector β (n - i)),
  Vector.mapFinIdxM.map xs f i j inv ys =
    match i, inv with
    | 0, inv_1 => pure (Vector.cast ⋯ ys)
    | i_1.succ, inv_1 =>
      have j_lt := ⋯;
      have this := ⋯;
      do
      let __do_lift ← f j xs[j] j_lt
      Vector.mapFinIdxM.map xs f i_1 (j + 1) this (Vector.cast ⋯ (ys.push __do_lift))
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_empty : ∀ {α : Type u_1} {ι : Sort u_5} {s : ι → Set α}, ⋃ i, s i = ∅ ↔ ∀ (i : ι), s i = ∅
-- Mathlib.Algebra.Ring.Commute
Commute.neg_one_right : ∀ {R : Type u} [inst : MulOneClass R] [inst_1 : HasDistribNeg R] (a : R), Commute a (-1)
-- Mathlib.Data.Set.Prod
Set.preimage_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (β i)) (f : (i : ι) → α i → β i),
  (fun g i => f i (g i)) ⁻¹' s.pi t = s.pi fun i => f i ⁻¹' t i
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map sending `x : H × H × H → A` to
`(g₁, g₂, g₃ : G × G × G) ↦ φ (x (f g₁, f g₂, f g₃))`.  -/
groupCohomology.cochainsMap₃ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k H} →
          {B : Rep.{u_1, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (ModuleCat.of k (H × H × H → ↑A) ⟶ ModuleCat.of k (G × G × G → ↑B))
-- Mathlib.Data.Vector.Basic
/-- The last element of a `Vector`, given that the vector is at least one element.  -/
List.Vector.last_def : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α (n + 1)}, v.last = v.get (Fin.last n)
-- Batteries.Data.List.Lemmas
List.lt_add_of_mem_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], ∀ y ∈ List.idxsOf x xs s, y < xs.length + s
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.clause : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc →
    Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise subtraction of sets `s - t` is defined as `{x - y | x ∈ s, y ∈ t}` in locale
`Pointwise`.  -/
Set.sub : {α : Type u_2} → [Sub α] → Sub (Set α)
-- Init.Data.SInt.Float32
/-- Obtains the `Float32` whose value is the same as the given `Int16`.

This function does not reduce in the kernel.
 -/
Int16.toFloat32 : Int16 → Float32
-- Mathlib.RingTheory.FreeCommRing
/-- The free commutative ring on `α` is isomorphic to the polynomial ring over ℤ with
variables in `α`  -/
freeCommRingEquivMvPolynomialInt : (α : Type u) → FreeCommRing α ≃+* MvPolynomial α ℤ
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.isoMk_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (e : F.toFunctor ≅ G.toFunctor)
  [inst_4 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  (CategoryTheory.LaxMonoidalFunctor.isoMk e).inv = CategoryTheory.LaxMonoidalFunctor.homMk e.inv
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Replacing a set by its closure does not change the Hausdorff distance.  -/
Metric.hausdorffDist_closure₂ : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, Metric.hausdorffDist s (closure t) = Metric.hausdorffDist s t
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- If a family of submodules is orthogonal and they span the whole space, then the orthogonal
projection provides a means to decompose the space into its submodules.

The projection function is `decompose V x i = (V i).orthogonalProjection x`.

See note [reducible non-instances].  -/
OrthogonalFamily.decomposition : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_4} →
            [inst_3 : DecidableEq ι] →
              [Fintype ι] →
                {V : ι → Submodule 𝕜 E} →
                  [∀ (i : ι), CompleteSpace ↥(V i)] →
                    (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
                      iSup V = ⊤ → DirectSum.Decomposition V
-- Mathlib.Computability.Reduce
_private.Mathlib.Computability.Reduce.0.ManyOneDegree.le_refl : ∀ (d : ManyOneDegree), d ≤ d
-- Init.Prelude
/-- Hierarchical names consist of a sequence of components, each of
which is either a string or numeric, that are written separated by dots (`.`).

Hierarchical names are used to name declarations and for creating
unique identifiers for free variables and metavariables.

You can create hierarchical names using a backtick:
```
`Lean.Meta.whnf
```
It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.

You can use double backticks to request Lean to statically check whether the name
corresponds to a Lean declaration in scope.
```
``Lean.Meta.whnf
```
If the name is not in scope, Lean will report an error.

There are two ways to convert a `String` to a `Name`:

 1. `Name.mkSimple` creates a name with a single string component.

 2. `String.toName` first splits the string into its dot-separated
    components, and then creates a hierarchical name.
 -/
Lean.Name : Type
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.isAtom : ∀ {α : Type u} (f : Ultrafilter α), IsAtom ↑f
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.integral_pullback_invFun_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] (f : CompactlySupportedContinuousMap B E) (b : B),
  ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) (ψ b))) a ∂μA = ∫ (a : A), (H.pullback f b) a ∂μA
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.nhds_zero_eq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F],
  nhds 0 = ⨅ s, ⨅ (_ : Bornology.IsVonNBounded 𝕜₁ s), ⨅ U ∈ nhds 0, Filter.principal {f | Set.MapsTo (⇑f) s U}
-- Init.Data.String.Basic
String.Slice.Pos.str_endPos : ∀ {s : String.Slice}, s.endPos.str = s.endExclusive
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkEqBwdPattern : List Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Group.Prod
MulEquiv.prodUnits.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N],
  MulEquiv.prodUnits =
    { toFun := ⇑((Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))),
      invFun := fun u => { val := (↑u.1, ↑u.2), inv := (↑u.1⁻¹, ↑u.2⁻¹), val_inv := ⋯, inv_val := ⋯ }, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Int.Lemmas
Int.injOn_natAbs_Iic : Set.InjOn Int.natAbs (Set.Iic 0)
-- Mathlib.Computability.PartrecCode
/-- Recursion on `Nat.Partrec.Code` is computable.  -/
Nat.Partrec.Code.computable_recOn : ∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
  Computable c →
    ∀ {z : α → σ},
      Computable z →
        ∀ {s : α → σ},
          Computable s →
            ∀ {l : α → σ},
              Computable l →
                ∀ {r : α → σ},
                  Computable r →
                    ∀ {pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                      Computable₂ pr →
                        ∀ {co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                          Computable₂ co →
                            ∀ {pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
                              Computable₂ pc →
                                ∀ {rf : α → Nat.Partrec.Code × σ → σ},
                                  Computable₂ rf →
                                    have PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
                                    have CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
                                    have PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
                                    have RF := fun a cf hf => rf a (cf, hf);
                                    have F := fun a c =>
                                      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
                                    Computable fun a => F a (c a)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInvolutiveNeg : {α : Type u_1} → [InvolutiveNeg α] → InvolutiveNeg (Colex α)
-- Mathlib.Computability.EpsilonNFA
εNFA.instInhabited : {α : Type u} → {σ : Type v} → Inhabited (εNFA α σ)
-- Mathlib.Data.Finsupp.Order
Finsupp.isLowerSet_range_embDomain : ∀ {α : Type u_3} {β : Type u_4} (f : α ↪ β), IsLowerSet (Set.range (Finsupp.embDomain f))
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
/-- Arithmetic-geometric sequence with starting value `u₀` and recurrence relation
`u (n + 1) = a * u n + b`.  -/
arithGeom : {R : Type u_1} → [Mul R] → [Add R] → R → R → R → ℕ → R
-- Mathlib.Topology.Maps.Strict.Basic
/-- A map is a strict map in the sense of Bourbaki if the natural map to its image
is a quotient map.  -/
Topology.IsStrictMap : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.break.injEq : ∀ (ref ref_1 : Lean.Syntax), (Lean.Elab.Term.Do.Code.break ref = Lean.Elab.Term.Do.Code.break ref_1) = (ref = ref_1)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_add_one_pow_atTop_atTop_of_pos : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α},
  0 < r → Filter.Tendsto (fun n => (r + 1) ^ n) Filter.atTop Filter.atTop
-- Mathlib.Data.Rat.Defs
Rat.addRightCancelSemigroup : AddRightCancelSemigroup ℚ
-- Mathlib.Order.UpperLower.Closure
LowerSet.iSup_Iic : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), ⨆ a ∈ s, LowerSet.Iic a = lowerClosure s
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.isBotZeroClass : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommMonoid N] [inst_2 : PartialOrder N]
  [IsBotZeroClass N], IsBotZeroClass (Colex (α →₀ N))
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balance1.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c) z d)
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              (z : α) →
                (d : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c)) z d)
  (h_3 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive a x b),
  (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
      a = RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a_1 x b) y c → False) →
    (∀ (a_1 : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
        a = RBTree.RBNode.node RBTree.RBColor.red a_1 x (RBTree.RBNode.node RBTree.RBColor.red b y c) → False) →
      (match a, x, b with
        | RBTree.RBNode.node RBTree.RBColor.red (RBTree.RBNode.node RBTree.RBColor.red a x b) y c, z, d =>
          h_1 a x b y c z d
        | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.red b y c), z, d =>
          h_2 a x b y c z d
        | a, x, b => h_3 a x b) =
        h_3 a x b
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- An epimorphism is surjective on pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.pseudo_surjective_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  [CategoryTheory.Epi f], Function.Surjective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.norm_def : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun i => E i),
  ‖x‖ = ⨅ p, PiTensorProduct.projectiveSeminormAux ↑p
-- Mathlib.Algebra.Algebra.Equiv
/-- `AlgEquiv.toAlgHom` as a `MonoidHom`.  -/
AlgEquiv.toAlgHomHom : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (A ≃ₐ[R] A) →* A →ₐ[R] A
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_succ_succ : ∀ {m n : ℤ}, ((m + 1)<...=n + 1).toArray = Array.map (fun x => x + 1) (m<...=n).toArray
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqDecl.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Lean.Compiler.LCNF.Decl pu → Bool
-- Mathlib.GroupTheory.CosetCover
/-- Let the group `G` be the union of finitely many left cosets `g i • H i`.
If the sum of the inverses of the indexes of the subgroups `H i` is equal to 1,
then the cosets of the subgroups of finite index are pairwise disjoint.  -/
Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
  ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
    ∀ [inst_1 : DecidablePred Subgroup.FiniteIndex],
      ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑({i ∈ s | (H i).FiniteIndex})).PairwiseDisjoint fun i => g i • ↑(H i)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.zpow_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → Group (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] (i : ι)
  (x : G i) (n : ℤ), ⟦⟨i, x⟩⟧ ^ n = ⟦⟨i, x ^ n⟩⟧
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.values_eq_values_toListModel : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.values = Std.Internal.List.values (Std.DHashMap.Internal.toListModel m.buckets)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.mem_prod : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G} {K : Subgroup N} {p : G × N},
  p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K
-- Mathlib.Data.ENat.Basic
ENat.coe_top_add_one : ↑⊤ + 1 = ↑⊤
-- Mathlib.Analysis.Asymptotics.Theta
Filter.EventuallyEq.trans_isTheta : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {l : Filter α} {f₁ f₂ : α → E}
  {g : α → F}, f₁ =ᶠ[l] f₂ → f₂ =Θ[l] g → f₁ =Θ[l] g
-- Mathlib.Analysis.Convex.StrictConvexSpace
not_sameRay_iff_abs_lt_norm_sub : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ¬SameRay ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
/-- a function `f : α × β → ℚ → ℝ` is called a rational conditional kernel CDF of `κ` with respect
to `ν` if is measurable, if `fun b ↦ f (a, b) x` is `(ν a)`-integrable for all `a : α` and `x : ℝ`
and for all measurable sets `s : Set β`, `∫ b in s, f (a, b) x ∂(ν a) = (κ a).real (s ×ˢ Iic x)`.
Also the `ℚ → ℝ` function `f (a, b)` should satisfy the properties of a Stieltjes function for
`(ν a)`-almost all `b : β`.  -/
ProbabilityTheory.IsRatCondKernelCDF : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        (α × β → ℚ → ℝ) → ProbabilityTheory.Kernel α (β × ℝ) → ProbabilityTheory.Kernel α β → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueD k (List.filter (fun p => !l₂.contains p.fst) l₁) fallback =
      if l₂.contains k = true then fallback else Std.Internal.List.getValueD k l₁ fallback
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.decompose_algebraMap : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : CommSemiring R]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (𝒜 : ι → Submodule R A) [inst_5 : GradedAlgebra 𝒜] (r : R),
  (DirectSum.decompose 𝒜) ((algebraMap R A) r) = (algebraMap R (DirectSum ι fun i => ↥(𝒜 i))) r
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.add_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Add γ] [inst_3 : ContinuousAdd γ] (f g : α →ₘ[μ] γ), (f + g).toGerm = f.toGerm + g.toGerm
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical ring homomorphism from the localization of `R` at `p` to the stalk
of the structure sheaf at the point `p`.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) ⟶
            (AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x