mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.det_map' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  (b : Module.Basis ι R M) (f : M ≃ₗ[R] M'), (b.map f).det = b.det.compLinearMap ↑f.symm
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`.  -/
InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → InnerProductGeometry.angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ₃.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.Ψ₃ =
    3 * Polynomial.X ^ 4 + Polynomial.C W.b₂ * Polynomial.X ^ 3 + 3 * Polynomial.C W.b₄ * Polynomial.X ^ 2 +
        3 * Polynomial.C W.b₆ * Polynomial.X +
      Polynomial.C W.b₈
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α} {v : β}, Std.DTreeMap.Const.get! (t.insert k v) k = v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∈ t ↔ t[a]?.isSome = true
-- Mathlib.Order.Partition.Finpartition
/-- Restricts a finpartition to avoid a given element.  -/
Finpartition.avoid : {α : Type u_1} →
  [inst : GeneralizedBooleanAlgebra α] → [DecidableEq α] → {a : α} → Finpartition a → (b : α) → Finpartition (a \ b)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.ker_toZMod : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)], RingHom.ker PadicInt.toZMod = IsLocalRing.maximalIdeal ℤ_[p]
-- Init.WF
/-- If all elements are accessible via `r`, then `r` is well-founded.
 -/
WellFounded.intro : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Std.Http.Protocol.H1
Std.Http.Protocol.H1.StepResult.mk.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (events : Array (Std.Http.Protocol.H1.Event dir))
  (output : Std.Http.Internal.ChunkedBuffer),
  sizeOf { events := events, output := output } = 1 + sizeOf events + sizeOf output
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.toSubmodule_injective : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L],
  Function.Injective LieRinehartSubalgebra.toSubmodule
-- Mathlib.Data.Num.Basic
instDecidableEqNum : DecidableEq Num
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRightIso_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (W : C),
  (CategoryTheory.MonoidalCategory.whiskerRightIso f W).symm = CategoryTheory.MonoidalCategory.whiskerRightIso f.symm W
-- Mathlib.Data.Stream.Init
Stream'.tail_iterate : ∀ {α : Type u} (f : α → α) (a : α), (Stream'.iterate f a).tail = Stream'.iterate f (f a)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformly.summableUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], SummableUniformly f → SummableUniformlyOn f s
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
SSet.coherentIso.invStructHom_homInvId : SSet.coherentIso.invStructHom.homInvId = SSet.coherentIso.homInvId
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.

See `Module.finrank_mul_finrank'` for a variant over a tower of domains that assumes the rings are
module-finite rather than the modules being free.  -/
Module.finrank_mul_finrank : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A],
  Module.finrank F K * Module.finrank K A = Module.finrank F A
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsClosedUnderIsomorphismsIsFinitePresentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat],
  (SheafOfModules.isFinitePresentation R).IsClosedUnderIsomorphisms
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.Context.mk : Lean.PHashMap Lean.MVarId (ℕ × Aesop.Script.Step) → Aesop.Script.DynStructureM.Context
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The ring map from `A⁰_ f` to the local sections of the structure sheaf of the projective spectrum of
`A` on the basic open set `D(f)` defined by sending `s ∈ A⁰_f` to the section `x ↦ s` on `D(f)`.
 -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ⟶
                  (AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj
                    (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 f))
-- Init.Data.Option.Lemmas
Option.filter_pbind : ∀ {α : Type u_1} {o : Option α} {β : Type u_2} {p : β → Bool} {f : (a : α) → o = some a → Option β},
  Option.filter p (o.pbind f) = (o.pfilter fun a h => Option.any p (f a h)).pbind fun a h => f a ⋯
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_k_eq_mul : ∀ {m₁ m₂ : Lean.Grind.CommRing.Mon}, m₁.mul_k m₂ = m₁.mul m₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The first inclusion of a binary cofan.  -/
CategoryTheory.Limits.BinaryCofan.inl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryCofan X Y) →
        (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶
          ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj
            { as := CategoryTheory.Limits.WalkingPair.left }
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.mk : (arr : Array Batteries.UFNode) →
  (∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size) →
    (∀ {i : ℕ},
        Batteries.UnionFind.parentD arr i ≠ i →
          Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)) →
      Batteries.UnionFind
