mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproduct comparison morphism is an iso, its inverse is natural.  -/
CategoryTheory.Limits.coprodComparison_inv_natural_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A A' B B' : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A' B']
  [inst_4 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_5 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B')
  [inst_6 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)]
  [inst_7 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] {Z : D}
  (h : F.obj A' ⨿ F.obj B' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')) h)
-- Mathlib.Tactic.Translate.ToAdditive
/-- The bundle of environment extensions for `to_additive`  -/
Mathlib.Tactic.ToAdditive.data : Mathlib.Tactic.Translate.TranslateData
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_ofDarts : ∀ {V : Type u} {G : SimpleGraph V} {l : List G.Dart} (hne : l ≠ []) (hchain : List.IsChain G.DartAdj l),
  (SimpleGraph.Walk.ofDarts l hne hchain).length = l.length
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_apply_right : ∀ {n : ℕ} (i : ℕ), (finSumNatEquiv n) (Sum.inr i) = n + i
-- Mathlib.Data.Seq.Computation
Computation.Bind.g.eq_1 : ∀ {α : Type u} {β : Type v} (a : β), Computation.Bind.g (Sum.inl a) = Sum.inl a
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
/-- The cardinal of the general linear group over a finite field.  -/
Matrix.card_GL_field : ∀ {𝔽 : Type u_1} [inst : Field 𝔽] [inst_1 : Fintype 𝔽] (n : ℕ),
  Nat.card (GL (Fin n) 𝔽) = ∏ i, (Fintype.card 𝔽 ^ n - Fintype.card 𝔽 ^ ↑i)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insert.eq_1 : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m : Std.ExtHashMap α β) (a : α) (b : β), m.insert a b = { inner := m.inner.insert a b }
-- Mathlib.Analysis.Fourier.AddCircle
fourier_apply : ∀ {T : ℝ} {n : ℤ} {x : AddCircle T}, (fourier n) x = ↑(n • x).toCircle
-- Init.Data.SInt.Basic
instMaxInt8 : Max Int8
-- Mathlib.Data.Finset.NAry
Finset.exists_mem_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {p : γ → Prop}, (∃ z ∈ Finset.image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'} {x : N}, MDiffAt f x → (MDiffAt fun x => (f x).1) x
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Raw.getEntryLED : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a → (a : α) × β a
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0)
  (hg₂ : S₂.g = 0),
  (CategoryTheory.ShortComplex.HomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂).right =
    CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros φ hf₁ hg₁ hf₂ hg₂
-- Mathlib.MeasureTheory.Group.Prod
/-- This is the computation performed in the proof of [Halmos, §60 Th. A].  -/
MeasureTheory.measure_add_lintegral_eq : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set G} [MeasurableNeg G] [μ.IsAddLeftInvariant]
  [ν.IsAddLeftInvariant],
  MeasurableSet s →
    ∀ (f : G → ENNReal), Measurable f → μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z + x) ⁻¹' s) * f (-x) ∂μ
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.comp : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x → ∀ (f : ι' → ι), Function.Injective f → AlgebraicIndependent R (x ∘ f)
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [(F.comp G).PreservesMonomorphisms] [G.ReflectsMonomorphisms],
  F.PreservesMonomorphisms
-- Init.Data.SInt.Lemmas
USize.toUSize_toISize : ∀ (x : USize), x.toISize.toUSize = x
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_inverse_obj_carrier : ∀ (R : CommRingCat) (A : CategoryTheory.Under R), ↑((commAlgCatEquivUnder R).inverse.obj A) = ↑A.right
-- Aesop.Tracing
Aesop.instInhabitedTraceOption : Inhabited Aesop.TraceOption
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.instIsRightCancelAddSubtypeLeOfNat : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [IsRightCancelAdd α],
  IsRightCancelAdd { x // 0 ≤ x }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.max! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Init.NotationExtra
_private.Init.NotationExtra.0.Lean.expandExplicitBindersAux.loop : Lean.Syntax →
  (idents : Array Lean.Syntax) → Option Lean.Syntax → (i : ℕ) → i ≤ idents.size → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.soln_gen : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} → ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 → ℤ_[p]
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.next_nat_succ : ∀ (i : ℕ), (ComplexShape.down ℕ).next (i + 1) = i
-- Mathlib.Data.Set.Basic
Set.Nonempty.to_subtype : ∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty ↑s
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_shiftLeft : ∀ (a b : UInt32), b < 8 → (a <<< b).toUInt8 = a.toUInt8 <<< b.toUInt8
-- Mathlib.Data.Stream.Defs
/-- Apply a function `f` to all elements of a stream `s`.  -/
Stream'.map : {α : Type u} → {β : Type v} → (α → β) → Stream' α → Stream' β
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.Quotient.isDPMorphism : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A} (hIJ : hI.IsSubDPIdeal (J ⊓ I)),
  hI.IsDPMorphism (DividedPowers.Quotient.dividedPowers hI hIJ) (Ideal.Quotient.mk J)
