mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₂ → Std.DHashMap.Const.get? (m₁.diff m₂) k = Std.DHashMap.Const.get? m₁ k
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.compHahnSeries_smul : ∀ {Γ : Type u_5} {Γ' : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_7} [inst_2 : CommRing R]
  {U : Type u_8} {V : Type u_9} {W : Type u_10} [inst_3 : AddCommGroup U] [inst_4 : Module R U]
  [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W]
  (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (r : R) (u : U),
  A.compHahnSeries B (r • u) = r • A.compHahnSeries B u
-- Mathlib.RingTheory.Extension.Generators
Algebra.FiniteType.iff_exists_generators : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.FiniteType R S ↔ ∃ n, Nonempty (Algebra.Generators R S (Fin n))
-- Mathlib.CategoryTheory.Action.Basic
Action.preservesColimits_forget : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasColimits V], CategoryTheory.Limits.PreservesColimits (Action.forget V G)
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_union_eq_left : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α},
  Disjoint s t →
    MulAction.stabilizer G s ≤ MulAction.stabilizer G t →
      MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G t →
        MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G s
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanShapeCoend_L : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J],
  (CategoryTheory.Limits.multispanShapeCoend J).L = CategoryTheory.Arrow J
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_counitIso_inv_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).counitIso.inv.app X).hom.app X_1 =
    X.obj.map (e.counitIso.hom.app (Opposite.unop X_1)).op
-- Mathlib.Tactic.Push
/-- `#push_discr_tree X` shows the discrimination tree of all lemmas used by `push X`.
This can be helpful when you are constructing a set of `push` lemmas for the constant `X`.
 -/
Mathlib.Tactic.Push.elabPushTree : Lean.Elab.Command.CommandElab
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsColimitsOfShape.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D},
  autoParam (∀ {K : CategoryTheory.Functor J C}, CategoryTheory.Limits.ReflectsColimit K F)
      CategoryTheory.Limits.ReflectsColimitsOfShape.reflectsColimit._autoParam →
    CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.instCoeOutComplex : CoeOut UpperHalfPlane ℂ
-- Mathlib.Order.WellQuasiOrder
/-- A preorder is well quasi-ordered iff it's well-founded and has no infinite antichains.  -/
wellQuasiOrderedLE_iff : ∀ {α : Type u_1} [inst : Preorder α],
  WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
-- Mathlib.Order.Heyting.Basic
Pi.instCoheytingAlgebra : {ι : Type u_1} → {α : ι → Type u_4} → [(i : ι) → CoheytingAlgebra (α i)] → CoheytingAlgebra ((i : ι) → α i)
-- Lean.Elab.Tactic.Ext
/-- Apply extensionality theorems as much as possible, using `pats` to introduce the variables
in extensionality theorems like `funext`. Returns a list of subgoals.

This is built on top of `withExtN`, running in `TermElabM` to build the list of new subgoals.
(And, for each goal, the patterns consumed.)
 -/
Lean.Elab.Tactic.Ext.extCore : Lean.MVarId →
  List (Lean.TSyntax `rcasesPat) →
    optParam ℕ 100 → optParam Bool true → Lean.Elab.TermElabM (ℕ × Array (Lean.MVarId × List (Lean.TSyntax `rcasesPat)))
