mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link_eq_link! : ∀ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced), (Std.DTreeMap.Internal.Impl.link k v l r hlb hrb).impl = Std.DTreeMap.Internal.Impl.link! k v l r
-- Init.Data.List.Basic
List.instAssociativeHAppend : ∀ {α : Type u}, Std.Associative fun x1 x2 => x1 ++ x2
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoFunctorOfIsoInverse_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C),
  i.isoFunctorOfIsoInverse.inv.app X =
    CategoryTheory.CategoryStruct.comp (G'.functor.map (G.unitIso.hom.app X))
      (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.hom.app (G.functor.obj X)))
        (G'.counitIso.hom.app (G.functor.obj X)))
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.associator_inv_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c d : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b)
  (y : b ⟶ c) (z : c ⟶ d),
  (CategoryTheory.Bicategory.associator x y z).inv.iso.inv = (CategoryTheory.Bicategory.associator x.of y.of z.of).hom
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.aemeasurable_limit : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [inst : TopologicalSpace E] [inst_1 : OpensMeasurableSpace E]
  {X : (i : ι) → Ω i → E} {l : Filter ι} {Z : Ω' → E} {μ : (i : ι) → MeasureTheory.Measure (Ω i)}
  [inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {μ' : autoParam (MeasureTheory.Measure Ω') MeasureTheory.TendstoInDistribution._auto_1}
  [inst_3 : MeasureTheory.IsProbabilityMeasure μ'], MeasureTheory.TendstoInDistribution X l Z μ μ' → AEMeasurable Z μ'
-- Mathlib.Data.Fin.Tuple.Take
Fin.take_zero : ∀ {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i), Fin.take 0 ⋯ v = fun i => i.elim0
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.neg : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {L : Filter (E × E)}, HasFDerivAtFilter f f' L → HasFDerivAtFilter (-f) (-f') L
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (d : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X))
  (d_mul :
    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d (a * b) = a • d b + b • d a)
      PresheafOfModules.Derivation.d_mul._autoParam)
  (d_map :
    autoParam
      (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
        d ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) = (CategoryTheory.ConcreteCategory.hom (M.map f)) (d x))
      PresheafOfModules.Derivation.d_map._autoParam)
  (d_app :
    autoParam (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
      PresheafOfModules.Derivation.d_app._autoParam)
  (d_1 : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X))
  (d_mul_1 :
    autoParam (∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), d_1 (a * b) = a • d_1 b + b • d_1 a)
      PresheafOfModules.Derivation.d_mul._autoParam)
  (d_map_1 :
    autoParam
      (∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)),
        d_1 ((CategoryTheory.ConcreteCategory.hom (R.map f)) x) =
          (CategoryTheory.ConcreteCategory.hom (M.map f)) (d_1 x))
      PresheafOfModules.Derivation.d_map._autoParam)
  (d_app_1 :
    autoParam (∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), d_1 ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0)
      PresheafOfModules.Derivation.d_app._autoParam),
  ({ d := d, d_mul := d_mul, d_map := d_map, d_app := d_app } =
      { d := d_1, d_mul := d_mul_1, d_map := d_map_1, d_app := d_app_1 }) =
    (d = d_1)
