mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
/-- A set with upper and lower bounds in a locally finite order is a fintype  -/
Set.fintypeOfMemBounds : {α : Type u_2} →
  {a b : α} →
    [inst : Preorder α] →
      [LocallyFiniteOrder α] →
        {s : Set α} → [DecidablePred fun x => x ∈ s] → a ∈ lowerBounds s → b ∈ upperBounds s → Fintype ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.opEquiv_symm_apply : ∀ {X : SSet} (y : X.N), (RelIso.symm SSet.N.opEquiv) y = SSet.N.mk (SSet.opObjEquiv.symm y.simplex) ⋯
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.one_lt_coe : ∀ {α : Type u_1} [inst : LT α] {a : α} [inst_1 : One α], 1 < ↑a ↔ 1 < a
-- Lean.DocString.Types
/-- The part's textual content  -/
Lean.Doc.Part.content : {i : Type u} → {b : Type v} → {p : Type w} → Lean.Doc.Part i b p → Array (Lean.Doc.Block i b)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- **Alias** of the forward direction of `MvPolynomial.totalDegree_zero_iff_isHomogeneous`. -/
MvPolynomial.isHomogeneous_of_totalDegree_zero : ∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R] {p : MvPolynomial σ R}, p.totalDegree = 0 → p.IsHomogeneous 0
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- Two morphisms of sheaves of types `P ⟶ Q` coincide if the precompositions
with morphisms `uliftYoneda.obj X ⟶ P` agree.  -/
CategoryTheory.GrothendieckTopology.hom_ext_uliftYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {P Q : CategoryTheory.Sheaf J (Type (max v v'))} {f g : P ⟶ Q},
  (∀ (X : C) (p : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ P),
      CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) →
    f = g
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.sset.inj : ∀ {x : Lean.IR.VarId} {i offset : ℕ} {y : Lean.IR.VarId} {ty : Lean.IR.IRType} {b : Lean.IR.FnBody}
  {x_1 : Lean.IR.VarId} {i_1 offset_1 : ℕ} {y_1 : Lean.IR.VarId} {ty_1 : Lean.IR.IRType} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.sset x i offset y ty b = Lean.IR.FnBody.sset x_1 i_1 offset_1 y_1 ty_1 b_1 →
    x = x_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1 ∧ b = b_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Auxiliary lemma for `biprod.uniqueUpToIso`.  -/
CategoryTheory.Limits.biprod.conePointUniqueUpToIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (hb : b.IsBilimit),
  (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.BinaryBiproduct.isLimit X Y)).hom =
    CategoryTheory.Limits.biprod.lift b.fst b.snd
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `leOnePart_eq_one`. -/
leOnePart_of_one_le : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α} [MulLeftMono α], 1 ≤ a → a⁻ᵐ = 1
-- Init.Data.Iterators.ToIterator
/-- Converts `x` into a monadic iterator.  -/
Std.ToIterator.iterM : {γ : Type u_1} → {m : Type u_2 → Type u_3} → {α β : Type u_2} → γ → [Std.ToIterator γ m α β] → Std.IterM m β
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)`. Is the tree empty?  -/
RBTree.RBSet.isEmpty : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → Bool
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_re_add_im : ∀ {X : Type u_1} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6} [inst_1 : RCLike 𝕜] {f : X → 𝕜}
  {i : Set X},
  MeasureTheory.IntegrableOn f i μ →
    ↑(∫ (x : X) in i, RCLike.re (f x) ∂μ) + ↑(∫ (x : X) in i, RCLike.im (f x) ∂μ) * RCLike.I = ∫ (x : X) in i, f x ∂μ
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.neg : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : StarAddMonoid R] {x : R}, IsSelfAdjoint x → IsSelfAdjoint (-x)
-- Std.Data.HashSet.Basic
/-- Removes all elements from the hash set for which the given function returns `false`.  -/
Std.HashSet.filter : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → (α → Bool) → Std.HashSet α → Std.HashSet α
-- Mathlib.Tactic.Push
/-- Function elaborating `Push.Config`.  -/
Mathlib.Tactic.Push.elabPushConfig : Lean.Syntax →
  optParam Mathlib.Tactic.Push.Config { } → optParam Bool true → Lean.Elab.Tactic.TacticM Mathlib.Tactic.Push.Config
-- Mathlib.Data.Ordmap.Ordset
Ordnode.erase.eq_def : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α) (x_1 : Ordnode α),
  Ordnode.erase x x_1 =
    match x_1 with
    | Ordnode.nil => Ordnode.nil
    | _t@h:(Ordnode.node size l y r) =>
      match cmpLE x y with
      | Ordering.lt => (Ordnode.erase x l).balanceR y r
      | Ordering.eq => l.glue r
      | Ordering.gt => l.balanceL y (Ordnode.erase x r)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The function `oddKernel a` has exponential decay at `+∞`, for any `a`.  -/
HurwitzZeta.isBigO_atTop_oddKernel : ∀ (a : UnitAddCircle), ∃ p, 0 < p ∧ HurwitzZeta.oddKernel a =O[Filter.atTop] fun x => Real.exp (-p * x)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- An algebra homomorphism into the base field, as a continuous linear map (since it is
automatically bounded).  -/
AlgHom.toContinuousLinearMap : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NormedRing A] → [inst_2 : NormedAlgebra 𝕜 A] → [CompleteSpace A] → (A →ₐ[𝕜] 𝕜) → StrongDual 𝕜 A
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  ((CategoryTheory.MorphismProperty.coproducts.{t, v, u} W).pushouts.transfiniteCompositionsOfShape J).retracts ≤
    W.rlp.llp
-- Mathlib.Data.Finite.Sum
Finite.instPSum : ∀ {α : Sort u_3} {β : Sort u_4} [Finite α] [Finite β], Finite (α ⊕' β)
-- Init.Dynamic
/-- Returns a declaration name of the type.
 -/
TypeName.typeName : (α : Type u_1) → [TypeName α] → Lean.Name
-- Mathlib.Data.Set.Sigma
Set.empty_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)}, ∅.sigma t = ∅
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- the vector addition on the Ore localization of additive monoids.  -/
AddOreLocalization.vadd : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_2} →
          [inst_2 : AddAction R X] → AddOreLocalization S R → AddOreLocalization S X → AddOreLocalization S X
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.mkSimpleHandler : String → optParam ℕ 2 → Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.Order.Defs.Unbundled
MinimalFor.le_of_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] {P : ι → Prop} {f : ι → α} {i j : ι},
  MinimalFor P f i → P j → f j ≤ f i → f i ≤ f j
-- Init.Data.Nat.Basic
Nat.add_one_ne_add_one_iff : ∀ {a b : ℕ}, a + 1 ≠ b + 1 ↔ a ≠ b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w outWidth : ℕ} (aig : Std.Sat.AIG α) (idx' : ℕ)
  (x : aig.RefVec w) (acc : aig.RefVec (w * idx')) (h : idx' ≤ w) (h' : outWidth = w * w) (idx : ℕ)
  (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx' x acc h h').aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend.go idx' x acc h h').aig.decls[idx] = aig.decls[idx]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ∀ {v : β k}, (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_pow_eq_sum : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ),
  (x ^ n).snd = (List.map (fun i => MulOpposite.op (x.fst ^ i) • x.fst ^ (n.pred - i) • x.snd) (List.range n)).sum
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpen : ∀ {α : Type u_1} [inst : UniformSpace α] {U : Set α}, IsOpen U → IsOpen {s | (s ∩ U).Nonempty}
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.Result : Type
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.ofComapInfPrincipal_mem : ∀ {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g),
  s ∈ Ultrafilter.ofComapInfPrincipal h
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.BasicMeasure.mk.inj : ∀ {toTerminationMeasure : Lean.Elab.TerminationMeasure} {natFn : Lean.Expr}
  {toTerminationMeasure_1 : Lean.Elab.TerminationMeasure} {natFn_1 : Lean.Expr},
  { toTerminationMeasure := toTerminationMeasure, natFn := natFn } =
      { toTerminationMeasure := toTerminationMeasure_1, natFn := natFn_1 } →
    toTerminationMeasure = toTerminationMeasure_1 ∧ natFn = natFn_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The `s` coefficient of an admissible linear change of variables.  -/
WeierstrassCurve.VariableChange.s : {R : Type u} → [inst : CommRing R] → WeierstrassCurve.VariableChange R → R
-- Mathlib.Algebra.Category.Grp.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)  -/
CommGrpCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections] →
        CategoryTheory.Limits.IsLimit (CommGrpCat.limitCone F)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.coe_toLinearEquiv : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), ⇑e.toLinearEquiv = ⇑e
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_mul : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] E),
  ContinuousLinearMap.rTensor G (f₁ * f₂) = ContinuousLinearMap.rTensor G f₁ * ContinuousLinearMap.rTensor G f₂
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.vadd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : VAdd 𝕜 β] [ContinuousVAdd 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f +ᵥ g)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.jacobson_idem : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson.jacobson = I.jacobson
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go.eq_2 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)) (size : ℕ) (k' : α) (v' : β)
  (l r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k (some (k', v')) l
    | Ordering.eq => some (k', v')
    | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best r
-- Mathlib.Topology.WithTopology
WithTopology.ofTopology_toTopology : ∀ {X : Type u_1} (t : TopologicalSpace X) (x : X), (WithTopology.toTopology t x).ofTopology = x
-- Lean.Elab.DocString
Lean.Doc.CodeSuggestion.mk.injEq : ∀ (role : Lean.Name) (args moreInfo : Option String) (role_1 : Lean.Name) (args_1 moreInfo_1 : Option String),
  ({ role := role, args := args, moreInfo := moreInfo } = { role := role_1, args := args_1, moreInfo := moreInfo_1 }) =
    (role = role_1 ∧ args = args_1 ∧ moreInfo = moreInfo_1)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.toIsMultiplicative : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasLeftCalculusOfFractions], W.IsMultiplicative
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_sub_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y z : E), inner 𝕜 x (y - z) = inner 𝕜 x y - inner 𝕜 x z
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_ofNat : ∀ {d : ℤ} (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).im = 0
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp},
  t₁.WF → (t₁ ∩ t₂).WF
-- Mathlib.Order.Basic
DenselyOrdered.dense' : ∀ {α : Type u_2} [inst : LT α] [DenselyOrdered α] (a₁ a₂ : α), a₁ < a₂ → ∃ a < a₂, a₁ < a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toList_insert_perm : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.insert k).toList.Perm (if k ∈ m then m.toList else k :: m.toList)
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_self : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.relIndex H = 1
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond_toMeasurable_eq : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s : Set Ω},
  μ[|MeasureTheory.toMeasurable μ s] = μ[|s]
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.skipSuffix?_prop_eq_some_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String} {pos : s.Pos},
  s.skipSuffix? P = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ P ((s.endPos.prev h).get ⋯)
-- Aesop.Util.Tactic.Unfold
_private.Aesop.Util.Tactic.Unfold.0.Aesop.mkToUnfold : Array Lean.Ident → Lean.MetaM (Std.HashMap Lean.Name (Option Lean.Name))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.size ≤ (t.insertManyIfNewUnit l).size
-- Init.Omega.Constraint
Lean.Omega.bmod_sat : ∀ (m : ℕ) (r : ℤ) (i : ℕ) (x v : Lean.Omega.Coeffs),
  x.length ≤ i →
    v.get i = Lean.Omega.bmod_div_term m x v →
      (Lean.Omega.Constraint.exact r).sat' x v = true →
        (Lean.Omega.Constraint.exact (r.bmod m)).sat' (Lean.Omega.bmod_coeffs m i x) v = true
-- Mathlib.Order.Filter.Bases.Finite
Set.PairwiseDisjoint.exists_mem_filter_basis : ∀ {α : Type u_1} {I : Type u_6} {l : I → Filter α} {ι : I → Sort u_7} {p : (i : I) → ι i → Prop}
  {s : (i : I) → ι i → Set α} {S : Set I},
  S.PairwiseDisjoint l →
    S.Finite →
      (∀ (i : I), (l i).HasBasis (p i) (s i)) →
        ∃ ind, (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun i => s i (ind i)
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_convMul : ∀ {R : Type u_5} {A : Type u_6} {C : Type u_7} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : SMulCommClass R A A]
  [inst_5 : IsScalarTower R A A] [inst_6 : StarRing A] [inst_7 : StarModule R A] [inst_8 : AddCommMonoid C]
  [inst_9 : Module R C] [inst_10 : StarAddMonoid C] [inst_11 : StarModule R C] [inst_12 : CoalgebraStruct R C],
  star (WithConv.toConv CoalgebraStruct.comul) =
      WithConv.toConv (↑(TensorProduct.comm R C C) ∘ₗ CoalgebraStruct.comul) →
    ∀ (f g : WithConv (C →ₗ[R] A)), star (f * g) = star g * star f
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.ofRepr.inj : ∀ {ι : Type u_1} {𝕜 : Type u_3} {inst : RCLike 𝕜} {E : Type u_4} {inst_1 : NormedAddCommGroup E}
  {inst_2 : InnerProductSpace 𝕜 E} {inst_3 : Fintype ι} {repr repr_1 : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι},
  { repr := repr } = { repr := repr_1 } → repr = repr_1
-- Lean.Elab.Util
Lean.Elab.MonadMacroAdapter.mk : {m : Type → Type} →
  [toMonadQuotation : Lean.MonadQuotation m] →
    m Lean.MacroScope → (Lean.MacroScope → m Unit) → Lean.Elab.MonadMacroAdapter m
-- Mathlib.GroupTheory.Exponent
Monoid.ExponentExists.isOfFinOrder : ∀ {G : Type u} [inst : Monoid G], Monoid.ExponentExists G → ∀ {g : G}, IsOfFinOrder g
-- Mathlib.Algebra.Lie.Prod
LieHom.pair_fst_snd : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂], (LieHom.fst R L₁ L₂).prod (LieHom.snd R L₁ L₂) = LieHom.id
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.sum_lt_of_isRegular : ∀ {c : Cardinal.{u}} {ι : Type u} {f : ι → Cardinal.{u}},
  c.IsRegular → Cardinal.mk ι < c → (∀ (i : ι), f i < c) → Cardinal.sum f < c
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.posRootForm_posForm_nondegenerate : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [inst_7 : LinearOrder S] [inst_8 : IsStrictOrderedRing S] [IsDomain R]
  [inst_10 : Algebra S R] [inst_11 : FaithfulSMul S R] [inst_12 : P.IsValuedIn S] [inst_13 : Module S M]
  [inst_14 : IsScalarTower S R M] [inst_15 : Module S N] [IsScalarTower S R N], (P.posRootForm S).posForm.Nondegenerate
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and `X₂ : C₂`, this is the obvious functor
`StructuredArrow X₂ T ⥤ StructuredArrow (R.obj X₂) B`.  -/
CategoryTheory.TwoSquare.structuredArrowDownwards : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B →
                          (X₂ : C₂) →
                            CategoryTheory.Functor (CategoryTheory.StructuredArrow X₂ T)
                              (CategoryTheory.StructuredArrow (R.obj X₂) B)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mk.sizeOf_spec : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] [inst_4 : SizeOf A] [inst_5 : SizeOf σ] (asHomogeneousIdeal : HomogeneousIdeal 𝒜)
  (isPrime : asHomogeneousIdeal.toIdeal.IsPrime)
  (not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal),
  sizeOf { asHomogeneousIdeal := asHomogeneousIdeal, isPrime := isPrime, not_irrelevant_le := not_irrelevant_le } =
    1 + sizeOf asHomogeneousIdeal + sizeOf isPrime
-- Mathlib.Data.Set.Insert
Set.pair_eq_singleton : ∀ {α : Type u_1} (a : α), {a, a} = {a}
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addCHaar_mem_clAddPrehaar : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (V : TopologicalSpace.OpenNhdsOf 0),
  MeasureTheory.Measure.haar.addCHaar K₀ ∈ MeasureTheory.Measure.haar.clAddPrehaar (↑K₀) V
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instFrame : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → Order.Frame (π i)] → Order.Frame ((i : ι) → π i)
-- Mathlib.Topology.Closure
IsOpen.subset_interior_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen s → (s ⊆ interior t ↔ s ⊆ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Pasting two pullback cones vertically is isomorphic to the pullback cone obtained by flipping
them, pasting horizontally, and then flipping the result again.  -/
CategoryTheory.Limits.PullbackCone.pasteVertFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) →
              {i₂ : t₁.pt ⟶ X₂} →
                (t₂ : CategoryTheory.Limits.PullbackCone i₂ f₂) →
                  (hi₂ : i₂ = t₁.snd) → (t₁.pasteVert t₂ hi₂).flip ≅ t₁.flip.pasteHoriz t₂.flip hi₂
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoalCore.mk.sizeOf_spec : ∀ (hyps : Array Lean.Widget.InteractiveHypothesisBundle) (type : Lean.Widget.CodeWithInfos)
  (ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo),
  sizeOf { hyps := hyps, type := type, ctx := ctx } = 1 + sizeOf hyps + sizeOf type + sizeOf ctx
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
_private.Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence.0.Mathlib.Tactic.Bicategory.«term_◁_» : Lean.TrailingParserDescr
-- Lean.Util.Recognizers
Lean.Expr.natAdd? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSymbolTag : BEq Lean.Lsp.SymbolTag
-- Mathlib.Logic.Function.Defs
Function.prod_fst_comp_snd_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (h : ι → α × β), Function.prod (Prod.fst ∘ h) (Prod.snd ∘ h) = h
-- Mathlib.Data.TypeVec
TypeVec.subtypeVal.eq_1 : ∀ (n : ℕ) (x_4 : TypeVec.{u} n.succ) (x_5 : x_4.Arrow (TypeVec.repeat n.succ Prop)) (i : Fin2 n),
  TypeVec.subtypeVal x_5 i.fs = TypeVec.subtypeVal (TypeVec.dropFun x_5) i
-- Std.Data.DTreeMap.Internal.Zipper
/-- Removes all elements with key less than to `lowerBound`.

Does not modify size information stored in the tree.
 -/
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.pruneLT : {α : Type u_1} → {β : α → Type u_2} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Group.Pi.Basic
Pi.semigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Semigroup (f i)],
  Pi.semigroup = { toMul := Pi.instMul, mul_assoc := ⋯ }
-- Mathlib.Order.WithBot
WithBot.eq_bot_iff_forall_le : ∀ {α : Type u_1} [inst : Preorder α] {x : WithBot α} [NoBotOrder α], x = ⊥ ↔ ∀ (b : α), x ≤ ↑b
-- Mathlib.Order.Heyting.Basic
sdiff_eq_bot_iff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b \ a = ⊥ ↔ b ≤ a
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.orbit_injective : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  Function.Injective MulAction.orbitRel.Quotient.orbit
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tprod_div₀ : ∀ {α : Type u_1} {K : Type u_4} [inst : CommGroupWithZero K] [inst_1 : TopologicalSpace K] {f g : α → K}
  {L : SummationFilter α} [ContinuousInv₀ K] [ContinuousMul K] [T2Space K] [L.NeBot],
  Multipliable f L →
    Multipliable g L → ∏'[L] (x : α), g x ≠ 0 → ∏'[L] (x : α), f x / g x = (∏'[L] (x : α), f x) / ∏'[L] (x : α), g x
-- Std.Data.DTreeMap.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DTreeMap.beq : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → [(k : α) → BEq (β k)] → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp → Bool
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.liftNC_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Mul G] {R : Type u_3} [inst_1 : Semiring R] [inst_2 : NonAssocSemiring k]
  [inst_3 : SMul G k] {g_hom : Type u_4} [inst_4 : FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom)
  (a b : SkewMonoidAlgebra k G),
  (∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)) →
    (SkewMonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (SkewMonoidAlgebra.liftNC ↑f ⇑g) a * (SkewMonoidAlgebra.liftNC ↑f ⇑g) b