mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instInhabited : (α : Type u_5) → [inst : NonUnitalNonAssocSemiring α] → Inhabited (CentroidHom α)
-- Std.Http.Server.Connection
/-- Handles the `Expect: 100-continue` protocol for a pending request head.
Races between the handler's decision (`Handler.onContinue`), the connection being
cancelled, and a lingering timeout. Returns the updated machine and whether
`pendingHead` should be cleared (i.e. when the request is rejected).
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.handleContinueEvent : {σ : Type} →
  [Std.Http.Server.Handler σ] →
    σ →
      Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
        Std.Http.Request.Head →
          Std.Http.Config →
            Std.CancellationContext →
              Std.Async.Async (Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving × Bool)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap
DifferentiableAt.continuousMultilinearMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} {H : Type u_6}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {f : E → ContinuousMultilinearMap 𝕜 G H} {g : (i : ι) → E → F i →L[𝕜] G i} {x : E}
  [Finite ι],
  DifferentiableAt 𝕜 f x →
    (∀ (i : ι), DifferentiableAt 𝕜 (g i) x) →
      DifferentiableAt 𝕜 (fun x => (f x).compContinuousLinearMap fun x_1 => g x_1 x) x
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.repr_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Fintype ι'] (b : OrthonormalBasis ι 𝕜 E) (e : ι ≃ ι')
  (x : E) (i' : ι'), ((b.reindex e).repr x).ofLp i' = (b.repr x).ofLp (e.symm i')
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- Construct a `Mor₁` expression from a Lean expression.  -/
Mathlib.Tactic.Monoidal.mor₁OfExpr : Lean.Expr → Mathlib.Tactic.Monoidal.MonoidalM Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_neg_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable (-ω) γ ↔ CurveIntegrable ω γ
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_eq_one_iff : ∀ {a b : ENNReal}, b ≠ 0 → b ≠ ⊤ → (a / b = 1 ↔ a = b)
-- Init.Data.Int.Lemmas
Int.negOfNat_mul_negSucc : ∀ (m n : ℕ), Int.negOfNat n * Int.negSucc m = Int.ofNat (n * m.succ)
-- Init.Data.List.Sublist
List.IsSuffix.eq_of_length : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁.length = l₂.length → l₁ = l₂
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₃ = f.left.hom
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- If `e` is an application that is a candidate for using field notation,
returns the parameter index and the field name to use.
Checks that there are enough arguments.
 -/
Lean.PrettyPrinter.Delaborator.appFieldNotationCandidate? : Lean.PrettyPrinter.Delaborator.DelabM (Option (ℕ × Lean.Name))
-- Mathlib.Algebra.Group.Submonoid.BigOperators
Submonoid.multiset_noncommProd_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (m : Multiset M) (comm : {x | x ∈ m}.Pairwise Commute),
  (∀ x ∈ m, x ∈ S) → m.noncommProd comm ∈ S
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.coe_quotient_vadd : ∀ {G : Type u} {X : Type v} [inst : AddGroup G] {H : AddSubgroup G} [inst_1 : H.Normal] [inst_2 : VAdd G X]
  [inst_3 : AddAction (G ⧸ H) X] [VAddAssocClass G (G ⧸ H) X] (g : G) (x : X), ↑g +ᵥ x = g +ᵥ x
-- Mathlib.Data.Nat.Nth
Nat.nth_mem_of_ne_zero : ∀ {p : ℕ → Prop} {n : ℕ}, Nat.nth p n ≠ 0 → p (Nat.nth p n)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE : ∀ {R : CommRingCat} (f g x : ↑R) (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.basicOpenIsoSpecAway x).inv
      ((AlgebraicGeometry.Spec R).homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
      (AlgebraicGeometry.basicOpenIsoSpecAway f).inv
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Reflective.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {R : CategoryTheory.Functor D C} →
          [toFull : R.Full] →
            [toFaithful : R.Faithful] → (L : CategoryTheory.Functor C D) → (L ⊣ R) → CategoryTheory.Reflective R
-- Mathlib.Algebra.Order.Field.Basic
IsLUB.mul_right : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α]
  {s : Set α}, 0 ≤ a → IsLUB s b → IsLUB ((fun b => b * a) '' s) (b * a)
