mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finmap
Finmap.keys_replace : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : Finmap β),
  (Finmap.replace a b s).keys = s.keys
-- Mathlib.Data.PNat.Factors
Nat.Primes.toPNat.eq_1 : ∀ (p : Nat.Primes), ↑p = ⟨↑p, ⋯⟩
-- Init.Data.Vector.Lemmas
Vector.contains_eq_any_beq : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a : α}, xs.contains a = xs.any fun x => a == x
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Slot.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (value : Option α) (pos remaining : ℕ),
  sizeOf { value := value, pos := pos, remaining := remaining } = 1 + sizeOf value + sizeOf pos + sizeOf remaining
-- Mathlib.Data.Finset.Sum
Finset.subset_disjSum : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)},
  u ⊆ s.disjSum t ↔ u.toLeft ⊆ s ∧ u.toRight ⊆ t
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.mk : Lean.Meta.ElimInfo → Array Lean.Expr → Lean.Elab.Tactic.ElimApp.Context✝
-- Init.Data.Option.Basic
Option.getD_none : ∀ {α : Type u_1} {a : α}, none.getD a = a
-- Mathlib.Algebra.Notation.Prod
Prod.swap_div : ∀ {G : Type u_8} {H : Type u_9} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).swap = a.swap / b.swap
-- Mathlib.Analysis.RCLike.Basic
RCLike.neg_iff_exists_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, z < 0 ↔ ∃ x < 0, ↑x = z
-- Mathlib.Data.Int.Range
Int.range.eq_1 : ∀ (m n : ℤ), m.range n = List.map (fun r => m + ↑r) (List.range (n - m).toNat)
-- Init.Data.BitVec.Lemmas
/-- If `x` is nonnegative (i.e., does not have its msb set),
then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
 -/
