mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.length_le : ∀ {n : ℕ} (c : OrderedFinpartition n), c.length ≤ n
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.splitter : {n : ℕ} →
  (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1) →
    (x : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      ((c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c))) →
        (Unit → motive (some none)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax left unity.  -/
CategoryTheory.OplaxFunctor.map₂_leftUnitor_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : self.obj a ⟶ self.obj b} (h : self.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom) h =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.id a) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom h))
-- Mathlib.Algebra.Ring.Prod
NonUnitalRingHom.prod_comp_prodMap : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [inst : NonUnitalNonAssocSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring S] [inst_2 : NonUnitalNonAssocSemiring R'] [inst_3 : NonUnitalNonAssocSemiring S']
  [inst_4 : NonUnitalNonAssocSemiring T] (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S'),
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Mathlib.Order.Filter.SmallSets
Filter.eventually_smallSets_forall : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop}, (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x
-- Init.Data.List.Monadic
List.filterMapM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α),
  List.filterMapM f as = List.filterMapM.loop f as []
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.iIndepFun.integral_fun_prod_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3}
  [inst_1 : Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i}
  {f : (i : ι) → 𝓧 i → 𝕜},
  ProbabilityTheory.iIndepFun X μ →
    (∀ (i : ι), AEMeasurable (X i) μ) →
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) (MeasureTheory.Measure.map (X i) μ)) →
        ∫ (ω : Ω), ∏ i, f i (X i ω) ∂μ = ∏ i, ∫ (ω : Ω), f i (X i ω) ∂μ
-- Init.Control.Lawful.Instances
EStateM.map.eq_1 : ∀ {ε σ α β : Type u} (f : α → β) (x : EStateM ε σ α) (s : σ),
  EStateM.map f x s =
    match x s with
    | EStateM.Result.ok a s => EStateM.Result.ok (f a) s
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_exchange_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g) h)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : AddZero P] (g : N →+ P)
  (f : M →+ N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Logic.Equiv.Defs
Equiv.surjective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Surjective ⇑e
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.instIsIsoH₀Hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀), CategoryTheory.IsIso (e.hom.h₀ i)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited CategoryTheory.Limits.WalkingPair
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  s₂ ⊆ s₁ →
    MeasurableSet s₂ →
      autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_sdiff._auto_1 → μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitInv_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : C} (f : Y ⟶ X) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inverse.map (e.functor.map f))
      (CategoryTheory.CategoryStruct.comp (e.unitInv.app X) h) =
    CategoryTheory.CategoryStruct.comp (e.unitInv.app Y) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `zero_apply`. -/
Seminorm.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Init.Data.Vector.Erase
Vector.eraseIdx_cast : ∀ {α : Type u_1} {n m : ℕ} {w : n = m} {xs : Vector α n} {k : ℕ} (h : k < m),
  (Vector.cast w xs).eraseIdx k h = Vector.cast ⋯ (xs.eraseIdx k ⋯)
-- Mathlib.Algebra.Homology.HomologySequence
/-- If `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` is an exact sequence of homological complexes, then
`X₁.opcycles i ⟶ X₂.opcycles i ⟶ X₃.opcycles i ⟶ 0` is exact. This lemma states
the exactness at `X₂.opcycles i`, while the fact that `X₂.opcycles i ⟶ X₃.opcycles i`
is an epi is an instance.  -/
HomologicalComplex.opcycles_right_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)),
  S.Exact →
    ∀ [CategoryTheory.Epi S.g] (i : ι) [inst_3 : S.X₁.HasHomology i] [inst_4 : S.X₂.HasHomology i]
      [inst_5 : S.X₃.HasHomology i],
      { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := HomologicalComplex.opcyclesMap S.f i,
          g := HomologicalComplex.opcyclesMap S.g i, zero := ⋯ }.Exact
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) → [mon : CategoryTheory.MonObj X] → [comm : CategoryTheory.IsCommMonObj X] → CategoryTheory.CommMon C
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.fst_prod : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f : ρ.IntertwiningMap σ) (g : ρ.IntertwiningMap τ),
  (Representation.IntertwiningMap.fst A σ τ).comp (f.prod g) = f
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_mk : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {s : Finset (BoxIntegral.Box ι)} {h₁ : ∀ J ∈ s, J ≤ I}
  {h₂ : (↑s).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)},
  J ∈ { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ } ↔ J ∈ s