-- Mathlib.Data.Int.Init
Int.gcd_right_comm : ∀ (a b c : ℤ), (↑(a.gcd b)).gcd c = (↑(a.gcd c)).gcd b
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.traceAtCmdPos : Lean.Name → (Unit → Lean.MessageData) → Lean.Elab.TermElabM Unit
-- Mathlib.Order.BoundedOrder.Basic
ULift.up_top : ∀ {α : Type u} [inst : Top α], { down := ⊤ } = ⊤
-- Mathlib.Data.Set.Semiring
Set.up_mul : ∀ {α : Type u_1} [inst : Mul α] (s t : Set α), Set.up (s * t) = Set.up s * Set.up t
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.copy_eq : ∀ {μ : YoungDiagram} (T : SemistandardYoungTableau μ) (entry' : ℕ → ℕ → ℕ) (h : entry' = ⇑T), T.copy entry' h = T
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit`.
 -/
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
              (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
                (s : CategoryTheory.Limits.Cocone F) →
                  (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ) →
                    s.pt.presheaf.obj U ⟶
                      ((TopCat.Presheaf.pushforward C
                                (CategoryTheory.Limits.colimit.desc
                                  (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
                                  ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj
                            (CategoryTheory.Limits.limit
                              (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp)).obj
                        U
-- Mathlib.Combinatorics.Enumerative.Stirling
Nat.stirlingSecond.eq_def : ∀ (x x_1 : ℕ),
  x.stirlingSecond x_1 =
    match x, x_1 with
    | 0, 0 => 1
    | 0, n.succ => 0
    | n.succ, 0 => 0
    | n.succ, k.succ => (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.map_mul₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : MulOneClass M} {x_1 : MulOneClass N} {x_2 : CommMonoid P}
  (f : M →* N →* P) (m₁ m₂ : M) (n : N), (f (m₁ * m₂)) n = (f m₁) n * (f m₂) n
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_zero : Ordinal.IsInitial 0
-- Mathlib.Data.Finmap
Finmap.insert_insert_of_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {b : β a} {b' : β a'} (s : Finmap β),
  a ≠ a' → Finmap.insert a' b' (Finmap.insert a b s) = Finmap.insert a b (Finmap.insert a' b' s)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yz_succ : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yz a1 (n + 1) = Pell.xz a1 n + Pell.yz a1 n * Pell.az a
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_tdiv : ∀ (a b : ℤ), (a.tdiv b).natAbs = a.natAbs.div b.natAbs
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ico_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Ico (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioc b a)
-- Lean.Elab.Deriving.Basic
Lean.Elab.applyDerivingHandlers : Lean.Name → Array Lean.Name → optParam Bool false → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.Convex.Function
/-- **Alias** of the reverse direction of `neg_concaveOn_iff`.

---

A function `-f` is concave iff `f` is convex.  -/
ConvexOn.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, ConvexOn 𝕜 s f → ConcaveOn 𝕜 s (-f)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.verify₁ : {w : UInt8} → UInt8 → ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done → Bool
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_iff_edist : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  (f : α → β), MeasureTheory.HasFiniteIntegral f μ ↔ ∫⁻ (a : α), edist (f a) 0 ∂μ < ⊤
-- Mathlib.Data.Matrix.Mul
Matrix.semiring : {n : Type u_3} → {α : Type v} → [Semiring α] → [Fintype n] → [DecidableEq n] → Semiring (Matrix n n α)
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Raw.toArray : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → Array ((a : α) × β a)
-- Init.Data.SInt.Bitwise
UInt16.toInt16_not : ∀ (a : UInt16), (~~~a).toInt16 = ~~~a.toInt16
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.not_quotedStringChar_ofNat_aux : ∀ c < 128,
  ¬Std.Http.Internal.Char.qdtext (Char.ofNat c) = true ∧ ¬(Char.ofNat c = '\"' ∨ Char.ofNat c = '\\') →
    ¬Std.Http.Internal.Char.quotedStringChar (Char.ofNat c) = true
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.congr_postcomp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} {N : Type v'} [inst_3 : AddCommGroup N] [inst_4 : Module A N]
  {solution' : relations.Solution M},
  solution = solution' → ∀ (f : M →ₗ[A] N), solution.postcomp f = solution'.postcomp f
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.Bimon C} {f g : X ⟶ Y},
  f = g ↔ f.hom.hom = g.hom.hom
-- Lean.Parser.Extra
Lean.Parser.adaptCacheableContext.formatter : (Lean.Parser.CacheableParserContext → Lean.Parser.CacheableParserContext) →
  Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Init.Data.String.Termination
String.Pos.wellFounded_lt : ∀ {s : String}, WellFounded fun p q => p < q
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.sum : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {C : ι → ℝ} {s : Finset ι},
  (∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) g) → Asymptotics.IsBigOWith (∑ i ∈ s, C i) l (∑ i ∈ s, A i) g
-- Mathlib.Algebra.CharP.Defs
CharP.exists' : ∀ (R : Type u_2) [inst : NonAssocRing R] [NoZeroDivisors R] [Nontrivial R],
  CharZero R ∨ ∃ p, Fact (Nat.Prime p) ∧ CharP R p
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.ColimitPresentation.changeDiag_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.ColimitPresentation J X) {F : CategoryTheory.Functor J C} (e : F ≅ P.diag),
  (P.changeDiag e).ι = CategoryTheory.CategoryStruct.comp e.hom P.ι
-- Mathlib.Logic.Equiv.Sum
Equiv.Perm.sumCongr_trans : ∀ {α : Type u_9} {β : Type u_10} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β),
  Equiv.trans (e.sumCongr f) (g.sumCongr h) = Equiv.Perm.sumCongr (Equiv.trans e g) (Equiv.trans f h)
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.piIsoPi_hom_π : ∀ (J : Type u) (f : J → CategoryTheory.Grpd) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Grpd.piIsoPi J f).hom (CategoryTheory.Limits.Pi.π f j) =
    CategoryTheory.Pi.eval (fun i => ↑(f i)) j
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Logic.Equiv.Set
Set.mem_image_equiv : ∀ {α : Type u_3} {β : Type u_4} {S : Set α} {f : α ≃ β} {x : β}, x ∈ ⇑f '' S ↔ f.symm x ∈ S
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.distinctConstantsTheory.eq_1 : ∀ (L : FirstOrder.Language) {α : Type u'} (s : Set α),
  L.distinctConstantsTheory s =
    (fun ab => ((L.con ab.1).term.equal (L.con ab.2).term).not) '' (s ×ˢ s ∩ (Set.diagonal α)ᶜ)
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_one_sub_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun x => 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℂ 1) 0 1
-- Mathlib.Logic.Equiv.Prod
/-- Four-way commutativity of `prod`. The name matches `mul_mul_mul_comm`.  -/
Equiv.prodProdProdComm : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (δ : Type u_12) → (α × β) × γ × δ ≃ (α × γ) × β × δ
-- Mathlib.Analysis.Complex.Basic
_private.Mathlib.Analysis.Complex.Basic.0.RCLike.termReC : Lean.ParserDescr
-- Mathlib.Logic.Unique
Unique.exists_iff : ∀ {α : Sort u_1} [inst : Unique α] {p : α → Prop}, Exists p ↔ p default
-- Mathlib.Data.List.Lattice
/-- **Alias** of `List.cons_bagInter_of_mem`. -/
List.cons_bagInter_of_pos : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
  a ∈ l₂ → (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)
-- Mathlib.Tactic.Translate.Core
/-- The `Syntax` element corresponding to the translation attribute,
which we need for adding definition ranges, and for logging messages.  -/
Mathlib.Tactic.Translate.Config.ref : Mathlib.Tactic.Translate.Config → Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.end_hom_mk_of_mk : ∀ {V : Type u} (G : SimpleGraph V) {s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j},
  s ∈ G.end →
    ∀ {K L : (Finset V)ᵒᵖ} (h : L ⟶ K) {v : V} (vnL : v ∉ Opposite.unop L),
      s L = G.componentComplMk vnL → s K = G.componentComplMk ⋯
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.limitConeOfIsGLB_isLimit : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {pt : C} (h : IsGLB (Set.range F.obj) pt),
  (Preorder.limitConeOfIsGLB F h).isLimit = Preorder.isLimitOfIsGLB F (Preorder.coneOfLowerBound F ⋯) h
-- Mathlib.Order.Fin.Basic
Fin.castLEOrderEmb_apply : ∀ {m n : ℕ} (h : n ≤ m) (i : Fin n), (Fin.castLEOrderEmb h) i = Fin.castLE h i
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget₂Mon_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  ((CategoryTheory.CommMon.forget₂Mon C).obj A).X = A.X
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp_int32ToInt : ∀ (x : Int32), ISize.ofIntClamp x.toInt = x.toISize
-- Init.Data.String.Basic
/-- Returns the character at position `p` of a string. If `p` is not a valid position, returns the
fallback value `(default : Char)`, which is `'A'`, but does not panic.

This function is overridden with an efficient implementation in runtime code. See
`String.Pos.Raw.utf8GetAux` for the reference implementation.

This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos` or another means of obtaining a `String.Pos`.

