mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.PosPart
Pi.oneLePart_apply : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → Group (α i)]
  (f : (i : ι) → α i) (i : ι), f⁺ᵐ i = (f i)⁺ᵐ
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `M → M → α` function to `ArchimedeanClass M → ArchimedeanClass M → α`.  -/
ArchimedeanClass.lift₂ : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {α : Type u_2} →
          (f : M → M → α) →
            (∀ (a₁ b₁ a₂ b₂ : M),
                ArchimedeanClass.mk a₁ = ArchimedeanClass.mk b₁ →
                  ArchimedeanClass.mk a₂ = ArchimedeanClass.mk b₂ → f a₁ a₂ = f b₁ b₂) →
              ArchimedeanClass M → ArchimedeanClass M → α
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (x : ι) → MeasurableSpace (β x)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.Kernel.IndepFun (f i) (f j) κ μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.DHashMap.Raw.Const.unitOfList l).getKey! k' = k
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mk''_I : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  [inst_2 : Topology.RelCWComplex E D] (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E) (n : ℕ),
  (Topology.RelCWComplex.Subcomplex.mk'' C E I union).I n = I n
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.sum_Iio_add_zero_comm : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : LinearOrder α] [inst_2 : LocallyFiniteOrderBot α]
  [inst_3 : Add α] [inst_4 : One α] [SuccAddOrder α] [NoMaxOrder α] (a : α) (f : α → M),
  ∑ i < a + 1, f i = f a + ∑ i < a, f i
-- Mathlib.Algebra.Algebra.Hom
AlgHom.commutes : ∀ {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] (φ : A →ₐ[R] B) (r : R), φ ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {η : ProbabilityTheory.Kernel γ δ}
  (κ : ProbabilityTheory.Kernel α β), ¬ProbabilityTheory.IsSFiniteKernel η → κ.parallelComp η = 0
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.fromOpposite_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.forInStep.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ),
  Std.DTreeMap.Internal.Impl.forInStep f init Std.DTreeMap.Internal.Impl.leaf = pure (ForInStep.yield init)
-- Mathlib.RingTheory.SimpleModule.Basic
instIsSemisimpleRingOfSubsingleton : ∀ (R : Type u_2) [inst : Ring R] [Subsingleton R], IsSemisimpleRing R
-- Mathlib.RingTheory.RootsOfUnity.Basic
mem_rootsOfUnity : ∀ {M : Type u_1} [inst : CommMonoid M] (k : ℕ) (ζ : Mˣ), ζ ∈ rootsOfUnity k M ↔ ζ ^ k = 1
-- Init.Data.UInt.Lemmas
USize.ofBitVec_ofNat : ∀ (n : ℕ), { toBitVec := BitVec.ofNat System.Platform.numBits n } = OfNat.ofNat n
-- Mathlib.Algebra.GroupWithZero.Regular
/-- A left-regular element of a `Nontrivial` `MulZeroClass` is non-zero.  -/
IsLeftRegular.ne_zero : ∀ {R : Type u_1} [inst : MulZeroClass R] {a : R} [Nontrivial R], IsLeftRegular a → a ≠ 0
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.not_isSingular_aleph_one : ¬(Cardinal.aleph 1).IsSingular
-- Mathlib.Tactic.Order.Graph.Basic
/-- Adds an `edge` to the graph.  -/
Mathlib.Tactic.Order.Graph.addEdge : Mathlib.Tactic.Order.Graph → Mathlib.Tactic.Order.Edge → Mathlib.Tactic.Order.Graph
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExcept_eq_tsum : ∀ (L : PeriodPair) (l₀ z x : ℂ),
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) →
    L.weierstrassPExcept l₀ z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₄_sq : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K], FermatLastTheoremForThreeGen.Solution.u₄✝ S ^ 2 = 1
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The function `evenKernel a - L` has exponential decay at `+∞`, where `L = 1` if
`a = 0` and `L = 0` otherwise.  -/
HurwitzZeta.isBigO_atTop_evenKernel_sub : ∀ (a : UnitAddCircle),
  ∃ p,
    0 < p ∧ (fun x => HurwitzZeta.evenKernel a x - if a = 0 then 1 else 0) =O[Filter.atTop] fun x => Real.exp (-p * x)
