mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_sub_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f g : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), ∫ (y : γ), f y - g y ∂η x ∂κ a =
        ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a - ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_one : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {x : A},
  x ∈ I → DividedPowers.OfInvertibleFactorial.dpow I 1 x = x
-- Init.Data.UInt.Lemmas
UInt8.toFin_ofNatLT : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatLT n hn).toFin = ⟨n, hn⟩
-- Mathlib.Topology.Connected.LocallyConnected
locallyConnectedSpace_iff_connectedComponentIn_open : ∀ {α : Type u} [inst : TopologicalSpace α],
  LocallyConnectedSpace α ↔ ∀ (F : Set α), IsOpen F → ∀ x ∈ F, IsOpen (connectedComponentIn F x)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.many.injEq : ∀ (name : Lean.Name) (type : Lean.Expr) (name_1 : Lean.Name) (type_1 : Lean.Expr),
  (Lean.Doc.ArgSpec.many✝ name type = Lean.Doc.ArgSpec.many✝ name_1 type_1) = (name = name_1 ∧ type = type_1)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) →
    CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd f g)
-- Init.Data.List.Lemmas
List.singleton_append : ∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l
-- Mathlib.Order.WithBot
/-- Lift a map `f : α → β` to `WithTop α → WithTop β`. Implemented using `Option.map`.  -/
WithTop.map : {α : Type u_1} → {β : Type u_2} → (α → β) → WithTop α → WithTop β
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsTensor_hom_ext_iff : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{u, u, v} k G} {M : ModuleCat k}
  {f g : ((Rep.coinvariantsTensor k G).obj A).obj B ⟶ M},
  f = g ↔
    (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom f) = (A.coinvariantsTensorMk B).compr₂ (ModuleCat.Hom.hom g)
