mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).unitIso.hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} (h' : k ∈ Std.DHashMap.filterMap f m),
  (f k (m.get k ⋯)).isSome = true
-- Mathlib.Topology.Separation.CompletelyRegular
separatesPoints_continuous_of_t35Space_Icc : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], {f | Continuous f}.SeparatesPoints
-- Lean.Meta.AppBuilder
/-- Returns `funext h`  -/
Lean.Meta.mkFunExt : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.Heyting.Basic
codisjoint_hnot_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α}, Codisjoint (￢a) a
-- Lean.Data.OpenDecl
Lean.OpenDecl.explicit : Lean.Name → Lean.Name → Lean.OpenDecl
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.mk.injEq : ∀ (triggerKind : Lean.Lsp.SignatureHelpTriggerKind) (triggerCharacter? : Option String) (isRetrigger : Bool)
  (activeSignatureHelp? : Option Lean.Lsp.SignatureHelp) (triggerKind_1 : Lean.Lsp.SignatureHelpTriggerKind)
  (triggerCharacter?_1 : Option String) (isRetrigger_1 : Bool) (activeSignatureHelp?_1 : Option Lean.Lsp.SignatureHelp),
  ({ triggerKind := triggerKind, triggerCharacter? := triggerCharacter?, isRetrigger := isRetrigger,
        activeSignatureHelp? := activeSignatureHelp? } =
      { triggerKind := triggerKind_1, triggerCharacter? := triggerCharacter?_1, isRetrigger := isRetrigger_1,
        activeSignatureHelp? := activeSignatureHelp?_1 }) =
    (triggerKind = triggerKind_1 ∧
      triggerCharacter? = triggerCharacter?_1 ∧
        isRetrigger = isRetrigger_1 ∧ activeSignatureHelp? = activeSignatureHelp?_1)
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated cancellative monoid with a single unit is generated by its (finitely many)
irreducible elements.  -/
Submonoid.closure_irreducible : ∀ {M : Type u_1} [inst : CancelCommMonoid M] [Subsingleton Mˣ] [Monoid.FG M], Submonoid.closure {p | Irreducible p} = ⊤
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For a finite subset `s` of `M ⊗[R] N`, there exists a finitely generated
submodule `M'` of `M`, such that `s` is contained in the image
of `M' ⊗[R] N` in `M ⊗[R] N`.  -/
TensorProduct.exists_finite_submodule_left_of_setFinite : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (s : Set (TensorProduct R M N)),
  s.Finite → ∃ M', Module.Finite R ↥M' ∧ s ⊆ ↑(LinearMap.rTensor N M'.subtype).range
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β],
  sSupHom.dual =
    { toFun := fun f => { toFun := ⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual, map_sInf' := ⋯ },
      invFun := fun f => { toFun := ⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual, map_sSup' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Complex.BigOperators
Complex.im_balance : ∀ {α : Type u_1} [inst : Fintype α] (f : α → ℂ) (a : α), (Fintype.balance f a).im = Fintype.balance (Complex.im ∘ f) a
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_eq_arith_mean2_weighted_iff_of_nonneg : ∀ {w₁ w₂ p₁ p₂ : ℝ},
  0 ≤ w₁ → 0 ≤ w₂ → 0 ≤ p₁ → 0 ≤ p₂ → w₁ + w₂ = 1 → (p₁ ^ w₁ * p₂ ^ w₂ = w₁ * p₁ + w₂ * p₂ ↔ w₁ = 0 ∨ w₂ = 0 ∨ p₁ = p₂)
-- Mathlib.RingTheory.Nilpotent.Exp
Module.End.exp_mul_of_derivation : ∀ (R : Type u_4) (B : Type u_5) [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing B] [inst_2 : Module R B]
  [SMulCommClass R B B] [IsScalarTower R B B] [inst_5 : Module ℚ B] (D : B →ₗ[R] B),
  (∀ (x y : B), D (x * y) = x * D y + D x * y) →
    IsNilpotent D → ∀ (x y : B), (IsNilpotent.exp D) (x * y) = (IsNilpotent.exp D) x * (IsNilpotent.exp D) y
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.elim : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {a : α}
  {p : Prop}, IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p
-- Init.Data.Int.DivMod.Lemmas
Int.mul_lt_mul_right : ∀ {a b c : ℤ}, 0 < a → (b * a < c * a ↔ b < c)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ {g₁ g₂ : Y ⟶ CategoryTheory.OrthogonalReflection.step W Z},
      CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂ →
        CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.OrthogonalReflection.fromStep W Z) =
          CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.OrthogonalReflection.fromStep W Z)
-- Batteries.Data.Array.Lemmas
/-- **Alias** of `Array.getElem_insertIdx_of_gt`. -/
Array.getElem_insertIdx_gt : ∀ {α : Type u} {xs : Array α} {x : α} {i k : ℕ} (w : k ≤ xs.size) (h : k > i), (xs.insertIdx i x ⋯)[k] = xs[k - 1]
-- Mathlib.RingTheory.TensorProduct.Basic
/-- If `N` is an `A` module, we may lift a linear map `M →ₗ[R] N` to `A ⊗[R] M →ₗ[A] N`  -/
LinearMap.liftBaseChange : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      (A : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      [inst_7 : Module A N] → [IsScalarTower R A N] → (M →ₗ[R] N) → TensorProduct R A M →ₗ[A] N
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.GeneralTheorems.mk : Lean.Meta.RefinedDiscrTree Mathlib.Meta.FunProp.GeneralTheorem → Mathlib.Meta.FunProp.GeneralTheorems
-- Mathlib.Analysis.Convex.Function
convexOn_id : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMul 𝕜 β] {s : Set β}, Convex 𝕜 s → ConvexOn 𝕜 s id
-- Init.Data.Int.Lemmas
Int.neg_one_mul : ∀ (a : ℤ), -1 * a = -a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.Scheme.Hom.isQuasiSeparated_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens},
  IsQuasiSeparated ↑U → IsQuasiSeparated ↑((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalCommRing` across an `Equiv`  -/
Equiv.nonUnitalCommRing : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalCommRing β] → NonUnitalCommRing α
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E]
  [ContinuousSMul 𝕜 E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜 F] [T2Space F]
  (f : E →L[𝕜] F) [FiniteDimensional 𝕜 ↥(↑f).range], (↑f).ker.ClosedComplemented
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.isOpenEmbedding_coe : Topology.IsOpenEmbedding UpperHalfPlane.coe
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- **Alias** of `ContDiffAt.implicitFunction`.

---

Implicit function `ψ` defined by `f (x, ψ x) = f u`.  -/
IsContDiffImplicitAt.implicitFunction : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {E₁ : Type u_2} →
      [inst_1 : NormedAddCommGroup E₁] →
        [inst_2 : NormedSpace 𝕜 E₁] →
          [CompleteSpace E₁] →
            {E₂ : Type u_3} →
              [inst_4 : NormedAddCommGroup E₂] →
                [inst_5 : NormedSpace 𝕜 E₂] →
                  [CompleteSpace E₂] →
                    {F : Type u_4} →
                      [inst_7 : NormedAddCommGroup F] →
                        [inst_8 : NormedSpace 𝕜 F] →
                          [CompleteSpace F] →
                            {u : E₁ × E₂} →
                              {f : E₁ × E₂ → F} →
                                {n : WithTop ℕ∞} →
                                  ContDiffAt 𝕜 n f u →
                                    n ≠ 0 → (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible → E₁ → E₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.toString : Std.Tactic.BVDecide.BVPred → String
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.isIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : DerivedCategory.Plus C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((DerivedCategory.Plus.homologyFunctor C n).map f)
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- Given the distribution up to tome `a`, `partialTraj κ a b` gives the distribution
of the trajectory up to time `b`, and composing this with `traj κ b` gives the distribution
of the whole trajectory.  -/
ProbabilityTheory.Kernel.traj_comp_partialTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a b : ℕ},
  a ≤ b →
    (ProbabilityTheory.Kernel.traj κ b).comp (ProbabilityTheory.Kernel.partialTraj κ a b) =
      ProbabilityTheory.Kernel.traj κ a
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single_map_f_self_assoc : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : V} (f : A ⟶ B) {Z : V} (h : ((HomologicalComplex.single V c j).obj B).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single V c j).map f).f j) h =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j B).inv h))
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
exists_finrank_eq_sigPos_and_posDef : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R],
  ∃ V, Module.finrank R ↥V = sigPos Q ∧ (QuadraticMap.restrict Q V).PosDef
-- Mathlib.Data.NNRat.Defs
NNRat.mk_divInt : ∀ (n d : ℕ), ⟨Rat.divInt ↑n ↑d, ⋯⟩ = NNRat.divNat n d
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.parents : Lean.Meta.Grind.ParentSet → List Lean.Expr
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.mul_lt_one_of_le_of_lt`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_le_of_lt`.  -/
mul_lt_one_of_le_of_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, a ≤ 1 → b < 1 → a * b < 1
-- Mathlib.Algebra.Group.Equiv.Defs
AddMonoidHom.toAddEquiv.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (g : N →+ M)
  (h₁ : g.comp f = AddMonoidHom.id M) (h₂ : f.comp g = AddMonoidHom.id N),
  f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.withAntiquotSuffixSplice.parenthesizer : Lean.SyntaxNodeKind →
  Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.inv : ∀ {G : Type u_4} [inst : InvolutiveInv G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {s : Set G},
  IsPathConnected s → IsPathConnected s⁻¹
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_sup : ∀ {α : Type u_1} [inst : DecidableEq α] (f g : α →₀ ℕ),
  Finsupp.toMultiset (f ⊔ g) = Finsupp.toMultiset f ∪ Finsupp.toMultiset g
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.asyncMode : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → Lean.EnvExtension.AsyncMode
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.sInter : ∀ {α : Type u_2} {S : Set (Set α)} [inst : LE α], (∀ s ∈ S, CountableInfClosed s) → CountableInfClosed (⋂₀ S)
-- Mathlib.Data.Sum.Interval
Sum.Iio_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : LocallyFiniteOrderBot β] (a : α), Finset.Iio (Sum.inl a) = Finset.map Function.Embedding.inl (Finset.Iio a)
-- Mathlib.Data.List.Cycle
Cycle.mem_lists_iff_coe_eq : ∀ {α : Type u_1} {s : Cycle α} {l : List α}, l ∈ s.lists ↔ ↑l = s
-- Mathlib.Data.DFinsupp.Module
/-- `DFinsupp.subtypeDomain` as a `LinearMap`.  -/
DFinsupp.subtypeDomainLinearMap : {ι : Type u} →
  (γ : Type w) →
    (β : ι → Type v) →
      [inst : Semiring γ] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] →
          [inst_2 : (i : ι) → Module γ (β i)] →
            (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) →ₗ[γ] Π₀ (i : Subtype p), β ↑i
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.lie_mem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (self : LieSubmodule R L M) {x : L} {m : M},
  m ∈ (↑self).carrier → ⁅x, m⁆ ∈ (↑self).carrier
-- Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
aemeasurable_smul_const : ∀ {α : Type u_1} [inst : MeasurableSpace α] {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_3 : MeasurableSpace 𝕜] [BorelSpace 𝕜] {E : Type u_3} [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E]
  [inst_7 : MeasurableSpace E] [BorelSpace E] {f : α → 𝕜} {μ : MeasureTheory.Measure α} {c : E},
  c ≠ 0 → (AEMeasurable (fun x => f x • c) μ ↔ AEMeasurable f μ)
-- Mathlib.Data.List.Forall2
List.forall₂_drop : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} (n : ℕ) {l₁ : List α} {l₂ : List β},
  List.Forall₂ R l₁ l₂ → List.Forall₂ R (List.drop n l₁) (List.drop n l₂)
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.toValuation_symm_eq : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀],
  AddValuation.toValuation.symm = AddValuation.ofValuation
-- Mathlib.Order.RelIso.Basic
/-- `Prod.map` as a relation embedding.  -/
RelEmbedding.prodLexMap : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {r : α → α → Prop} →
          {s : β → β → Prop} → {t : γ → γ → Prop} → {u : δ → δ → Prop} → r ↪r s → t ↪r u → Prod.Lex r t ↪r Prod.Lex s u
-- Mathlib.GroupTheory.Nilpotent
addCommGroupOfNilpotencyClass.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : AddGroup.IsNilpotent G] (h : AddGroup.nilpotencyClass G ≤ 1),
  addCommGroupOfNilpotencyClass h = AddGroup.addCommGroupOfCenterEqTop ⋯
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ext : ∀ {X : Type u_5} {inst : TopologicalSpace X} {x y : DiscreteQuotient X}, ⇑x.toSetoid = ⇑y.toSetoid → x = y
-- Std.Data.String.ToInt
String.Slice.toInt?_congr : ∀ {s t : String.Slice}, s.copy = t.copy → s.toInt? = t.toInt?
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_int_of_map_zero : ∀ (f : CircleDeg1Lift) (n : ℤ), f ↑n = f 0 + ↑n
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  IntermediateField.fixedField ⊥ = ⊤
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.slice.injEq : ∀ (numPrefix numSuffix numPrefix_1 numSuffix_1 : ℕ),
  (Lean.Elab.Term.Quotation.HeadCheck.slice numPrefix numSuffix =
      Lean.Elab.Term.Quotation.HeadCheck.slice numPrefix_1 numSuffix_1) =
    (numPrefix = numPrefix_1 ∧ numSuffix = numSuffix_1)
-- Mathlib.Algebra.Lie.TraceForm
killingForm_apply_apply : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L),
  ((killingForm R L) x) y = (LinearMap.trace R L) ((LieAlgebra.ad R L) x ∘ₗ (LieAlgebra.ad R L) y)
-- Mathlib.Data.Int.Cast.Prod
Prod.snd_intCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β] (n : ℤ), (↑n).2 = ↑n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstr.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Meta.Grind.Arith.Linear.RingEqCnstr.brecOn.go t F_1 F_2).2
-- Mathlib.MeasureTheory.Measure.Dirac
HasSum.isProbabilityMeasure_sum_dirac_ennreal : ∀ {δ : Type u_3} {ι : Type u_4} {mδ : MeasurableSpace δ} {c : ι → ENNReal} {d : ι → δ},
  HasSum c 1 →
    MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (d i))
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- If `A` has doubling strictly less than `3 / 2`, then `A⁻¹ * A` is a subgroup.

Note that this is sharp: `A = {0, 1}` in `ℤ` has doubling `3 / 2` and `A⁻¹ * A` isn't a subgroup.  -/
Finset.invMulSubgroup : {G : Type u_1} →
  [inst : Group G] → [inst_1 : DecidableEq G] → (A : Finset G) → ↑(A * A).card < 3 / 2 * ↑A.card → Subgroup G
-- Std.Data.DHashMap.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.DHashMap.erase : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → Std.DHashMap α β
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_sdiff_Ico_same : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Icc a b \ Set.Ico a b = {b}
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.center_le_centralizer : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (s : Set R),
  NonUnitalSubsemiring.center R ≤ NonUnitalSubsemiring.centralizer s
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_nonempty_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ} {s : Set α}, (Metric.thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty
-- Lean.Message
Lean.MessageData.tagged.injEq : ∀ (a : Lean.Name) (a_1 : Lean.MessageData) (a_2 : Lean.Name) (a_3 : Lean.MessageData),
  (Lean.MessageData.tagged a a_1 = Lean.MessageData.tagged a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.instBialgEquivClass : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  BialgEquivClass (A ≃ₐc[R] B) R A B
-- Mathlib.RingTheory.WittVector.Defs
/-- The polynomials used for defining the element `1` of the ring of Witt vectors.  -/
WittVector.wittOne : (p : ℕ) → [hp : Fact (Nat.Prime p)] → ℕ → MvPolynomial (Fin 0 × ℕ) ℤ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_union_of_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∈ m₁ → k ∈ m₁ ∪ m₂
-- Mathlib.GroupTheory.Focal
Subgroup.ker_transferFocal_inf_eq_focalSubgroup : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G) [inst_2 : (↑P).FiniteIndex],
  (↑P).transferFocal.ker ⊓ ↑P = (↑P).focalSubgroup
-- Mathlib.Analysis.Calculus.FDeriv.Const
HasFDerivWithinAt.of_notMem_tsupport : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s : Set E} {x : E}, x ∉ tsupport f → HasFDerivWithinAt f 0 s x
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.restrict.congr_simp : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  (w w_1 : Convexity.StdSimplex K X) (e_w : w = w_1) (s s_1 : Set X) (e_s : s = s_1) (hs : ∃ x ∈ s, w.weights x ≠ 0),
  w.restrict s hs = w_1.restrict s_1 ⋯
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (X : CategoryTheory.GradedObject I C), CategoryTheory.GradedObject.Monoidal.tensorUnit.HasTensor X
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.fun_neg : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Neg β]
  [ContinuousNeg β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun i => -f i
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_of_ne_zero : ∀ {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}),
  o ≠ 0 → Ordinal.veblenWith f o = Ordinal.derivFamily fun x => Ordinal.veblenWith f ↑x
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.inclusionOfMooreComplex_app : ∀ (A : Type u_2) [inst : CategoryTheory.Category.{v_2, u_2} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A),
  (AlgebraicTopology.inclusionOfMooreComplex A).app X = AlgebraicTopology.inclusionOfMooreComplexMap X
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.toEquiv_inj : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, e.toEquiv = e'.toEquiv ↔ e = e'
-- Mathlib.Tactic.SetNotationForOrder
/-- Elaborator for `x ⊇ y` notation.  -/
Mathlib.Meta.SetNotationForOrder.elabSupsetStx' : Lean.Elab.Term.TermElab
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.le.sizeOf_spec : sizeOf Lean.Elab.WF.GuessLex.GuessLexRel.le = 1