-- Mathlib.RingTheory.Trace.Basic
Normal.algHomEquivAut.eq_1 : ∀ (F : Type u_1) [inst : Field F] (K₁ : Type u_3) [inst_1 : Field K₁] [inst_2 : Algebra F K₁] (E : Type u_6)
  [inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra E K₁] [inst_6 : IsScalarTower F E K₁]
  [inst_7 : Normal F E],
  Normal.algHomEquivAut F K₁ E =
    { toFun := fun σ => σ.restrictNormal' E, invFun := fun σ => (IsScalarTower.toAlgHom F E K₁).comp ↑σ, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.vadd_symm : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : ContinuousConstVAdd G α] {g : G}, (Homeomorph.vadd g).symm = Homeomorph.vadd (-g)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_commute : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R} {m : M} [inst_1 : Mul M],
  (∀ (m' : M), Commute m m') →
    (∀ (r' : R), Commute r r') → ∀ (x : MonoidAlgebra R M), Commute (MonoidAlgebra.single m r) x
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.pointwiseProductCompEvaluation_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4}
  [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) (d : D) (X : (i : α) → I i),
  (CategoryTheory.Limits.pointwiseProductCompEvaluation F d).inv.app X =
    (CategoryTheory.Limits.piObjIso ((CategoryTheory.Functor.pi F).obj X) d).inv
-- Mathlib.RepresentationTheory.Rep.Basic
Representation.equivOfIso_invFun : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (i : A ≅ B) (a : ↑B),
  (Representation.equivOfIso i).invFun a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
/-- If `x = {x_i : A | i : ι}` and `f = {f_i : MvPolynomial ι R | i : ι}` are algebraically
independent over `R`, then `{f_i(x) | i : ι}` is also algebraically independent over `R`.
For the partial converse, see `AlgebraicIndependent.of_aeval`.  -/
AlgebraicIndependent.aeval_of_algebraicIndependent : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ {f : ι → MvPolynomial ι R},
      AlgebraicIndependent R f → AlgebraicIndependent R fun i => (MvPolynomial.aeval x) (f i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_mul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  (f g : G ⟶ H), (f * g).hom = f.hom * g.hom
-- Mathlib.Topology.Constructions.SumProd
Filter.EventuallyEq.prodMap_nhds : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {α : Type u_5} {β : Type u_6}
  {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y},
  f₁ =ᶠ[nhds x] f₂ → g₁ =ᶠ[nhds y] g₂ → Prod.map f₁ g₁ =ᶠ[nhds (x, y)] Prod.map f₂ g₂
-- Init.Data.UInt.Lemmas
UInt32.sub_eq_iff_eq_add : ∀ {a b c : UInt32}, a - b = c ↔ a = c + b
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instCompleteSemilatticeSup : {ι : Type u_1} → CompleteSemilatticeSup (AbstractSimplicialComplex ι)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
NonUnitalStarAlgHom.restrictScalars.congr_simp : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Star A]
  [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : NonUnitalNonAssocSemiring B]
  [inst_6 : MulAction R S] [inst_7 : DistribMulAction S A] [inst_8 : DistribMulAction S B]
  [inst_9 : DistribMulAction R A] [inst_10 : DistribMulAction R B] [inst_11 : IsScalarTower R S A]
  [inst_12 : IsScalarTower R S B] (f f_1 : A →⋆ₙₐ[S] B),
  f = f_1 → NonUnitalStarAlgHom.restrictScalars R f = NonUnitalStarAlgHom.restrictScalars R f_1
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Pi.isoLimit.eq_1 : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasLimit X],
  CategoryTheory.Limits.Pi.isoLimit X =
    (CategoryTheory.Limits.productIsProduct' X).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit X)
-- Mathlib.GroupTheory.CoprodI
/-- The index first letter of tail of a `Pair M i` is not equal to `i`  -/
Monoid.CoprodI.Word.Pair.fstIdx_ne : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (self : Monoid.CoprodI.Word.Pair M i),
  self.tail.fstIdx ≠ some i
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.yoneda_preservesLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) (X : C), CategoryTheory.Limits.PreservesLimit F (CategoryTheory.yoneda.obj X)
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an encoded query parameter from an encoded string.
 -/
Std.Http.URI.EncodedQueryParam.fromString? : String → Option Std.Http.URI.EncodedQueryParam
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α} (h' : a ∈ t),
  t.getKey? a = some (t.getKey a h')
-- Init.Data.Nat.Lemmas
Nat.lt_of_div_lt_div : ∀ {a b c : ℕ}, a / c < b / c → a < b
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.ιChainComplex_d : ∀ {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 : ℕ} (x : X.obj (Opposite.op { len := n + 1 })),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x) ((X.chainComplex R).d (n + 1) n) =
    ∑ i, (-1) ^ ↑i • X.ιChainComplex ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X i)) x)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.center.coe_div : ∀ {K : Type u} [inst : DivisionRing K] (a b : ↥(Subring.center K)), ↑(a / b) = ↑a / ↑b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_total : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] (x y : R), x ≤ᵥ y ∨ y ≤ᵥ x
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_eq_zero_iff : ∀ {α : Type u_2} [inst : SubtractionMonoid α] {s t : Set α}, s + t = 0 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a + b = 0
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.filter_univ_mem : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), {x | x ∈ s} = s
-- Init.Grind.Ring.Field
Lean.Grind.Field.div_div_right : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {x y z : α}, x / (y / z) = x * z / y
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul.injEq : ∀ (k : ℤ) (e : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k_1 : ℤ) (e_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul k e = Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.mul k_1 e_1) =
    (k = k_1 ∧ e = e_1)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.Adhesive.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [hasPullback_of_mono_left :
    ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g]
  [hasPushout_of_mono_left :
    ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g],
  (∀ {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Mono f]
      (H : CategoryTheory.IsPushout f g h i), H.IsVanKampen) →
    CategoryTheory.Adhesive C
