mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.instNonemptyIsoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty],
  P.isoClosure.Nonempty
-- Init.Data.BitVec.Lemmas
BitVec.sub_eq_xor : ∀ {a b : BitVec 1}, a - b = a ^^^ b
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNatCast : {R : Type u_1} → [NatCast R] → NatCast Rᵃᵒᵖ
-- Lean.EnvExtension
Lean.TagDeclarationExtension.tag : Lean.TagDeclarationExtension → Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ico_union_Ici' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c ≤ b → Set.Ico a b ∪ Set.Ici c = Set.Ici (min a c)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.image_closedBall_subset_compact : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : TopologicalSpace M₂]
  [inst_4 : AddCommMonoid M₂] [inst_5 : NormedSpace 𝕜₁ M₁] [inst_6 : Module 𝕜₂ M₂] [ContinuousConstSMul 𝕜₂ M₂]
  {f : M₁ →ₛₗ[σ₁₂] M₂}, IsCompactOperator ⇑f → ∀ (r : ℝ), ∃ K, IsCompact K ∧ ⇑f '' Metric.closedBall 0 r ⊆ K
-- Lean.Elab.Tactic.Grind.Basic
_private.Lean.Elab.Tactic.Grind.Basic.0.Lean.Elab.Tactic.Grind.evalGrindTactic.handleEx : Lean.Elab.Tactic.Grind.SavedState →
  Array Lean.Elab.Tactic.Grind.EvalTacticFailure →
    Lean.Exception →
      (Array Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Elab.Tactic.Grind.GrindTacticM Unit) →
        Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Algebra.Group.Defs
SubtractionMonoid.toSubNegMonoid : {G : Type u} → [self : SubtractionMonoid G] → SubNegMonoid G
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.GradedNatTrans.mk : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {A : CategoryTheory.Center V} →
                {F G : CategoryTheory.EnrichedFunctor V C D} →
                  (app : (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X) →
                    (∀ (X Y : C),
                        CategoryTheory.CategoryStruct.comp (A.snd.β (X ⟶[V] Y)).hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map X Y) (app Y))
                              (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom (app X) (G.map X Y))
                            (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))) →
                      CategoryTheory.GradedNatTrans A F G
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_mul_one_le : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atTop → (∀ (x : α), 1 ≤ g x) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_eq_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α} {h : a ∈ m}, Std.DHashMap.Raw.Const.get m a h = Std.DHashMap.Raw.Const.get! m a
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition of a continuous function `f` with compact support with another continuous function
`g` sending `0` to `0` from the left yields another continuous function `g ∘ f` with compact
support.

If `g` doesn't send `0` to `0`, `f.compLeft g` defaults to `0`.  -/
CompactlySupportedContinuousMap.compLeft : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {γ : Type u_5} →
            [inst_3 : TopologicalSpace γ] →
              [inst_4 : Zero γ] → C(β, γ) → CompactlySupportedContinuousMap α β → CompactlySupportedContinuousMap α γ
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.nndist_eq : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F) (x y : α), nndist (f x) (f y) = nndist x y
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_refl : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x : X ⊕ Y}, f ∈ GromovHausdorff.candidates X Y → f (x, x) = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.size_eq_zero : ∀ {α : Type u_1} {t : Ordnode α}, t.Sized → (t.size = 0 ↔ t = Ordnode.nil)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toEquiv : α ≃ β)
  (measurable_toFun : autoParam (Measurable ⇑toEquiv) MeasurableEquiv.measurable_toFun._autoParam)
  (measurable_invFun : autoParam (Measurable ⇑toEquiv.symm) MeasurableEquiv.measurable_invFun._autoParam),
  sizeOf { toEquiv := toEquiv, measurable_toFun := measurable_toFun, measurable_invFun := measurable_invFun } =
    1 + sizeOf toEquiv