-- Mathlib.GroupTheory.Congruence.Hom
/-- Surjective monoid homomorphisms constant on a congruence relation `c`'s equivalence classes
induce a surjective homomorphism on `c`'s quotient.  -/
Con.lift_surjective_of_surjective : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {c : Con M} {f : M →* P}
  (h : c ≤ Con.ker f), Function.Surjective ⇑f → Function.Surjective ⇑(c.lift f h)
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.subsingleton_orbit_iff_mem_fixedPoints : ∀ {M : Type u} [inst : AddMonoid M] {α : Type v} [inst_1 : AddAction M α] {a : α},
  (AddAction.orbit M a).Subsingleton ↔ a ∈ AddAction.fixedPoints M α
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.f_modif.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E),
  P.f_modif =
    ((Set.Ioi 1).indicator fun x => P.f x - P.f₀) +
      (Set.Ioo 0 1).indicator fun x => P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.extend_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [inst_2 : TopologicalSpace γ] [T2Space γ] (di : IsDenseInducing i) {f : α → γ},
  Continuous f → ∀ (a : α), di.extend f (i a) = f a
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.iUnion_skeletonLT_eq_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  ⋃ n, ↑(Topology.RelCWComplex.skeletonLT C ↑n) = C
-- Init.Data.Option.Instances
Option.eq_of_eq_some : ∀ {α : Type u} {x y : Option α}, (∀ (z : α), x = some z ↔ y = some z) → x = y
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_eq_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s : Finset β}
  {a : α} [inst_3 : Fintype β], a • s = Finset.univ ↔ s = Finset.univ
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.op_δ : ∀ (X : SSet) {n : ℕ} (i : Fin (n + 2)) (x : X.op.obj (Opposite.op { len := n + 1 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X.op i)) x =
    SSet.opObjEquiv.symm
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i.rev)) (SSet.opObjEquiv x))
-- Mathlib.Order.Hom.Basic
OrderHomClass.mono : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : FunLike F α β]
  [OrderHomClass F α β] (f : F), Monotone ⇑f
-- Mathlib.Order.ModularLattice
Disjoint.disjoint_sup_right_of_disjoint_sup_left : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : OrderBot α] [IsModularLattice α],
  Disjoint a b → Disjoint (a ⊔ b) c → Disjoint a (b ⊔ c)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_constToArray_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toArray t₁).Perm (Std.DTreeMap.Const.toArray t₂) → t₁.Equiv t₂
-- Mathlib.Dynamics.Flow
Flow.continuous_toFun : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) (t : τ), Continuous (ϕ.toFun t)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.next : ∀ (α : Type u_2) [inst : AddGroup α] [inst_1 : One α] (i : α), (ComplexShape.down α).next i = i - 1
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.functoriality`.

---

A functor `G : C ⥤ D` sends cocones over `F` to cocones over `F ⋙ G` functorially.  -/
CategoryTheory.Limits.Cocones.functoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (F : CategoryTheory.Functor J C) →
              (G : CategoryTheory.Functor C D) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (F.comp G))
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.relationsSet.eq_1 : ∀ {B : Type u_1} (M : CoxeterMatrix B), M.relationsSet = Set.range (Function.uncurry M.relation)
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_iff_ultrafilter : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → Cauchy ↑f
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.summable : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F]
  (p : FormalMultilinearSeries 𝕜 E F) {x : E}, x ∈ Metric.eball 0 p.radius → Summable fun n => (p n) fun x_1 => x
-- Mathlib.Analysis.Complex.RealDeriv
ContDiff.real_of_complex : ∀ {e : ℂ → ℂ} {n : WithTop ℕ∞}, ContDiff ℂ n e → ContDiff ℝ n fun x => (e ↑x).re
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- A linear map induces a linear map on adic Cauchy sequences.  -/
AdicCompletion.AdicCauchySequence.map : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {M : Type u_2} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {N : Type u_3} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (M →ₗ[R] N) → AdicCompletion.AdicCauchySequence I M →ₗ[R] AdicCompletion.AdicCauchySequence I N
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image2_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, Set.image2 (fun x1 x2 => x1 -ᵥ x2) s t = s -ᵥ t
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.inv_lt_one_iff`.