-- Init.Data.String.Basic
String.Slice.toByteArray_copy : ∀ {s : String.Slice},
  s.copy.toByteArray = s.str.toByteArray.extract s.startInclusive.offset.byteIdx s.endExclusive.offset.byteIdx
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- The closure of a singleton `{a}` in the upper set topology is the right-closed left-infinite
interval $(-∞,a]$.
 -/
Topology.IsUpperSet.closure_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] {a : α},
  closure {a} = Set.Iic a
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasTensorXTensorUnit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C] {I : Type u_2}
  [inst_4 : AddMonoid I] {c : ComplexShape I} (K : HomologicalComplex C c) [inst_5 : DecidableEq I]
  [∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)],
  CategoryTheory.GradedObject.HasTensor (HomologicalComplex.tensorUnit C c).X K.X
-- Batteries.Data.List.Count
List.count_concat : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (a : α) (l : List α), List.count a (l.concat a) = List.count a l + 1
-- Mathlib.Data.Real.Basic
Real.cauchy_nnratCast : ∀ (q : ℚ≥0), (↑q).cauchy = ↑q
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.of_preimage_eq_empty : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} (I : Type u_3)
  [inst_2 : TopologicalSpace I] [IsEmpty I] {x : X} {U : Set X}, U ∈ nhds x → f ⁻¹' U = ∅ → IsEvenlyCovered f x I
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalSemiring : {R : Type u_1} → [NonUnitalSemiring R] → NonUnitalSemiring Rᵐᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.egirth_le_length : ∀ {α : Type u_1} {G : SimpleGraph α} {a : α} {w : G.Walk a a}, w.IsCycle → G.egirth ≤ ↑w.length
-- Mathlib.Data.Countable.Defs
not_uncountable : ∀ {α : Sort u} [Countable α], ¬Uncountable α
-- Lean.Meta.LazyDiscrTree
/-- Following matches based on key of trie.  -/
Lean.Meta.LazyDiscrTree.Trie.children : {α : Type} → Lean.Meta.LazyDiscrTree.Trie α → Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} (ι : Type v) (dim : ι → ℕ)
  (simplex : (s : ι) → X.obj (Opposite.op { len := dim s + 1 })) (index : (s : ι) → Fin (dim s + 2))
  (nonDegenerate₁ : ∀ (s : ι), simplex s ∈ X.nonDegenerate (dim s + 1))
  (nonDegenerate₂ :
    ∀ (s : ι),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) ∈
        X.nonDegenerate (dim s))
  (notMem₁ : ∀ (s : ι), simplex s ∉ A.obj (Opposite.op { len := dim s + 1 }))
  (notMem₂ :
    ∀ (s : ι),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) ∉
        A.obj (Opposite.op { len := dim s }))
  (injective_type₁' :
    ∀ {s t : ι}, { dim := dim s + 1, simplex := simplex s } = { dim := dim t + 1, simplex := simplex t } → s = t)
  (injective_type₂' :
    ∀ {s t : ι},
      { dim := dim s,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) } =
          { dim := dim t,
            simplex :=
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t))) (simplex t) } →
        s = t)
  (type₁_ne_type₂' :
    ∀ (s t : ι),
      { dim := dim s + 1, simplex := simplex s } ≠
        { dim := dim t,
          simplex :=
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index t))) (simplex t) })
  (surjective' :
    ∀ (x : A.N),
      ∃ s,
        x.toS = { dim := dim s + 1, simplex := simplex s } ∨
          x.toS =
            { dim := dim s,
              simplex :=
                (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X (index s))) (simplex s) }),
  sizeOf
      { ι := ι, dim := dim, simplex := simplex, index := index, nonDegenerate₁ := nonDegenerate₁,
        nonDegenerate₂ := nonDegenerate₂, notMem₁ := notMem₁, notMem₂ := notMem₂, injective_type₁' := injective_type₁',
        injective_type₂' := injective_type₂', type₁_ne_type₂' := type₁_ne_type₂', surjective' := surjective' } =
    1 + sizeOf ι
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The cocone itself  -/
CategoryTheory.Limits.ColimitCocone.cocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.ColimitCocone F → CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
orthonormal_subsingleton_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [Subsingleton ι] {v : ι → E}, Orthonormal 𝕜 v ↔ ∀ (i : ι), ‖v i‖ = 1
-- Mathlib.CategoryTheory.Limits.Final.Connected
CategoryTheory.final_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.IsConnected C], (CategoryTheory.Prod.snd C D).Final
-- Mathlib.GroupTheory.FiniteAbelian.Basic
/-- The **Structure theorem of finitely generated abelian groups** in a multiplicative version:
Any finitely generated abelian group is the product of a power of `ℤ`
and a direct product of some `ZMod (p i ^ e i)` for some prime powers `p i ^ e i`.  -/
CommGroup.equiv_free_prod_prod_multiplicative_zmod : ∀ (G : Type u_1) [inst : CommGroup G] [hG : Group.FG G],
  ∃ ι j x x p,
    ∃ (_ : ∀ (i : ι), Nat.Prime (p i)),
      ∃ e, Nonempty (G ≃* (j → Multiplicative ℤ) × ((i : ι) → Multiplicative (ZMod (p i ^ e i))))
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined on a complete space,
then it is automatically continuous.  -/
LinearMap.IsSymmetric.continuous : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → Continuous ⇑T
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The uniform structure induced by a family of seminorms is exactly the infimum of the ones
induced by each seminorm individually. We express this as a characterization of
`WithSeminorms p`.  -/
SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [u : UniformSpace E] [IsUniformAddGroup E] (p : SeminormFamily 𝕜 E ι),
  WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.DSimpCacheKey.mk : Lean.Name → Lean.Elab.Tactic.Grind.DSimpArgs → Lean.Elab.Tactic.Grind.DSimpCacheKey
