mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk''_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (S : CategoryTheory.StrictPseudofunctorPreCore B C) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictPseudofunctor.mk'' S).mapComp f g = CategoryTheory.eqToIso ⋯
-- Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
Algebra.Generators.compLocalizationAwayAlgHom.eq_1 : ∀ {R : Type u_1} {S : Type u_2} (T : Type u_3) {ι : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (g : S) [inst_7 : IsLocalization.Away g T] (P : Algebra.Generators R S ι),
  Algebra.Generators.compLocalizationAwayAlgHom T g P =
    MvPolynomial.aeval
      (Sum.elim (fun x => IsLocalization.Away.invSelf ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g))) fun i =>
        (algebraMap P.Ring (Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)))) (MvPolynomial.X i))
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Over X)} (t : CategoryTheory.Limits.Cone K),
  (CategoryTheory.WithTerminal.coneLift✝.obj t).pt = t.pt.left
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.const_isBounded : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [inst : SeminormedRing 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] (ι : Type u_11) [Nonempty ι]
  {p : Seminorm 𝕜 E} {q : ι' → Seminorm 𝕜₂ F} (f : E →ₛₗ[σ₁₂] F),
  Seminorm.IsBounded (fun x => p) q f ↔ ∀ (i : ι'), ∃ C, (q i).comp f ≤ C • p
-- Mathlib.Data.Set.Finite.Basic
Multiset.finite_toSet_toFinset : ∀ {α : Type u} [inst : DecidableEq α] (s : Multiset α), ⋯.toFinset = s.toFinset
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_of_not_completeSpace : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ¬CompleteSpace G → ∫ (a : α), f a ∂μ = 0
-- Mathlib.Analysis.Convex.Between
affineSegment_vadd_const_image : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : V) (p : P),
  (fun x => x +ᵥ p) '' affineSegment R x y = affineSegment R (x +ᵥ p) (y +ᵥ p)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldM_eq_foldM_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] {γ : Type w} {it : Std.Iter β} {init : γ} {f : γ → β → m γ},
  Std.Iter.foldM f init it = Std.IterM.foldM f init it.toIterM
-- Lean.Data.Json.Basic
Lean.Json.instBEq : BEq Lean.Json
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If two `R`-multilinear maps from `R` are equal on 1, then they are equal.

This is the multilinear version of `LinearMap.ext_ring`.  -/
MultilinearMap.ext_ring : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [Finite ι] ⦃f g : MultilinearMap R (fun x => R) M₂⦄, ((f fun x => 1) = g fun x => 1) → f = g
-- Mathlib.Data.List.Nodup
List.nodup_iff_getElem?_ne_getElem? : ∀ {α : Type u} {l : List α}, l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_comp_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) g = f ↔
    g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
baseChange_ext_iff : ∀ {R : Type uR} {A : Type uA} {M₂ : Type uM₂} {N₁ : Type uN₁} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N₁] [inst_4 : Algebra R A] [inst_5 : Module R N₁]
  [inst_6 : Module A N₁] [IsScalarTower R A N₁] [inst_8 : Module R M₂]
  {Q₁ Q₂ : QuadraticMap A (TensorProduct R A M₂) N₁}, Q₁ = Q₂ ↔ ∀ (m : M₂), Q₁ (1 ⊗ₜ[R] m) = Q₂ (1 ⊗ₜ[R] m)
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- The isomorphism from the group of group homomorphisms from a finite cyclic group `G` of order
`n` into another group `G'` to the group of `n`th roots of unity in `G'` determined by a generator
`g` of `G`. It sends `φ : G →* G'` to `φ g`.  -/
IsCyclic.monoidHomMulEquivRootsOfUnityOfGenerator : {G : Type u_7} →
  [inst : CommGroup G] →
    {g : G} →
      (∀ (x : G), x ∈ Subgroup.zpowers g) →
        (G' : Type u_8) → [inst_1 : CommGroup G'] → (G →* G') ≃* ↥(rootsOfUnity (Nat.card G) G')
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
/-- The image of the intermediate field `F` of `L/K` under the inclusion `L ⊆ M`, viewed as an
intermediate field of `M/K`.
 -/
