mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Quot
/-- Recursion on a `Quotient` argument `a`, result type depends on `⟦a⟧`.  -/
Quotient.hrecOn' : {α : Sort u_1} →
  {s₁ : Setoid α} →
    {φ : Quotient s₁ → Sort u_5} →
      (qa : Quotient s₁) → (f : (a : α) → φ (Quotient.mk'' a)) → (∀ (a₁ a₂ : α), a₁ ≈ a₂ → f a₁ ≍ f a₂) → φ qa
-- Init.Data.String.Basic
String.instDecidableIsValid : {s : String} → {p : String.Pos.Raw} → Decidable (String.Pos.Raw.IsValid s p)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D)
  [inst_4 : ∀ (A B : C), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F],
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatIso F).inv =
    CategoryTheory.inv (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Composing any `V`-enriched functor with the identity functor is isomorphic to the former
functor.  -/
CategoryTheory.EnrichedCat.rightUnitor : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₁} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              (F : CategoryTheory.EnrichedFunctor V C D) →
                CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.id V D) ≅ F
-- Mathlib.RingTheory.PrincipalIdealDomain
isPrincipalIdealRing_prod_iff : ∀ {R : Type u} {S : Type u_1} [inst : Semiring R] [inst_1 : Semiring S],
  IsPrincipalIdealRing (R × S) ↔ IsPrincipalIdealRing R ∧ IsPrincipalIdealRing S
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ico_eq_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → Set.Iic a ∪ Set.Ico a b = Set.Iio b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.congr_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.DHashMap α β},
  m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.abs_arg_inv : ∀ (x : ℂ), |x⁻¹.arg| = |x.arg|
-- Std.Time.Format.Modifier
Std.Time.Modifier.A.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.A presentation = Std.Time.Modifier.A presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.bound : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G), ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.Algebra.Group.Even
IsSquare.one : ∀ {α : Type u_2} [inst : MulOneClass α], IsSquare 1
-- Mathlib.Probability.Moments.ComplexMGF
ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ),
      HasDerivAt (iteratedDeriv n (ProbabilityTheory.complexMGF X μ))
        (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * Complex.exp (z * ↑(X ω))) x ∂μ) z
-- Lean.MetavarContext
Lean.isLevelMVarAssignable : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.LMVarId → m Bool
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_map_toListRev : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.drain = (fun x => PUnit.unit) <$> it.toListRev
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ), sq.unop.f₁₂ = sq.f₂₄.unop
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (Q H : C) (p : S.X₂ ⟶ Q) (ι : H ⟶ Q)
  (wp : CategoryTheory.CategoryStruct.comp S.f p = 0)
  (hp : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p wp))
  (wι : CategoryTheory.CategoryStruct.comp ι (hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0)
  (hι : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι wι)) (Q_1 H_1 : C) (p_1 : S.X₂ ⟶ Q_1)
  (ι_1 : H_1 ⟶ Q_1) (wp_1 : CategoryTheory.CategoryStruct.comp S.f p_1 = 0)
  (hp_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p_1 wp_1))
  (wι_1 : CategoryTheory.CategoryStruct.comp ι_1 (hp_1.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) = 0)
  (hι_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι_1 wι_1)),
  ({ Q := Q, H := H, p := p, ι := ι, wp := wp, hp := hp, wι := wι, hι := hι } =
      { Q := Q_1, H := H_1, p := p_1, ι := ι_1, wp := wp_1, hp := hp_1, wι := wι_1, hι := hι_1 }) =
    (Q = Q_1 ∧ H = H_1 ∧ p ≍ p_1 ∧ ι ≍ ι_1 ∧ hp ≍ hp_1 ∧ hι ≍ hι_1)
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.MVarErrorInfo.logError.appendExtra : Option Lean.MessageData → Lean.MessageData → Lean.MessageData
-- Mathlib.RingTheory.Ideal.Quotient.Basic
Ideal.Quotient.mk_span_range : ∀ {ι : Type u_1} {R : Type u_3} [inst : Ring R] (f : ι → R) [inst_1 : (Ideal.span (Set.range f)).IsTwoSided] (i : ι),
  (Ideal.Quotient.mk (Ideal.span (Set.range f))) (f i) = 0
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRioSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRioSlice._auto_1) →
    Std.Rio.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RioSlice α)