-- Init.Data.String.Basic
String.sliceTo_toSlice : ∀ {s : String} {p : s.Pos}, s.toSlice.sliceTo p.toSlice = s.sliceTo p
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.toOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)),
  f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
/-- A "proxy type" equivalent to `CategoryTheory.Limits.WalkingMulticospan` that is constructed from `Unit`, `PLift`, `Sigma`, `Empty`, and `Sum`. See `CategoryTheory.Limits.WalkingMulticospan.proxyTypeEquiv` for the equivalence. (Generated by the `proxy_equiv%` elaborator.) -/
CategoryTheory.Limits.WalkingMulticospan.proxyType : CategoryTheory.Limits.MulticospanShape → Type (max w w')
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
IsNilpotent.isTopologicallyNilpotent : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : MonoidWithZero R] {a : R},
  IsNilpotent a → IsTopologicallyNilpotent a
-- Mathlib.Order.SuccPred.WithBot
/-- The successor of `a : WithBot α` as an element of `α`.  -/
WithBot.succ : {α : Type u_1} → [inst : Preorder α] → [OrderBot α] → [SuccOrder α] → WithBot α → α
-- Lean.CoreM
Lean.MonadDeclNameGenerator.getDeclNGen : {m : Type → Type} → [self : Lean.MonadDeclNameGenerator m] → m Lean.DeclNameGenerator
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.eq_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B},
  ¬IsIntegral A x → minpoly A x = 0
-- Mathlib.Logic.Function.Basic
/-- As a map from the left argument to a unary function, `f` is injective.  -/
Function.Injective2.left' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β → γ},
  Function.Injective2 f → ∀ [Nonempty β], Function.Injective f
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.ext : ∀ {X : Type u_3} {x y : FundamentalGroupoid X}, x.as = y.as → x = y
-- Mathlib.Algebra.Polynomial.Div
Polynomial.rootMultiplicity_eq_zero : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {x : R}, ¬p.IsRoot x → Polynomial.rootMultiplicity x p = 0
-- Mathlib.Logic.Equiv.Option
Equiv.some_removeNone_iff : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α}, some (e.removeNone x) = e none ↔ e.symm none = some x
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
CommCStarAlgebra.norm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCommCStarAlgebra A] {a b : A}, a * b = 0 → ‖a + b‖ = max ‖a‖ ‖b‖
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.ShiftSequence.shiftIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ),
  (CochainComplex.ShiftSequence.shiftIso C n a a' ha').inv.app K =
    CategoryTheory.ShortComplex.homologyMap ((CochainComplex.shiftShortComplexFunctorIso C n a a' ha').inv.app K)