-- Mathlib.NumberTheory.LSeries.Dirichlet
LSeries.convolution_one_eq_convolution_zeta : ∀ {R : Type u_1} [inst : Semiring R] (f : ℕ → R),
  LSeries.convolution f 1 = LSeries.convolution f fun x => ↑(ArithmeticFunction.zeta x)
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderSubobjectsIsZeroOfHasZeroMorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ObjectProperty.IsClosedUnderSubobjects CategoryTheory.Limits.IsZero
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.zero_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [inst : MulZeroClass α], Matrix.hadamard 0 A = 0
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.brecOn.go : {motive : Turing.PartrecToTM2.Λ' → Sort u} →
  (t : Turing.PartrecToTM2.Λ') →
    ((t : Turing.PartrecToTM2.Λ') → Turing.PartrecToTM2.Λ'.below t → motive t) →
      motive t ×' Turing.PartrecToTM2.Λ'.below t
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sInter_subset_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (S : Set (Set α)) (t : Set β),
  Set.image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, Set.image2 f s t
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.mono : ∀ {G : Type u_1} {β : Type u_5} [inst : Monoid G] {x : G} [inst_1 : Monoid β] {y : β},
  IsOfFinOrder x → orderOf y ∣ orderOf x → IsOfFinOrder y
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Abelian C]
  (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [inst_2 : e₁.IsTruncLE]
  [inst_3 : e₂.IsTruncGE] (ac : e₁.AreComplementary e₂), QuasiIso (K.shortComplexTruncLEX₃ToTruncGE ac)
-- Init.Data.Sum.Lemmas
Sum.isLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (val : α), (Sum.inl val).isLeft = true
-- Mathlib.Topology.DiscreteQuotient
/-- For every point `x`, the set `{ y | Rel x y }` is an open set.  -/
DiscreteQuotient.isOpen_setOfPred_rel : ∀ {X : Type u_5} [inst : TopologicalSpace X] (self : DiscreteQuotient X) (x : X), IsOpen (Set.ofPred (self.toSetoid x))
-- Init.Data.Int.Order
Int.mul.eq_3 : ∀ (m_2 n_2 : ℕ), (Int.negSucc m_2).mul (Int.ofNat n_2) = Int.negOfNat (m_2.succ * n_2)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_left_iff : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α],
  IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `contMDiffAt_iff_localFrameCoeff`.

---

A section `s` of `V` is `C^k` at `x ∈ e.baseSet` iff each of its
coefficients `(LinearMap.piApply (b.localFrameCoeff e i) s)` in a local frame near `x` is  -/
contMDiffAt_iff_localFrame_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {k : WithTop ℕ∞}
  {x' : M} [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜] [ContMDiffVectorBundle k F V I],
  x' ∈ e.baseSet →
    (ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) k (fun x => ⟨x, s x⟩) x' ↔
      ∀ (i : ι),
        ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) k
          ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s) x')
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β),
  CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h = CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h
