mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.liftAux_spec : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (a b : FreeNonUnitalNonAssocAlgebra R X),
  FreeLieAlgebra.Rel R X a b → (FreeLieAlgebra.liftAux R f) a = (FreeLieAlgebra.liftAux R f) b
-- Mathlib.Data.Set.Countable
Set.countable_iff_exists_injective : ∀ {α : Type u} {s : Set α}, s.Countable ↔ ∃ f, Function.Injective f
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.instInhabited : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] → {𝒜 : ι → σ} → [inst_5 : GradedRing 𝒜] → Inhabited (HomogeneousIdeal 𝒜)
-- Mathlib.Order.SupIndep
iSupIndep_def'' : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.restrictedYonedaObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  {X Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).map f = TypeCat.ofHom fun u => u.map₂ f.unop.left ⋯
-- Std.Time.Date.Unit.Weekday
_private.Std.Time.Date.Unit.Weekday.0.Std.Time.Weekday.toOrdinal.eq_2 : Std.Time.Weekday.tuesday.toOrdinal = 2
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- Constructor for morphisms from `mapBifunctorMapObj F p X Y k`.  -/
CategoryTheory.GradedObject.mapBifunctorMapObjDesc : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    {p : I × J → K} →
                      {X : CategoryTheory.GradedObject I C₁} →
                        {Y : CategoryTheory.GradedObject J C₂} →
                          {A : C₃} →
                            {k : K} →
                              [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] →
                                ((i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) →
                                  (CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k ⟶ A)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.brecOn.eq : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {motive : Turing.TM2.Stmt Γ Λ σ → Sort u}
  (t : Turing.TM2.Stmt Γ Λ σ) (F_1 : (t : Turing.TM2.Stmt Γ Λ σ) → Turing.TM2.Stmt.below t → motive t),
  Turing.TM2.Stmt.brecOn t F_1 = F_1 t (Turing.TM2.Stmt.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- If `J` is a precoverage on `D`, we obtain a precoverage on `C` by declaring a presieve on `D`
to be covering if its image under `F` is.  -/
CategoryTheory.Precoverage.comap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Functor C D → CategoryTheory.Precoverage D → CategoryTheory.Precoverage C
-- Mathlib.GroupTheory.Complement
Subgroup.LeftTransversal.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.LeftTransversal = { S // Subgroup.IsComplement S ↑H }
-- Mathlib.AlgebraicGeometry.Fiber
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton`. -/
AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] (y : ↥Y), IsCompact (⇑f ⁻¹' {y})
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  s.toKaroubiNondegComplexIsoN₁.hom.f.f n =
    CategoryTheory.CategoryStruct.comp
      ((s.cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (AlgebraicTopology.DoldKan.PInfty.f n)
-- Init.Data.Ord.SInt
Int8.instTransOrd : Std.TransOrd Int8
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The image of an `AddSubmonoid` along an `AddMonoidHom` is an `AddSubmonoid`.  -/
AddSubmonoid.map : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {F : Type u_4} → [inst_2 : FunLike F M N] → [mc : AddMonoidHomClass F M N] → F → AddSubmonoid M → AddSubmonoid N
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaUncurry_apply : ∀ {ι : Type v} [inst : DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w}
  [inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j)
  (i : ι) (j : α i), (DirectSum.sigmaUncurry f) ⟨i, j⟩ = (f i) j
-- Lean.Parser.Basic
Lean.Parser.checkColGeFn : String → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_id_eq_coev : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A X : C)
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.MonoidalClosed.curry
      (CategoryTheory.CategoryStruct.id
        (CategoryTheory.MonoidalCategoryStruct.tensorObj A ((CategoryTheory.Functor.id C).obj X))) =
    (CategoryTheory.ihom.coev A).app X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insertMany_list : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    (∀ a ∈ m, (List.map Sigma.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (numNewEqs : ℕ),
  sizeOf { mvarId := mvarId, subst := subst, numNewEqs := numNewEqs } =
    1 + sizeOf mvarId + sizeOf subst + sizeOf numNewEqs
-- Init.Data.Int.OfNat
Int.Nonneg.add : ∀ (a b : ℤ), a ≥ 0 → b ≥ 0 → a + b ≥ 0
-- Init.WF
InvImage.accAux : ∀ {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {b : β}, Acc r b → ∀ (x : α), f x = b → Acc (InvImage r f) x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, deriv f y` equals `f b - f a`.  -/
intervalIntegral.integral_deriv_of_contDiffOn_Icc : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E],
  ContDiffOn ℝ 1 f (Set.Icc a b) → a ≤ b → ∫ (x : ℝ) in a..b, deriv f x = f b - f a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → (Std.TreeMap.Raw.ofList l cmp).getD k' fallback = v
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- The Jacobi sum of twice the trivial multiplicative character on a finite field `F`
equals `#F-2`.  -/
jacobiSum_trivial_trivial : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R],
  jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = ↑(Fintype.card F) - 2
-- Mathlib.Data.W.Constructions
/-- The arities of each constructor for lists, `nil` takes no arguments, `cons hd` takes one  -/
WType.Listβ : (γ : Type u) → WType.Listα γ → Type u
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0.step.match_1.eq_2 : ∀ {Γ : Type u_1} (motive : Turing.TM0.Stmt Γ → Sort u_2) (a : Γ)
  (h_1 : (d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) (h_2 : (a : Γ) → motive (Turing.TM0.Stmt.write a)),
  (match Turing.TM0.Stmt.write a with
    | Turing.TM0.Stmt.move d => h_1 d
    | Turing.TM0.Stmt.write a => h_2 a) =
    h_2 a
-- Init.Data.List.Find
List.find?_filter : ∀ {α : Type u_1} {xs : List α} {p q : α → Bool},
  List.find? q (List.filter p xs) = List.find? (fun a => decide (p a = true ∧ q a = true)) xs
-- Mathlib.Topology.Category.Compactum
Compactum.str_hom_commute : ∀ (X Y : Compactum) (f : X ⟶ Y) (xs : Ultrafilter X.A),
  (CategoryTheory.ConcreteCategory.hom f) (X.str xs) =
    Y.str (Ultrafilter.map (⇑(CategoryTheory.ConcreteCategory.hom f)) xs)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The functor which sends `S : SnakeInput C` to `S.L₁'` which is
`S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.functorL₁' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex.SnakeInput C) (CategoryTheory.ShortComplex C)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instIsScalarTowerOfReal : ∀ {R : Type u_1} {S : Type u_2} [inst : SMul R S] [inst_1 : SMul R ℝ] [inst_2 : SMul S ℝ] [IsScalarTower R S ℝ],
  IsScalarTower R S ℂ
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_inf : ∀ {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : SemilatticeInf M] (f g : α → M),
  (Function.mulSupport fun x => f x ⊓ g x) ⊆ Function.mulSupport f ∪ Function.mulSupport g
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IsCharP` instance for `type` if available.  -/
Lean.Meta.Grind.Arith.Linear.Struct.charInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option (Lean.Expr × ℕ)
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.transportStruct_tensorObj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D) (X Y : D),
  CategoryTheory.MonoidalCategoryStruct.tensorObj X Y =
    e.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (e.inverse.obj X) (e.inverse.obj Y))
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.bucket : {α : Type u} →
  {β : α → Type v} →
    [Hashable α] →
      (self : Array (Std.DHashMap.Internal.AssocList α β)) → 0 < self.size → α → Std.DHashMap.Internal.AssocList α β
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_pure_pure : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Filter.Tendsto f (pure a) (pure (f a))
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.link.eq_def : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
  (hr : r.Balanced),
  Std.DTreeMap.Internal.Impl.link k v l r hl hr =
    match l, hl with
    | Std.DTreeMap.Internal.Impl.leaf, hl =>
      let d := Std.DTreeMap.Internal.Impl.insertMin k v r ⋯;
      { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }
    | Std.DTreeMap.Internal.Impl.inner szl k' v' l' r', hl =>
      match r, hr with
      | Std.DTreeMap.Internal.Impl.leaf, hr =>
        let d := Std.DTreeMap.Internal.Impl.insertMax k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') ⋯;
        { impl := d.impl, balanced_impl := ⋯, size_impl := ⋯ }
      | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr =>
        if h₁ : Std.DTreeMap.Internal.delta * szl < szr then
          match Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r') l'' ⋯ ⋯ with
          | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
            { impl := Std.DTreeMap.Internal.Impl.balanceLErase k'' v'' ℓ r'' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
        else
          if h₂ : Std.DTreeMap.Internal.delta * szr < szl then
            match Std.DTreeMap.Internal.Impl.link k v r' (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') ⋯ ⋯ with
            | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
              { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
          else
            {
              impl :=
                Std.DTreeMap.Internal.Impl.inner (szl + 1 + szr) k v (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r')
                  (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r''),
              balanced_impl := ⋯, size_impl := ⋯ }
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.Entry.global : {α : Type} → α → Lean.ScopedEnvExtension.Entry α
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.underEquivOfIsTerminal_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.underEquivOfIsTerminal.{w, v_1, u_1} X h).functor =
    CategoryTheory.Functor.star (CategoryTheory.Under X)
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.Grind.elabConfigItems : Lean.Grind.Config → Array Lean.Syntax → Lean.Elab.TermElabM Lean.Grind.Config
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_eq_getD_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β},
  Std.DHashMap.Const.getD m a fallback = (Std.DHashMap.Const.get? m a).getD fallback
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.mk.inj : ∀ {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)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {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)}
  {pullHom'_hom_self :
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj i))}
  {pullHom'_hom_comp :
    ∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
            ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯
            ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯}
  {obj_1 : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  {hom_1 :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj_1 i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj_1 j)}
  {pullHom'_hom_self_1 :
    ∀ (i : ι),
      CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (f i) (CategoryTheory.CategoryStruct.id (X i))
          (CategoryTheory.CategoryStruct.id (X i)) ⋯ ⋯ =
        CategoryTheory.CategoryStruct.id
          ((F.map (CategoryTheory.CategoryStruct.id (X i)).op.toLoc).toFunctor.obj (obj_1 i))}
  {pullHom'_hom_comp_1 :
    ∀ (i₁ i₂ i₃ : ι),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂
            ⋯ ⋯)
          (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃
            ⋯ ⋯) =
        CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom_1 (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯
          ⋯},
  { obj := obj, hom := hom, pullHom'_hom_self := pullHom'_hom_self, pullHom'_hom_comp := pullHom'_hom_comp } =
      { obj := obj_1, hom := hom_1, pullHom'_hom_self := pullHom'_hom_self_1,
        pullHom'_hom_comp := pullHom'_hom_comp_1 } →
    obj = obj_1 ∧ hom ≍ hom_1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.IsReducedRowEchelon.eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] [inst_3 : One R]
  {A : Matrix m n R}, A.IsReducedRowEchelon → ∀ ⦃i₁ i₂ : m⦄ ⦃c : n⦄, i₁ < i₂ → A.IsLeadingEntry i₂ c → A i₁ c = 0
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.RootOrdered.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (x_1 : α) →
        ((x : α) → motive RBTree.RBNode.Path.root x) →
          ((c : RBTree.RBColor) →
              (parent : RBTree.RBNode.Path α) →
                (x : α) → (r : RBTree.RBNode α) → (v : α) → motive (RBTree.RBNode.Path.left c parent x r) v) →
            ((c : RBTree.RBColor) →
                (l : RBTree.RBNode α) →
                  (x : α) →
                    (parent : RBTree.RBNode.Path α) → (v : α) → motive (RBTree.RBNode.Path.right c l x parent) v) →
              motive x x_1