---

Uses `left` co(ntra)variant.  -/
inv_lt_one_iff_one_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, a⁻¹ < 1 ↔ 1 < a
-- Init.Data.SInt.Float32
/-- Truncates a floating-point number to the nearest 32-bit signed integer, rounding towards zero.

If the `Float` is larger than the maximum value for `Int32` (including `Inf`), returns the maximum
value of `Int32` (i.e. `Int32.maxValue`). If it is smaller than the minimum value for `Int32`
(including `-Inf`), returns the minimum value of `Int32` (i.e. `Int32.minValue`). If it is `NaN`,
returns `0`.

This function does not reduce in the kernel.
 -/
Float32.toInt32 : Float32 → Int32
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instDecidableMem : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → {m : Std.DTreeMap α β cmp} → {a : α} → Decidable (a ∈ m)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.take_coe : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} (n : ℕ) (x : ↥T), ↑(Descriptive.Tree.take n x) = List.take n ↑x
-- Mathlib.Topology.Sheaves.Presheaf
/-- `restrict_tac?` passes along `Try this` from `aesop`  -/
TopCat.Presheaf.restrict_tac? : Lean.ParserDescr
-- Lean.Compiler.CSimpAttr
Lean.Compiler.CSimp.State.mk.inj : ∀ {map : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry} {thmNames : Lean.SSet Lean.Name}
  {map_1 : Lean.SMap Lean.Name Lean.Compiler.CSimp.Entry} {thmNames_1 : Lean.SSet Lean.Name},
  { map := map, thmNames := thmNames } = { map := map_1, thmNames := thmNames_1 } → map = map_1 ∧ thmNames = thmNames_1
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.le_card_support_of_mem_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {n : ℕ} {σ : Equiv.Perm α},
  n ∈ σ.cycleType → n ≤ σ.support.card
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.mk.sizeOf_spec : ∀ (res? : Except Lean.Exception Dynamic) (snap? : Option Lean.Language.SnapshotTree),
  sizeOf { res? := res?, snap? := snap? } = 1 + sizeOf res? + sizeOf snap?
-- Mathlib.Topology.Compactness.Compact
/-- If a filter has a unique cluster point `y` in a compact topological space,
then the filter is less than or equal to `𝓝 y`.  -/
le_nhds_of_unique_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {l : Filter X} {y : X},
  (∀ (x : X), ClusterPt x l → x = y) → l ≤ nhds y
-- Lean.Meta.Tactic.Simp.Types
/-- For `pre` procedures, continue transformation by visiting subexpressions, and then
executing `post` procedures.

For `post` procedures, this is equivalent to returning `visit`.
 -/