BitVec.toInt_udiv_of_msb : ∀ {w : ℕ} {x : BitVec w}, x.msb = false → ∀ (y : BitVec w), (x / y).toInt = ↑x.toNat / ↑y.toNat
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go.induct : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α)
  (motive : α → Lean.Grind.Linarith.Poly → Prop),
  (∀ (r : α), motive r Lean.Grind.Linarith.Poly.nil) →
    (∀ (r : α) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
        motive (r + Lean.Grind.Linarith.Var.denote ctx v) p → motive r (Lean.Grind.Linarith.Poly.add 1 v p)) →
      (∀ (r : α) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
          (k = 1 → False) →
            motive (r + k • Lean.Grind.Linarith.Var.denote ctx v) p → motive r (Lean.Grind.Linarith.Poly.add k v p)) →
        ∀ (r : α) (p : Lean.Grind.Linarith.Poly), motive r p
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.mk : {B : Type u_2} →
  {F : Type u_3} →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        {E : B → Type u_5} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              (∀ (b : B), Topology.IsInducing (Bundle.TotalSpace.mk b)) →
                (trivializationAtlas' : Set (Bundle.Trivialization F Bundle.TotalSpace.proj)) →
                  (trivializationAt' : B → Bundle.Trivialization F Bundle.TotalSpace.proj) →
                    (∀ (b : B), b ∈ (trivializationAt' b).baseSet) →
                      (∀ (b : B), trivializationAt' b ∈ trivializationAtlas') → FiberBundle F E
-- Mathlib.LinearAlgebra.Matrix.Trace
/-- `Matrix.trace` as an `AddMonoidHom`  -/
Matrix.traceAddMonoidHom : (n : Type u_3) → (R : Type u_6) → [Fintype n] → [inst : AddCommMonoid R] → Matrix n n R →+ R
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
CochainComplex.isIso_liftCycles_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℕ) {X : C} (φ : X ⟶ K.X 0) [inst_2 : HomologicalComplex.HasHomology K 0]
  (hφ : CategoryTheory.CategoryStruct.comp φ (K.d 0 1) = 0),
  CategoryTheory.IsIso (HomologicalComplex.liftCycles K φ 1 CochainComplex.isIso_liftCycles_iff._proof_1 hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X 1, f := φ, g := K.d 0 1, zero := hφ }.Exact ∧ CategoryTheory.Mono φ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j_eq_zero_iff : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] [IsReduced R], W.j = 0 ↔ W.c₄ = 0
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- Shrink the indexing type of `LocalGeneratorsData` into the universe of the site.  -/
SheafOfModules.LocalGeneratorsData.shrink : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.LocalGeneratorsData → M.LocalGeneratorsData
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The underlying set of a non-empty directed Sup of `NonUnitalSubring`s is just a union of the
`NonUnitalSubring`s. Note that this fails without the directedness assumption (the union of two
`NonUnitalSubring`s is typically not a `NonUnitalSubring`)  -/
NonUnitalSubring.mem_iSup_of_directed : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → NonUnitalSubring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
-- Init.Data.SInt.Lemmas
Int64.zero_add : ∀ (a : Int64), 0 + a = a
-- Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint : ∀ {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.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C}
  [inst_4 : CategoryTheory.Limits.PreservesFiniteLimits G] [inst_5 : CategoryTheory.Limits.PreservesFiniteColimits G]
  {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful],
  G.kernel.isoModSerre = CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range F.obj
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.containsThenInsert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α) (b : β a),
  m.containsThenInsert a b =
    if h : 0 < m.buckets.size then
      match Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, h⟩ a b with
      | (replaced, ⟨r, property⟩) => (replaced, r)
    else (false, m)
-- Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
CategoryTheory.Monoidal.rigidFunctorCategory : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Groupoid C] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.RigidCategory D] → CategoryTheory.RigidCategory (CategoryTheory.Functor C D)
-- Mathlib.RingTheory.LaurentSeries
/-- Through the isomorphism `LaurentSeriesRingEquiv`, power series land in the unit ball inside the
completion of `K⟮X⟯`.  -/
LaurentSeries.mem_integers_of_powerSeries : ∀ (K : Type u_2) [inst : Field K] (F : PowerSeries K),
  (LaurentSeries.LaurentSeriesRingEquiv K) ((HahnSeries.ofPowerSeries ℤ K) F) ∈
    IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.nsmul_eq_ofNat_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] {k : ℕ} {a : α}, k • a = OfNat.ofNat k * a
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
/-- The product over a sigma type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Finset.prod_sigma`.  -/
Finset.prod_sigma' : ∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
  (f : (a : α) → σ a → β), ∏ a ∈ s, ∏ s ∈ t a, f a s = ∏ x ∈ s.sigma t, f x.fst x.snd
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- A cochain complex that is both strictly `≤ n` and `≥ n` is isomorphic to
a complex `(single _ _ n).obj M` for some object `M`.  -/
CochainComplex.exists_iso_single : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ) [K.IsStrictlyGE n]
  [K.IsStrictlyLE n], ∃ M, Nonempty (K ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj M)
-- Mathlib.Data.Seq.Computation
Computation.instLawfulMonad : LawfulMonad Computation
-- Init.Prelude
Lean.Name.instBEq : BEq Lean.Name
-- Init.Prelude
/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈`  -/
Lean.Name.mkStr8 : String → String → String → String → String → String → String → String → Lean.Name
-- Init.Data.Format.Basic
/-- Creates a new flattening group for the given inner `Format`.   -/
Std.Format.group : Std.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Std.Format
-- Aesop.Rule
Aesop.RegularRule.withRule : {β : Sort u_1} → ({α : Type} → Aesop.Rule α → β) → Aesop.RegularRule → β
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_map_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ}
  {g : β → δ}, Measurable f → (κ.map fun x => (f x, g x)).snd = κ.map g
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is a monotone function taking values in a complete lattice
and `g` tends to `atBot` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.  -/
Monotone.iInf_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  [OrderBot γ] {l : Filter α} [l.NeBot] {f : β → γ},
  Monotone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨅ a, f (g a) = ⨅ b, f b
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model from the total space of a tangent bundle.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromTotalSpace.tangentSpace : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme), AlgebraicGeometry.Surjective (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.CategoryTheory.Category.Bipointed
/-- Composition of morphisms of `Bipointed`.  -/
Bipointed.Hom.comp : {X Y Z : Bipointed} → X.Hom Y → Y.Hom Z → X.Hom Z
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.reindex.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T) {ι : Type w'}
  (e : ι ≃ E.I₀), E.reindex e = E.restrictIndex ⇑e
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum over `s.subtype pred` equals one over `{x ∈ s | pred x}`.  -/
Finset.weightedVSub_subtype_eq_filter : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop)
  [inst_3 : DecidablePred pred],
  (((Finset.subtype pred s).weightedVSub fun i => p ↑i) fun i => w ↑i) = ({x ∈ s | pred x}.weightedVSub p) w