-- Mathlib.Algebra.Order.Ring.Cone
/-- A (positive) cone in a ring is a subsemiring that
does not contain both `a` and `-a` for any nonzero `a`.
This is equivalent to being the set of non-negative elements of
some order making the ring into a partially ordered ring.  -/
RingCone : (R : Type u_1) → [Ring R] → Type u_1
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_εIso_hom : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  (CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G).εIso.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (F.map (CategoryTheory.Functor.OplaxMonoidal.η L)))
-- Init.Core
DoResultBC.break.sizeOf_spec : ∀ {σ : Type u} [inst : SizeOf σ] (a : σ), sizeOf (DoResultBC.break a) = 1 + sizeOf a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_6 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (l r : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr l)
  (rhs : Std.Tactic.BVDecide.BVExpr r) (h : w = l + r),
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.append rhs h) =
    ⋯ ▸ (Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.one_le_blocksFun : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length), 1 ≤ c.blocksFun i
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_6 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (f g : Turing.ToPartrec.Code)
  (h_1 : Unit → motive Turing.ToPartrec.Code.zero') (h_2 : Unit → motive Turing.ToPartrec.Code.succ)
  (h_3 : Unit → motive Turing.ToPartrec.Code.tail) (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs))
  (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g)) (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g))
  (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match f.case g with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_6 f g
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.restrictSource_iso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source),
  (f.restrictSource U hU hU').iso =
    (AlgebraicGeometry.Scheme.Opens.isoOfLE hU').symm ≪≫
      AlgebraicGeometry.Scheme.Hom.isoImage f.iso.hom ((TopologicalSpace.Opens.map f.source.ι.base).obj U) ≪≫
        AlgebraicGeometry.Scheme.Hom.isoImage f.target.ι
          ((AlgebraicGeometry.Scheme.Hom.opensFunctor f.iso.hom).obj
            ((TopologicalSpace.Opens.map f.source.ι.base).obj U))
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableOfFromJsonOfToJson : {α : Type} → [Lean.FromJson α] → [Lean.ToJson α] → Lean.Server.RpcEncodable α
-- Mathlib.CategoryTheory.Galois.Equivalence
CategoryTheory.PreGaloisCategory.functorToContAction_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.PreGaloisCategory.functorToContAction F).map f =
    CategoryTheory.ObjectProperty.homMk ((CategoryTheory.PreGaloisCategory.functorToAction F).map f)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.toEquiv : {L : FirstOrder.Language} →
  {M : Type w} → {N : Type w'} → [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Equiv M N → M ≃ N
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- The finset of vertices in a complete equipartite subgraph.  -/
SimpleGraph.CompleteEquipartiteSubgraph.verts : {V : Type u_1} → {G : SimpleGraph V} → {r t : ℕ} → G.CompleteEquipartiteSubgraph r t → Finset V
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective equivariant map is equivariant.  -/
AddActionHom.inverse' : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : VAdd M X] →
          {Y : Type u_6} →
            [inst_1 : VAdd N Y] →
              {φ' : N → M} →
                (f : X →ₑ[φ] Y) →
                  (g : Y → X) →
                    Function.RightInverse φ' φ → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → Y →ₑ[φ'] X
-- Mathlib.Topology.Algebra.InfiniteSum.Group
HasProd.hasProd_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  {a₁ a₂ : α} {s : Set β}, HasProd (f ∘ Subtype.val) a₁ → (HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.maxKey! = k ↔
      (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true)
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `G` is `H.Free`, then `G.deleteIncidenceSet v` is also `H.Free` and has at most
`extremalNumber (card V-1) H` many edges.  -/
SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V] [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V],
  H.Free G → ∀ (v : V), (G.deleteIncidenceSet v).edgeFinset.card ≤ SimpleGraph.extremalNumber (Fintype.card V - 1) H
-- Batteries.Recycling.RBTree.Basic
/-- `O(n * log n)`. Constructs the set of all elements satisfying `p`.  -/
RBTree.RBSet.filter : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Bool) → RBTree.RBSet α cmp
-- Init.Data.Vector.Basic
/-- Reverse the elements of a vector.  -/
Vector.reverse : {α : Type u_1} → {n : ℕ} → Vector α n → Vector α n
-- Mathlib.GroupTheory.Index
AddSubgroup.index_eq_zero_of_relIndex_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K = 0 → H.index = 0
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- For a selfadjoint element `x` in a C⋆-algebra, this is the path from `1` to `expUnitary x`
given by `t ↦ expUnitary (t • x)`.  -/
selfAdjoint.expUnitaryPathToOne : {A : Type u_1} → [inst : CStarAlgebra A] → (x : ↥(selfAdjoint A)) → Path 1 (selfAdjoint.expUnitary x)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The identity modification.  -/
CategoryTheory.Oplax.OplaxTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (η : F ⟶ G) → CategoryTheory.Oplax.OplaxTrans.Modification η η
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.val_injective : ∀ {α : Type u} [inst : AddMonoid α], Function.Injective AddUnits.val
-- Lean.Elab.Do.Control
Lean.Elab.Do.ControlStack.earlyReturnT : Lean.Elab.Do.MonadInfo → Lean.Expr → Lean.Elab.Do.ControlStack → Lean.Elab.Do.ControlStack
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddMonoid.mk : {E : Type u_8} →
  [inst : TopologicalSpace E] →
    [toESeminormedAddMonoid : ESeminormedAddMonoid E] → (∀ (x : E), ‖x‖ₑ = 0 ↔ x = 0) → ENormedAddMonoid E
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- TODO : refactor to use `Maximal`.  -/
exists_maximal_linearIndepOn' : ∀ {ι : Type u'} (R : Type u_2) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : ι → M), ∃ s, LinearIndepOn R v s ∧ ∀ (t : Set ι), s ⊆ t → LinearIndepOn R v t → s = t
-- Mathlib.CategoryTheory.Products.Basic
_private.Mathlib.CategoryTheory.Products.Basic.0.CategoryTheory.prodOpEquiv.match_3.eq_1 : ∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] {X Y : Cᵒᵖ × Dᵒᵖ} (motive : (X ⟶ Y) → Sort u_5) (f : X.1 ⟶ Y.1)
  (g : X.2 ⟶ Y.2) (h_1 : (f : X.1 ⟶ Y.1) → (g : X.2 ⟶ Y.2) → motive (f, g)),
  (match (f, g) with
    | (f, g) => h_1 f g) =
    h_1 f g
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.linearIndependent_short_long : ∀ {ι : 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)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R],
  LinearIndependent R ![RootPairing.EmbeddedG2.shortRoot P, RootPairing.EmbeddedG2.longRoot P]
-- Std.Sat.AIG.CachedGatesLemmas
/-- Encoding of or as boolean expression in AIG form.
 -/
