mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instBracketSubtypeMem : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          (L' : LieRinehartSubalgebra A L) →
            {M : Type u_3} → [inst_3 : AddCommGroup M] → [LieRingModule L M] → Bracket (↥L') M
-- Mathlib.Logic.Function.Basic
Function.rightInverse_invFun : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
  Function.Surjective f → Function.RightInverse (Function.invFun f) f
-- Mathlib.Algebra.Group.ConjFinite
ConjClasses.instFintypeElemCarrier : {α : Type u_1} → [inst : Monoid α] → [Fintype α] → [DecidableRel IsConj] → {x : ConjClasses α} → Fintype ↑x.carrier
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.πTruncGENatTrans_app : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c'), (e.πTruncGENatTrans C).app K = K.πTruncGE e
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.mem_toArray_iff_mem : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {a : α}, a ∈ r.toArray ↔ a ∈ r
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.splitter : (motive : Turing.ToPartrec.Cont → Sort u_1) →
  (x : Turing.ToPartrec.Cont) →
    (Unit → motive Turing.ToPartrec.Cont.halt) →
      ((c : Turing.ToPartrec.Code) →
          (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k)) →
        ((a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k)) →
          ((c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k)) →
            ((c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)) →
              motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.has_smallest_coproducts_of_hasCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasCoproducts C
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_right_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ s₃ : Finset α), s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
Std.IterM.toExtHashSet_eq_ofList : ∀ {α β : Type w} {x : BEq β} {x_1 : Hashable β} [inst : EquivBEq β] [inst_1 : LawfulHashable β] {m : Type w → Type w'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_6 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.toExtHashSet = Std.ExtHashSet.ofList <$> it.toList
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_lt_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x ^ z⁻¹ < y ↔ y ^ z < x)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_zero_of_irreducible_ne : ∀ {R : Type u_3} [inst : CommMonoidWithZero R] [Subsingleton Rˣ] {a b : R},
  Irreducible a → Irreducible b → a ≠ b → emultiplicity a b = 0
-- Lean.Parser.Term
Lean.Parser.Term.binop.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instPreservesLimitsOfSizeUliftFunctor : ∀ (R : Type u) [inst : Ring R],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v, max v v', max u (v + 1), max (max u (v + 1)) (v' + 1)}
    (ModuleCat.uliftFunctor.{v', v, u} R)
-- Mathlib.Algebra.Module.Presentation.Cokernel
_private.Mathlib.Algebra.Module.Presentation.Cokernel.0.Module.Presentation.cokernelRelations.match_1.eq_2 : ∀ {A : Type u_4} [inst : Ring A] {M₂ : Type u_5} [inst_1 : AddCommGroup M₂] [inst_2 : Module A M₂]
  (pres₂ : Module.Presentation A M₂) {ι : Type u_2} (motive : pres₂.R ⊕ ι → Sort u_6) (i : ι)
  (h_1 : (r : pres₂.R) → motive (Sum.inl r)) (h_2 : (i : ι) → motive (Sum.inr i)),
  (match Sum.inr i with
    | Sum.inl r => h_1 r
    | Sum.inr i => h_2 i) =
    h_2 i
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.coe_of : ∀ (R : Type u) [inst : AddGroup R], ↑(AddGrpCat.of R) = R
-- Init.Data.Array.Bootstrap
Array.foldrM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β} {xs : Array α},
  List.foldrM f init xs.toList = Array.foldrM f init xs
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalClearValue : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Homology.HomologySequence
/-- The connecting homomorphism `S.X₃.homology i ⟶ S.X₁.homology j` for a short exact
short complex `S`.  -/
CategoryTheory.ShortComplex.ShortExact.δ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            S.ShortExact → (i j : ι) → c.Rel i j → (S.X₃.homology i ⟶ S.X₁.homology j)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associatorImpl_hom_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (X.associatorImpl Y Z).hom.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
-- Init.Data.UInt.Basic
instShiftLeftUInt16 : ShiftLeft UInt16
-- Mathlib.Data.Set.Constructions
FiniteInter.finiteInterClosure_finiteInter : ∀ {α : Type u_1} (S : Set (Set α)), FiniteInter (FiniteInter.finiteInterClosure S)
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero : ∀ {M : Type u_1} [inst : CommGroupWithZero M] {r : ℤ},
  r = 0 → ∀ {x : M}, x ≠ 0 → ∀ (l : Mathlib.Tactic.FieldSimp.NF M), ((r, x) ::ᵣ l).eval = l.eval
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.apply_eq_of_dist_lt : ∀ {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ}, dist x y < (1 / 2) ^ n → ∀ {i : ℕ}, i ≤ n → x i = y i
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofBitVec : ∀ (n : BitVec 32), { toBitVec := n }.toBitVec = n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_lt_of_neg' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b < c → a < 0 → b + a < c
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ ⦃A B : C⦄ (c : CategoryTheory.Limits.BinaryCofan A B) (x : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.Mono c.inl) →
    CategoryTheory.Limits.MonoCoprod C
-- Mathlib.Logic.Equiv.Basic
/-- `ℕ ⊕ PUnit` is equivalent to `ℕ`.  -/
Equiv.natSumPUnitEquivNat : ℕ ⊕ PUnit.{u_9 + 1} ≃ ℕ
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- Consider a parameterized integral `x ↦ ∫ y, L (g y) (f x y)` where `L` is bilinear,
`g` is locally integrable and `f` is continuous and uniformly compactly supported. Then the
integral depends continuously on `x`.  -/
continuousOn_integral_bilinear_of_locally_integrable_of_compact_support : ∀ {Y : Type u_2} {E : Type u_3} {F : Type u_4} {X : Type u_5} {G : Type u_6} {𝕜 : Type u_7} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y}
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace ℝ E]
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace 𝕜 G]
  [inst_11 : NormedSpace 𝕜 E] (L : F →L[𝕜] G →L[𝕜] E) {f : X → Y → G} {s : Set X} {k : Set Y} {g : Y → F},
  IsCompact k →
    ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
      (∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) →
        MeasureTheory.IntegrableOn g k μ → ContinuousOn (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- List of row lengths of a Young diagram  -/
YoungDiagram.rowLens : YoungDiagram → List ℕ
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.wideSubcategoryInclusion.obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative] (X : CategoryTheory.WideSubcategory P),
  (CategoryTheory.wideSubcategoryInclusion P).obj X = X.obj