-- Mathlib.Algebra.Group.Pi.Basic
Pi.instIsCancelAdd : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Add (f i)] [∀ (i : I), IsCancelAdd (f i)],
  IsCancelAdd ((i : I) → f i)
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
Matrix.ProjectiveSpecialLinearGroup.rank_two_simple' : ∀ {F : Type u_2} [inst : Field F],
  (∃ a, a ≠ 0 ∧ a ^ 2 ≠ 1) → IsSimpleGroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F)
-- Mathlib.Tactic.Sat.FromLRAT
/-- Main entry point. Given strings `cnf` and `lrat` with unparsed file data, and a name `name`,
adds `theorem name : type := proof` where `type` is a propositional theorem like
`∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1`.

Also creates auxiliaries named `name.ctx_1` (for the CNF formula)
and `name.proof_1` (for the LRAT proof), with `name` itself containing the reification proof.  -/
Mathlib.Tactic.Sat.fromLRAT : String → String → Lean.Name → Lean.MetaM Unit
-- Lean.Server.Completion.CompletionCollectors
/-- Compares `n₁` and `n₂` modulo private prefixes. Similar to `Name.cmp` but ignores all
private prefixes in both names.
Necessary because the namespaces of private names do not contain private prefixes.
 -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.cmpModPrivate : Lean.Name → Lean.Name → Ordering
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.closedComplemented_range_of_leftInverse : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} {N : Type u_3} [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace N] [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M]
  [inst_6 : Module R N] (f₁ : M →L[R] N) (f₂ : N →L[R] M), Function.LeftInverse ⇑f₂ ⇑f₁ → (↑f₁).range.ClosedComplemented
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.of_mulSupport_subset_isCompact : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : One β] {f : α → β} {K : Set α} [R1Space α],
  IsCompact K → Function.mulSupport f ⊆ K → HasCompactMulSupport f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DHashMap.Internal.Raw₀.Const.alter m k f).getKey? k' =
        if (k == k') = true then if (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true then some k else none
        else m.getKey? k'
-- Mathlib.CategoryTheory.EqToHom
/-- Reducible form of `congrArg_mpr_hom_right`  -/
CategoryTheory.congrArg_cast_hom_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y),
  cast ⋯ p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_lt_mul_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LT α] [DenselyOrdered α] [MulLeftStrictMono α] {a b c : α},
  c < a * b → ∃ b' < b, c < a * b'
-- Init.Data.Array.Basic
/-- Folds a function over an array from the right, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the array in reverse order, using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (exclusive) to `stop` (inclusive), so no folding occurs unless `start > stop`.
By default, the entire array is used.

Examples:
 * `#[a, b, c].foldr f init  = f a (f b (f c init))`
 * `#[1, 2, 3].foldr (toString · ++ ·) "" = "123"`
 * `#[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"`
 -/