Lean.Meta.Simp.Step.continue : optParam (Option Lean.Meta.Simp.Result) none → Lean.Meta.Simp.Step
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImport.mk : Lean.Lsp.LeanModule → Lean.Lsp.LeanImportKind → Lean.Lsp.LeanImport
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_assoc : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (m n k : α),
  gcd (gcd m n) k = gcd m (gcd n k)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.comp 0 = Polynomial.C (Polynomial.eval 0 p)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocEntry.try : Lean.Meta.Simp.SimprocEntry → ℕ → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_nil_iff : ∀ {m n : ℤ}, (m<...n).toArray = #[] ↔ n ≤ m + 1
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.map_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5}
  [inst_2 : ConditionallyCompleteLattice β] {f : α → β}, Monotone f → s.Nonempty → f (sInf s) = sInf (f '' s)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_f_fromNormalizedChainComplex_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp ((X.toNormalizedChainComplex R).f n) ((X.fromNormalizedChainComplex R).f n) =
    AlgebraicTopology.DoldKan.PInfty.f n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l →
      ∀ {h : k' ∈ ↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)},
        (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).get k' h = cast ⋯ v
-- Mathlib.Data.Finset.Max
Finset.max_union : ∀ {α : Type u_2} [inst : LinearOrder α] {s t : Finset α}, (s ∪ t).max = max s.max t.max
-- Mathlib.RingTheory.DualNumber
TrivSqZeroExt.isNilpotent_inl_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] (r : R), IsNilpotent (TrivSqZeroExt.inl r) ↔ IsNilpotent r
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.nonempty_completion_iff : ∀ (α : Type u_1) [inst : UniformSpace α], Nonempty (UniformSpace.Completion α) ↔ Nonempty α
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁.subset s₂` checks whether `s₁` is a subset of `s₂`.
It assumes `s₁` and `s₂` are sorted.
 -/
Lean.Grind.AC.Seq.subset : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.SubsetResult
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSetPathLength : {V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype ↑{p | p.IsPath ∧ p.length = n}
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_natCast : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) (n : ℕ),
  Polynomial.eval₂ f x ↑n = ↑n
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left unitor `λ_ f`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.leftUnitorM' : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeCommMonCat : Coe AddCommGrpCat AddCommMonCat
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeBlockSuggestionsUnsafe : Lean.Elab.TermElabM (Array (Lean.StrLit → Lean.Doc.DocM (Array Lean.Doc.CodeBlockSuggestion)))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.keys_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).keys = []
-- Init.Data.String.Substring
/-- Returns the longest common suffix of two substrings.

The returned substring uses the same underlying string as `s`.
 -/
Substring.Raw.commonSuffix : Substring.Raw → Substring.Raw → Substring.Raw
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde_mul_vandermonde_transpose : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v w : Fin n → R) (i j : Fin n),
  (Matrix.vandermonde v * (Matrix.vandermonde w).transpose) i j = ∑ k, (v i * w j) ^ ↑k
-- ProofWidgets.Component.RefreshComponent
/-- A reference to a `RefreshState`.
Only exists because `TypeName` is not derivable for compound types.  -/
ProofWidgets.RefreshComponent.RefreshRef : Type
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (L : CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject.HoCat C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject.HoCat C))],
  (HomotopicalAlgebra.FibrantObject.toHoCat.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instReflLe : Std.Refl fun x1 x2 => x1 ⊆ x2
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- **Alias** of `MonoidHom.domRestrict_eq_one_iff`. -/
MonoidHom.restrict_eq_one_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {N : Type u_5} {S : Type u_6} [inst_1 : MulOneClass N] {f : M →* N}
  [inst_2 : SetLike S M] [inst_3 : SubmonoidClass S M] {s : S}, f.domRestrict s = 1 ↔ ∀ x ∈ s, f x = 1
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.ascii_turnstile.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
/-- The rank of `Π i, M i` at a prime `p` is the sum of the ranks of `M i` at `p`.  -/
Module.rankAtStalk_pi : ∀ {R : Type uR} [inst : CommRing R] {ι : Type u_1} [Finite ι] (M : ι → Type u_2) [inst_2 : (i : ι) → AddCommGroup (M i)]
  [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Flat R (M i)] [∀ (i : ι), Module.Finite R (M i)]
  (p : PrimeSpectrum R), Module.rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), Module.rankAtStalk (M i) p
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.det_transvection_of_ne : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) [inst_2 : Fintype n],
  i ≠ j → ∀ (c : R), (Matrix.transvection i j c).det = 1
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.path_image_Ioc_of_ne : ∀ {x y : Circle}, x ≠ y → ⇑(x.path y) '' Set.Ioc 0 1 = ⇑Circle.exp '' Set.Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
-- Mathlib.Data.Finsupp.Basic
/-- Given `AddCommMonoid M` and `e : α ≃ β`, `domCongr e` is the corresponding `Equiv` between
`α →₀ M` and `β →₀ M`.

This is `Finsupp.equivCongrLeft` as an `AddEquiv`.  -/
Finsupp.domCongr : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : AddCommMonoid M] → α ≃ β → (α →₀ M) ≃+ (β →₀ M)