mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMinEntryD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {fallback : α × β},
  t₁.WF →
    t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.minEntryD t₁ fallback = Std.DTreeMap.Raw.Const.minEntryD t₂ fallback
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_left_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Sbtw R w y z → Sbtw R w x y → Sbtw R x y z
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.next_eq_posGT : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, p.next h = s.posGT p.offset ⋯
-- Std.Data.DHashMap.Basic
/-- Carries out a monadic action on each mapping in the hash map in some order.  -/
Std.DHashMap.Const.forMUncurried : {α : Type u} →
  {m : Type w → Type w'} →
    [Monad m] →
      {x : BEq α} →
        {x_1 : Hashable α} → {β : Type v} → (α × β → m PUnit.{w + 1}) → (Std.DHashMap α fun x => β) → m PUnit.{w + 1}
-- Init.Grind.Config
/-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names.  -/
Lean.Grind.Config.clean : Lean.Grind.Config → Bool
-- Mathlib.Tactic.DepRewrite
/-- Cached `p.toNumArgs`.  -/
Mathlib.Tactic.DepRewrite.Context.pNumArgs : Mathlib.Tactic.DepRewrite.Context → ℕ
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_right : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x + y, y} = Ideal.span {x, y}
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_left_le_size_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.size ≤ (m₁ ∪ m₂).size
-- Init.Data.Nat.Basic
Nat.lt_add_one_of_le : ∀ {n m : ℕ}, n ≤ m → n < m + 1
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.ext_of_edgeSet : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H.edgeSet = G.edgeSet → H ≤s G → H = G
-- Mathlib.Algebra.Group.Even
instDecidablePredAddOppositeEven : {α : Type u_2} → [inst : Add α] → [DecidablePred Even] → DecidablePred Even
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The statement `Λ'.Supports S q` means that `contSupp k ⊆ S` for any `ret k`
reachable from `q`.
(This is a technical condition used in the proof that the machine is supported.)  -/
Turing.PartrecToTM2.Λ'.Supports : Finset Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ' → Prop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_nndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [SecondCountableTopology α], Measurable fun p => nndist p.1 p.2
-- Std.Async.Signal
/-- Profiling timer expired.
 -/
Std.Async.Signal.sigprof : Std.Async.Signal
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xz.eq_1 : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.xz a1 n = ↑(Pell.xn a1 n)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_zero : ↑0 = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.sInter_of_orderTop : ∀ {α : Type v} [inst : LinearOrder α] {s : Set (Set α)} [OrderTop α], (∀ x ∈ s, IsClub x) → IsClub (⋂₀ s)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst.eq_def : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ),
  p.addConst k =
    match p with
    | Int.Internal.Linear.Poly.num k' => Int.Internal.Linear.Poly.num (k + k')
    | Int.Internal.Linear.Poly.add k' v' p => Int.Internal.Linear.Poly.add k' v' (p.addConst k)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_eq_zero_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree < n → p.coeff n = 0
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an `AddCommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to
the equivalence class of `(x, y)` in the localization of `M` at `S`.  -/
AddLocalization.mk : {M : Type u_1} → [inst : AddCommMonoid M] → {S : AddSubmonoid M} → M → ↥S → AddLocalization S
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_le_iff : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, s.length' ≤ ↑n ↔ s.TerminatedAt n
-- Init.Data.Nat.Basic
Nat.lt_eq : ∀ {x y : ℕ}, x.lt y = (x < y)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom_id : ∀ {R : Type u} [inst : Semiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SemimoduleCat.ofHom LinearMap.id = CategoryTheory.CategoryStruct.id (SemimoduleCat.of R M)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_const_left : ∀ {w a b : ℕ} {c : BitVec w}, BitVec.ofNat w a + (BitVec.ofNat w b + c) = BitVec.ofNat w a + BitVec.ofNat w b + c
-- Lean.Meta.Tactic.Simp.Attr
/-- Registers the given name as a custom simp set. Applying the name as an attribute to a name adds it
to the simp set, and using the name as a parameter to the `simp` tactic causes `simp` to use the
included lemmas.

Custom simp sets must be registered during [initialization](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=initialization).

The description should be a short, singular noun phrase that describes the contents of the custom
simp set.
 -/
Lean.Meta.registerSimpAttr : Lean.Name → String → autoParam Lean.Name Lean.Meta.registerSimpAttr._auto_1 → IO Lean.Meta.SimpExtension
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Composition of two equivariant maps.  -/
MulActionHom.comp : {M : Type u_2} →
  {N : Type u_3} →
    {P : Type u_4} →
      {φ : M → N} →
        {ψ : N → P} →
          {χ : M → P} →
            {X : Type u_5} →
              [inst : SMul M X] →
                {Y : Type u_6} →
                  [inst_1 : SMul N Y] →
                    {Z : Type u_7} →
                      [inst_2 : SMul P Z] → (Y →ₑ[ψ] Z) → (X →ₑ[φ] Y) → [κ : CompTriple φ ψ χ] → X →ₑ[χ] Z
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.isMulCommutative_iSup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {ι : Type u_1} [inst_4 : StarRing R] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : StarModule R A] [Nonempty ι] {S : ι → NonUnitalStarSubalgebra R A}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed version of the mates correspondence.  -/
CategoryTheory.mateEquiv_counit : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F}
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F}
  {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (α : CategoryTheory.TwoSquare G L₁ L₂ H) (d : D),
  CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.mateEquiv adj₁ adj₂) α).app d))
      (adj₂.counit.app (H.obj d)) =
    CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (H.map (adj₁.counit.app d))
-- Mathlib.Computability.Encoding
Computability.Γ'.bra : Computability.Γ'
-- Mathlib.Order.Interval.Finset.Box
Int.existsUnique_mem_box : ∀ (x : ℤ × ℤ), ∃! n, x ∈ Finset.box n
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.uniformizingPolynomial_isUniformizer : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1)
  [hv : v.IsRankOneDiscrete], v.IsUniformizer ↑(RatFunc.uniformizingPolynomial hle)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.coveringNumber ε A = ⨅ C, ⨅ (_ : C ⊆ A), ⨅ (_ : Metric.IsCover ε A C), C.encard
-- Mathlib.Algebra.Group.Finsupp
Finsupp.update_eq_sub_add_single : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] (f : ι →₀ G) (a : ι) (b : G),
  f.update a b = (f - fun₀ | a => f a) + fun₀ | a => b
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.uniq.eq_1 : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'}
  [inst_3 : AddCommGroup N] [inst_4 : Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation),
  h.uniq h' = LinearEquiv.ofLinearMap (h.desc solution') (h'.desc solution) ⋯ ⋯
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.instInhabited : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → Inhabited (PiTensorProduct R fun i => s i)
-- Init.Data.Order.Classes
/-- This typeclass states that the order structure on `α`, represented by an `LE α` instance,
is a partial order.
In other words, the less-or-equal relation is reflexive, transitive and antisymmetric.
 -/
Std.IsPartialOrder : (α : Type u) → [LE α] → Prop
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.natDegree_taylor : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (r : R), ((Polynomial.taylor r) p).natDegree = p.natDegree
-- Init.Data.Float.Model.Float32
/-- Returns `true` if the float is `NaN`.
 -/
Float32.Model.isNaN : Float32.Model → Bool
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A sequence of finite measures such that `μ = sum (sfiniteSeq μ)` (see `sum_sfiniteSeq`).  -/
MeasureTheory.sfiniteSeq : {α : Type u_1} →
  {m0 : MeasurableSpace α} → (μ : MeasureTheory.Measure α) → [h : MeasureTheory.SFinite μ] → ℕ → MeasureTheory.Measure α
-- Mathlib.Analysis.Analytic.Order
/-- The order of an analytic function `f` at `z₀` is finite iff `f` can locally be written as `f z =
  (z - z₀) ^ analyticOrderNatAt f z₀ • g z`, where `g` is analytic and does not vanish at `z₀`.

See `MeromorphicNFAt.order_eq_zero_iff` for an analogous statement about meromorphic functions in
normal form.
 -/
AnalyticAt.analyticOrderAt_ne_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    (analyticOrderAt f z₀ ≠ ⊤ ↔
      ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhds z₀] fun z => (z - z₀) ^ analyticOrderNatAt f z₀ • g z)
-- Mathlib.NumberTheory.Real.Irrational
Irrational.add_intCast : ∀ {x : ℝ}, Irrational x → ∀ (m : ℤ), Irrational (x + ↑m)
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.NormCastExtension.mk.sizeOf_spec : ∀ (up down squash : Lean.Meta.SimpExtension),
  sizeOf { up := up, down := down, squash := squash } = 1 + sizeOf up + sizeOf down + sizeOf squash
-- Init.Data.List.MinMaxIdx
List.getElem_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []), xs[List.minIdxOn f xs h] = List.minOn f xs h
-- Lean.Elab.DefView
Lean.Elab.instNonemptyDefParsed : Nonempty Lean.Elab.DefParsed
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.toContinuousMultilinearMap_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : ContinuousAdd N] (f g : M [⋀^ι]→L[R] N),
  (f + g).toContinuousMultilinearMap = f.toContinuousMultilinearMap + g.toContinuousMultilinearMap
-- Init.Data.Array.Lemmas
Array.back?_append : ∀ {α : Type u_1} {xs ys : Array α}, (xs ++ ys).back? = ys.back?.or xs.back?
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Variant of `f.extend_left_inv I`, stated in terms of images.  -/
OpenPartialHomeomorph.extend_left_inv' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {t : Set M},
  t ⊆ f.source → ↑(f.extend I).symm ∘ ↑(f.extend I) '' t = t
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.circleTransformBoundingFunction.eq_1 : ∀ (R : ℝ) (z : ℂ) (w : ℂ × ℝ),
  Complex.circleTransformBoundingFunction R z w = Complex.circleTransformDeriv R z w.1 (fun x => 1) w.2
-- Mathlib.Analysis.RCLike.Inner
/-- The weight function making `wInner` into the compact inner product.  -/
RCLike.cWeight : {ι : Type u_1} → [Fintype ι] → ι → ℝ
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coe_add_linearMap : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (D1 D2 : LieDerivation R L M), ↑(D1 + D2) = ↑D1 + ↑D2
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.NatTrans.sum'_app_inl : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor A C}
  {H I : CategoryTheory.Functor B C} (α : F ⟶ G) (β : H ⟶ I) (a : A),
  (CategoryTheory.NatTrans.sum' α β).app (Sum.inl a) = α.app a
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck : Type
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.instIsScalarTower : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M]
  [inst_2 : Mul M] [inst_3 : MulMemClass S M] [IsScalarTower R M M] (s : S), IsScalarTower R ↥s ↥s
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
contDiffOn_infty_iff_deriv_of_isOpen : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜},
  IsOpen s → (ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (deriv f) s)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_non_aestronglyMeasurable : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  ¬MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.setToFun μ T hT f = 0
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_inf : ∀ {V : Type u} {G : SimpleGraph V} {H H' : G.Subgraph} (v : V),
  (H ⊓ H').neighborSet v = H.neighborSet v ∩ H'.neighborSet v
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.EnoughProjectives.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (X : C), Nonempty (CategoryTheory.ProjectivePresentation X)) → CategoryTheory.EnoughProjectives C
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.load a q) x x_1 = Turing.TM2.stepAux q (a x) x_1
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapOpcyclesIso_inv_naturality : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasRightHomology]
  [inst_6 : S₂.HasRightHomology] [inst_7 : F.PreservesRightHomologyOf S₁] [inst_8 : F.PreservesRightHomologyOf S₂],
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.opcyclesMap φ)) (S₂.mapOpcyclesIso F).inv =
    CategoryTheory.CategoryStruct.comp (S₁.mapOpcyclesIso F).inv
      (CategoryTheory.ShortComplex.opcyclesMap (F.mapShortComplex.map φ))
-- Mathlib.Tactic.Linarith.Preprocessing
/-- Processor that recursively replaces `P ∧ Q` hypotheses with the pair `P` and `Q`.  -/
Mathlib.Tactic.Linarith.splitConjunctions : Mathlib.Tactic.Linarith.Preprocessor
-- Std.Data.TreeMap.Basic
/-- Returns an array of all values present in the tree map in ascending  order.  -/
Std.TreeMap.valuesArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → Array β
-- Mathlib.Topology.Connected.Clopen
/-- The preimage of a singleton in `connectedComponents` is the connected component
of an element in the equivalence class.  -/
connectedComponents_preimage_singleton : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α},
  ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x
-- Batteries.Data.List.Basic
List.takeList.eq_2 : ∀ {α : Type u_1} (x : List α) (n : ℕ) (ns : List ℕ),
  x.takeList (n :: ns) =
    match List.splitAt n x with
    | (xs₁, xs₂) =>
      match xs₂.takeList ns with
      | (xss, rest) => (xs₁ :: xss, rest)
-- Lean.Parser.Term
Lean.Parser.Termination.partialFixpoint.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.Const.unitOfArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : Array α}, (Std.DHashMap.Raw.Const.unitOfArray a).WF
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.ext : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {f g : ContDiffMapSupportedIn E F n K},
  (∀ (a : E), f a = g a) → f = g
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_add`. -/
AddGroupSeminorm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x), h.codChart ∈ IsManifold.maximalAtlas J n N
-- Init.Data.SInt.Basic
/-- Converts 16-bit signed integers to 64-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.toInt64 : Int16 → Int64
-- Mathlib.Data.Finset.Card
Finset.card_le_card : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t → s.card ≤ t.card
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
PiToModule.fromMatrix_apply_single_one : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (A : Matrix ι ι R) (j : ι),
  ((PiToModule.fromMatrix R b) A) (Pi.single j 1) = ∑ i, A i j • b i
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_ofHom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X] [inst_3 : CommRing Y]
  [inst_4 : Algebra R Y] (f : X →ₐ[R] Y), CommAlgCat.Hom.hom (CommAlgCat.ofHom f) = f
-- Init.GetElem
List.getElem_mem : ∀ {α : Type u_1} {l : List α} {n : ℕ} (h : n < l.length), l[n] ∈ l
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.listToPath.eq_2 : ∀ {α : Type u_1} (a : α) (l : List α), Quiver.SingleObj.listToPath (a :: l) = (Quiver.SingleObj.listToPath l).cons a
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.mk : {G : Type u_6} →
  [inst : AddGroup G] →
    (toNonarchAddGroupSeminorm : NonarchAddGroupSeminorm G) →
      (∀ (x : G), toNonarchAddGroupSeminorm.toFun x = 0 → x = 0) → NonarchAddGroupNorm G
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instSingletonSigmaOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Singleton ((a : α) × β a) (Std.ExtDHashMap α β)
-- Mathlib.RingTheory.Ideal.Over
Ideal.LiesOver.trans : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C) (P : Ideal B)
  (p : Ideal A) [𝔓.LiesOver P] [P.LiesOver p], 𝔓.LiesOver p
-- Mathlib.Analysis.SpecificLimits.Normed
geom_series_mul_shift : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R),
  ‖x‖ < 1 → x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)
-- Mathlib.Analysis.Normed.Module.Normalize
/-- For a nonzero vector `x`, `normalize x` is the unit-length vector that points
in the same direction as `x`. If `x = 0`, then `normalize x = 0`.  -/
NormedSpace.normalize : {V : Type u_1} → [inst : NormedAddCommGroup V] → [NormedSpace ℝ V] → V → V
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.lastStep_nonempty : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p : Besicovitch.TauPackage β α),
  {i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
-- Mathlib.Algebra.Homology.Embedding.TruncLE
ComplexShape.Embedding.truncLE'Functor.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e e_1 : c.Embedding c') (e_e : e = e_1)
  [inst : e.IsTruncLE] (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.CategoryWithHomology C],
  e.truncLE'Functor C = e_1.truncLE'Functor C
-- Mathlib.ModelTheory.Syntax
/-- The negation of a bounded formula is also a bounded formula.  -/
FirstOrder.Language.BoundedFormula.not : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n
-- Mathlib.NumberTheory.Dioph
Poly.coe_one : ∀ {α : Type u_1}, ⇑1 = ⇑(Poly.const 1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_eq_true_of_skipSuffixWhile_le_bool : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  s.skipSuffixWhile p ≤ pos → ∀ (h' : pos < s.endPos), p (pos.get ⋯) = true
-- Std.Http.Data.Headers
/-- Gets the number of headers.
 -/
Std.Http.Headers.size : Std.Http.Headers → ℕ
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
Subsemiring.toSubsemiring_homogeneousCore_le : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜] (R : Subsemiring A),
  (Subsemiring.homogeneousCore 𝒜 R).toSubsemiring ≤ R
-- Lean.InternalExceptionId
Lean.InternalExceptionId.mk.inj : ∀ {idx idx_1 : ℕ}, { idx := idx } = { idx := idx_1 } → idx = idx_1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.leftUnitor_hom_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor α).hom.τl = (CategoryTheory.Bicategory.leftUnitor α.l).hom