Examples:
* `"abc".get ⟨1⟩ = 'b'`
* `"abc".get ⟨3⟩ = (default : Char)` because byte `3` is at the end of the string.
* `"L∃∀N".get ⟨2⟩ = (default : Char)` because byte `2` is in the middle of `'∃'`.
 -/
String.Pos.Raw.get : String → String.Pos.Raw → Char
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_add_ofNat : ∀ (r : ENNReal) (n : ℕ) [inst : n.AtLeastTwo], ⌊r + OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ + OfNat.ofNat n
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.Pivot.listTransvecRow.eq_1 : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
  Matrix.Pivot.listTransvecRow M =
    List.ofFn fun i =>
      Matrix.transvection (Sum.inr ()) (Sum.inl i) (-M (Sum.inr ()) (Sum.inl i) / M (Sum.inr ()) (Sum.inr ()))
-- Mathlib.Tactic.DefEqAbuse
/-- For failures with syntactically identical LHS and RHS (e.g. `⊤ =?= ⊤`), re-render with
progressively more verbose pp settings to disambiguate. This modifies only the rendering
of the `MessageData` (via `withPPOptions`), not the analysis — the captured `MetavarContext`
and trace structure are preserved, so transition-point detection remains correct.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.disambiguateFailures : Array Lean.MessageData → BaseIO (Array Lean.MessageData)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ],
  (CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration I κ).F =
    CategoryTheory.SmallObject.iterationFunctor I κ
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getExprPatternVarsEx : Lean.TSyntax `Lean.Parser.Term.matchExprPat → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_neg : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : F) [ModularFormClass F Γ k], UpperHalfPlane.qExpansion h (-⇑f) = -UpperHalfPlane.qExpansion h ⇑f
-- Lean.Data.Lsp.Basic
Lean.Lsp.LocationLink : Type
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearEquiv.coe_ofBijective : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] (f : E →SL[σ] F) (hinj : (↑f).ker = ⊥) (hsurj : (↑f).range = ⊤),
  ↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →ₙ+ N` is the type of functions `M → N` that preserve addition. The `ₙ` in the notation
