mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_map_left_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y) (X_1 : D),
  ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).map φ).left.app X_1 = φ.left.app (G.obj X_1)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_3.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : Std.DHashMap.Internal.AssocList α β → δ → Sort u_3)
  (acc : δ) (h_1 : (acc : δ) → motive Std.DHashMap.Internal.AssocList.nil acc)
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DHashMap.Internal.AssocList α β) →
          (acc : δ) → motive (Std.DHashMap.Internal.AssocList.cons k v t) acc),
  (match Std.DHashMap.Internal.AssocList.nil, acc with
    | Std.DHashMap.Internal.AssocList.nil, acc => h_1 acc
    | Std.DHashMap.Internal.AssocList.cons k v t, acc => h_2 k v t acc) =
    h_1 acc
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Wedge.ext_inv_hom : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} {W₁ W₂ : CategoryTheory.Limits.Wedge F}
  (e : W₁.pt ≅ W₂.pt)
  (he :
    autoParam
      (∀ (j : J),
        CategoryTheory.Limits.Multifork.ι W₁ j =
          CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.Limits.Multifork.ι W₂ j))
      CategoryTheory.Limits.Wedge.ext._auto_1),
  (CategoryTheory.Limits.Wedge.ext e he).inv.hom = e.inv
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- An induction principle for reasoning about objects in `SimplexCategoryGenRel`. This should be
used instead of identifying an object with `mk` of its `len`.  -/
SimplexCategoryGenRel.rec : {P : SimplexCategoryGenRel → Sort u_1} → ((n : ℕ) → P (SimplexCategoryGenRel.mk n)) → (x : SimplexCategoryGenRel) → P x
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- Any two `IsKleinFour` groups are isomorphic.  -/
IsKleinFour.nonempty_mulEquiv : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [IsKleinFour G₁] [IsKleinFour G₂],
  Nonempty (G₁ ≃* G₂)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.adjoin_le_equalizer : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ₁ φ₂ : A →ₐ[R] B) {s : Set A},
  Set.EqOn (⇑φ₁) (⇑φ₂) s → Algebra.adjoin R s ≤ φ₁.equalizer φ₂
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquivKer.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a : α),
  f.fiberEquivKer a = (Equiv.setCongr ⋯).trans (AddSubgroup.leftCosetEquivAddSubgroup a)
-- Std.Time.DateTime.PlainDateTime
/-- The `Date` component of a `PlainDate`
 -/
Std.Time.PlainDateTime.date : Std.Time.PlainDateTime → Std.Time.PlainDate
-- Mathlib.Data.List.Sort
List.length_insertionSort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (l : List α), (List.insertionSort r l).length = l.length
-- Mathlib.Algebra.Symmetrized
SymAlg.addGroup : {α : Type u_1} → [AddGroup α] → AddGroup αˢʸᵐ
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Poly.denoteN.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.add k v p with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_2 k v p
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.smulCommClass_right : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {X : Type u_4} {Y : Type u_5}
  [inst_3 : SMul X Y] [inst_4 : SMul L Y] [SMulCommClass X L Y] (F : IntermediateField K L), SMulCommClass X (↥F) Y
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.instSubsingletonDiscreteHom : ∀ {α : Type u₁} (X Y : CategoryTheory.Discrete α), Subsingleton (X ⟶ Y)
-- Mathlib.CategoryTheory.GlueData
/-- (Implementation detail) the constructed `GlueData.f` from a `GlueData'`.  -/
CategoryTheory.GlueData'.f' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (D : CategoryTheory.GlueData' C) → (i j : D.J) → (if h : i = j then D.U i else D.V i j h) ⟶ D.U i
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv_counitIso : ∀ {V : Type u'} [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {W : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} W] [inst_3 : CategoryTheory.MonoidalCategory W]
  (F : CategoryTheory.Functor V W) [inst_4 : F.LaxMonoidal] (D : Type u) [inst_5 : CategoryTheory.EnrichedCategory V D]
  (e :
    (v : V) →
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v))
  (h :
    ∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
      (e v) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)),
  (CategoryTheory.TransportEnrichment.forgetEnrichmentEquiv F D e h).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse F D e h).comp
                (CategoryTheory.TransportEnrichment.forgetEnrichmentEquivFunctor F D e h)).obj
            x))
      ⋯