-- Mathlib.RingTheory.QuotSMulTop
/-- If `M'` is isomorphic to `M''` as `R`-modules, then `M'⧸rM'` is isomorphic to `M''⧸rM''`.  -/
QuotSMulTop.congr : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      {M' : Type u_3} →
        {M'' : Type u_4} →
          [inst_1 : AddCommGroup M'] →
            [inst_2 : Module R M'] →
              [inst_3 : AddCommGroup M''] →
                [inst_4 : Module R M''] → (M' ≃ₗ[R] M'') → QuotSMulTop r M' ≃ₗ[R] QuotSMulTop r M''
-- Mathlib.Data.Subtype
Subtype.equivalence : ∀ {α : Sort u_1} [inst : Setoid α] (p : α → Prop), Equivalence HasEquiv.Equiv
-- Lean.Meta.Tactic.SolveByElim
/-- Create or modify a `SolveByElimConfig` which calls `intro` on any goal for which no lemma applies.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.introsAfter : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } → Lean.Meta.SolveByElim.SolveByElimConfig
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero : ¬DifferentiableWithinAt ℝ InformationTheory.klFun (Set.Ioi 0) 0
-- Init.Data.Format.Basic
Std.Format.group.sizeOf_spec : ∀ (a : Std.Format) (behavior : optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone),
  sizeOf (a.group behavior) = 1 + sizeOf a + sizeOf behavior
-- Mathlib.Topology.Neighborhoods
IsOpen.closure_inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → closure s ∩ t ⊆ closure (s ∩ t)
-- Mathlib.GroupTheory.Perm.List
List.mem_of_formPerm_apply_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {x : α}, l.formPerm x ≠ x → x ∈ l
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff! m₂) k = none
-- Mathlib.Order.Filter.Map
Filter.map_bind : ∀ {γ : Type u_3} {α : Type u_6} {β : Type u_7} (m : β → γ) (f : Filter α) (g : α → Filter β),
  Filter.map m (f.bind g) = f.bind (Filter.map m ∘ g)
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.invOf : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S}
  [inst_3 : Invertible x], IsAlgebraic R x → IsAlgebraic R ⅟x
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.mul_def : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e e' : E ≃ₗᵢ[R] E), e * e' = e'.trans e
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The canonical multilinear map on `R^ι` when `ι` is finite, associating to `m` the product of
all the `m i` (multiplied by a fixed reference element `z` in the target module). See also
`mkPiAlgebra` for a more general version.  -/
MultilinearMap.mkPiRing : (R : Type uR) →
  (ι : Type uι) →
    {M₂ : Type v₂} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₂] → [inst_2 : Module R M₂] → [Fintype ι] → M₂ → MultilinearMap R (fun x => R) M₂
-- Mathlib.Data.List.Basic
List.tail_append_singleton_of_ne_nil : ∀ {α : Type u} {a : α} {l : List α}, l ≠ [] → (l ++ [a]).tail = l.tail ++ [a]
-- Init.Data.UInt.Lemmas
USize.ofNatLT_mod : ∀ {a b : ℕ} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits),
  USize.ofNatLT (a % b) ⋯ = USize.ofNatLT a ha % USize.ofNatLT b hb
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.mk.sizeOf_spec : ∀ (toIndGroupInfo : Lean.Elab.Structural.IndGroupInfo) (levels : List Lean.Level) (params : Array Lean.Expr),
  sizeOf { toIndGroupInfo := toIndGroupInfo, levels := levels, params := params } =
    1 + sizeOf toIndGroupInfo + sizeOf levels + sizeOf params
-- Mathlib.Analysis.LocallyConvex.Separation
/-- If `s` and `t` are convex, `interior s` is nonempty and disjoint from `t`, then a continuous
linear functional weakly separates `s` and `t`. If `t` is nonempty, this follows from
`geometric_hahn_banach_of_nonempty_interior`; if `t = ∅`, the zero functional works.  -/
geometric_hahn_banach_of_nonempty_interior' : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E],
  Convex ℝ s →
    Convex ℝ t → Disjoint (interior s) t → (interior s).Nonempty → ∃ f u, (∀ a ∈ s, f a ≤ u) ∧ ∀ b ∈ t, u ≤ f b
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.prod.fst.match_1.splitter : (motive : (x : ℕ) → TypeVec.{u_1} x → TypeVec.{u_1} x → Fin2 x → Sort u_2) →
  (x : ℕ) →
    (x_1 x_2 : TypeVec.{u_1} x) →
      (x_3 : Fin2 x) →
        ((n : ℕ) → (α β : TypeVec.{u_1} n.succ) → (i : Fin2 n) → motive n.succ α β i.fs) →
          ((n : ℕ) → (x x_4 : TypeVec.{u_1} n.succ) → motive n.succ x x_4 Fin2.fz) → motive x x_1 x_2 x_3
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (F.map h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom) h_1) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
            h_1)))