-- Mathlib.Tactic.ApplyWith
/-- A configuration with at least one configuration option.

In comparison, `optConfig` allows zero or more options.
 -/
Mathlib.Tactic.manyConfig : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_apply_le_zero_of_ne : ∀ (n : ℕ) (i j : Fin n), i ≠ j → CartanMatrix.A n i j ≤ 0
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_nonempty`. -/
Set.diff_nonempty : ∀ {α : Type u_1} {s t : Set α}, (s \ t).Nonempty ↔ ¬s ⊆ t
-- Mathlib.Tactic.FieldSimp
/-- Given `l : qNF M`, obtain `l' : qNF M` by removing all `l`'s exponent-zero entries where the
corresponding atom can be proved nonzero, and construct a proof that their associated expressions
are equal.  -/
Mathlib.Tactic.FieldSimp.qNF.removeZeros : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      (iM : Q(CommGroupWithZero «$M»)) →
        (l : Mathlib.Tactic.FieldSimp.qNF M) →
          Lean.MetaM
            ((l' : Mathlib.Tactic.FieldSimp.qNF M) ×
              have a := l'.toNF;
              have a_1 := l.toNF;
              Q(«$a_1».eval = «$a».eval))
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.instOrderBot : {X : Type u_1} →
  {R : Type u_2} →
    [inst : AddCommMonoid R] → [inst_1 : LinearOrder R] → [AddLeftStrictMono R] → OrderBot (PseudoMetric X R)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C), CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁.app T = T.mor₃