-- Mathlib.Order.Bounds.Defs
IsCoinitial.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsCoinitial s = ∀ (x : α), ∃ y ∈ s, y ≤ x
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_sdiff_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, Set.Ioc b a \ {a} = Set.Ioo b a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk.inj : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {inst : Ring k} {inst_1 : AddCommGroup V} {inst_2 : Module k V}
  {inst_3 : AddTorsor V P} {carrier : Set P}
  {smul_vsub_vadd_mem' :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier}
  {carrier_1 : Set P}
  {smul_vsub_vadd_mem'_1 :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier_1 → p₂ ∈ carrier_1 → p₃ ∈ carrier_1 → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier_1},
  { carrier := carrier, smul_vsub_vadd_mem' := smul_vsub_vadd_mem' } =
      { carrier := carrier_1, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'_1 } →
    carrier = carrier_1
-- Mathlib.RingTheory.Flat.Rank
Algebra.rankAtStalk_eq_of_isPushout : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (R' : Type u_5)
  (S' : Type u_6) [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [Algebra.IsPushout R S R' S'] [Module.Flat R S] [Module.Finite R S] (x : PrimeSpectrum R'),
  Module.rankAtStalk S' x = Module.rankAtStalk S (PrimeSpectrum.comap (algebraMap R R') x)
-- Mathlib.Data.Subtype
Subtype.coe_inj : ∀ {α : Sort u_1} {p : α → Prop} {a b : Subtype p}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.EpiMono
/-- A split epi category is a category in which every epimorphism is split.  -/
CategoryTheory.SplitEpiCategory : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.basisOfBasisRight.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b b_1 : Module.Basis ι R ↥B),
  b = b_1 → H.basisOfBasisRight H' b = H.basisOfBasisRight H' b_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variables to their "lower" bounds. We say a relational constraint `c` is a lower bound for a variable `x`
if `x` is the maximal variable in `c`, and `x` coefficient in `c` is negative.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.lowers : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.IneqCnstr)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_disjUnion_Iio : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : Fintype α] [inst_2 : LocallyFiniteOrderTop α]
  [inst_3 : LocallyFiniteOrderBot α] (a : α), (Finset.Ioi a).disjUnion (Finset.Iio a) ⋯ = {a}ᶜ
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (I.cocomplex.d 0 1) = 0
-- Mathlib.Order.Hom.CompleteLattice
/-- The type of frame homomorphisms from `α` to `β`. They preserve finite meets and arbitrary joins.
 -/