-- Mathlib.Topology.Sheaves.Abelian
/-- The stalk functor is additive  -/
TopCat.instAdditivePresheafStalkFunctor : ∀ {X : TopCat} (p₀ : ↑X) {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasColimits C], (TopCat.Presheaf.stalkFunctor C p₀).Additive
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ M.mulVec 1 = 1 ∧ Matrix.vecMul 1 M = 1
-- Mathlib.Data.Stream.Init
Stream'.even_cons_cons : ∀ {α : Type u} (a₁ a₂ : α) (s : Stream' α), (Stream'.cons a₁ (Stream'.cons a₂ s)).even = Stream'.cons a₁ s.even
-- Mathlib.Control.Traversable.Basic
/-- The function commuting a traversable functor `t` with an arbitrary applicative functor `m`.  -/
Traversable.traverse : {t : Type u → Type u} →
  [self : Traversable t] → {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t α → m (t β)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.log : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.log (f x)
-- Mathlib.Data.Finset.Sups
Finset.sups_sups_sups_comm : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t u v : Finset α),
  s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v)
-- Mathlib.Tactic.DefEqTransformations
/-- `beta_reduce at loc` completely beta reduces the given location.
This also exists as a `conv`-mode tactic.

This means that whenever there is an applied lambda expression such as
`(fun x => f x) y` then the argument is substituted into the lambda expression
yielding an expression such as `f y`.
 -/
Mathlib.Tactic.betaReduceStx : Lean.ParserDescr
-- Mathlib.Topology.Bases
IsOpenMap.separableSpace_of_isInducing : ∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β] [TopologicalSpace.SeparableSpace β]
  {f : α → β}, IsOpenMap f → Topology.IsInducing f → TopologicalSpace.SeparableSpace α
-- Init.Data.String.FindPos
/-- Iterates `p.prev` `n` times.

If this would move `p` past the start of `s`, the result is `s.endPos`.
 -/
String.Slice.Pos.prevn : {s : String.Slice} → s.Pos → ℕ → s.Pos
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_iff_bddBelow_bddAbove : ∀ {α : Type u_3} {s : Set α} [Nonempty α] [inst : Lattice α] [LocallyFiniteOrder α], s.Finite ↔ BddBelow s ∧ BddAbove s
-- Mathlib.Analysis.Real.Cardinality
/-- The cardinality of the interval $[a, b)$.  -/
Cardinal.mk_Ico_real : ∀ {a b : ℝ}, a < b → Cardinal.mk ↑(Set.Ico a b) = Cardinal.continuum
-- Mathlib.Algebra.Free
FreeSemigroup.instMonad.eq_1 : FreeSemigroup.instMonad =
  { map := fun {α β} f x => (fun {α β} x f => (FreeSemigroup.lift f) x) x ((fun {α} => FreeSemigroup.of) ∘ f),
    pure := fun {α} => FreeSemigroup.of,
    seq := fun {α β} f x =>
      (fun {α β} x f => (FreeSemigroup.lift f) x) f fun y =>
        (fun {α β} x f => (FreeSemigroup.lift f) x) (x ()) ((fun {α} => FreeSemigroup.of) ∘ y),
    seqLeft := fun {α β} x y =>
      (fun {α β} x f => (FreeSemigroup.lift f) x) x fun a =>
        (fun {α β} x f => (FreeSemigroup.lift f) x) (y ()) fun x => (fun {α} => FreeSemigroup.of) a,
    seqRight := fun {α β} x y => (fun {α β} x f => (FreeSemigroup.lift f) x) x fun x => y (),
    bind := fun {α β} x f => (FreeSemigroup.lift f) x }
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
/-- Given two composable morphisms `f` and `g` in the category of cochain complexes,
this is the `homotopyInvHomId` field of the homotopy equivalence
`mappingConeCompHomotopyEquiv f g` between `mappingCone g` and the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`.  -/
CochainComplex.MappingConeCompHomotopyEquiv.homotopyInvHomId : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ X₃ : CochainComplex C ℤ} →
          (f : X₁ ⟶ X₂) →
            (g : X₂ ⟶ X₃) →
              Homotopy
                (CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.inv f g)
                  (CochainComplex.MappingConeCompHomotopyEquiv.hom f g))
                (CategoryTheory.CategoryStruct.id
                  (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁))
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith.disjoint_iff_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {w w' : α × Bool},
  Disjoint (FreeGroup.startsWith w) (FreeGroup.startsWith w') ↔ w ≠ w'
-- Init.Grind.Ring.Basic
/-- Numerals are consistently defined with respect to addition.  -/
Lean.Grind.Semiring.ofNat_succ : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : ℕ), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.range_weylGroupToPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.weylGroupToPerm.range = Subgroup.closure (Set.range P.reflectionPerm)
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} (x : E),
  f.normed μ (c - x) = f.normed μ (c + x)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The presentation of `UniversalFactorizationRing`.
Its jacobian is the resultant of the two factors (up to sign).  -/
Polynomial.UniversalFactorizationRing.presentation : {R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Algebra.PreSubmersivePresentation R (Polynomial.UniversalFactorizationRing m k hn p) (Fin m ⊕ Fin k) (Fin n)
-- Mathlib.Data.Num.Basic
instOneNum : One Num
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff! m₂).getKey? k = none
-- Std.Internal.UV.UDP
/-- Sets the time-to-live (TTL) value for multicast packets.
 -/
Std.Internal.UV.UDP.Socket.setMulticastTTL : Std.Internal.UV.UDP.Socket → UInt32 → IO Unit
-- Std.Time.DateTime.PlainDateTime
/-- Adds a `Month.Offset` to a `PlainDateTime`, rolling over excess days to the following month if needed.
 -/
Std.Time.PlainDateTime.addMonthsRollOver : Std.Time.PlainDateTime → Std.Time.Month.Offset → Std.Time.PlainDateTime
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Pythagorean theorem, if-and-if vector inner product form using square roots.  -/
norm_add_eq_sqrt_iff_real_inner_eq_zero : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x y : F},
  ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ inner ℝ x y = 0
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.instMonoidalFunctorInverseCongrLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u_1) →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
            [inst_3 : CategoryTheory.MonoidalCategory E] → (e : C ≌ D) → e.congrLeft.inverse.Monoidal
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_of_mem_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  a ∈ m.erase k → a ∈ m
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ (X₃ ⊗ X₁) ⊗ X₂`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).getKeyD k fallback =
    if (f (Std.DTreeMap.Const.get? t k)).isSome = true then k else fallback
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : SizeOf C]
  (coverings : (X : C) → Set (CategoryTheory.Presieve X)), sizeOf { coverings := coverings } = 1
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The pullback of two morphisms `f,g` in `CompHaus`, constructed explicitly as the set of
pairs `(x,y)` such that `f x = g y`, with the topology induced by the product.
 -/