Array.foldr : {α : Type u} → {β : Type v} → (α → β → β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → β
-- Mathlib.Order.Hom.Bounded
TopHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Top α] [inst_1 : Top β] [inst_2 : Top γ] {g : TopHom β γ}
  {f₁ f₂ : TopHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.NumberTheory.MahlerMeasure
Polynomial.one_le_mahlerMeasure_of_ne_zero : ∀ {p : Polynomial ℤ}, p ≠ 0 → 1 ≤ (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure
-- Mathlib.Topology.Separation.Profinite
nhds_basis_clopen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] (x : X),
  (nhds x).HasBasis (fun s => x ∈ s ∧ IsClopen s) id
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infEDist_smul : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {M : Type u_2} [inst_1 : SMul M α] [IsIsometricSMul M α] (c : M) (x : α)
  (s : Set α), Metric.infEDist (c • x) (c • s) = Metric.infEDist x s
-- Init.Data.Nat.ToString
/-- Transforms a list of characters into a natural number, *assuming that all characters are in the
range from `'0'` to `'9'`*.
 -/
Nat.ofDigitChars : ℕ → List Char → ℕ → ℕ
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.liftHom₂_congr : ∀ {B : Type u₁} [inst : Quiver B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] (F : B ⥤q C)
  {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} {η θ : CategoryTheory.FreeBicategory.Hom₂ f g},
  CategoryTheory.FreeBicategory.Rel η θ →
    CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.genWrapper.build.eq_def : ∀ (declName : Lean.Name) (i : ℕ) (argSpec : Array Lean.Doc.ArgSpec✝) (args : Array Lean.Expr) (body : Option Lean.Expr),
  Lean.Doc.genWrapper.build✝ declName i argSpec args body =
    if h : i < argSpec.size then
      match argSpec[i] with
      | Lean.Doc.ArgSpec.positional✝ name type => do
        let arg ← Lean.Meta.mkAppOptM `Lean.Doc.getPositional #[some type, none, some (Lean.toExpr name)]
        let k ←
          Lean.Meta.withLocalDecl name Lean.BinderInfo.default type fun v => do
              let __do_lift ← Lean.Doc.genWrapper.build✝ declName (i + 1) argSpec (args.push v) body
              Lean.Meta.mkLambdaFVars #[v] __do_lift
        Lean.Meta.mkAppM `Bind.bind #[arg, k]
      | Lean.Doc.ArgSpec.named✝ name type default => do
        let arg ← Lean.Meta.mkAppOptM `Lean.Doc.getNamed #[some type, none, some (Lean.toExpr name), some default]
        let k ←
          Lean.Meta.withLocalDecl name Lean.BinderInfo.default type fun v => do
              let __do_lift ← Lean.Doc.genWrapper.build✝ declName (i + 1) argSpec (args.push v) body
              Lean.Meta.mkLambdaFVars #[v] __do_lift
        Lean.Meta.mkAppM `Bind.bind #[arg, k]
      | Lean.Doc.ArgSpec.many✝ name type => do
        let arg ← Lean.Meta.mkAppOptM `Lean.Doc.getMany #[some type, none, some (Lean.toExpr name)]
        let __do_lift ← Lean.Meta.mkAppM `Array #[type]
        let k ←
          Lean.Meta.withLocalDecl name Lean.BinderInfo.default __do_lift fun v => do
              let __do_lift ← Lean.Doc.genWrapper.build✝ declName (i + 1) argSpec (args.push v) body
              Lean.Meta.mkLambdaFVars #[v] __do_lift
        Lean.Meta.mkAppM `Bind.bind #[arg, k]
      | Lean.Doc.ArgSpec.flag✝ name default => do
        let arg ← Lean.Meta.mkAppM `Lean.Doc.getFlag #[Lean.toExpr name, Lean.toExpr default]
        let k ←
          Lean.Meta.withLocalDecl name Lean.BinderInfo.default (Lean.Expr.const `Bool []) fun v => do
              let __do_lift ← Lean.Doc.genWrapper.build✝ declName (i + 1) argSpec (args.push v) body
              Lean.Meta.mkLambdaFVars #[v] __do_lift
        Lean.Meta.mkAppM `Bind.bind #[arg, k]
    else do
      let last ← Lean.Meta.mkAppM `Lean.Doc.done #[]
      let __do_lift ← Lean.Meta.mkListLit (Lean.Expr.const `Lean.SyntaxNodeKind []) [Lean.toExpr `doc_arg]
      let __do_lift ← Lean.Meta.mkAppM `Lean.TSyntax #[__do_lift]
      let __do_lift ← Lean.Meta.mkAppM `Array #[__do_lift]
      let __do_lift_1 ← Lean.Meta.mkAppM `Lean.Doc.DocM #[]
      let m ← Lean.Meta.mkAppM `StateT #[__do_lift, __do_lift_1]
      let __do_lift ← Lean.Elab.Term.mkFreshBinderName
      let k ←
        Lean.Meta.withLocalDecl __do_lift Lean.BinderInfo.default (Lean.Expr.const `Unit []) fun u =>
            have args := (Option.map (fun x => args.push x) body).getD args;
            do
            let __do_lift ← Lean.Meta.mkAppM declName args
            let __do_lift ← Lean.Meta.mkAppOptM `liftM #[none, some m, none, none, some __do_lift]
            Lean.Meta.mkLambdaFVars #[u] __do_lift
      Lean.Meta.mkAppM `Bind.bind #[last, k]
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countableOrCountablyGenerated_right_of_prod_left_of_nonempty : ∀ {β : Type u_2} {α : Type u_3} {γ : Type u_4} [inst : MeasurableSpace γ] [Nonempty α]
  [h : MeasurableSpace.CountableOrCountablyGenerated (α × β) γ], MeasurableSpace.CountableOrCountablyGenerated β γ
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- Embedding of the complete graph on `ι` into `completeMultipartiteGraph` on `ι` nonempty parts  -/
SimpleGraph.completeMultipartiteGraph.topEmbedding : {ι : Type u_3} → (V : ι → Type u_4) → ((i : ι) → V i) → ⊤ ↪g SimpleGraph.completeMultipartiteGraph V
-- Mathlib.Algebra.Opposites
/-- A recursor for `MulOpposite`. Use as `induction x`.  -/
MulOpposite.rec' : {α : Type u_1} → {F : αᵐᵒᵖ → Sort u_3} → ((X : α) → F (MulOpposite.op X)) → (X : αᵐᵒᵖ) → F X
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_right_closedEBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x + a) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (b - a) r
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift.0.Std.IterM.step_uLift.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a b : α},
  a ≤ b → ¬IsMin a → insert a (Set.Ioc a b) = Set.Ioc (a - 1) b
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Ioo : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.succ (Finset.Ioo i j) = Finset.Ioo i.succ j.succ
-- Mathlib.Condensed.Discrete.LocallyConstant
Function.Fiber.mk.eq_1 : ∀ {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y), Function.Fiber.mk f y = ⟨f ⁻¹' {f y}, ⋯⟩
-- Mathlib.Data.Multiset.Filter
Multiset.of_mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α}, a ∈ Multiset.filter p s → p a
-- Init.Data.Array.Lemmas
Array.size_eq_zero_iff : ∀ {α : Type u_1} {xs : Array α}, xs.size = 0 ↔ xs = #[]
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.comap_comap : ∀ {R : Type u_2} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid O] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R O] (g : N →ₗ[R] O) (f : M →ₗ[R] N) (C : ConvexCone R O),
  ConvexCone.comap f (ConvexCone.comap g C) = ConvexCone.comap (g ∘ₗ f) C
-- Std.Sync.Notify
Std.Notify.Consumer.normal.injEq : ∀ {α : Type} (promise promise_1 : IO.Promise α),
  (Std.Notify.Consumer.normal promise = Std.Notify.Consumer.normal promise_1) = (promise = promise_1)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `t : LeftExtension f (g ≫ 𝟙 c)` is a Kan extension, then `t.ofCompId : LeftExtension f g`
is also a Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.ofCompId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (t :
              CategoryTheory.Bicategory.LeftExtension f
                (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c))) →
            t.IsKan → t.ofCompId.IsKan
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionCore : Lean.Name → Lean.MetaM Unit