FrameHom : (α : Type u_8) → (β : Type u_9) → [CompleteLattice α] → [CompleteLattice β] → Type (max u_8 u_9)
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `C` is also filtered, see
`IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful`.  -/
CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) → F.Final
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  (∀ (l r : Std.DTreeMap.Internal.Impl α β),
      l.size + r.size ≤ 1 → motive l r (Std.DTreeMap.Internal.Impl.bin k v l r)) →
    (∀ (l : Std.DTreeMap.Internal.Impl α β) (size : ℕ) (rk : α) (rv : β rk) (rl rr : Std.DTreeMap.Internal.Impl α β),
        (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size →
          ¬l.size + (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size ≤ 1 →
            (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size →
              motive l (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr)
                (Std.DTreeMap.Internal.Impl.rotateL k v l rk rv rl rr)) →
      (∀ (r : Std.DTreeMap.Internal.Impl α β) (size : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
          ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size →
            (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size →
              ¬(Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size + r.size ≤ 1 →
                ¬r.size > Std.DTreeMap.Internal.delta * (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size →
                  (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr).size > Std.DTreeMap.Internal.delta * r.size →
                    motive (Std.DTreeMap.Internal.Impl.inner size lk lv ll lr) r
                      (Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r)) →
        (∀ (l r : Std.DTreeMap.Internal.Impl α β),
            ¬l.size + r.size ≤ 1 →
              ¬r.size > Std.DTreeMap.Internal.delta * l.size →
                ¬l.size > Std.DTreeMap.Internal.delta * r.size → motive l r (Std.DTreeMap.Internal.Impl.bin k v l r)) →
          ∀ (l r : Std.DTreeMap.Internal.Impl α β), motive l r (Std.DTreeMap.Internal.Impl.balanceₘ k v l r)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.IsExtension.exact : ∀ {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : LieAlgebra R L} {inst_3 : LieRing N} {inst_4 : LieAlgebra R N} {inst_5 : LieRing M}
  {inst_6 : LieAlgebra R M} {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} [self : LieAlgebra.IsExtension i p],
  i.range = LieIdeal.toLieSubalgebra R L p.ker
-- Mathlib.Order.KrullDimension
/-- The **coheight** of an element `a` in a preorder `α` is the supremum of the rightmost index of all
relation series of `α` ordered by `<` and beginning with `a`. In other words, it is
the largest `n` such that there's a series `a = a₀ < a₁ < ... < aₙ` (or `∞` if there is
no largest `n`).

The definition of `coheight` is via the `height` in the dual order, in order to easily transfer
theorems between `height` and `coheight`. See `coheight_eq` for the definition with a
series ordered by `<` and beginning with `a`.
 -/
Order.coheight : {α : Type u_1} → [Preorder α] → α → ℕ∞
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α] {k : α} {f : β → β}, (t.modify k f).maxKey! = t.maxKey!
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Given an edge labeling and a choice of label `k`, construct the graph corresponding to the edges
labeled `k`.
 -/
SimpleGraph.EdgeLabeling.labelGraph : {V : Type u_1} → {G : SimpleGraph V} → {K : Type u_3} → G.EdgeLabeling K → K → SimpleGraph V
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.H = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- The underlying 2-isomorphisms of the naturality constraint.  -/
CategoryTheory.Lax.LaxTrans.StrongCore.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η : F ⟶ G} →
            CategoryTheory.Lax.LaxTrans.StrongCore η →
              {a b : B} →
                (f : a ⟶ b) →
                  CategoryTheory.CategoryStruct.comp (η.app a) (G.map f) ≅
                    CategoryTheory.CategoryStruct.comp (F.map f) (η.app b)
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- Auxiliary definition for `lift`.  -/
CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux : {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] →
        {G : CategoryTheory.Functor C D} →
          {A : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              {J : CategoryTheory.GrothendieckTopology C} →
                {K : CategoryTheory.GrothendieckTopology D} →
                  [G.IsCocontinuous J K] →
                    {F : CategoryTheory.Functor Cᵒᵖ A} →
                      CategoryTheory.Presheaf.IsSheaf J F →
                        {R : CategoryTheory.Functor Dᵒᵖ A} →
                          (G.op.comp R ⟶ F) →
                            {X : D} →
                              {S : K.Cover X} →
                                (s : CategoryTheory.Limits.Multifork (S.index R)) →
                                  {Y : C} → (G.obj Y ⟶ X) → (s.pt ⟶ F.obj (Opposite.op Y))
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousWithinAt.sub : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Sub G]
  [ContinuousSub G] {f g : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f - g) s x
-- Lean.Parser.Term
Lean.Parser.Term.arrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Constructions
isOpen_range_sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι}, IsOpen (Set.range (Sigma.mk i))
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.toBilin'_apply : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix n n R₁) (x y : n → R₁), ((Matrix.toBilin' M) x) y = ∑ i, ∑ j, x i * M i j * y j
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.sub_self : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ - μ = 0
-- Mathlib.Algebra.Lie.Weights.Chain
/-- This is the largest `n : ℕ` such that `-i • α + β` is a weight for all `0 ≤ i ≤ n`.  -/
LieModule.chainBotCoeff : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [IsAddTorsionFree R] →
                        [IsDomain R] →
                          [Module.IsTorsionFree R M] → [IsNoetherian R M] → (L → R) → LieModule.Weight R L M → ℕ
-- Mathlib.Lean.Meta.CongrTheorems
/-- Introduce variables for equalities between the arrays of variables. Uses `fixedParams`
to control whether to introduce an equality for each pair. The array of triples passed to `k`
consists of (1) the simple congr lemma HEq arg, (2) the richer HEq arg, and (3) how to
compute 1 in terms of 2.  -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.withNewEqs : Lean.Meta.FunInfo →
  {α : Type} →
    Array Lean.Expr →
      Array Lean.Expr →
        Array Bool →
          (Array Lean.Meta.CongrArgKind → Array (Option (Lean.Expr × Lean.Expr × Lean.Expr)) → Lean.MetaM α) →
            Lean.MetaM α
-- Mathlib.Topology.Closure
forall_isClosed_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : Set X → Prop},
  (∀ (t : Set X), IsClosed t → p t) ↔ ∀ (t : Set X), p (closure t)
-- Mathlib.RingTheory.Kaehler.TensorProduct
/-- If `B` is the tensor product of `S` and `A` over `R`,
then `Ω[B⁄S]` is the base change of `Ω[A⁄R]` along `R → S`.
 -/