stands for "non-unital" because it is intended to match the notation for `NonUnitalAlgHom` and
`NonUnitalRingHom`, so a `AddHom` is a non-unital additive monoid hom.

When possible, instead of parametrizing results over `(f : AddHom M N)`,
you should parametrize over `(F : Type*) [AddHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `AddHomClass`.
 -/
AddHom : (M : Type u_10) → (N : Type u_11) → [Add M] → [Add N] → Type (max u_10 u_11)
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_mul_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α β : K),
  NumberField.house (α * β) ≤ NumberField.house α * NumberField.house β
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.mk : {α : Type} → Lean.Lsp.ProgressToken → α → Lean.Lsp.ProgressParams α
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.not_nhds_le_map : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  [inst_2 : TopologicalSpace β],
  IsLocalMinOn f s a → ∀ [(nhdsWithin (f a) (Set.Iio (f a))).NeBot], ¬nhds (f a) ≤ Filter.map f (nhdsWithin a s)
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.mem_falling : ∀ {α : Type u_2} [inst : DecidableEq α] {k : ℕ} {𝒜 : Finset (Finset α)} {s : Finset α},
  s ∈ Finset.falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.coe_natCast : ∀ {q : ℕ} (n : ℕ), ↑↑n = ↑n
-- Mathlib.Algebra.Group.Subgroup.Actions
Subgroup.smulCommClass_right : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst_1 : SMul α β] [inst_2 : MulAction G β]
  [SMulCommClass α G β] (S : Subgroup G), SMulCommClass α (↥S) β
-- Mathlib.Algebra.Algebra.RestrictScalars
instAddCommMonoidRestrictScalars : (R : Type u_1) → (S : Type u_2) → (M : Type u_3) → [I : AddCommMonoid M] → AddCommMonoid (RestrictScalars R S M)
-- Std.Http.Data.Method
/-- Establish a tunnel to a server (often for TLS).
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.6
 -/
Std.Http.Method.connect : Std.Http.Method
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.whiskerRight_out_app : ∀ {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]
  {E : Type u₂} [inst_4 : CategoryTheory.EnrichedCategory V E] {F G : CategoryTheory.EnrichedFunctor V C D} (α : F ⟶ G)
  (H : CategoryTheory.EnrichedFunctor V D E) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.whiskerRight α H).out.app X =
    CategoryTheory.ForgetEnrichment.homOf V
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homTo V (α.out.app X))
        (H.map (F.obj (CategoryTheory.ForgetEnrichment.to V X)) (G.obj (CategoryTheory.ForgetEnrichment.to V X))))
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_basisDivisor_right : ∀ {F : Type u_1} [inst : Field F] {x y : F}, Polynomial.eval y (Lagrange.basisDivisor x y) = 0
-- Std.Data.Iterators.Lemmas.Producers.Repeat
_private.Std.Data.Iterators.Lemmas.Producers.Repeat.0.Nat.repeat.match_1.eq_2 : ∀ {α : Type u_2} (motive : ℕ → α → Sort u_1) (n : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (n : ℕ) → (a : α) → motive n.succ a),
  (match n.succ, a with
    | 0, a => h_1 a
    | n.succ, a => h_2 n a) =
    h_2 n a
-- Mathlib.Order.RelSeries
/-- The strict series `0 < … < n` in `ℕ`.  -/
LTSeries.range : ℕ → LTSeries ℕ
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyConnected : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.GeometricallyConnected
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_μ : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : CategoryTheory.Mon C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Mon.forget C) X Y =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.X Y.X)
-- Mathlib.Data.Sym.Sym2
/-- Non-dependent recursor on members of a `fromRel` set  -/
Sym2.fromRelNdrec : {α : Type u_1} →
  {r : α → α → Prop} →
    {motive : Sort u_4} →
      {sym : Std.Symm r} →
        (z : Sym2 α) →
          z ∈ Sym2.fromRel sym →
            (f : (a b : α) → r a b → motive) → (∀ (a b : α) (h : r a b), f a b h = f b a ⋯) → motive
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_else_not_ite : ∀ (cond : Bool) {a b c : Bool}, (bif cond then a else !bif cond then b else c) = bif cond then a else !c
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_single : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁) (i j : n), ((Matrix.toBilin' M) (Pi.single i 1)) (Pi.single j 1) = M i j
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isZeroOrProbabilityMeasureSMul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.IsZeroOrProbabilityMeasure ((μ Set.univ)⁻¹ • μ)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instInhabited : (R : Type u) → [inst : Ring R] → Inhabited (FGModuleCat R)