-- Mathlib.Algebra.Ring.Subring.Defs
/-- Two subrings are equal if they have the same elements.  -/
Subring.ext : ∀ {R : Type u} [inst : NonAssocRing R] {S T : Subring R}, (∀ (x : R), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.Analysis.Complex.Norm
Complex.nndist_of_im_eq : ∀ {z w : ℂ}, z.im = w.im → nndist z w = nndist z.re w.re
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isCtorIdxHasNotBit? : Lean.Expr → Option Lean.FVarId
-- Mathlib.Order.Filter.Map
Filter.eventuallyEq_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ},
  g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_eventually_congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  s =ᶠ[nhds x] t → fderivWithin 𝕜 f s =ᶠ[nhds x] fderivWithin 𝕜 f t
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (curr : ℕ) → curr ≤ w → aig.Ref → aig.RefVec w → aig.RefVec w → aig.RefVec curr → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance to a set (as `ℝ≥0`) is uniformly continuous in point  -/
Metric.uniformContinuous_infNndist_pt : ∀ {α : Type u} [inst : PseudoMetricSpace α] (s : Set α), UniformContinuous fun x => Metric.infNndist x s
-- Mathlib.Data.PNat.Prime
PNat.Coprime.pow : ∀ {m n : ℕ+} (k l : ℕ), m.Coprime n → (↑m ^ k).Coprime (↑n ^ l)
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
/-- The equivalence between `Finset.finsuppAntidiag s n` and the subtype of `s →₀ μ` whose sum is
`n`.  -/
Finset.finsuppAntidiagEquivSubtype : {ι : Type u_1} →
  {μ : Type u_2} →
    [inst : DecidableEq ι] →
      [inst_1 : AddCommMonoid μ] →
        [inst_2 : Finset.HasAntidiagonal μ] →
          [inst_3 : DecidableEq μ] →
            (s : Finset ι) → (n : μ) → ↥(s.finsuppAntidiag n) ≃ { P // (P.sum fun x => id) = n }
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.of_ringEquiv : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] (e : K ≃+* L) [NumberField K], NumberField L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Tactic.Widget.Conv
/-- Given an `e : Expr` and `pos : SubExpr.Pos`, `Path.ofSubExprPosArray expr pos.toArray` generates
the `Path` corresponding to traversing `pos` starting at the reference expression `e`.
 -/