KaehlerDifferential.isBaseChange : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [h : Algebra.IsPushout R S A B], IsBaseChange S (↑R (KaehlerDifferential.map R S A B))
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Int.zmultiples_sup : ∀ (a b : ℤ), AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples b = AddSubgroup.zmultiples ↑(a.gcd b)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm_extends : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L] (k : K),
  (spectralAlgNorm K L) ((algebraMap K L) k) = ‖k‖
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.eqToHom_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (h : x₀ = x₁),
  CategoryTheory.eqToHom ⋯ = (Path.Homotopic.Quotient.refl x₁).cast h ⋯
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_one_eq_const : SimplexCategory.δ 1 = { len := 0 }.const { len := 0 + 1 } 0
-- Mathlib.Analysis.Matrix.Spectrum
/-- The spectrum of a matrix `A` coincides with the spectrum of `toLpLin p p A`.  -/
Matrix.spectrum_toLpLin : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (p : ENNReal), spectrum 𝕜 ((Matrix.toLpLin p p) A) = spectrum 𝕜 A
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtension.id : {σ : Type} → Lean.Meta.Sym.SymExtension σ → ℕ
-- Init.Data.Array.MinMax
List.max?_toArray : ∀ {α : Type u_1} [inst : Max α] {l : List α}, l.toArray.max? = l.max?
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.diff.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (m₁ m₁_1 : Std.ExtDTreeMap α β cmp),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtDTreeMap α β cmp), m₂ = m₂_1 → m₁.diff m₂ = m₁_1.diff m₂_1
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Units.instIsManifoldModelWithCornersSelf : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {n : WithTop ℕ∞} {𝕜 : Type u_2}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAlgebra 𝕜 R], IsManifold (modelWithCornersSelf 𝕜 R) n Rˣ
-- Mathlib.Order.Concept
Concept.instSupSet : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → SupSet (Concept α β r)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- `ConcreteCategory.hom` bundled as an `Equiv`.
 -/
CategoryTheory.ConcreteCategory.homEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] → {X Y : C} → (X ⟶ Y) ≃ CategoryTheory.ToHom X Y
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.star : Lean.Meta.DiscrTree.Key
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- The map on images induced by a commutative square.  -/
CategoryTheory.Limits.image.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          (sq : f ⟶ g) →
            [CategoryTheory.Limits.HasImageMap sq] →
              CategoryTheory.Limits.image f.hom ⟶ CategoryTheory.Limits.image g.hom
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 1-coboundaries `B¹(G, A)` of `A : Rep k G`, defined as the image of the map
`A → Fun(G, A)` sending `(a, g) ↦ ρ_A(g)(a) - a.`  -/
groupCohomology.coboundaries₁ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{max u u_1, u, u} k G) → Submodule k (G → ↑A)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listEncode.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : ℕ) (x_1 : L.BoundedFormula α x),
  x_1.listEncode =
    match x, x_1 with
    | n, FirstOrder.Language.BoundedFormula.falsum => [Sum.inr (Sum.inr (n + 2))]
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => [Sum.inl ⟨x, t₁⟩, Sum.inl ⟨x, t₂⟩]
    | n, FirstOrder.Language.BoundedFormula.rel R ts =>
      [Sum.inr (Sum.inl ⟨l, R⟩), Sum.inr (Sum.inr n)] ++ List.map (fun i => Sum.inl ⟨n, ts i⟩) (List.finRange l)
    | x, φ₁.imp φ₂ => Sum.inr (Sum.inr 0) :: φ₁.listEncode ++ φ₂.listEncode
    | x, φ.all => Sum.inr (Sum.inr 1) :: φ.listEncode
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.WEquiv.below.trans : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n}
  {motive : (a a_1 : (MvQPF.P F).W α) → MvQPF.WEquiv a a_1 → Prop} (u v w : (MvQPF.P F).W α) (a : MvQPF.WEquiv u v)
  (a_1 : MvQPF.WEquiv v w),
  MvQPF.WEquiv.below a → motive u v a → MvQPF.WEquiv.below a_1 → motive v w a_1 → MvQPF.WEquiv.below ⋯
-- Mathlib.Data.Multiset.ZeroCons
Multiset.nodup_zero : ∀ {α : Type u_1}, Multiset.Nodup 0
-- Lean.Server.References
/-- Reference information from this ILean.  -/
Lean.Server.LoadedILean.refs : Lean.Server.LoadedILean → Lean.Lsp.ModuleRefs
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
hasFDerivAt_pi_polarCoord_symm : ∀ {ι : Type u_1} [Finite ι] (p : ι → ℝ × ℝ),
  HasFDerivAt (fun x i => ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, ∅.size = 0
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.coe_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : α), ↑(a * b) = ↑a * ↑b
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_injective : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Injective (PolynomialModule.ofCoeff R)
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalNestedTacticCore : Lean.Elab.Tactic.Tactic