-- Init.Data.Array.BinSearch
/-- Inserts an element `k` into a sorted array `as` such that the resulting array is sorted.

The ordering predicate `lt` should be a total order on elements, and the array `as` should be sorted
with respect to `lt`.

If an element that `lt` equates to `k` is already present in `as`, then `merge` is applied to the
existing element to determine the value of that position in the resulting array. If no element equal
to `k` is present, then `add` is used to determine the value to be inserted.
 -/
Array.binInsertM : {α : Type u} → {m : Type u → Type v} → [Monad m] → (α → α → Bool) → (α → m α) → (Unit → m α) → Array α → α → m (Array α)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₀_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder]
  {Z : HomologicalComplex C c} (h : K ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₀ K)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) h) =
    h
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- If a `GradedRingHom` is `R`-linear, then it is a `GradedAlgHom`.  -/
GradedAlgHom.mk' : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {ι : Type u_10} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : DecidableEq ι] →
                    [inst_6 : AddMonoid ι] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] →
                              (f : 𝒜 →+*ᵍ ℬ) → (∀ (c : R) (x : A), f (c • x) = c • f x) → 𝒜 →ₐᵍ[R] ℬ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.cellFrontier_subset_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ⊆ Topology.RelCWComplex.closedCell n i
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α}, Std.Internal.List.getKeyD (Std.Internal.List.minKey! l) l fallback = Std.Internal.List.minKey! l
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.truncLT_smul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] {V : Type u_8} [inst_1 : Zero V] [inst_2 : SMulZeroClass R V]
  [inst_3 : DecidableLT Γ] (c : Γ) (r : R) (x : HahnSeries Γ V),
  (HahnSeries.truncLT c) (r • x) = r • (HahnSeries.truncLT c) x
-- Mathlib.Analysis.Convex.Uniform
exists_forall_closed_ball_dist_add_le_two_sub : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [UniformConvexSpace E] {ε : ℝ} [NormedSpace ℝ E],
  0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.toOrderEmbedding.eq_1 : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : α → β)
  (hf : RightOrdContinuous f) (h : Function.Injective f),
  RightOrdContinuous.toOrderEmbedding f hf h =
    { toEmbedding := { toFun := f, inj' := h, map_rel_iff' := ⋯ }.toEmbedding, map_rel_iff' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
_private.Mathlib.Analysis.SpecialFunctions.Pochhammer.0.piecewise_Ici_descPochhammer_eval_zero_eq_descFactorial : ∀ (k n : ℕ), (Set.Ici (↑n - 1)).piecewise (fun x => Polynomial.eval x (descPochhammer ℝ n)) 0 ↑k = ↑(k.descFactorial n)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- The isomorphism `F.obj i ≅ F.obj j` induced by `φ : i ⟶ j`,
when `h : F.IsEventuallyConstantTo i₀` and there exists a map `j ⟶ i₀`.  -/
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantTo i₀ → {i j : J} → (i ⟶ j) → Nonempty (j ⟶ i₀) → (F.obj i ≅ F.obj j)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.transformed : Lean.Elab.Tactic.TacticParsedSnapshot →
  Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_apply_4 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} {σ₄ : Type u_4} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄),
  Lean.Order.CompleteLattice.ofProp p s₁ s₂ s₃ s₄ = p
-- Init.Data.Nat.Lemmas
Nat.dvd_iff_dvd_dvd : ∀ (n d : ℕ), d ∣ n ↔ ∀ (k : ℕ), k ∣ d → k ∣ n
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.fixedIndicesToParams.go : List (Array Bool) → Array Bool → ℕ → Lean.Expr → List Lean.Expr → Lean.MetaM ℕ
-- Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances
NumberField.LiesOver.completionMap_coe : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L} [inst_3 : w.LiesOver v] (x : WithAbs ↑v),
  NumberField.LiesOver.completionMap { toCompletion := ↑x } =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }