mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X), (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).obj ⟨Order.succ j, ⋯⟩ = X
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.mkSharedExprs : Lean.Meta.Sym.AlphaShareCommonM Lean.Meta.Sym.SharedExprs
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
Antitone.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftMono α] [MulRightMono α]
  [inst_4 : Preorder β] {f : β → α}, Antitone f → Monotone fun x => (f x)⁻¹
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- If `(F ⋙ forget (ModuleCat R)).sections` is `u`-small, `F` has a limit.  -/
ModuleCat.hasLimit : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections], CategoryTheory.Limits.HasLimit F
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableCtorInfo : Hashable Lean.Compiler.LCNF.CtorInfo
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_insert_le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {k : α}, (cmp (t.insert k).min! t.min!).isLE = true
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Constructor for objects in `CardinalFilteredPoset κ`.  -/
CategoryTheory.CardinalDirectedPoset.of : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : PartOrdEmb) → [CategoryTheory.IsCardinalFiltered (↑J) κ] → CategoryTheory.CardinalDirectedPoset κ
-- Mathlib.Algebra.Lie.Basic
IsLieTower.mk : ∀ {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} [inst : Bracket L₁ L₂] [inst_1 : Bracket L₁ M] [inst_2 : Bracket L₂ M]
  [inst_3 : Add M], (∀ (x : L₁) (y : L₂) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆) → IsLieTower L₁ L₂ M
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableOn_neg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, DifferentiableOn 𝕜 (-f) s ↔ DifferentiableOn 𝕜 f s
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.toAddMonoid : {G : Type u} → [self : SubNegMonoid G] → AddMonoid G
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_add_self : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  {i j : n}, i ≠ j → (A.updateRow i (A i + A j)).det = A.det
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.custom.inj : ∀ {msgData msgData_1 : Lean.MessageData},
  Lean.Elab.Term.MVarErrorKind.custom msgData = Lean.Elab.Term.MVarErrorKind.custom msgData_1 → msgData = msgData_1
-- Mathlib.Order.SuccPred.Tree
SubRootedTree.bot_mem_iff : ∀ {t : RootedTree} (r : SubRootedTree t), ⊥ ∈ r ↔ r.root = ⊥
-- Lean.Elab.App
/-- The following field is used to implement the `propagateExpectedType` heuristic.
It is set to `true` true when `expectedType` still has to be propagated.
 -/
Lean.Elab.Term.ElabAppArgs.State.propagateExpected : Lean.Elab.Term.ElabAppArgs.State → Bool
-- Mathlib.CategoryTheory.Sites.Canonical
/-- **Alias** of `CategoryTheory.Presieve.isSheafFor_trans`. -/
CategoryTheory.Sheaf.isSheafFor_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1))
  (R S : CategoryTheory.Sieve X),
  CategoryTheory.Presieve.IsSheafFor P R.arrows →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
        S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
        CategoryTheory.Presieve.IsSheafFor P S.arrows
-- Mathlib.Algebra.Group.Semiconj.Units
/-- If `a` semiconjugates a unit `x` to a unit `y`, then it semiconjugates `x⁻¹` to `y⁻¹`.  -/
SemiconjBy.units_inv_right : ∀ {M : Type u_1} [inst : Monoid M] {a : M} {x y : Mˣ}, SemiconjBy a ↑x ↑y → SemiconjBy a ↑x⁻¹ ↑y⁻¹
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.comp : Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
/-- Up to rotation, the contractible triangle `X ⟶ X ⟶ 0 ⟶ X⟦1⟧` for `X : Cᵒᵖ` corresponds
to the contractible triangle for `X.unop` in `C`.  -/
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            (X : Cᵒᵖ) →
              CategoryTheory.Pretriangulated.contractibleTriangle X ≅
                (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj
                  (Opposite.op (CategoryTheory.Pretriangulated.contractibleTriangle (Opposite.unop X)).invRotate)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.quot_mk_eq_mk : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K),
  Quot.mk (PerfectClosure.R K p) x = PerfectClosure.mk K p x
-- Init.Data.Array.Lemmas
Array.mem_map_of_mem : ∀ {α : Type u_1} {β : Type u_2} {l : Array α} {a : α} {f : α → β}, a ∈ l → f a ∈ Array.map f l
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t₁ t₂ : Set β}, s +ᵥ t₁ ∪ t₂ = (s +ᵥ t₁) ∪ (s +ᵥ t₂)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.ringObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (self : CategoryTheory.RingObjCat C) → CategoryTheory.RingObj self.X
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_pred_right_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  a < b → insert (Order.pred b) (Set.Ico a (Order.pred b)) = Set.Ico a b
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.instDecidableEq : {ι : Type v} →
  {β : ι → Type w} →
    [DecidableEq ι] →
      [inst : (i : ι) → AddCommMonoid (β i)] → [(i : ι) → DecidableEq (β i)] → DecidableEq (DirectSum ι β)
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.join_map_ret : ∀ {α : Type u} (s : Stream'.Seq α), (Stream'.Seq.map Stream'.Seq1.ret s).join = s
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- A vector is in the direction of a nonempty affine subspace if and only if it is the subtraction
of two vectors in the subspace.  -/
AffineSubspace.mem_direction_iff_eq_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P},
  (↑s).Nonempty → ∀ (v : V), v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
-- Mathlib.Logic.Relation
Std.Refl.comap : ∀ {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Refl r] (f : α → β), Std.Refl (Function.onFun r f)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
/-- Finds a nonnegative vector `v`, such that `A v = 0` and some of its coordinates from
`strictCoords`
are positive, in the case such `v` exists. If not, throws the error. The latter prevents
`linarith` from doing useless post-processing.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.findPositiveVector : {n m : ℕ} →
  {matType : ℕ → ℕ → Type} →
    [Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
      matType n m → List ℕ → Lean.MetaM (Array ℚ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, (compare k (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey!).isLE = true
-- Mathlib.Algebra.Group.Basic
one_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (n : ℤ), 1 ^ n = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f g : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0)
  (hg : CategoryTheory.CategoryStruct.comp (K.d p' p) g = 0),
  CochainComplex.HomComplex.Cocycle.toSingleMk (f + g) h p' hp' ⋯ =
    CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf +
      CochainComplex.HomComplex.Cocycle.toSingleMk g h p' hp' hg
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {x : CommGroup α} {x_1 : Preorder α} {x_2 : CommGroup β} {x_3 : PartialOrder β}
  (f : α ≃ β) (hf : ∀ {a b : α}, f a ≤ f b ↔ a ≤ b) (map_mul : ∀ (a b : α), f (a * b) = f a * f b),
  OrderMonoidIso.mk' f hf map_mul = { toMulEquiv := MulEquiv.mk' f map_mul, map_le_map_iff' := ⋯ }
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_div_cast_of_nonneg : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {n : ℤ},
  0 ≤ n → ∀ (a : k), ⌊a / ↑n⌋ = ⌊a⌋ / n
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The limit cone exhibiting `⨁ Subtype.restrict pᶜ f` as the kernel of
`biproduct.toSubtype f p`  -/
CategoryTheory.Limits.kernelForkBiproductToSubtype : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : Type} →
        [inst_2 : Finite K] →
          [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            (f : K → C) →
              (p : K → Prop) →
                CategoryTheory.Limits.LimitCone
                  (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.toSubtype f p) 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α} {hc : t.minKeyD fallback ∈ t}, t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
-- Mathlib.GroupTheory.Schreier
Subgroup.exists_finset_card_le_mul : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [H.FiniteIndex] {S : Finset G},
  Subgroup.closure ↑S = ⊤ → ∃ T, T.card ≤ H.index * S.card ∧ Subgroup.closure ↑T = ⊤
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- `G.between s t` is bipartite if the sets `s` and `t` are disjoint.  -/
SimpleGraph.between_isBipartite : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, Disjoint s t → (SimpleGraph.between s t G).IsBipartite
-- Lean.Meta.Tactic.SolveByElim
/-- If `suggestions` is `true`, `solve_by_elim` will invoke the currently configured library
suggestion engine on the current goal, and attempt to use the resulting suggestions as
additional lemmas.
 -/
Lean.Meta.SolveByElim.SolveByElimConfig.suggestions : Lean.Meta.SolveByElim.SolveByElimConfig → Bool
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.monoidalCategoryStruct : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.MonoidalCategoryStruct (CategoryTheory.LocalizedMonoidal L W ε)
-- Mathlib.Computability.Reduce
ManyOneEquiv.of_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {e : α ≃ β},
  e.Computable → ∀ {p : β → Prop}, ManyOneEquiv (p ∘ ⇑e) p
-- Mathlib.Order.CompleteLattice.Defs
le_sInf_iff : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α}, a ≤ sInf s ↔ ∀ b ∈ s, a ≤ b
-- Mathlib.Data.List.Intervals
List.Ico.filter_le_of_le : ∀ {n m l : ℕ}, n ≤ l → List.filter (fun x => decide (l ≤ x)) (List.Ico n m) = List.Ico l m
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [inst : Fintype ↑(G'.neighborSet v)],
  G'.degree v = 1 ↔ ∃! w, G'.Adj v w
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryLE.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Init.Data.String.Lemmas.FindPos
String.Slice.offset_posLE_le : ∀ {s : String.Slice} {p : String.Pos.Raw}, (s.posLE p).offset ≤ p
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.eq_zero_of_pair : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {x y : M},
  LinearIndependent R ![x, y] → ∀ {s t : R}, s • x + t • y = 0 → s = 0 ∧ t = 0
-- Std.Http.Data.Chunk
Std.Http.Chunk.ExtensionName.mk.injEq : ∀ (value : String)
  (isValidExtensionName :
    autoParam (Std.Http.Chunk.IsValidExtensionName value) Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam)
  (value_1 : String)
  (isValidExtensionName_1 :
    autoParam (Std.Http.Chunk.IsValidExtensionName value_1)
      Std.Http.Chunk.ExtensionName.isValidExtensionName._autoParam),
  ({ value := value, isValidExtensionName := isValidExtensionName } =
      { value := value_1, isValidExtensionName := isValidExtensionName_1 }) =
    (value = value_1)
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.colim_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.PreservesColimits CategoryTheory.Limits.colim
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.map_comap_eq : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (s : Subfield L),
  Subfield.map f (Subfield.comap f s) = s ⊓ f.fieldRange
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_left_inverse' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ∀ᶠ (y : X) in nhds (↑e.symm x), ↑e.symm (↑e y) = y
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- A functor that preserves the limit of `(StructuredArrow.proj L c ⋙ F)` preserves
the pointwise right Kan extension of `F` along `L` at c.  -/
CategoryTheory.Functor.preservesPointwiseRightKanExtensionAtOfPreservesLimit : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (c : C)
  [CategoryTheory.Limits.PreservesLimit ((CategoryTheory.StructuredArrow.proj c L).comp F) G],
  G.PreservesPointwiseRightKanExtensionAt F L c
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instSMulZeroClassQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : Zero M] → [inst_1 : SMulZeroClass S M] → (c : SMulCon S M) → SMulZeroClass S (SMulCon.Quotient M c)
-- Lean.PrettyPrinter.Delaborator.SubExpr
/-- Assumes the `SubExpr` is a lambda or forall.
Creates a local declaration for this binder using the name `n`, enters the binding body, and evaluates `x`.
 -/
Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [MonadReaderOf Lean.SubExpr m] →
        [MonadWithReaderOf Lean.SubExpr m] → [MonadControlT Lean.MetaM m] → Lean.Name → m α → m α
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Stats.toString : Lean.PersistentHashMap.Stats → String
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The canonical linear map to the completion.  -/
AdicCompletion.of : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M →ₗ[R] AdicCompletion I M
-- Mathlib.Probability.CentralLimitTheorem
ProbabilityTheory.tendsto_charFun_inv_sqrt_mul_pow : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {X : Ω → ℝ},
  AEMeasurable X P →
    ∫ (x : Ω), X x ∂P = 0 →
      ∫ (x : Ω), (X ^ 2) x ∂P = 1 →
        ∀ (t : ℝ),
          Filter.Tendsto (fun n => MeasureTheory.charFun (MeasureTheory.Measure.map X P) ((√↑n)⁻¹ * t) ^ n) Filter.atTop
            (nhds (Complex.exp (-↑t ^ 2 / 2)))
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.zero_of_target_iso_zero' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIsomorphic Y 0 → f = 0
-- Mathlib.Data.Ordmap.Invariants
Ordnode.dual_balanceL : ∀ {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α), (l.balanceL x r).dual = r.dual.balanceR x l.dual
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_id_eq_sSup : ∀ {α : Type u_2} [inst : CompleteLattice α] (s : Finset α), s.sup id = sSup ↑s
-- Std.Sync.Channel
/-- A multi-producer multi-consumer FIFO channel that offers both bounded and unbounded buffering
and a synchronous API. This type acts as a convenient layer to use a channel in a blocking fashion
and is not actually different from the original channel.

Additionally `Std.CloseableChannel.Sync` can be closed if necessary, unlike `Std.Channel.Sync`.
This introduces the need to handle errors in some cases, thus it is usually easier to use
`Std.Channel` if applicable.
 -/
Std.CloseableChannel.Sync : Type → Type
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_5 : HSub Std.Time.PlainDateTime Std.Time.Second.Offset Std.Time.PlainDateTime
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_zero : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ}
  {N : ι}, MeasureTheory.upperCrossingTime a b f N 0 = ⊥
-- Lean.Data.PersistentArray
Lean.PersistentArray.root : {α : Type u} → Lean.PersistentArray α → Lean.PersistentArrayNode α
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.succ.match_1.eq_2 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit1)
  (h_3 : (n : PosNum) → motive n.bit0),
  (match n.bit1 with
    | PosNum.one => h_1 ()
    | n.bit1 => h_2 n
    | n.bit0 => h_3 n) =
    h_2 n
-- Mathlib.Topology.Algebra.Monoid
Submonoid.topologicalClosure_minimal : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M] (s : Submonoid M)
  {t : Submonoid M}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.Data.Ineq
Mathlib.instDecidableEqIneq : DecidableEq Mathlib.Ineq
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
/-- If `[c, d]` is a subinterval of `[a, b]`, then the distance between `c` and `d` is less than or
equal to that of `a` and `b`  -/
Set.abs_sub_le_of_uIcc_subset_uIcc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  Set.uIcc c d ⊆ Set.uIcc a b → |d - c| ≤ |b - a|
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.IsExpansionOn.map_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} {inst : L.Structure M}
  {inst_1 : L'.Structure M} [self : ϕ.IsExpansionOn M] {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.hashPtrExpr : Lean.Expr → UInt64
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.instTensorUnit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (X : D),
  CategoryTheory.ModObj.instTensorUnit X =
    { smul := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, one_smul := ⋯,
      mul_smul := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsFinite f],
  AlgebraicGeometry.IsFinite (f ∣_ V)
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalWithUnfoldingNone : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Subgroup.Even
Subgroup.square_toSubmonoid : ∀ {G : Type u_1} [inst : CommGroup G], (Subgroup.square G).toSubmonoid = Submonoid.square G
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.ofIdComp_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t :
    CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)),
  t.ofIdComp.hom = CategoryTheory.CategoryStruct.comp t.counit (CategoryTheory.Bicategory.leftUnitor g).hom
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.u₃` and `S.Z` be any elements such that
`S.Z ^ 3 * S.u₃ = S.z`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Z : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → NumberField.RingOfIntegers K
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Module.Basis.ofSplitExact.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {K : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f f_1 : K →ₗ[R] M} (e_f : f = f_1) {g g_1 : M →ₗ[R] P} (e_g : g = g_1) {s s_1 : M →ₗ[R] K} (e_s : s = s_1)
  (hs : s ∘ₗ f = LinearMap.id) (hfg : Function.Exact ⇑f ⇑g) {ι : Type u_5} {κ : Type u_6} {σ : Type u_7} {a a_1 : κ → ι}
  (e_a : a = a_1) {b b_1 : σ → ι} (e_b : b = b_1) (hg : Function.Surjective ⇑g) (v v_1 : Module.Basis ι R M)
  (e_v : v = v_1) (hainj : Function.Injective a) (hsa : ∀ (i : κ), s (v (a i)) = 0)
  (hlib : LinearIndependent R (⇑s ∘ ⇑v ∘ b)) (hab : Codisjoint (Set.range a) (Set.range b)),
  Module.Basis.ofSplitExact hs hfg hg v hainj hsa hlib hab = Module.Basis.ofSplitExact ⋯ ⋯ ⋯ v_1 ⋯ ⋯ ⋯ ⋯