-- Mathlib.Data.Int.Init
Int.natMod_lt : ∀ {m : ℤ} {n : ℕ}, n ≠ 0 → m.natMod ↑n < n
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.realize_iff_of_model_completeTheory : ∀ {L : FirstOrder.Language} (M : Type w) (N : Type u_1) [inst : L.Structure M] [inst_1 : L.Structure N]
  [N ⊨ L.completeTheory M] (φ : L.Sentence), N ⊨ φ ↔ M ⊨ φ
-- Mathlib.Tactic.Ring.Common
/-- Attempts to prove that a monomial expression in `ℕ` is positive.

* `0 < c` (where `c` is a numeral) is true by the normalization invariant (`c` is not zero)
* `0 < x ^ e * b` if `0 < x` and `0 < b`
 -/
Mathlib.Tactic.Ring.Common.ExProdNat.evalPos : {a : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExProdNat a → Option Q(0 < «$a»)
-- Mathlib.Algebra.Algebra.ZMod
/-- The `ZMod p`-algebra structure on a ring of characteristic `p`. This is not an
instance since it creates a diamond with `Algebra.id`.
See note [reducible non-instances].  -/
ZMod.algebra : (R : Type u_1) → [inst : Ring R] → (p : ℕ) → [CharP R p] → Algebra (ZMod p) R
-- Mathlib.Algebra.Order.Interval.Basic
Interval.coe_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : One α], ↑1 = 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.Algebra.RingQuot
RingQuot.preLiftAlgHom : (S : Type u_1) →
  [inst : CommSemiring S] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra S A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra S B] →
                {s : A → A → Prop} → {f : A →ₐ[S] B} → (∀ ⦃x y : A⦄, s x y → f x = f y) → RingQuot s →ₐ[S] B
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `StructuredArrow.pre` is a special case of `StructuredArrow.map₂` up to natural isomorphism.  -/
CategoryTheory.StructuredArrow.preIsoMap₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (S : D) →
              (F : CategoryTheory.Functor B C) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.StructuredArrow.pre S F G ≅
                    CategoryTheory.StructuredArrow.map₂ (CategoryTheory.CategoryStruct.id S)
                      (CategoryTheory.CategoryStruct.id (F.comp G))
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_U : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens), I.glueData.U U = I.glueDataObj U
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_toSheafify : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  (P : CategoryTheory.Functor Cᵒᵖ A), J.W (CategoryTheory.toSheafify J P)
-- Mathlib.Data.Finset.Lattice.Fold
/-- Given nonempty finset `s` then `s.sup' H f` is the supremum of its image under `f` in (possibly
unbounded) join-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a bottom element
you may instead use `Finset.sup` which does not require `s` nonempty.  -/
Finset.sup' : {α : Type u_2} → {β : Type u_3} → [SemilatticeSup α] → (s : Finset β) → s.Nonempty → (β → α) → α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The homeomorphism induced from a two-sided continuous isomorphism of groups.  -/
ContinuousMulEquiv.toHomeomorph : {G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} → [inst_1 : TopologicalSpace H] → [inst_2 : Mul G] → [inst_3 : Mul H] → G ≃ₜ* H → G ≃ₜ H
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.ExtDTreeMap.foldrM f init t = List.foldrM (fun a b => f a.fst a.snd b) init t.toList
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {k a : α} {v : β}, (m.insertIfNew k v)[a]! = if (k == a) = true ∧ k ∉ m then v else m[a]!
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass.eq_1 : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (t : Finset ι) (w : ι → R) (z : ι → E), t.centerMass w z = (∑ i ∈ t, w i)⁻¹ • ∑ i ∈ t, w i • z i
-- Mathlib.Order.Fin.Finset
/-- This is the order isomorphism from `Fin 3`
to a finset `{a, b, c}` when `a < b` and `b < c`.  -/
Fin.orderIsoTriple : {α : Type u_1} → [inst : Preorder α] → [inst_1 : DecidableEq α] → (a b c : α) → a < b → b < c → Fin 3 ≃o ↥{a, b, c}
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent.  -/
Module.End.isNilpotent_restrict_genEigenspace_top : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R)
  (h : optParam (Set.MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ⊤) ↑((f.genEigenspace μ) ⊤)) ⋯),
  IsNilpotent (LinearMap.restrict (f - μ • 1) h)
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real tangent function, defined as the real part of the complex tangent  -/
Real.tan : ℝ → ℝ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {f : β → β}
  {fallback : α}, cmp ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Complex.measurable_re : Measurable Complex.re