IntermediateField.extendRight : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          IntermediateField K L →
            (M : Type u_3) →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] → [inst_5 : Algebra L M] → [IsScalarTower K L M] → IntermediateField K M
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmptyLIE_apply : ∀ (𝕜 : Type u) (E : Type wE) (F : Type wF) (ι : Type v) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : IsEmpty ι] (m : F),
  (ContinuousAlternatingMap.constOfIsEmptyLIE 𝕜 E F ι) m = ContinuousAlternatingMap.constOfIsEmpty 𝕜 E ι m
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat : IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ UpperHalfPlane
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projection on the empty set is the zero map.  -/
GeneralSchauderBasis.proj_empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} {L : SummationFilter β} (b : GeneralSchauderBasis β 𝕜 X L), b.proj ∅ = 0
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` is nontrivial.  -/
PadicComplex.nontriviallyNormedField : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NontriviallyNormedField ℂ_[p]
-- Mathlib.Order.BoundedOrder.Basic
Prod.instBoundedOrder : (α : Type u) →
  (β : Type v) → [inst : LE α] → [inst_1 : LE β] → [BoundedOrder α] → [BoundedOrder β] → BoundedOrder (α × β)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPushout.of_horiz_isIso_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P} [CategoryTheory.Epi f] [CategoryTheory.IsIso inr],
  CategoryTheory.CommSq f g inl inr → CategoryTheory.IsPushout f g inl inr
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- The canonical projection `TrivSqZeroExt R M → R`.  -/
TrivSqZeroExt.fst : {R : Type u} → {M : Type v} → TrivSqZeroExt R M → R
-- Batteries.Data.Stream
Std.Stream.drop.eq_2 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (n : ℕ),
  Std.Stream.drop s n.succ =
    match Std.Stream.next? s with
    | none => s
    | some (fst, s) => Std.Stream.drop s n
-- Mathlib.Topology.Instances.Matrix
Continuous.matrix_adjugate : ∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
  [inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R},
  Continuous A → Continuous fun x => (A x).adjugate
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_ite_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M]
  [inst_3 : DecidableEq ι] (i : ι) (f : ι → M),
  (Finset.univ.expect fun j => if i = j then f j else 0) = (↑(Fintype.card ι))⁻¹ • f i
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.parseFirstByte.eq_def : ∀ (b : UInt8),
  ByteArray.utf8DecodeChar?.parseFirstByte b =
    if (b &&& 128 == 0) = true then ByteArray.utf8DecodeChar?.FirstByte.done
    else
      if (b &&& 224 == 192) = true then ByteArray.utf8DecodeChar?.FirstByte.oneMore
      else
        if (b &&& 240 == 224) = true then ByteArray.utf8DecodeChar?.FirstByte.twoMore
        else
          if (b &&& 248 == 240) = true then ByteArray.utf8DecodeChar?.FirstByte.threeMore
          else ByteArray.utf8DecodeChar?.FirstByte.invalid
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
Module.finiteDimensional_iff_of_rank_eq_nsmul : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Type v}
  [inst_3 : AddCommGroup W] [inst_4 : Module K W] {n : ℕ},
  n ≠ 0 → Module.rank K V = n • Module.rank K W → (FiniteDimensional K V ↔ FiniteDimensional K W)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.of.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} [inst_2 : SizeOf B] [inst_3 : SizeOf C]
  (as : CategoryTheory.Oplax.LaxTrans.Modification η θ), sizeOf { as := as } = 1 + sizeOf as
-- Mathlib.Order.Nucleus
Nucleus.coe_mk : ∀ {X : Type u_1} [inst : SemilatticeInf X] (f : InfHom X X) (h1 : ∀ (x : X), f.toFun (f.toFun x) ≤ f.toFun x)
  (h2 : ∀ (x : X), x ≤ f.toFun x), ⇑{ toInfHom := f, idempotent' := h1, le_apply' := h2 } = ⇑f
-- Aesop.Rule.Forward
Aesop.ForwardRule.instOrd : Ord Aesop.ForwardRule
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_def : ∀ (coeff : ℕ) (a : Nat.Internal.Linear.Expr),
  Nat.Internal.Linear.Expr.toPoly.go coeff a =
    match (motive := Nat.Internal.Linear.Expr → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly) a with
    | Nat.Internal.Linear.Expr.num k => bif k == 0 then id else fun x => (coeff * k, Nat.Internal.Linear.fixedVar) :: x
    | Nat.Internal.Linear.Expr.var i => fun x => (coeff, i) :: x
    | a.add b => Nat.Internal.Linear.Expr.toPoly.go coeff a ∘ Nat.Internal.Linear.Expr.toPoly.go coeff b
    | Nat.Internal.Linear.Expr.mulL k a => bif k == 0 then id else Nat.Internal.Linear.Expr.toPoly.go (coeff * k) a
    | a.mulR k => bif k == 0 then id else Nat.Internal.Linear.Expr.toPoly.go (coeff * k) a
-- Lean.Meta.WrapInstance
Lean.Meta.backward.inferInstanceAs.wrap : Lean.Option Bool
-- Lean.Parser.Term
Lean.Parser.Term.waitIfContainsMVar : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The identity continuous homomorphism.  -/
ContinuousAddMonoidHom.id : (A : Type u_2) → [inst : AddMonoid A] → [inst_1 : TopologicalSpace A] → A →ₜ+ A
-- Mathlib.CategoryTheory.Generator.HomologicalComplex
HomologicalComplex.instHasSeparator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop]
  [CategoryTheory.Limits.HasCoproductsOfShape ι C] [inst_3 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasSeparator C],
  CategoryTheory.HasSeparator (HomologicalComplex C c)
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.jdecl.inj : ∀ {j : Lean.IR.JoinPointId} {xs : Array Lean.IR.Param} {v b : Lean.IR.FnBody} {j_1 : Lean.IR.JoinPointId}
  {xs_1 : Array Lean.IR.Param} {v_1 b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.jdecl j xs v b = Lean.IR.FnBody.jdecl j_1 xs_1 v_1 b_1 → j = j_1 ∧ xs = xs_1 ∧ v = v_1 ∧ b = b_1
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sSameSide_incenter_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide s.incenter (s.points i)
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addLeft_apply : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G] (c x : G),
  (IsometryEquiv.addLeft c) x = c + x
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
SimpleGraph.measurableEmbedding_edgeSet : ∀ {V : Type u_1} [Countable V], MeasurableEmbedding SimpleGraph.edgeSet
-- Lean.Elab.Do.Basic
/-- Registers a `do` element elaborator for the given syntax node kind.

A `do` element elaborator should have type `DoElab` (which is
`Lean.Syntax → DoElemCont → DoElabM Expr`), i.e. should take syntax of the given syntax node kind
and a `DoElemCont` as parameters and produce an expression.

When elaborating a `do` block `do e; rest`, the elaborator for `e` is invoked with the syntax of `e`
and the `DoElemCont` representing `rest`.

The `elab_rules` and `elab` commands should usually be preferred over using this attribute
directly.
 -/
Lean.Elab.Do.doElemElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Do.DoElab
-- Mathlib.Order.RelClasses
WellFoundedLT.fix.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : WellFoundedLT α] {motive : α → Sort u_1},
  WellFoundedLT.fix = IsWellFounded.fix fun x1 x2 => x1 < x2
-- Mathlib.Data.Set.Order
Set.antitone_ofPred : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {p : α → β → Prop},
  (∀ (b : β), Antitone fun a => p a b) → Antitone fun a => {b | p a b}
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_add_smul_left_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] (b : S),
  LinearIndependent R ![x + b • y, y] ↔ LinearIndependent R ![x, y]
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.eq_X_add_C_of_degree_le_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.degree ≤ 1 → p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0)
-- Init.Data.Fin.Lemmas
/-- This is not a global instance, but may be activated locally via `open Fin.IntCast in ...`.

See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
Fin.IntCast.instIntCast : (n : ℕ) → [NeZero n] → IntCast (Fin n)
-- Lean.Parser.Term
Lean.Parser.Term.matchAltsWhereDecls.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instRightCancelMonoid : {α : Type u_1} → [LeftCancelMonoid α] → RightCancelMonoid αᵐᵒᵖ
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0), PowerSeries.expand p hp = MvPowerSeries.expand p hp
-- Batteries.Data.List.Basic
/-- `sublists' l` is the list of all (non-contiguous) sublists of `l`.
It differs from `sublists` only in the order of appearance of the sublists;
`sublists'` uses the first element of the list as the MSB,
`sublists` uses the first element of the list as the LSB.
```
sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]
```
 -/