_private.Mathlib.Tactic.Widget.Conv.0.Mathlib.Tactic.Conv.Path.ofSubExprPosArray : Lean.Expr → Array ℕ → Lean.MetaM Mathlib.Tactic.Conv.Path
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.eAdj_comm : ∀ {α : Type u_1} {H : Hypergraph α} (e f : Set α), H.EAdj e f ↔ H.EAdj f e
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.eq_2 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α) (n : ℕ),
  MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i n.succ =
    MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n),
            have this := ⋯;
            MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i k)
-- Mathlib.Logic.Encodable.Pi
/-- If `α` is encodable, then so is `Fin n → α`.  -/
Encodable.finArrow : {α : Type u_1} → [Encodable α] → {n : ℕ} → Encodable (Fin n → α)
-- Init.Data.String.Basic
String.Slice.utf8ByteSize_slice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.slice newStart newEnd h).utf8ByteSize = newStart.offset.byteDistance newEnd.offset
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprPort : Repr Std.Http.URI.Port
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousComponent_C_mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) (r : R),
  (MvPolynomial.homogeneousComponent n) (MvPolynomial.C r * φ) =
    MvPolynomial.C r * (MvPolynomial.homogeneousComponent n) φ
-- Init.Control.Lawful.MonadAttach.Lemmas
Classical.ofNonempty.congr_simp : ∀ {α : Sort u} [inst : Nonempty α], Classical.ofNonempty = Classical.ofNonempty
-- Init.Data.Vector.Lemmas
_private.Init.Data.Vector.Lemmas.0.Array.isPrefixOf.eq_1 : ∀ {α : Type u} [inst : BEq α] (as bs : Array α),
  as.isPrefixOf bs = if h : as.size ≤ bs.size then as.isPrefixOfAux bs h 0 else false