-- Mathlib.Topology.Algebra.AffineSubspace
AffineSubspace.coe_ofEq_apply : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s t : AffineSubspace R P} [inst_5 : Nonempty ↥s]
  [inst_6 : Nonempty ↥t] (h : s = t) (x : ↥s), ↑((AffineSubspace.ofEq h) x) = ↑x
-- Mathlib.Algebra.Ring.Rat
Rat.mkRat_pow : ∀ (num den n : ℕ), mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)
-- Mathlib.Algebra.Group.End
/-- `Equiv.Perm.sumCongr` as a `MonoidHom`, with its two arguments bundled into a single `Prod`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between `α` and `β`.  -/
Equiv.Perm.sumCongrHom : (α : Type u_7) → (β : Type u_8) → Equiv.Perm α × Equiv.Perm β →* Equiv.Perm (α ⊕ β)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t : Finset α}, (s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
-- Init.Grind.Ring.Basic
/-- A semiring, i.e. a type equipped with addition, multiplication, and a map from the natural numbers,
satisfying appropriate compatibilities.

Use `Ring` instead if the type also has negation,
`CommSemiring` if the multiplication is commutative,
or `CommRing` if the type has negation and multiplication is commutative.
 -/
Lean.Grind.Semiring : Type u → Type u
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_modEq_two : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 n ≡ n [MOD 2]
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.norm_incl : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] {V' : AddSubgroup V} (x : ↥V'), ‖(NormedAddGroupHom.incl V') x‖ = ‖x‖
-- Mathlib.Logic.Function.Defs
/-- Product of functions: `Function.prod f g i = (f i, g i)`, where the types of `f i` and
`g i` may depend on `i`.  -/
Function.prod : {ι : Sort u_3} → {α : ι → Type u_1} → {β : ι → Type u_2} → ((i : ι) → α i) → ((i : ι) → β i) → (i : ι) → α i × β i
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mem_inv_smul_finset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s : Finset β}
  {a : α} {b : β}, b ∈ a⁻¹ • s ↔ a • b ∈ s
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_lt : ∀ {r : ENNReal} {n : ℕ∞}, ⌊r⌋ₑ < n ↔ r < ↑n
-- Lean.Meta.Sym.InstantiateS
/-- Similar to `Lean.Expr.instantiateRevRange`.
It assumes the input is maximally shared, and ensures the output is too.
It assumes `beginIdx ≤ endIdx` and `endIdx ≤ subst.size`
 -/
Lean.Meta.Sym.instantiateRevRangeS : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.isFractional_of_le : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I : Submodule R P} {J : FractionalIdeal S P}, I ≤ ↑J → IsFractional S I
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.linearMap_repr_apply : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {ι₁ : Type u_6} {ι₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (x : M₁ →ₗ[R] M₂),
  (b₁.linearMap b₂).repr x = (Matrix.stdBasis R ι₂ ι₁).repr ((LinearMap.toMatrix b₁ b₂) x)
-- Mathlib.Data.Finset.NAry
Finset.mem_image₂_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {a : α} {b : β}, Function.Injective2 f → (f a b ∈ Finset.image₂ f s t ↔ a ∈ s ∧ b ∈ t)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.algebraTensorAlgEquiv_symm_relation : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (r : σ),
  (MvPolynomial.algebraTensorAlgEquiv R₀ R).symm (P.relation r) = 1 ⊗ₜ[R₀] Algebra.Presentation.relationOfHasCoeffs R₀ r
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instAddCommGroup : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} →
          [inst_2 : AddCommGroup X] → [inst_3 : DistribMulAction R X] → AddCommGroup (OreLocalization S X)
-- Mathlib.LinearAlgebra.Contraction
dualTensorHom_bijective_of_finite_projective_right : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.Finite R N] [Module.Projective R N],
  Function.Bijective ⇑(dualTensorHom R M N)