-- Mathlib.Order.Cover
wcovBy_of_eq_or_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → (∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b) → a ⩿ b
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mean_smul_eq_mean : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.SMulInvariantMeasure G X μ],
  IsFoelner G μ (↑u) F → ∀ (g : G) (s : Set X), IsFoelner.mean μ u F (g • s) = IsFoelner.mean μ u F s
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.minDegree_pos_of_nontrivial : ∀ {V : Type u} [Nontrivial V] [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj],
  G.Preconnected → 0 < G.minDegree
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
`r / s` in each of the stalks (which are localizations at various prime ideals).
 -/
AlgebraicGeometry.StructureSheaf.IsFraction : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} →
          ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x) → Prop
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_singleton : ∀ {m n : ℕ}, n = m + 1 → (m...n).toList = [m]
-- Mathlib.Algebra.Lie.Derivation.Basic
/-- The `LinearMap` underlying a `LieDerivation`.  -/
LieDerivation.toLinearMap : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → LieDerivation R L M → L →ₗ[R] M
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α},
  Std.Internal.List.containsKey a l = true →
    Std.Internal.List.getKey? a l = some (Std.Internal.List.getKeyD a l fallback)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.mk : Option Lean.Meta.Grind.Goal →
  List Lean.MessageData →
    Lean.Grind.Config →
      Lean.Meta.Grind.Counters →
        Lean.Meta.Simp.Stats →
          Lean.PArray Lean.Meta.Grind.SplitDiagInfo →
            Lean.PArray Lean.Meta.Grind.EMatchDiagInfo → Lean.Meta.Grind.Result
-- Mathlib.Topology.Separation.Regular
RegularSpace.mk : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ {s : Set X} {a : X}, IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)) → RegularSpace X
-- Init.Data.Nat.Fold
Nat.all_eq_allTR : Nat.all = Nat.allTR
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_mapDomainBialgHomMulEquiv_apply_ofConv_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommGroup G]
  [inst_3 : CommGroup H] (a : G →* H) (a_1 : MonoidAlgebra R G),
  ((MonoidAlgebra.mapDomainBialgHomMulEquiv a).ofConv a_1).coeff = Finsupp.mapDomain (⇑a) a_1.coeff
-- Std.Http.Data.Status
/-- 413 Payload Too Large
 -/
Std.Http.Status.payloadTooLarge : Std.Http.Status
-- Init.Data.Rat.Lemmas
Rat.neg_divInt_neg : ∀ (num den : ℤ), Rat.divInt (-num) (-den) = Rat.divInt num den
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F.leftOp : Jᵒᵖ ⥤ C` into a limit for `F : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isLimitConeOfCoconeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F.leftOp} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c)
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_nonempty_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E},
  (balancedCore 𝕜 s).Nonempty ↔ 0 ∈ s
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.infDist_pos_iff_notMem_closure : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α}, s.Nonempty → (x ∉ closure s ↔ 0 < Metric.infDist x s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_toSpecΓ : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp hU.fromSpec X.toSpecΓ =
    AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_iff_forall_mul_nonpos`. -/
Antivary.sub_mul_sub_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Antivary f g → ∀ (i j : ι), (f j - f i) * (g j - g i) ≤ 0
-- Lean.Meta.Basic
/-- Return the user-facing name for the given free variable.  -/
Lean.FVarId.getUserName : Lean.FVarId → Lean.MetaM Lean.Name
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).getKey? k = if k ∈ m₂ then m₁.getKey? k else none
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.congr_vertex : ∀ {X : SSet} {n : ℕ} {f g : X.Path n}, f = g → ∀ (i : Fin (n + 1)), f.vertex i = g.vertex i