CompHausLike.pullback : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} → (f : X ⟶ B) → (g : Y ⟶ B) → [CompHausLike.HasExplicitPullback f g] → CompHausLike P
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_inj : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R), Polynomial.toLaurent f = Polynomial.toLaurent g ↔ f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.map_interval : ∀ {n : ℕ} {X Y : SSet.Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (j l : ℕ) (h : j + l ≤ m),
  (f.map σ).interval j l h = (f.interval j l h).map σ
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)}
  {app : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X}
  {dinaturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
            (CategoryTheory.CategoryStruct.comp (app X) ((G.obj (Opposite.op X)).map f)) =
          CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
            (CategoryTheory.CategoryStruct.comp (app Y) ((G.map f.op).app Y)))
      CategoryTheory.DinatTrans.dinaturality._autoParam}
  {app_1 : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X}
  {dinaturality_1 :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
            (CategoryTheory.CategoryStruct.comp (app_1 X) ((G.obj (Opposite.op X)).map f)) =
          CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
            (CategoryTheory.CategoryStruct.comp (app_1 Y) ((G.map f.op).app Y)))
      CategoryTheory.DinatTrans.dinaturality._autoParam},
  { app := app, dinaturality := dinaturality } = { app := app_1, dinaturality := dinaturality_1 } → app = app_1
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.isLeadingEntry : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n} [inst_1 : LT m]
  [inst_2 : LT n] {i : m} {c : n}, A.IsPivotedBy l → l i = ↑c → A.IsLeadingEntry i c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF)
  {h' : k ∈ (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl},
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.get k h' = t.get k ⋯
-- Mathlib.Analysis.Normed.Group.BallSphere
/-- We equip the sphere, in a seminormed group, with a formal operation of negation, namely the
antipodal map.  -/
instInvolutiveNegElemSphereOfNat : {E : Type u_1} → [i : SeminormedAddCommGroup E] → {r : ℝ} → InvolutiveNeg ↑(Metric.sphere 0 r)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The function obtained by "multiplying away" the pole of `L χ` for a trivial Dirichlet
character `χ`. Its (negative) logarithmic derivative is used to prove Dirichlet's Theorem
on primes in arithmetic progression.  -/
DirichletCharacter.LFunctionTrivChar₁ : (n : ℕ) → [NeZero n] → ℂ → ℂ
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.mk.sizeOf_spec : ∀ (eq : Bool) (lhs rhs : Nat.Internal.Linear.Poly),
  sizeOf { eq := eq, lhs := lhs, rhs := rhs } = 1 + sizeOf eq + sizeOf lhs + sizeOf rhs
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.eq_def : ∀ (cfg : Lean.Meta.Tactic.Backtrack.BacktrackConfig) (trace : optParam Lean.Name Lean.Name.anonymous)
  (next : Lean.MVarId → (List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Lean.MetaM (List Lean.MVarId))
  (goals : List Lean.MVarId) (n : ℕ) (curr acc : List Lean.MVarId),
  Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals n curr acc =
    match n with
    | 0 => Lean.throwError (Lean.toMessageData "Backtrack exceeded the recursion limit")
    | n.succ => do
      let procResult? ←
        tryCatch (cfg.proc goals curr) fun e =>
            Lean.withTraceNode trace
              (fun x => pure (Lean.toMessageData "BacktrackConfig.proc failed: " ++ Lean.toMessageData e.toMessageData))
              (throw e)
      match procResult? with
        | some curr' => Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals n curr' acc
        | none =>
          match curr with
          | [] => Lean.withTraceNode trace (fun x => pure (Lean.toMessageData "success!")) (pure acc.reverse)
          | g :: gs => do
            let __do_lift ← g.isAssigned
            if __do_lift = true then
                Lean.withTraceNode trace
                  (fun x => pure (Lean.toMessageData "discarding already assigned goal " ++ Lean.toMessageData g))
                  (Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals (n + 1) gs acc)
              else
                Lean.withTraceNode trace
                  (fun x => do
                    let __do_lift ← Lean.addMessageContextFull (Lean.MessageData.ofGoal g)
                    pure (Lean.toMessageData "working on: " ++ Lean.toMessageData __do_lift))
                  do
                  let __do_lift ← cfg.suspend g
                  if __do_lift = true then
                      Lean.withTraceNode trace
                        (fun x => pure (Lean.toMessageData "⏸️ suspending search and returning as subgoal"))
                        (Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals (n + 1) gs (g :: acc))
                    else
                      tryCatch
                        (next g fun r =>
                          Lean.observing?
                            (Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals n (r ++ gs) acc))
                        fun x => do
                        let __do_lift ← cfg.discharge g
                        match __do_lift with
                          | none =>
                            Lean.withTraceNode trace
                              (fun x => pure (Lean.toMessageData "⏭️ deemed acceptable, returning as subgoal"))
                              (Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals (n + 1) gs (g :: acc))
                          | some l =>
                            Lean.withTraceNode trace
                              (fun x => pure (Lean.toMessageData "⏬ discharger generated new subgoals"))
                              (Lean.Meta.Tactic.Backtrack.Backtrack.run✝ cfg trace next goals n (l ++ gs) acc)
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.instHasDimensionLETensorObjObjSimplexCategoryStdSimplexMkHAddNat : ∀ {p q : ℕ},
  (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
        (SSet.stdSimplex.obj { len := q })).HasDimensionLE
    (p + q)
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal_toSubtype' : ∀ {n : ℕ} {α : TypeVec.{u_1} n} (r : (α.prod α).Arrow (TypeVec.repeat n Prop)),
  TypeVec.comp (TypeVec.subtypeVal r) (TypeVec.toSubtype' r) = fun i x => TypeVec.prod.mk i (↑x).1 (↑x).2
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.ext_iff : ∀ {L : Type u_1} {x y : LeftPreLieRing L},
  x = y ↔
    Add.add = Add.add ∧
      Zero.zero = Zero.zero ∧
        NSMul.nsmul = NSMul.nsmul ∧
          Neg.neg = Neg.neg ∧ Sub.sub = Sub.sub ∧ ZSMul.zsmul = ZSMul.zsmul ∧ Mul.mul = Mul.mul
-- ProofWidgets.Presentation.Expr
_private.ProofWidgets.Presentation.Expr.0.ProofWidgets.getExprPresentations.addPresenterIfApplicable : ProofWidgets.ExprWithCtx →
  Lean.Name → Array ProofWidgets.ExprPresentationData → Lean.Server.RequestM (Array ProofWidgets.ExprPresentationData)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.splitMono.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  h.splitMono = { retraction := h.r, id := ⋯ }
-- Mathlib.Data.EReal.Inv
EReal.inv_inv : ∀ {a : EReal}, a ≠ ⊥ → a ≠ ⊤ → a⁻¹⁻¹ = a
-- Mathlib.Algebra.Group.Hom.Defs
/-- Additive group homomorphisms preserve subtraction.  -/
AddMonoidHom.map_sub : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β] (f : α →+ β) (g h : α),
  f (g - h) = f g - f h
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.map_mk'_self : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], AddSubgroup.map (QuotientAddGroup.mk' N) N = ⊥