-- Init.Data.BitVec.Lemmas
BitVec.ofNat_sub_ofNat : ∀ {n : ℕ} (x y : ℕ), BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)
-- Mathlib.Analysis.Normed.Group.Basic
norm_prod_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) (f : ι → E),
  ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- The complex consisting of only the faces present in both of its arguments.  -/
AbstractSimplicialComplex.instMin : {ι : Type u_1} → Min (AbstractSimplicialComplex ι)
-- Mathlib.Order.RelClasses
instIsTransLt : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun x1 x2 => x1 < x2
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_add_of_le_left : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a ≤ b → a ≤ b + c
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.valuation_Δ_aux.congr_simp : ∀ (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 W_1 : WeierstrassCurve K),
  W = W_1 → WeierstrassCurve.valuation_Δ_aux R W = WeierstrassCurve.valuation_Δ_aux R W_1
-- Mathlib.Data.TypeVec
TypeVec.Arrow.inhabited : {n : ℕ} → (α : TypeVec.{u_1} n) → (β : TypeVec.{u_2} n) → [(i : Fin2 n) → Inhabited (β i)] → Inhabited (α.Arrow β)
-- Mathlib.CategoryTheory.Center.Linear
/-- The `R`-module structure on the type `X ⟶ Y` of morphisms in
a category `C` equipped with a ring morphism `R →+* CatCenter C`.  -/
CategoryTheory.Linear.homModuleOfRingMorphism : {R : Type w} →
  [inst : Ring R] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Preadditive C] → (R →+* CategoryTheory.CatCenter C) → (X Y : C) → Module R (X ⟶ Y)
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- Given `I : MulticospanIndex J (Type u)`, this is a type which identifies
to the sections of the functor `I.multicospan`.  -/
CategoryTheory.Limits.MulticospanIndex.sections : {J : CategoryTheory.Limits.MulticospanShape} → CategoryTheory.Limits.MulticospanIndex J (Type u) → Type (max u u_1)
-- Mathlib.GroupTheory.PushoutI
/-- The equivalence between `NormalWord`s and pairs. We can turn a `NormalWord` into a
pair by taking the head of the `List` if it is in `G i` and multiplying it by the element of the
base group.  -/
Monoid.PushoutI.NormalWord.equivPair : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [DecidableEq ι] →
                [(i : ι) → DecidableEq (G i)] →
                  (i : ι) → Monoid.PushoutI.NormalWord d ≃ Monoid.PushoutI.NormalWord.Pair d i
-- Mathlib.Data.Nat.PrimeFin
Nat.mem_primeFactors : ∀ {n p : ℕ}, p ∈ n.primeFactors ↔ Nat.Prime p ∧ p ∣ n ∧ n ≠ 0
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt
CFC.toLinearMap_conjSqrt : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : SeparatelyContinuousMul A] (c : A),
  ↑(CFC.conjSqrt c) = LinearMap.mulLeftRight ℝ (CFC.sqrt c, CFC.sqrt c)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_I : Complex.log Complex.I = ↑Real.pi / 2 * Complex.I
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Internal.Raw₀.Const.getD (m₁.union m₂) k fallback =
          Std.DHashMap.Internal.Raw₀.Const.getD m₂ k (Std.DHashMap.Internal.Raw₀.Const.getD m₁ k fallback)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_of_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b b) B).det ≠ 0 → B.SeparatingLeft
-- Mathlib.Data.Set.Prod
Set.disjoint_diagonal_offDiag : ∀ {α : Type u_1} (s : Set α), Disjoint (Set.diagonal α) s.offDiag
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearEquiv.multilinearMapCongrLeft_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (e : (i : ι) → M₁ i ≃ₗ[R] M₁' i) (g : MultilinearMap R M₁' M₂),
  (LinearEquiv.multilinearMapCongrLeft e) g = g.compLinearMap fun x => ↑(e x)