List.sublists' : {α : Type u_1} → List α → List (List α)
-- Mathlib.Topology.Algebra.Monoid
Filter.TendstoNhdsWithinIoi.const_mul : ∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [SeparatelyContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [PosMulStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Ioi c)) →
        Filter.Tendsto (fun a => b * f a) l (nhdsWithin (b * c) (Set.Ioi (b * c)))
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.ne_top_iff_ne_one : ∀ (p q : ENNReal) [p.HolderConjugate q], p ≠ ⊤ ↔ q ≠ 1
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.instFibrationOfIsIso : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.IsIso f], HomotopicalAlgebra.Fibration f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.write.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (a : Bool)
  (l : List Bool),
  Turing.TM1to1.write (a :: l) x =
    Turing.TM1.Stmt.write (fun x x_1 => a) (Turing.TM1.Stmt.move Turing.Dir.right (Turing.TM1to1.write l x))
-- Mathlib.Algebra.Group.Invertible.Basic
/-- This is the `Invertible` version of `Units.isUnit_units_mul`  -/
invertibleOfInvertibleMul : {α : Type u} → [inst : Monoid α] → (a b : α) → [Invertible a] → [Invertible (a * b)] → Invertible b
-- Mathlib.Data.List.Nodup
List.Nodup.tail : ∀ {α : Type u} {l : List α}, l.Nodup → l.tail.Nodup
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.iUnion : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set (Set Ω)}
  {s' : Set (Set Ω)}, (∀ (n : ι), ProbabilityTheory.IndepSets (s n) s' μ) → ProbabilityTheory.IndepSets (⋃ n, s n) s' μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPushout_obj_map : ∀ {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₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) [inst_3 : CategoryTheory.Limits.HasPushouts C₃]
  (f₁ : CategoryTheory.Arrow C₁) {X Y : CategoryTheory.Arrow C₂} (sq : X ⟶ Y),
  (F.leibnizPushout.obj f₁).map sq =
    (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁.hom X.hom).mapArrowRight
      (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F f₁.hom Y.hom) sq
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInPolyTime.toTM2ComputableAux : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInPolyTime ea eb f → Turing.TM2ComputableAux αΓ βΓ
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForILeansParams.mk : Option Lean.Lsp.DocumentUri → Option ℕ → Lean.Lsp.WaitForILeansParams
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.coeff_killComplFun : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (p : MvPowerSeries τ R) (x : σ →₀ ℕ),
  (MvPowerSeries.coeff x) (MvPowerSeries.killComplFun e p) = (MvPowerSeries.coeff (Finsupp.embDomain e x)) p
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffAt.inv` -/
ContDiffAt.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'}, ContDiffAt 𝕜 n f x → f x ≠ 0 → ContDiffAt 𝕜 n (fun i => (f i)⁻¹) x
-- Mathlib.Data.List.AList
AList.mem_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : AList β}, a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₂ : CategoryTheory.GradedObject I₂ C₂)
  (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂) (h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂),
  CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.CategoryStruct.comp
      ((G.map (CategoryTheory.GradedObject.ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃))
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq_spec : ∀ (x x_1 : Lean.Grind.AC.Seq),
  (x == x_1) =
    match x, x_1 with
    | Lean.Grind.AC.Seq.var a, Lean.Grind.AC.Seq.var b => a == b
    | Lean.Grind.AC.Seq.cons a a_1, Lean.Grind.AC.Seq.cons b b_1 => a == b && a_1 == b_1
    | x, x_2 => false
-- Mathlib.RingTheory.RingHom.PurelyInseparable
RingHom.IsPurelyInseparable.containsIdentities : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => RingHom.IsPurelyInseparable
-- Mathlib.Data.Set.Operations
Set.mem_sdiff_of_mem : ∀ {α : Type u} {s t : Set α} {x : α}, x ∈ s → x ∉ t → x ∈ s \ t
-- Std.Async.Basic
/-- An asynchronous computation that may produce an error of type `ε`.
 -/
Std.Async.EAsync : Type → Type → Type
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.single_eq_algebraMap_mul_of : ∀ {R : Type u_1} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Monoid M] (m : M) (r : R),
  MonoidAlgebra.single m r = (algebraMap R (MonoidAlgebra R M)) r * (MonoidAlgebra.of R M) m
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.mem_idealOfSet_compl_singleton : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] (x : X) (f : C(X, R)), f ∈ ContinuousMap.idealOfSet R {x}ᶜ ↔ f x = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.contDiffAt_arccos : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → ∀ {n : WithTop ℕ∞}, ContDiffAt ℝ n Real.arccos x
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.instInhabitedUnit : Inhabited (ContinuousMap.HomotopyEquiv Unit Unit)
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the pure predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first match. The outputs of `it` are
examined in order of iteration.
 -/
Std.IterM.any : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → (β → Bool) → Std.IterM m β → m (ULift.{w, 0} Bool)
-- Init.BinderPredicates
/-- Declare `∃ x ≤ y, ...` as syntax for `∃ x, x ≤ y ∧ ...`  -/
Lean.«binderPred≤_» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Defs
/-- Let `R` be a commutative semiring, let `A` be a semiring with a `Module R` structure.
If `(r • x) * y = x * (r • y) = r • (x * y)` for all `r : R` and `x y : A`, then `A`
is an `Algebra` over `R`.

See note [reducible non-instances].  -/
Algebra.ofModule : {R : Type u} →
  {A : Type w} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Module R A] →
          (∀ (r : R) (x y : A), r • x * y = r • (x * y)) → (∀ (r : R) (x y : A), x * r • y = r • (x * y)) → Algebra R A
-- Mathlib.Order.Lattice
inf_congr_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ⊓ c ≤ b → a ⊓ b ≤ c → a ⊓ b = a ⊓ c
-- Init.Control.Lawful.Basic
bind_map_left : ∀ {m : Type u_1 → Type u_2} {α β γ : Type u_1} [inst : Monad m] [LawfulMonad m] (f : α → β) (x : m α) (g : β → m γ),
  (do
      let b ← f <$> x
      g b) =
    do
    let a ← x
    g (f a)