-- Mathlib.Order.Interval.Finset.Nat
Nat.uIcc_eq_range' : ∀ (a b : ℕ), Finset.uIcc a b = { val := ↑(List.range' (min a b) (max a b + 1 - min a b)), nodup := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The canonical isomorphism `W ⨿[Y] (Y ⨿[X] Z) ≅ W ⨿[X] Z`  -/
CategoryTheory.Limits.pushoutRightPushoutInlIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (f' : Y ⟶ W) →
            [inst_1 : CategoryTheory.Limits.HasPushout f g] →
              [inst_2 : CategoryTheory.Limits.HasPushout f' (CategoryTheory.Limits.pushout.inl f g)] →
                CategoryTheory.Limits.pushout f' (CategoryTheory.Limits.pushout.inl f g) ≅
                  CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp f f') g
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given an `AddCommMonoid` homomorphism `g : M →+ P` where for AddSubmonoids `S ⊆ M, T ⊆ P` we
have `g(S) ⊆ T`, the induced AddMonoid homomorphism from the Localization of `M` at `S` to the
Localization of `P` at `T`: if `f : M →+ N` and `k : P →+ Q` are Localization maps for `S` and
`T` respectively, we send `z : N` to `k (g x) - k (g y)`, where `(x, y) : M × S` are such
that `z = f x - f y`.  -/
AddSubmonoid.LocalizationMap.map : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {N : Type u_2} →
        [inst_1 : AddCommMonoid N] →
          {P : Type u_3} →
            [inst_2 : AddCommMonoid P] →
              S.LocalizationMap N →
                {g : M →+ P} →
                  {T : AddSubmonoid P} →
                    (∀ (y : ↥S), g ↑y ∈ T) → {Q : Type u_4} → [inst : AddCommMonoid Q] → T.LocalizationMap Q → N →+ Q
-- Mathlib.Data.Int.Log
Int.log_zero_left : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] (r : R), Int.log 0 r = 0
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.coeff_toMultiplicativeBialgEquiv_apply : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : AddMonoid M] (a : AddMonoidAlgebra A M),
  ((AddMonoidAlgebra.toMultiplicativeBialgEquiv R A M) a).coeff = Finsupp.mapDomain (⇑Multiplicative.ofAdd) a.coeff
-- Mathlib.CategoryTheory.Shift.InducedShiftSequence
CategoryTheory.Functor.ShiftSequence.induced_shiftMap : ∀ {C : Type u_1} {D : Type u_2} {A : 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} A]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D A} {G : CategoryTheory.Functor C A} (e : L.comp F ≅ G)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : G.ShiftSequence M]
  (F' : M → CategoryTheory.Functor D A) (e' : (m : M) → L.comp (F' m) ≅ G.shift m)
  [inst_6 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Full]
  [inst_7 : ((CategoryTheory.Functor.whiskeringLeft C D A).obj L).Faithful] [inst_8 : CategoryTheory.HasShift D M]
  [inst_9 : L.CommShift M] {n : M} {X Y : C} (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (a a' : M)
  (h : n + a = a'),
  F.shiftMap (CategoryTheory.CategoryStruct.comp (L.map f) ((CategoryTheory.Functor.commShiftIso L n).hom.app Y)) a a'
      h =
    CategoryTheory.CategoryStruct.comp ((e' a).hom.app X)
      (CategoryTheory.CategoryStruct.comp (G.shiftMap f a a' h) ((e' a').inv.app Y))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_top_const : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  (c : E), MeasureTheory.MemLp (fun x => c) ⊤ μ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If `i = i'` and `j = j'` this is the isomorphism between the `1`-component at
`congrIndexOneOfEq k : E.I₁ i' j'` and the `1`-component at `k : E.I₁ i j`.

Note: This isomorphism could also be constructed inline from `eqToIso`. We only
use `eqToIso` directly to construct isomorphisms `E.Y k ≅ E.Y k'` where `k k' : E.I₁ i j`
and whenever `k : E.I₁ i j` and `k' : E.I₁ i' j'` have to be related we use `congrIndexOneOfEqIso`,
possibly combined with an additional `eqToIso` instead. The reason for this is
that the lemmas around `eqToHom_naturality` are hard to apply in the case where there is a
mismatch in the type of the index.
 -/
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {i i' j j' : E.I₀} →
          (hii' : i = i') →
            (hjj' : j = j') →
              (k : E.I₁ i j) → E.Y ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k) ≅ E.Y k
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getHSMulIntFn? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_empty : ∀ {α : Type u_1} [inst : EDist α], ∅.infsep = 0
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toRingEquiv_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] [inst_3 : Mul β] [inst_4 : Add β]
  [inst_5 : LE β] (f : α ≃+*o β), f.toRingEquiv = f.toRingEquiv
-- Mathlib.Algebra.RingQuot
RingQuot.smul_quot : ∀ {R : Type uR} [inst : Semiring R] {S : Type uS} [inst_1 : CommSemiring S] (r : R → R → Prop) [inst_2 : Algebra S R]
  {n : S} {a : R}, n • { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (n • a) }
-- Mathlib.Topology.UnitInterval
unitInterval.instConnectedSpaceElemReal : ConnectedSpace ↑unitInterval
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.hom_ext' : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y) {T : H} {f g : (CategoryTheory.StructuredArrow.right E).obj Y ⟶ T},
  (∀ ⦃X : C⦄ (φ : L.obj X ⟶ Y),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map φ) f) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map φ) g)) →
    f = g
-- Batteries.Data.List.Lemmas
List.findIdxNth_cons_zero_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} {a : α}, p a = true → List.findIdxNth p (a :: xs) 0 = 0
-- Lean.Data.Json.Basic
Lean.JsonNumber : Type
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.map_integerMultiple : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S) (i : ↥s),
  (algebraMap R S) (IsLocalization.integerMultiple M s f i) = IsLocalization.commonDenom M s f • f ↑i
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_ciSup_eq_right : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrderBot α] {b : β} {f : (x : β) → b = x → α},
  ⨆ x, ⨆ (h : b = x), f x h = f b ⋯
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.comp_liftCycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : A ⟶ S.X₂) (hk : CategoryTheory.CategoryStruct.comp k S.g = 0)
  [inst_2 : S.HasLeftHomology] {A' : C} (α : A' ⟶ A) {Z : C} (h : S.cycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp α (CategoryTheory.CategoryStruct.comp (S.liftCycles k hk) h) =
    CategoryTheory.CategoryStruct.comp (S.liftCycles (CategoryTheory.CategoryStruct.comp α k) ⋯) h
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.SpecMap_ΓSpecIso_inv_toSpecΓ : ∀ (R : CommRingCat),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv)
      (AlgebraicGeometry.Spec R).toSpecΓ =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤)))