-- Mathlib.Order.Interval.Basic
Interval.exists : ∀ {α : Type u_1} [inst : LE α] {p : Interval α → Prop}, (∃ s, p s) ↔ p ⊥ ∨ ∃ s, p ↑s
-- Mathlib.Data.Fin.Fin2
Fin2.ofFin_toFin : ∀ {n : ℕ} (i : Fin2 n), Fin2.ofFin i.toFin = i
-- Mathlib.Lean.Meta.CongrTheorems
/-- Similar to doing `forallBoundedTelescope` twice, but makes use of the `fixed` array, which
is used as a hint for whether both variables should be the same. This is only a hint though,
since we respect it only if the binding domains are equal.
We affix `'` to the second list of variables, and all the variables are introduced
with default binder info. Calls `k` with the xs, ys, and a revised `fixed` array  -/
_private.Mathlib.Lean.Meta.CongrTheorems.0.Lean.Meta.mkRichHCongr.doubleTelescope : {α : Type} → Lean.Expr → ℕ → Array Bool → (Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.MetaM α) → Lean.MetaM α
-- Std.Http.Server.Handler
/-- Function called for each incoming request.
 -/
Std.Http.Server.StatelessHandler.onRequest : Std.Http.Server.StatelessHandler →
  Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Left unitor for the vertical composition of lax natural transformations.  -/
CategoryTheory.Oplax.LaxTrans.leftUnitor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          (η : F ⟶ G) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id F) η ≅ η
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.uniqueAlgEquiv_monomial : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : Unique σ] {d : σ →₀ ℕ} {r : R},
  (MvPolynomial.uniqueAlgEquiv R σ) ((MvPolynomial.monomial d) r) = (Polynomial.monomial (d default)) r