-- Mathlib.Data.Set.Sigma
Set.singleton_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} {i : ι}, {i}.sigma t = Sigma.mk i '' t i
-- Mathlib.Data.PNat.Basic
PNat.add_one_le_iff : ∀ {a b : ℕ+}, a + 1 ≤ b ↔ a < b
-- Mathlib.Topology.EMetricSpace.Pi
edist_pi_le_iff : ∀ {β : Type v} {X : β → Type u_2} [inst : Fintype β] [inst_1 : (b : β) → EDist (X b)] {f g : (b : β) → X b}
  {d : ENNReal}, edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.min?.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (v : α) (r : RBTree.RBNode α)
  (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (c : RBTree.RBColor) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c RBTree.RBNode.nil v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c RBTree.RBNode.nil v r with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c RBTree.RBNode.nil v r => h_2 c v r
    | RBTree.RBNode.node c l v r => h_3 c l v r) =
    h_2 c v r
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_eq_iff : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} {p : Fin (n + 1)} {a : α p} {f : (i : Fin n) → α (p.succAbove i)}
  {g : (j : Fin (n + 1)) → α j}, p.insertNth a f = g ↔ a = g p ∧ f = p.removeNth g
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree
-- Mathlib.Data.Finset.Lattice.Basic
/-- `s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`.  -/
Finset.instInter : {α : Type u_1} → [DecidableEq α] → Inter (Finset α)
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsAntitoneBasis.mk : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {s'' : ι'' → Set α},
  Filter.IsBasis (fun x => True) s'' → Antitone s'' → Filter.IsAntitoneBasis s''
-- Mathlib.Data.Matrix.Mul
Matrix.instRing : {n : Type u_3} → {α : Type v} → [Fintype n] → [DecidableEq n] → [Ring α] → Ring (Matrix n n α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul.go.eq_def : ∀ (p₂ p₁ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mul.go p₂ p₁ acc =
    match p₁ with
    | Lean.Grind.CommRing.Poly.num k => acc.combine (Lean.Grind.CommRing.Poly.mulConst k p₂)
    | Lean.Grind.CommRing.Poly.add k m p₁ =>
      Lean.Grind.CommRing.Poly.mul.go p₂ p₁ (acc.combine (Lean.Grind.CommRing.Poly.mulMon k m p₂))
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.iInter_of_cof_le_one : ∀ {α : Type v} [inst : LinearOrder α] {ι : Type u_1} {f : ι → Set α},
  Order.cof α ≤ 1 → (∀ (i : ι), IsClub (f i)) → IsClub (⋂ i, f i)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
HasMFDerivAt.add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f g : M → E'} {f' g' : TangentSpace I z →L[𝕜] E'},
  HasMFDerivAt% f z f' → HasMFDerivAt% g z g' → HasMFDerivAt% (f + g) z (f' + g')
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.leftHomologyMap'_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) (a : R),
  CategoryTheory.ShortComplex.leftHomologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.eventually_atBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α],
  (∀ᶠ (x : α) in Filter.atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b
-- Init.Data.Nat.Lemmas
Nat.mul_add_div : ∀ {m : ℕ}, m > 0 → ∀ (x y : ℕ), (m * x + y) / m = x + y / m
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinLM_eq_setIntegral : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.IntegrableOn φ (↑K) μ →
    ∀ {f : ContDiffMapSupportedIn E F₁ n K},
      (ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ) f = ∫ (x : E) in ↑K, (B (f x)) (φ x) ∂μ
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- Deleting the incidence set of the vertex `x` retains the same number of edges as in the induced
subgraph of the vertices `{x}ᶜ`.  -/
SimpleGraph.card_edgeFinset_induce_compl_singleton : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (x : V),
  (SimpleGraph.induce {x}ᶜ G).edgeFinset.card = (G.deleteIncidenceSet x).edgeFinset.card
-- Std.Data.ExtTreeMap.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.ExtTreeMap.valuesArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → Array β
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.integrable_martingalePart : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0} [CompleteSpace E],
  (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) →
    ∀ (n : ℕ), MeasureTheory.Integrable (MeasureTheory.martingalePart f ℱ μ n) μ
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.pre_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.pre F E)
      (CategoryTheory.Limits.limit.π (E.comp F) k) =
    CategoryTheory.Limits.limit.π F (E.obj k)
-- Mathlib.Algebra.Group.Shrink
equivShrink_inv : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Inv α] (x : α), (equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