-- Init.Data.Array.Attach
Array.pmap_append : ∀ {ι : Type u_1} {α : Type u_2} {p : ι → Prop} {f : (a : ι) → p a → α} {xs ys : Array ι} (h : ∀ a ∈ xs ++ ys, p a),
  Array.pmap f (xs ++ ys) h = Array.pmap f xs ⋯ ++ Array.pmap f ys ⋯
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_def`. -/
dvd_iff_exists_eq_mul_right : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b ↔ ∃ c, b = a * c
-- Mathlib.Order.RelIso.Basic
RelIso.preimage_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : β → β → Prop) (a : α), (RelIso.preimage f s) a = f a
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.onIocAux.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {G : Type u_3} [inst_1 : AddCommGroup G] (f : α → G) (s : Set α),
  MeasureTheory.AddContent.onIocAux f s =
    if h : ∃ p, p.1 ≤ p.2 ∧ s = Set.Ioc p.1 p.2 then f h.choose.2 - f h.choose.1 else 0
-- Mathlib.LinearAlgebra.Matrix.Cartan
/-- The Cartan matrix of type F₄. See [bourbaki1968] plate VIII, page 288.  -/
CartanMatrix.F₄ : Matrix (Fin 4) (Fin 4) ℤ
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.measure_stieltjesOfMeasurableRat_univ : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α),
  (ProbabilityTheory.stieltjesOfMeasurableRat f hf a).measure Set.univ = 1
-- Std.Data.Iterators.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.productiveRel_of_remaining : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [inst : Std.Iterator α m β]
  [inst_1 : Std.Iterators.Productive α m] {it it' : Std.IterM m β},
  it'.internalState.remaining < it.internalState.remaining → Std.Iterators.Types.Drop.ProductiveRel✝ m it' it
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
/-- A set of vertices represents a set of components if it contains exactly one vertex from
each component.  -/
SimpleGraph.ConnectedComponent.Represents : {V : Type u} → {G : SimpleGraph V} → Set V → Set G.ConnectedComponent → Prop
-- Std.Data.ExtDTreeMap.Basic
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.ExtDTreeMap.alter : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] →
        [Std.LawfulEqCmp cmp] →
          Std.ExtDTreeMap α β cmp → (a : α) → (Option (β a) → Option (β a)) → Std.ExtDTreeMap α β cmp
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α} {k : α}
  {fallback : Unit},
  Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)) k fallback = ()
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.mkTermContext : Lean.Elab.Command.Context → Lean.Elab.Command.State → Lean.Elab.Command.CommandElabM Lean.Elab.Term.Context
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) → [ringObj : CategoryTheory.RingObj X] → CategoryTheory.RingObjCat C
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_ne_natCast : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), ⊥ ≠ ↑n
-- Mathlib.Order.Bounds.Image
Monotone.image_lowerBounds_subset_lowerBounds_image : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {s : Set α}, f '' lowerBounds s ⊆ lowerBounds (f '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g' : W ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g) g'] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackLeftPullbackSndIso f g g').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f g) g')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (CategoryTheory.CategoryStruct.comp g' g))
      h
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_adj : ∀ {V : Type u_1} {v w : V} {G : SimpleGraph V} {s : Set (Sym2 V)}, (G.deleteEdges s).Adj v w ↔ G.Adj v w ∧ s(v, w) ∉ s
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.comm₁₂ : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ),
  pres.toExtension.cotangentComplex ∘ₗ Algebra.Presentation.differentials.hom₁ pres =
    ↑pres.cotangentSpaceBasis.repr.symm ∘ₗ pres.differentialsRelations.map
-- Mathlib.Algebra.Group.Conj
AddConjClasses.exists_rep : ∀ {α : Type u} [inst : AddMonoid α] (a : AddConjClasses α), ∃ a0, AddConjClasses.mk a0 = a
-- Init.Data.List.Basic
List.mapTR.loop.eq_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : List β) (a_1 : α) (as : List α),
  List.mapTR.loop f (a_1 :: as) a = List.mapTR.loop f as (f a_1 :: a)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.ofMessage? : Lean.JsonRpc.Message → Option (Lean.JsonRpc.Notification Lean.Json)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {t : Std.DTreeMap.Internal.Impl α β} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forInStep f init t =
    Std.DTreeMap.Internal.Impl.foldlM
      (fun x =>
        match (motive := ForInStep δ → (a : α) → β a → m (ForInStep δ)) x with
        | ForInStep.yield d => fun k v => f k v d
        | ForInStep.done d => fun x x_1 => pure (ForInStep.done d))
      (ForInStep.yield init) t
-- Mathlib.NumberTheory.Height.Basic
Height.AdmissibleAbsValues.mk : {K : Type u_1} →
  [inst : Field K] →
    (archAbsVal : Multiset (AbsoluteValue K ℝ)) →
      (nonarchAbsVal : Set (AbsoluteValue K ℝ)) →
        (∀ v ∈ nonarchAbsVal, IsNonarchimedean ⇑v) →
          (∀ {x : K}, x ≠ 0 → Function.HasFiniteMulSupport fun v => ↑v x) →
            (∀ {x : K}, x ≠ 0 → (Multiset.map (fun x_2 => x_2 x) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ↑v x = 1) →
              Height.AdmissibleAbsValues K
-- Mathlib.Topology.ClusterPt
Filter.HasBasis.clusterPt_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ιX : Sort u_3} {ιF : Sort u_4} {pX : ιX → Prop} {sX : ιX → Set X}
  {pF : ιF → Prop} {sF : ιF → Set X} {F : Filter X},
  (nhds x).HasBasis pX sX →
    F.HasBasis pF sF → (ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty)
-- Mathlib.Data.Finsupp.Defs
Finsupp.embDomain_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_4} [inst : Zero M] (f : α ↪ β) (v : α →₀ M) (b : β),
  (Finsupp.embDomain f v) b = if h : ∃ a, f a = b then v h.choose else 0
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_two_mul_add_one_done : ∀ {n a b n' a' : ℕ}, Mathlib.Meta.NormNum.IsFibAux n a b → 2 * n + 1 = n' → a * a + b * b = a' → Nat.fib n' = a'
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_unitIso_hom_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete (J ⊕ K)),
  CategoryTheory.Discrete.sumEquiv.unitIso.hom.app X =
    (match X.as with
      | Sum.inl x => CategoryTheory.Iso.refl { as := Sum.inl x }
      | Sum.inr x => CategoryTheory.Iso.refl { as := Sum.inr x }).hom
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ},
  R.extEquivCohomologyClass.symm 0 = 0
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
AddEquiv.mk'.congr_simp : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f f_1 : M ≃ N) (e_f : f = f_1)
  (h : ∀ (x y : M), f (x + y) = f x + f y), AddEquiv.mk' f h = AddEquiv.mk' f_1 ⋯
-- Mathlib.Data.Matrix.Mul
Matrix.one_submatrix_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype m] [Finite o]
  [inst_2 : NonAssocSemiring α] [inst_3 : DecidableEq o] (e₁ : l → o) (e₂ : m ≃ o) (M : Matrix m n α),
  Matrix.submatrix 1 e₁ ⇑e₂ * M = M.submatrix (⇑e₂.symm ∘ e₁) id
-- Aesop.Script.Step
Aesop.Script.LazyStep.runFirstSuccessfulTacticBuilder : Aesop.Script.LazyStep → Lean.MetaM Aesop.Script.Tactic
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.congr_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} {d : AddCon N} (e : M ≃+ N)
  (h : c = AddCon.comap ⇑e ⋯ d), (AddCon.congr e h).symm = AddCon.congr e.symm ⋯