-- Init.Omega.Int
Lean.Omega.Fin.not_le : ∀ {n : ℕ} {i j : Fin n}, ¬i ≤ j ↔ j < i
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetricProjection.isIdempotentElem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetricProjection → IsIdempotentElem T
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- `primitiveRoots n K` is a subset of the roots of the minimal polynomial of a primitive
`n`-th root of unity `μ`.  -/
IsPrimitiveRoot.is_roots_of_minpoly : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n →
    ∀ [inst_1 : IsDomain K] [CharZero K] [inst_3 : DecidableEq K],
      primitiveRoots n K ⊆ (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
-- Std.Http.Protocol.H1.Parser
/-- Parses a trailer header (used after a chunked body), rejecting forbidden field names per RFC 9112
§6.5. Fields used for message framing (`content-length`, `transfer-encoding`), routing (`host`),
or connection management (`connection`, `te`, `upgrade`) are rejected to prevent trailer injection
attacks where a downstream proxy might re-interpret them.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseTrailerHeader : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser (Option (String × String))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftUnshift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ γ_1 : CochainComplex.HomComplex.Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'),
  γ = γ_1 → ∀ (n : ℤ) (hn : n + a = n'), γ.leftUnshift n hn = γ_1.leftUnshift n hn
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- A submonoid `S` of a monoid `R` is (left) Ore if common factors on the right can be turned
into common factors on the left, and if each pair of `r : R` and `s : S` admits an Ore numerator
`v : R` and an Ore denominator `u : S` such that `u * r = v * s`.  -/
OreLocalization.OreSet : {R : Type u_1} → [inst : Monoid R] → Submonoid R → Type u_1
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_gen : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  (Summable fun i => ‖f i‖ ^ p.toReal) → Memℓp f p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).ι.app none = f
-- Mathlib.Data.Fin.SuccPred
Fin.pred_succAbove : ∀ {n : ℕ} (x : Fin n) (y : Fin (n + 1)) (h : y ≤ x.castSucc) (h' : optParam (y.succAbove x ≠ 0) ⋯),
  (y.succAbove x).pred h' = x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- Let `s` be a set of real places, define the continuous linear equiv of the mixed space that
swaps sign at places in `s` and leaves the rest unchanged.  -/
NumberField.mixedEmbedding.negAt : {K : Type u_1} →
  [inst : Field K] →
    Set { w // w.IsReal } → NumberField.mixedEmbedding.mixedSpace K ≃L[ℝ] NumberField.mixedEmbedding.mixedSpace K
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.subsemigroupCongr.eq_1 : ∀ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M} (h : S = T),
  AddEquiv.subsemigroupCongr h = { toEquiv := Equiv.setCongr ⋯, map_add' := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ℚ → ℝ},
  ProbabilityTheory.IsMeasurableRatCDF f → ∀ (a : α), Filter.Tendsto (f a) Filter.atTop (nhds 1)
-- Mathlib.Tactic.Simps.Basic
/-- List of types in which we are not recursing to generate simplification lemmas.
E.g. if we write `@[simps] def e : α × β ≃ β × α := ...` we will generate `e_apply` and not
`e_apply_fst`.  -/
Simps.Config.notRecursive : Simps.Config → List Lean.Name
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.isBounded_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α},
  Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
InformationTheory.rightDeriv_klFun_one : derivWithin InformationTheory.klFun (Set.Ioi 1) 1 = 0
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The cumulant-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `t ↦ μ * t + v * t ^ 2 / 2`.  -/
ProbabilityTheory.cgf_gaussianReal : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {p : MeasureTheory.Measure Ω} {μ : ℝ} {v : NNReal} {X : Ω → ℝ},
  MeasureTheory.Measure.map X p = ProbabilityTheory.gaussianReal μ v →
    ∀ (t : ℝ), ProbabilityTheory.cgf X p t = μ * t + ↑v * t ^ 2 / 2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.ofHom.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A B : C}
  [inst_2 : CategoryTheory.MonObj A] [inst_3 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_4 : CategoryTheory.IsMonHom f], CategoryTheory.Mon.ofHom f = { hom := f, isMonHom_hom := inst_4 }
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictAnti_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] [FirstCountableTopology α] (x : α),
  ∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.Rel.zero : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}, Multiset.Rel r 0 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {hc : t.min! ∈ t}, t.get t.min! hc = t.min!
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instZeroHom.eq_1 : ∀ (G H : AddGrpCat), G.instZeroHom H = { zero := AddGrpCat.ofHom 0 }
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The left inverse of matrix A is unique when existing.  -/
Matrix.left_inv_eq_left_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B C : Matrix n n α},
  B * A = 1 → C * A = 1 → B = C
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.instNontrivial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, Nontrivial (CategoryTheory.Sieve X)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_iUnion`. -/
EMetric.infEdist_iUnion : ∀ {ι : Sort u_1} {α : Type u} [inst : PseudoEMetricSpace α] (f : ι → Set α) (x : α),
  Metric.infEDist x (⋃ i, f i) = ⨅ i, Metric.infEDist x (f i)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.linearIsometryBoundedOfCompact_toIsometryEquiv : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E],
  (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toIsometryEquiv = ContinuousMap.isometryEquivBoundedOfCompact α E
-- Mathlib.Logic.Equiv.List
Denumerable.list_ofNat_succ : ∀ {α : Type u_1} [inst : Denumerable α] (v : ℕ),
  Denumerable.ofNat (List α) v.succ =
    Denumerable.ofNat α (Nat.unpair v).1 :: Denumerable.ofNat (List α) (Nat.unpair v).2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.inter_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.inter m₂ = m₁ ∩ m₂
-- Lean.Elab.Tactic.Omega.Frontend
/-- If `e : Expr` is the `n`-th atom, construct the proof that
`e = (coordinate n).eval atoms`.  -/
Lean.Elab.Tactic.Omega.mkCoordinateEvalAtomsEq : Lean.Expr → ℕ → Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_congr : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → (f₁ =O[𝕜; l] g₁ ↔ f₂ =O[𝕜; l] g₂)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.sum_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {ι : Type u_5}
  (s : Finset ι) (f : ι → NormedAddGroupHom V₁ V₂) (v : V₁), (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `smul_apply`. -/
GroupSeminorm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.instNeBotAsymptoticNhds : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {v : V},
  (AffineSpace.asymptoticNhds k P v).NeBot
-- Mathlib.Topology.Algebra.Module.Basic
LinearMap.isClosed_range_coe : ∀ (M₁ : Type u_1) (M₂ : Type u_2) {R : Type u_4} {S : Type u_5} [inst : TopologicalSpace M₂] [T2Space M₂]
  [inst_2 : Semiring R] [inst_3 : Semiring S] [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module S M₂] [ContinuousConstSMul S M₂] [ContinuousAdd M₂] (σ : R →+* S),
  IsClosed (Set.range DFunLike.coe)
-- Init.Data.List.Find
List.get_find?_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {p : α → Bool} (h : (List.find? p (List.replicate n a)).isSome = true),
  (List.find? p (List.replicate n a)).get h = a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Antitone.intervalIntegrable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [inst_2 : ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ},
  Antitone u → IntervalIntegrable u μ a b
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Compactness of candidates (in `BoundedContinuousFunction`s) follows.  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.isCompact_candidatesB : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [CompactSpace X] [CompactSpace Y],
  IsCompact (GromovHausdorff.candidatesB✝ X Y)
-- Std.Sync.Broadcast
/-- Global message sequence number for the next message to be sent.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.pos : {α : Type} → Std.Bounded.State✝ α → ℕ
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_ofSlice_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  q < String.Slice.Pos.ofSlice p ↔ ∃ (h₁ : q ≤ p₁), ∀ (h₀ : p₀ ≤ q), q.slice p₀ p₁ h₀ h₁ < p
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv Y)
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalAddTorsor : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G], IsTopologicalAddTorsor G
-- Init.Omega.Int
Lean.Omega.Int.neg_le_natAbs : ∀ {a : ℤ}, -a ≤ ↑a.natAbs
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_st' : ∀ {x : ℝ*}, ¬x.Infinite → x.IsSt x.st
-- Mathlib.Order.Heyting.Basic
/-- A co-Heyting algebra is a bounded lattice with an additional binary difference operation `\`
such that `(· \ a)` is left adjoint to `(· ⊔ a)`.  -/
CoheytingAlgebra : Type u_4 → Type u_4
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.π_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] (W : C)
  (k : (b : J.R) → I.right b ⟶ W)
  (h :
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp (I.fst a) (k (J.fst a)) =
        CategoryTheory.CategoryStruct.comp (I.snd a) (k (J.snd a)))
  (b : J.R) {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π I b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.desc I W k h) h_1) =
    CategoryTheory.CategoryStruct.comp (k b) h_1