-- Init.Data.Vector.MapIdx
Vector.mapFinIdxM.eq_1 : ∀ {n : ℕ} {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (xs : Vector α n)
  (f : (i : ℕ) → α → i < n → m β), xs.mapFinIdxM f = Vector.mapFinIdxM.map xs f n 0 ⋯ (Vector.cast ⋯ #v[])
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerived_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {F G H : CategoryTheory.Functor C D} [inst_5 : F.Additive] [inst_6 : G.Additive]
  [inst_7 : H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.rightDerived n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.comp α β) n)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived α n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightDerived β n) h)
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroClass.mk : {M₀ : Type u} →
  [toMul : Mul M₀] → [toZero : Zero M₀] → (∀ (a : M₀), 0 * a = 0) → (∀ (a : M₀), a * 0 = 0) → MulZeroClass M₀
-- Batteries.Recycling.RBTree.Lemmas
/-- A statement of the least-ness of the result of `upperBoundP?`. If `x` is the return value of
`upperBoundP?` and it is strictly greater than the cut, then any other `y < x` in the tree is in
fact strictly less than the cut (so there is no exact match, and nothing closer to the cut).
 -/
RBTree.RBSet.upperBoundP?_least : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp]
  [RBTree.RBNode.IsCut cmp cut],
  t.upperBoundP? cut = some x → y ∈ t → cmp y x = Ordering.lt → cut x = Ordering.lt → cut y = Ordering.gt
-- Mathlib.Algebra.Category.BoolRing
/-- The underlying type.  -/
BoolRing.carrier : BoolRing → Type u
-- Mathlib.Algebra.Star.Pi
Function.star_sumElim : ∀ {I : Type u_1} {J : Type u_2} {α : Type u_3} (x : I → α) (y : J → α) [inst : Star α],
  star (Sum.elim x y) = Sum.elim (star x) (star y)
-- Init.Data.List.Monadic
List.foldrM_wfParam : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : List α}
  {f : α → β → m β} {init : β}, List.foldrM f init (wfParam xs) = List.foldrM f init xs.attach.unattach
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_bot_left : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsZeroOrProbabilityMeasure μ], ProbabilityTheory.Indep ⊥ m' μ
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.mem_nonunits : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ_[p]}, z ∈ nonunits ℤ_[p] ↔ ‖z‖ < 1
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Composition of `StrictlyUnitaryPseudofunctor`.  -/
CategoryTheory.StrictlyUnitaryPseudofunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.StrictlyUnitaryPseudofunctor B C →
              CategoryTheory.StrictlyUnitaryPseudofunctor C D → CategoryTheory.StrictlyUnitaryPseudofunctor B D
-- Std.Async.Timer
/-- If:
- `s` is not yet running start it and return an `Async` computation that will complete once the previously
   configured `duration` has elapsed.
- `s` is already or not anymore running return the same `Async` computation as the first call to `wait`.
 -/
Std.Async.Sleep.wait : Std.Async.Sleep → Std.Async.Async Unit
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_of_subset : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], s ⊆ t → (t \ s).card = t.card - s.card
-- Mathlib.Data.Finsupp.Fin
Finsupp.tail_apply : ∀ {n : ℕ} (i : Fin n) {M : Type u_1} [inst : Zero M] (t : Fin (n + 1) →₀ M), t.tail i = t i.succ
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries.map : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → ∀ (n : ℕ), Subgroup.map f (Subgroup.upperCentralSeries G n) ≤ Subgroup.upperCentralSeries H n
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- `SimplexCategory` is a skeleton of `NonemptyFinLinOrd`.
 -/
SimplexCategory.isSkeletonOf : CategoryTheory.IsSkeletonOf NonemptyFinLinOrd SimplexCategory SimplexCategory.skeletalFunctor
-- Mathlib.Topology.IsLocalHomeomorph
/-- A local homeomorphism is continuous.  -/
IsLocalHomeomorph.continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsLocalHomeomorph f → Continuous f
-- Mathlib.CategoryTheory.Category.Preorder
/-- A categorical equivalence between partial orders is just an order isomorphism.  -/
CategoryTheory.Equivalence.toOrderIso : {X : Type u} → {Y : Type v} → [inst : PartialOrder X] → [inst_1 : PartialOrder Y] → (X ≌ Y) → X ≃o Y
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.instLinear : (R : Type u_1) →
  [inst : CommRing R] →
    (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Linear R (CategoryTheory.Free R C)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instNonUnitalAlgSemiHomClass : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B], NonUnitalAlgSemiHomClass (A →ₛₙₐ[φ] B) φ A B
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.eq_append_of_dropSuffix?_slice_eq_some : ∀ {pat s res : String.Slice}, s.dropSuffix? pat = some res → s.copy = res.copy ++ pat.copy