_private.Std.Sat.AIG.CachedGatesLemmas.0.Std.Sat.AIG.or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk.congr_simp : ∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} (weights weights_1 : M →₀ R)
  (e_weights : weights = weights_1) (nonneg : 0 ≤ weights) (total : (weights.sum fun x r => r) = 1),
  { weights := weights, nonneg := nonneg, total := total } = { weights := weights_1, nonneg := ⋯, total := ⋯ }
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.instReprArgSpec.repr.match_1.eq_1 : ∀ (motive : Lean.Doc.ArgSpec✝ → Sort u_1) (a : Lean.Name) (a_1 : Lean.Expr)
  (h_1 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.positional✝ a a_2))
  (h_2 : (a : Lean.Name) → (a_2 a_3 : Lean.Expr) → motive (Lean.Doc.ArgSpec.named✝ a a_2 a_3))
  (h_3 : (a : Lean.Name) → (a_2 : Lean.Expr) → motive (Lean.Doc.ArgSpec.many✝ a a_2))
  (h_4 : (a : Lean.Name) → (a_2 : Bool) → motive (Lean.Doc.ArgSpec.flag✝ a a_2)),
  (match Lean.Doc.ArgSpec.positional✝ a a_1 with
    | Lean.Doc.ArgSpec.positional✝ a a_2 => h_1 a a_2
    | Lean.Doc.ArgSpec.named✝ a a_2 a_3 => h_2 a a_2 a_3
    | Lean.Doc.ArgSpec.many✝ a a_2 => h_3 a a_2
    | Lean.Doc.ArgSpec.flag✝ a a_2 => h_4 a a_2) =
    h_1 a a_1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_tensor_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X') (Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X' (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X' Y Z).hom h))
-- Mathlib.Data.Seq.Computation
Computation.head_pure : ∀ {α : Type u} (a : α), (Computation.pure a).head = some a
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic in normal form at `x`, then `f` has order zero iff it does not vanish at
`x`.

See `AnalyticAt.order_eq_zero_iff` for an analogous statement about analytic functions.  -/
MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicNFAt f x → (meromorphicOrderAt f x = 0 ↔ f x ≠ 0)
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `HasDerivAt.sub` -/
HasDerivAt.fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {f' g' : F} {x : 𝕜},
  HasDerivAt f f' x → HasDerivAt g g' x → HasDerivAt (fun i => f i - g i) (f' - g') x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Next unique id for `EqCnstr`s.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.nextId : Lean.Meta.Grind.Arith.CommRing.CommRing → ℕ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofList_eq_insertMany_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {l : List (α × β)},
  Std.DHashMap.Raw.Const.ofList l = Std.DHashMap.Raw.Const.insertMany ∅ l
-- Mathlib.Algebra.Field.Shrink
Shrink.instNNRatCast : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NNRatCast α] → NNRatCast (Shrink.{v, u_1} α)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.comp_toPrelaxFunctor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.Pseudofunctor B C) (G : CategoryTheory.Pseudofunctor C D),
  (F.comp G).toPrelaxFunctor = F.comp G.toPrelaxFunctor
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`,
returns a multiplicative equivalence with `toFun = f` and `invFun = g`.  This constructor is
useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms.  -/
MonoidHom.toMulEquiv : {M : Type u_4} →
  {N : Type u_5} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (f : M →* N) → (g : N →* M) → g.comp f = MonoidHom.id M → f.comp g = MonoidHom.id N → M ≃* N
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroupClass.seminormedAddGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : AddSubgroupClass S E]
  (s : S),
  AddSubgroupClass.seminormedAddGroup s =
    { norm := fun a => ‖↑s a‖, toAddGroup := AddSubgroupClass.toAddGroup s,
      toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams.toTextDocumentPositionParams : Lean.Lsp.TypeDefinitionParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Data.NNRat.Floor
NNRat.floor_natCast_div_natCast : ∀ (n d : ℕ), ⌊↑n / ↑d⌋₊ = n / d
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instAddHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Add (T₁ ⟶ T₂)
-- Mathlib.Probability.Martingale.Basic
/-- A predictable martingale is a.e. equal to its initial state.  -/
MeasureTheory.Martingale.eq_zero_of_predictable : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [CompleteSpace E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Martingale f 𝒢 μ → (MeasureTheory.StronglyAdapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), f n =ᵐ[μ] f 0
-- Mathlib.Data.Finset.Defs
Finset.isWellFounded_ssubset : ∀ {α : Type u_1}, IsWellFounded (Finset α) fun x1 x2 => x1 ⊂ x2
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.choose_two_mul_succ_mul_div_eq : ∀ {k m : ℕ} (x : ℚ),
  m < k → ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
-- Mathlib.Combinatorics.Matroid.Closure
/-- The closure of `X ⊆ M.E` is the intersection of all the flats of `M` containing `X`.
A set `X` that doesn't satisfy `X ⊆ M.E` has the junk value `M.closure X := M.closure (X ∩ M.E)`.  -/
Matroid.closure : {α : Type u_2} → Matroid α → Set α → Set α
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.inter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (m₁ m₂ : Std.DTreeMap.Internal.Impl α β) (h₁ : m₁.Balanced),
  m₁.inter m₂ h₁ =
    if m₁.size ≤ m₂.size then
      (Std.DTreeMap.Internal.Impl.filter (fun k x => Std.DTreeMap.Internal.Impl.contains k m₂) m₁ h₁).impl
    else m₁.interSmaller m₂
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_comp_orderMonoidHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
/-- If `X` is geometrically integral over a field, then it is integral.  -/
AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_subsingleton : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIntegral f] [Subsingleton ↥S]
  [AlgebraicGeometry.IsIntegral S], AlgebraicGeometry.IsIntegral X
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLawfulHasSizeNat : Std.Rxc.LawfulHasSize ℕ
-- Plausible.Arbitrary
Plausible.UInt32.Arbitrary : Plausible.Arbitrary UInt32
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.foldr.match_1.eq_2 : ∀ {α : Type u_1} {σ : Sort u_3} (motive : RBTree.RBNode α → σ → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α)
  (v : α) (r : RBTree.RBNode α) (b : σ) (h_1 : (b : σ) → motive RBTree.RBNode.nil b)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → (b : σ) → motive (RBTree.RBNode.node c l v r) b),
  (match RBTree.RBNode.node c l v r, b with
    | RBTree.RBNode.nil, b => h_1 b
    | RBTree.RBNode.node c l v r, b => h_2 c l v r b) =
    h_2 c l v r b
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- One of the antipode axioms for a Hopf algebra.  -/
HopfAlgebra.mul_antipode_lTensor_comul : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : Semiring A} [self : HopfAlgebra R A],
  LinearMap.mul' R A ∘ₗ LinearMap.lTensor A (HopfAlgebraStruct.antipode R) ∘ₗ CoalgebraStruct.comul =
    Algebra.linearMap R A ∘ₗ CoalgebraStruct.counit
-- Mathlib.Algebra.Order.Monoid.Units
Units.instOrd : {α : Type u_1} → [inst : Monoid α] → [Ord α] → Ord αˣ
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.ref : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → Lean.Syntax
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The equivalence between the nonsingular points on a Weierstrass curve `W` in affine coordinates
and the set of pairs `⟨x, y⟩` satisfying `W.Nonsingular x y` with zero.  -/
WeierstrassCurve.Affine.nonsingularPointEquiv : {R : Type r} →
  [inst : CommRing R] → (W' : WeierstrassCurve.Affine R) → W'.Point ≃ WithZero { xy // W'.Nonsingular xy.1 xy.2 }
-- Mathlib.Analysis.Normed.Group.Basic
toReal_enorm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E), ‖x‖ₑ.toReal = ‖x‖
-- Mathlib.NumberTheory.Height.NumberField
NumberField.totalWeight_eq_finrank : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Height.totalWeight K = Module.finrank ℚ K
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
_private.Mathlib.GroupTheory.SpecificGroups.Cyclic.0.card_nsmul_eq_zero_eq_addOrderOf_aux : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | n • a = 0}.card ≤ n) → ∀ (a : α), {b | addOrderOf a • b = 0}.card = addOrderOf a
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getEntry! : {α : Type u} → {β : α → Type v} → [BEq α] → α → [Inhabited ((a : α) × β a)] → List ((a : α) × β a) → (a : α) × β a
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.associative_ε₁_eq_mul : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {I₁₂ : Type u_4} {I₂₃ : Type u_5} {J : Type u_6}
  (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₃ : ComplexShape I₃) (c₁₂ : ComplexShape I₁₂) (c₂₃ : ComplexShape I₂₃)
  (c : ComplexShape J) [inst : TotalComplexShape c₁ c₂ c₁₂] [inst_1 : TotalComplexShape c₁₂ c₃ c]
  [inst_2 : TotalComplexShape c₂ c₃ c₂₃] [inst_3 : TotalComplexShape c₁ c₂₃ c] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
  c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker_hom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  CategoryTheory.StructuredArrow.Hom.right
      (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIsoWhisker f g h).hom =
    CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)
-- Init.Data.Nat.Lemmas
Nat.decidableBallLT : (n : ℕ) →
  (P : (k : ℕ) → k < n → Prop) →
    [(n_1 : ℕ) → (h : n_1 < n) → Decidable (P n_1 h)] → Decidable (∀ (n_1 : ℕ) (h : n_1 < n), P n_1 h)