-- Lean.Declaration
Lean.instBEqConstructor.beq : Lean.Constructor → Lean.Constructor → Bool
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.eq_zero_of_fst_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {z : S} {x : R} {y : ↥M},
  z * (algebraMap R S) ↑y = (algebraMap R S) x → x = 0 → z = 0
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.ext_of_iInf : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type w}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B) [Algebra.FormallyUnramified R A],
  ⨅ i, I ^ i = ⊥ →
    ∀ {g₁ g₂ : A →ₐ[R] B}, (∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)) → g₁ = g₂
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ) {Z : C} (h : X.left.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.s n) (CategoryTheory.CategoryStruct.comp (X.left.δ 0) h) = h
-- Std.Http.Protocol.H1
/-- Handles fixed-length writer state when no user bytes are currently buffered.

If the producer closed without providing all declared bytes, closes both
reader and writer and terminates the connection.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.processFixedIdleBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Order.Concept
Concept.codisjoint_extent_intent : ∀ {α : Type u_2} {r' : α → α → Prop} {c' : Concept α α r'} [Std.Trichotomous r'] [IsTrans α r'],
  Codisjoint c'.extent c'.intent
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasSplitMultiplicativeReduction.toHasMultiplicativeReduction : ∀ {R : Type u_1} {inst : CommRing R} {inst_1 : IsDomain R} {inst_2 : IsDiscreteValuationRing R} {K : Type u_2}
  {inst_3 : Field K} {inst_4 : Algebra R K} {inst_5 : IsFractionRing R K} {W : WeierstrassCurve K}
  [self : WeierstrassCurve.HasSplitMultiplicativeReduction R W], WeierstrassCurve.HasMultiplicativeReduction R W
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.isLimitWeightedLimCone_fac_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F] {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x))
  ⦃j : J⦄ (x : W.obj j) {Z_1 : C} (h : F.obj j ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp ((W.isLimitWeightedLimCone F).lift π hπ) (W.weightedLimObjObjπ F x)) h =
    CategoryTheory.CategoryStruct.comp (π x) h
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`.  -/
mul_div_mul_right_le : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : Preorder G₀] {a b c : G₀}, 0 ≤ a / b → a * c / (b * c) ≤ a / b
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.polynomialEquiv_D : ∀ (R : Type u) [inst : CommRing R] (P : Polynomial R),
  (KaehlerDifferential.polynomialEquiv R) ((KaehlerDifferential.D R (Polynomial R)) P) = Polynomial.derivative P
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_toSubring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R Aᵐᵒᵖ),
  S.unop.toSubring = S.toSubring.unop
-- Mathlib.SetTheory.Cardinal.Regular
/-- **Alias** of `Ordinal.iSup_lt_omega_one`.

---

A countable supremum of countable ordinals is countable.  -/
Cardinal.iSup_sequence_lt_omega_one : ∀ {α : Type u_1} [Countable α] {f : α → Ordinal.{u_2}}, (∀ (i : α), f i < Ordinal.omega 1) → ⨆ i, f i < Ordinal.omega 1
-- Mathlib.Order.Defs.Unbundled
trans : ∀ {α : Sort u_1} {r : α → α → Prop} {a b c : α} [IsTrans α r], r a b → r b c → r a c
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioc_succ : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioc a.succ b.succ, f i = ∑ i ∈ Finset.Ioc a b, f i.succ
-- Init.Data.AC
Lean.Data.AC.evalList.eq_2 : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (x_1 : ℕ),
  Lean.Data.AC.evalList β ctx [x_1] = Lean.Data.AC.EvalInformation.evalVar ctx x_1
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams.workDoneToken? : Lean.Lsp.WorkDoneProgressParams → Option Lean.Lsp.ProgressToken
-- Mathlib.Order.CompleteBooleanAlgebra
compl_sInf' : ∀ {α : Type u} [inst : CompleteBooleanAlgebra α] {s : Set α}, (sInf s)ᶜ = sSup (compl '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : α → C)
  [inst_1 : CategoryTheory.Limits.HasProduct Z] (b : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π Z b).op
      (CategoryTheory.Limits.opProductIsoCoproduct Z).hom =
    CategoryTheory.Limits.Sigma.ι (fun x => Opposite.op (Z x)) b
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- coordinates of the lower and upper corners of the box  -/
BoxIntegral.Box.upper : {ι : Type u_2} → BoxIntegral.Box ι → ι → ℝ
-- Init.Data.SInt.Basic
ISize.ofUSize : USize → ISize
-- Mathlib.Algebra.Group.Prod
/-- Combine two `AddMonoidHom`s `f : AddHom M N`, `g : AddHom M P` into
`f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)`  -/
AddHom.prod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → (M →ₙ+ N) → (M →ₙ+ P) → M →ₙ+ N × P
-- Init.Data.List.Zip
/-- Variant of `getElem?_zipWith` using `Option.map` and `Option.bind` rather than a `match`.  -/
List.getElem?_zipWith' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → β → γ} {i : ℕ},
  (List.zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.sumNodes_eq_coeff : ∀ {n : ℕ} {P : Polynomial ℝ},
  P.degree ≤ ↑n → Polynomial.Chebyshev.sumNodes n (Polynomial.Chebyshev.leadingCoeffC✝ n) P = P.coeff n
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- An absolute left Kan extension is a left Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.isKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → {f : a ⟶ b} → {g : a ⟶ c} → {t : CategoryTheory.Bicategory.LeftExtension f g} → t.IsAbsKan → t.IsKan
-- Mathlib.Algebra.Group.Action.End
MulAut.applyMulAction.eq_1 : ∀ {M : Type u_2} [inst : Monoid M], MulAut.applyMulAction = { smul := fun x1 x2 => x1 x2, mul_smul := ⋯, one_smul := ⋯ }
-- Lean.Meta.Tactic.Grind.EMatchTheoremParam
/-- Returns pairs `(type, anchor)` where `type` is the type of a local theorem,
and `anchor` the anchor associated with it.
 -/
Lean.Meta.Grind.getLocalTheoremAnchors : Lean.Meta.Grind.Goal → Lean.Meta.Grind.GrindM (Array Lean.Meta.Grind.ExprWithAnchor)
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.asymm`. -/
RelEmbedding.isAsymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Asymm s], Std.Asymm r
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.lift.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2}
  (f : { a // a ≠ 1 } → α)
  (h : ∀ (a b : { a // a ≠ 1 }), FiniteMulArchimedeanClass.mk ↑a ⋯ = FiniteMulArchimedeanClass.mk ↑b ⋯ → f a = f b)
  (A : MulArchimedeanClass M) (hA : A ≠ ⊤),
  FiniteMulArchimedeanClass.lift f h ⟨A, hA⟩ =
    (MulArchimedeanClass.lift (fun b => if h : b = 1 then ⊤ else ↑(f ⟨b, h⟩)) ⋯ A).untop ⋯
-- Mathlib.Data.Finset.SDiff
Finset.cons_sdiff_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α},
  a ≠ b → ∀ (ha : a ∉ s) (hb : b ∉ s), Finset.cons a s ha \ Finset.cons b s hb = {a}
-- Mathlib.Algebra.DirectSum.Module
/-- Given `Fintype α`, `linearEquivFunOnFintype R` is the natural `R`-linear equivalence
between `⨁ i, M i` and `∀ i, M i`.  -/
DirectSum.linearEquivFunOnFintype : (R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → [Fintype ι] → (DirectSum ι fun i => M i) ≃ₗ[R] (i : ι) → M i
-- Mathlib.Tactic.Variable
/-- The `variable?` command has the same syntax as `variable`, but it will auto-insert
missing instance arguments wherever they are needed.
It does not add variables that can already be deduced from others in the current context.
By default the command checks that variables aren't implied by earlier ones, but it does *not*
check that earlier variables aren't implied by later ones.
Unlike `variable`, the `variable?` command does not support changing variable binder types.

The `variable?` command will give a suggestion to replace itself with a command of the form
`variable? ...binders... => ...binders...`.  The binders after the `=>` are the completed
list of binders. When this `=>` clause is present, the command verifies that the expanded
binders match the post-`=>` binders.  The purpose of this is to help keep code that uses
`variable?` resilient against changes to the typeclass hierarchy, at least in the sense
that this additional information can be used to debug issues that might arise.
One can also replace `variable? ...binders... =>` with `variable`.

The core algorithm is to try elaborating binders one at a time, and whenever there is a
typeclass instance inference failure, it synthesizes binder syntax for it and adds it to
the list of binders and tries again, recursively. There are no guarantees that this
process gives the "correct" list of binders.

Structures tagged with the `variable_alias` attribute can serve as aliases for a collection
of typeclasses. For example, given
```lean
@[variable_alias]
structure VectorSpace (k V : Type*) [Field k] [AddCommGroup V] [Module k V]
```
then `variable? [VectorSpace k V]` is
equivalent to `variable {k V : Type*} [Field k] [AddCommGroup V] [Module k V]`, assuming
that there are no pre-existing instances on `k` and `V`.
Note that this is not a simple replacement: it only adds instances not inferable
from others in the current scope.

A word of warning: the core algorithm depends on pretty printing, so if terms that appear
in binders do not round trip, this algorithm can fail. That said, it has some support
for quantified binders such as `[∀ i, F i]`.  -/
Mathlib.Command.Variable.elabVariables : Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos.eq_1 : ∀ (z : ℂ), Complex.cos z = (Complex.exp (z * Complex.I) + Complex.exp (-z * Complex.I)) / 2
-- Mathlib.Order.Hom.Bounded
TopHom.instInhabited : {α : Type u_2} → {β : Type u_3} → [inst : Top α] → [inst_1 : Top β] → Inhabited (TopHom α β)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).maxKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftLeft_shiftRight_cancel : ∀ (a : ℤ) (b : ℕ), a <<< b >>> b = a
-- Mathlib.Data.Ordmap.Invariants
/-- A right balance operation. This will rebalance a concatenation, assuming the original nodes are
not too far from balanced.  -/
Ordnode.balanceR' : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_eq_getLast!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t.max! = t.toList.getLast!
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_sdiff_Ioo_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ioo a b = {a, b}
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- The multiplicative closure of a multiplicative property is equal to itself.  -/
CategoryTheory.MorphismProperty.multiplicativeClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) [W.IsMultiplicative],
  W.multiplicativeClosure = W
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_union₀' : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.AEDisjoint μ s t → μ (s ∪ t) = μ s + μ t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {km : α} {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.mapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ≅ Y) (g : X ≅ Z), (CategoryTheory.Limits.prod.mapIso f g).inv = CategoryTheory.Limits.prod.map f.inv g.inv
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_left_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (g : MvPolynomial σ R), m.sPolynomial 0 g = 0
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductSwap_inv_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C) (X_1 : J₂ × J₁),
  ((CategoryTheory.MonoidalCategory.externalProductSwap J₁ J₂ C).inv.app X).app X_1 =
    (β_ (X.1.obj X_1.2) (X.2.obj X_1.1)).inv
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_lt_top : ∀ {r : ENNReal}, ∑' (n : ℕ), r ^ n < ⊤ ↔ r < 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonParameterInformationLabel : Lean.ToJson Lean.Lsp.ParameterInformationLabel
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.append.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {lw rw : ℕ}
  (refs : Vector Std.Sat.AIG.Fanin lw) (hrefs : ∀ {i : ℕ} (h : i < lw), refs[i].gate < aig.decls.size)
  (refs_1 : Vector Std.Sat.AIG.Fanin rw) (hrefs_1 : ∀ {i : ℕ} (h : i < rw), refs_1[i].gate < aig.decls.size),
  { refs := refs, hrefs := hrefs }.append { refs := refs_1, hrefs := hrefs_1 } = { refs := refs ++ refs_1, hrefs := ⋯ }
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    DFunLike (CategoryTheory.GrothendieckTopology C) C fun X => Set (CategoryTheory.Sieve X)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The minimum natural number level `n` through which `χ` factors.  -/
DirichletCharacter.conductor : {R : Type u_1} → [inst : CommMonoidWithZero R] → {n : ℕ} → DirichletCharacter R n → ℕ
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
/-- The class in `Ext S.X₃ S.X₁ 1` that is attached to a short exact
short complex `S` in an abelian category.  -/
CategoryTheory.ShortComplex.ShortExact.extClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {S : CategoryTheory.ShortComplex C} → S.ShortExact → CategoryTheory.Abelian.Ext S.X₃ S.X₁ 1
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- If `M` and `M` are each other's inverse matrices, `Matrix.toLin M` and `Matrix.toLin M'`
form a linear equivalence.  -/
Matrix.toLinOfInv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq n] →
            {M₁ : Type u_5} →
              {M₂ : Type u_6} →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : AddCommMonoid M₂] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        Module.Basis n R M₁ →
                          Module.Basis m R M₂ →
                            [inst_7 : Fintype m] →
                              [inst_8 : DecidableEq m] →
                                {M : Matrix m n R} → {M' : Matrix n m R} → M * M' = 1 → M' * M = 1 → M₁ ≃ₗ[R] M₂
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_Ici_of_tendsto_atTop_atTop : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R],
  Filter.Tendsto (↑f) Filter.atTop Filter.atTop → ∀ (x : R), f.measure (Set.Ici x) = ⊤
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x