mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Comparable
compRel_swap_apply : ∀ {α : Type u_1} {a b : α} (r : α → α → Prop), CompRel (Function.swap r) a b ↔ CompRel r a b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.pOpcycles_comp_opcyclesIso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0)
      (groupHomology.opcyclesIso₀ A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₀ A).hom ((Rep.coinvariantsMk k G).app A)
-- Mathlib.CategoryTheory.Sites.Closed
/-- The `J`-closure of a sieve is the collection of arrows which it covers.  -/
CategoryTheory.GrothendieckTopology.close : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → {X : C} → CategoryTheory.Sieve X → CategoryTheory.Sieve X
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.mk : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} →
                            [inst_6 : Algebra S S'] →
                              (val : ι → P'.Ring) →
                                (∀ (i : ι), (MvPolynomial.aeval P'.val) (val i) = (algebraMap S S') (P.val i)) →
                                  P.Hom P'
-- Init.Data.BitVec.Lemmas
/-- The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
when `k` is less than the bitwidth `w`.
 -/
BitVec.udiv_twoPow_eq_of_lt : ∀ {w : ℕ} {x : BitVec w} {k : ℕ}, k < w → x / BitVec.twoPow w k = x >>> k
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_p₁_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j))
  (i₁ i₂ : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯ = hom i₁ i₂
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.NoSuffixPatternModel.of_length_toList_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat],
  (∀ (s t : String),
      String.Slice.Pattern.Model.PatternModel.Matches pat s →
        String.Slice.Pattern.Model.PatternModel.Matches pat t → s.toList.length = t.toList.length) →
    String.Slice.Pattern.Model.NoSuffixPatternModel pat
-- Mathlib.Tactic.Linter.Header
/-- The set of files outside the `Mathlib` package to run the header style linter on,
because they are files that test the linter.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.headerTestFiles : Lean.NameSet
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- A commutative additive monoid object is an additive monoid object in the category
of additive monoid objects.  -/
CategoryTheory.AddMon.instAddMonObjOfIsCommAddMonObjX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M : CategoryTheory.AddMon C} → [CategoryTheory.IsCommAddMonObj M.X] → CategoryTheory.AddMonObj M
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.extension_instLieRing : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : LieRing N] [inst_4 : LieAlgebra R N] [inst_5 : LieRing M]
  [inst_6 : LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : LieAlgebra.IsExtension i p),
  h.extension.instLieRing = inst_1
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuous.comp` -/
ScottContinuous.fun_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {g : β → γ}, ScottContinuous f → ScottContinuous g → ScottContinuous fun x => g (f x)
-- Mathlib.Topology.UrysohnsLemma
/-- `n`-th approximation to a continuous function `f : X → ℝ` such that `f = 0` on `c.C` and `f = 1`
outside of `c.U`.  -/
Urysohns.CU.approx : {X : Type u_1} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → ℕ → Urysohns.CU P → X → ℝ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq_spec_2 : ∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
  (b_2 : Lean.Grind.CommRing.Poly),
  (Lean.Grind.CommRing.Poly.add a a_1 a_2 == Lean.Grind.CommRing.Poly.add b b_1 b_2) =
    (a == b && (a_1 == b_1 && a_2 == b_2))
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.exp_add : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I),
  a ∈ I → b ∈ I → hI.exp (a + b) = hI.exp a * hI.exp b
-- Init.Data.String.Basic
String.Slice.Pos.cast_lt_iff : ∀ {s t : String.Slice} {pos : s.Pos} {pos' : t.Pos} {h : s.copy = t.copy}, pos.cast h < pos' ↔ pos < pos'.cast ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg), (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h).app 0 = f
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk_left_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} {f : X ⟶ Y} {g : CategoryTheory.Arrow T}
  (sq : CategoryTheory.Arrow.mk f ⟶ g) {Z : T} (h : g.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_hom' : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] (s : Multiset ι)
  {F : Type u_8} [inst_2 : FunLike F M N] [MonoidHomClass F M N] (f : F) (g : ι → M),
  (Multiset.map (fun i => f (g i)) s).prod = f (Multiset.map g s).prod
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasBinaryProduct_zero_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] (X : C), CategoryTheory.Limits.HasBinaryProduct 0 X
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [toIsHausdorff : IsHausdorff I M] [toIsPrecomplete : IsPrecomplete I M], IsAdicComplete I M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.Algebra.Category.CoalgCat.Basic
CoalgCat.concreteCategory : {R : Type u} →
  [inst : CommRing R] → CategoryTheory.ConcreteCategory (CoalgCat R) fun x1 x2 => ↑x1.toModuleCat →ₗc[R] ↑x2.toModuleCat
-- Mathlib.CategoryTheory.Shift.Quotient
/-- When `r : HomRel C` is compatible with the shift by an additive monoid, and
`F : C ⥤ D` is a functor which commutes with the shift and is compatible with `r`, then
the induced functor `Quotient.lift r F _ : Quotient r ⥤ D` also commutes with the shift.  -/
CategoryTheory.Quotient.liftCommShift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (F : CategoryTheory.Functor C D) →
          (r : HomRel C) →
            (A : Type w) →
              [inst_2 : AddMonoid A] →
                [inst_3 : CategoryTheory.HasShift C A] →
                  [inst_4 : CategoryTheory.HasShift D A] →
                    [inst_5 : r.IsCompatibleWithShift A] →
                      [F.CommShift A] →
                        (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) →
                          (CategoryTheory.Quotient.lift r F hF).CommShift A
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivWithinAt_sub_const_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt (fun x => f x - c) f' s x ↔ HasDerivWithinAt f f' s x
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
`finrank`.  -/
Module.finrank_eq_card_basis' : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [FiniteDimensional K V] {ι : Type w} (h : Module.Basis ι K V), ↑(Module.finrank K V) = Cardinal.mk ι
-- Mathlib.Logic.Basic
congr_refl_left : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) {a b : α} (h : a = b), ⋯ = ⋯
-- Mathlib.Data.List.InsertIdx
List.map_insertIdx : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α) (n : ℕ) (a : α),
  List.map f (l.insertIdx n a) = (List.map f l).insertIdx n (f a)
-- Init.MetaTypes
/-- When `true` (default: `true`), performs zeta reduction of `let` and `have` expressions.
That is, `let x := v; e[x]` reduces to `e[v]`.
If `zetaHave` is `false` then `have` expressions are not zeta reduced.
See also `zetaDelta`.
 -/
Lean.Meta.Simp.Config.zeta : Lean.Meta.Simp.Config → Bool
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_eqOnSource_of_eqOn' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y} {s : Set X},
  IsOpen s → Set.EqOn (↑e) (↑e') s → e'.source ∩ s ⊆ e.source → e.restr (e'.source ∩ s) ≈ e'.restr s
-- Init.Data.UInt.Lemmas
UInt16.ofNatTruncate_bitVecToNat : ∀ (n : BitVec 16), UInt16.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_strictMono : StrictMono Cardinal.ord
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.toCircle_coe : ∀ (x : ℝ), (↑x).toCircle = Circle.exp x
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddress : DecidableEq Std.Net.SocketAddress
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.getKey? km = some km
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.le_normalizer_iff_commutator_le_left : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ Subgroup.normalizer ↑K ↔ ⁅K, H⁆ ≤ K
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le : ∀ {R : Type u_1} [inst : CommSemiring R] {p q : Polynomial R},
  p.Monic → p ∣ q → q.natDegree ≤ p.natDegree → q = Polynomial.C q.leadingCoeff * p
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality₃_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (f₃ : X₃ ⟶ Y₃) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) f₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ f₃))
        h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_le_of_forall_sum_le : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
  0 < p.toReal →
    ∀ {C : ℝ}, 0 ≤ C → ∀ {f : ↥(lp E p)}, (∀ (s : Finset α), ∑ i ∈ s, ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal) → ‖f‖ ≤ C
-- Init.Data.Array.Find
Array.isSome_find? : ∀ {α : Type u_1} {xs : Array α} {f : α → Bool}, (Array.find? f xs).isSome = xs.any fun x => f x
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isAddQuotientCoveringMap_of_properlyDiscontinuousVAdd : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E],
  Topology.IsQuotientMap f →
    ∀ [ContinuousConstVAdd G E],
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit G e₂) →
        ∀ [ProperlyDiscontinuousVAdd G E] [LocallyCompactSpace E] [T2Space E] [IsCancelVAdd G E],
          IsAddQuotientCoveringMap f G
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.congr_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {f g : F.HomObj G A},
  f = g → ∀ (X : C) (a : A.obj X), f.app X a = g.app X a
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- The predicate that a (co)root is positive with respect to a base.  -/
RootPairing.Base.IsPos : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → {P : RootPairing ι R M N} → P.Base → [CharZero R] → ι → Prop
-- Mathlib.Algebra.Module.Rat
/-- `nnqsmul` is equal to any other module structure via a cast.  -/
NNRat.cast_smul_eq_nnqsmul : ∀ {M : Type u_1} (R : Type u_3) [inst : DivisionSemiring R] [inst_1 : MulAction R M] [inst_2 : MulAction ℚ≥0 M]
  [IsScalarTower ℚ≥0 R M] (q : ℚ≥0) (x : M), ↑q • x = q • x
-- Batteries.Control.LawfulMonadState
/-- `modifyGet f` is equal to getting the state, modifying it, and returning a result.  -/
LawfulMonadStateOf.modifyGet_eq : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] {α : Type u_1} (f : σ → α × σ),
  modifyGet f = do
    let z ← f <$> get
    set z.2
    pure z.1
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.alter.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (y : α) (h_1 : Unit → motive none) (h_2 : (y : α) → motive (some y)),
  (match some y with
    | none => h_1 ()
    | some y => h_2 y) =
    h_2 y
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.intCast_inj : ∀ {m n : ℤ} {R : Type u_1} [inst : Ring R] [CharZero R], ↑m = ↑n ↔ m = n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure
-- Init.Data.Nat.Lemmas
Nat.sub_pos_iff_lt : ∀ {n m : ℕ}, 0 < n - m ↔ m < n
-- Mathlib.LinearAlgebra.Orientation
/-- Given a basis and an orientation, return a basis giving that orientation: either the original
basis, or one constructed by negating a single (arbitrary) basis vector.  -/
Module.Basis.adjustToOrientation : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommGroup M] →
            [inst_4 : Module R M] →
              {ι : Type u_3} →
                [Fintype ι] →
                  [DecidableEq ι] → [Nonempty ι] → Module.Basis ι R M → Orientation R M ι → Module.Basis ι R M
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_add_pi_div_two : ∀ (x : ℂ), Complex.cos (x + ↑Real.pi / 2) = -Complex.sin x
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.instAddCommGroup : {α : Type u_1} → {E : α → Type u_2} → [inst : (i : α) → NormedAddCommGroup (E i)] → AddCommGroup (PreLp E)
-- Mathlib.Analysis.Normed.Group.Hom
/-- A morphism of seminormed abelian groups is a bounded group homomorphism.  -/
NormedAddGroupHom : (V : Type u_1) → (W : Type u_2) → [SeminormedAddCommGroup V] → [SeminormedAddCommGroup W] → Type (max u_1 u_2)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listR.eq_2 : ∀ {α : Type u_1} (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (v : α) (r : RBTree.RBNode α),
  (RBTree.RBNode.Path.left c parent v r).listR = v :: r.toList ++ parent.listR
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The free topological module over a topological space.  -/
TopModuleCat.freeObj : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → TopCat → TopModuleCat R
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a commutative division monoid under pointwise operations if `α` is.  -/
Set.divisionCommMonoid : {α : Type u_2} → [DivisionCommMonoid α] → DivisionCommMonoid (Set α)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.mk.injEq : ∀ {P : Type u_2} [inst : Preorder P] (I : Order.Ideal P) (F : Order.PFilter P) (isCompl_I_F : IsCompl ↑I ↑F)
  (I_1 : Order.Ideal P) (F_1 : Order.PFilter P) (isCompl_I_F_1 : IsCompl ↑I_1 ↑F_1),
  ({ I := I, F := F, isCompl_I_F := isCompl_I_F } = { I := I_1, F := F_1, isCompl_I_F := isCompl_I_F_1 }) =
    (I = I_1 ∧ F = F_1)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.mk.injEq : ∀ (base : Lean.VisibilityMap✝ Lean.Kernel.Environment) (serverBaseExts : Array Lean.EnvExtensionState)
  (checked : Task Lean.Kernel.Environment) (asyncConstsMap : Lean.VisibilityMap✝ Lean.AsyncConsts✝)
  (asyncCtx? : Option Lean.AsyncContext✝) (importRealizationCtx? : Option Lean.RealizationContext✝)
  (localRealizationCtxMap : Lean.NameMap Lean.RealizationContext✝)
  (allRealizations : Task (Lean.NameMap Lean.AsyncConst✝)) (isExporting : Bool)
  (base_1 : Lean.VisibilityMap✝ Lean.Kernel.Environment) (serverBaseExts_1 : Array Lean.EnvExtensionState)
  (checked_1 : Task Lean.Kernel.Environment) (asyncConstsMap_1 : Lean.VisibilityMap✝ Lean.AsyncConsts✝)
  (asyncCtx?_1 : Option Lean.AsyncContext✝) (importRealizationCtx?_1 : Option Lean.RealizationContext✝)
  (localRealizationCtxMap_1 : Lean.NameMap Lean.RealizationContext✝)
  (allRealizations_1 : Task (Lean.NameMap Lean.AsyncConst✝)) (isExporting_1 : Bool),
  ({ base := base, serverBaseExts := serverBaseExts, checked := checked, asyncConstsMap := asyncConstsMap,
        asyncCtx? := asyncCtx?, importRealizationCtx? := importRealizationCtx?,
        localRealizationCtxMap := localRealizationCtxMap, allRealizations := allRealizations,
        isExporting := isExporting } =
      { base := base_1, serverBaseExts := serverBaseExts_1, checked := checked_1, asyncConstsMap := asyncConstsMap_1,
        asyncCtx? := asyncCtx?_1, importRealizationCtx? := importRealizationCtx?_1,
        localRealizationCtxMap := localRealizationCtxMap_1, allRealizations := allRealizations_1,
        isExporting := isExporting_1 }) =
    (base = base_1 ∧
      serverBaseExts = serverBaseExts_1 ∧
        checked = checked_1 ∧
          asyncConstsMap = asyncConstsMap_1 ∧
            asyncCtx? = asyncCtx?_1 ∧
              importRealizationCtx? = importRealizationCtx?_1 ∧
                localRealizationCtxMap = localRealizationCtxMap_1 ∧
                  allRealizations = allRealizations_1 ∧ isExporting = isExporting_1)
-- Mathlib.Order.UpperLower.Closure
/-- The biggest lower subset of a lower set `s` disjoint from a set `t`.  -/
LowerSet.sdiff : {α : Type u_1} → [inst : Preorder α] → LowerSet α → Set α → LowerSet α
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_himp_self : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q : l} [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel Q (Lean.Order.himp P P)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.instMulOneClass : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] →
      [inst_1 : MulAction R M] →
        [inst_2 : MulOneClass M] → [IsScalarTower R M M] → [SMulCommClass R M M] → MulOneClass (SubMulAction R M)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
right Kan extension iff `E'` is.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionEquivOfIso : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E E' : L.RightExtension F} →
                  (E ≅ E') → E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension
-- Init.Data.List.Scan.Lemmas
List.scanl_nil : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β}, List.scanl f init [] = [init]
-- Mathlib.Algebra.Exact.Basic
Function.Exact.of_comp_of_mem_range : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : Zero P],
  g ∘ f = 0 → (∀ (x : N), g x = 0 → x ∈ Set.range f) → Function.Exact f g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two strictly antitone functions is strictly antitone.  -/
StrictAnti.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α}
  [AddLeftStrictMono α] [AddRightStrictMono α], StrictAnti f → StrictAnti g → StrictAnti fun x => f x + g x
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- If a measurable space admits a countable sequence of measurable sets separating points,
it admits a measurable injection into the Cantor space `ℕ → Bool`
(equipped with the product sigma algebra).  -/
MeasurableSpace.measurable_injection_nat_bool_of_countablySeparated : ∀ (α : Type u_1) [inst : MeasurableSpace α] [MeasurableSpace.CountablySeparated α],
  ∃ f, Measurable f ∧ Function.Injective f
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.range_lmapDomain : ∀ {α : Type u_1} {R : Type u_5} [inst : Semiring R] {β : Type u_7} (u : α → β),
  (Finsupp.lmapDomain R R u).range = Submodule.span R (Set.range fun x => fun₀ | u x => 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_union_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} (mem : t₂.contains k = true),
  Std.ExtDTreeMap.Const.get (t₁.union t₂) k ⋯ = Std.ExtDTreeMap.Const.get t₂ k mem
-- Mathlib.Order.CompleteLattice.Basic
Antitone.le_map_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β]
  {f : α → β}, Antitone f → ⨆ i, f (s i) ≤ f (iInf s)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- finite = integral + finite type  -/
RingHom.finite_iff_isIntegral_and_finiteType : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.Finite ↔ f.IsIntegral ∧ f.FiniteType