mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ExactSequence
/-- the composition of two consecutive arrows is zero  -/
CategoryTheory.ComposableArrows.IsComplex.zero_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.IsComplex →
    ∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.IsComplex._auto_1) {Z : C}
      (h : S.obj ⟨i + 2, ⋯⟩ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯)
          (CategoryTheory.CategoryStruct.comp (S.map' (i + 1) (i + 2) ⋯ hi) h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Order.Fin.Tuple
Fin.castLEOrderIso_symm_apply : ∀ {n m : ℕ} (h : n ≤ m) (i : { i // ↑i < n }), (RelIso.symm (Fin.castLEOrderIso h)) i = ⟨↑↑i, ⋯⟩
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the iterator yields no values.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

This variant terminates after finitely many steps and requires a proof that the iterator is
productive. If such a proof is not available, consider using `Iter.isEmpty`.

Examples:
* `[].iter.isEmpty = true`
* `[1].iter.isEmpty = false`
 -/
Std.Iter.Total.isEmpty : {α β : Type w} →
  [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → [Std.Iterators.Productive α Id] → Std.Iter.Total β → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey? k = t.getKey? k
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_filterWithPostcondition : ∀ {α β δ : Type w} {m : Type w → Type w'} {ps : Std.Do.PostShape} {n : Type w → Type w''} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [LawfulMonad n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_9 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)}
  {g : δ → β → δ} {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __do_lift ← (f b).run
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.filterWithPostcondition f it) ⦃Q⦄
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.one_apply : ∀ (G H : CommGrpCat) (g : ↑G), (CategoryTheory.ConcreteCategory.hom 1) g = 1
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.mapTR.loop.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (bs : List β) (h_1 : (bs : List β) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.div_def : ∀ {K : Type u_1} [inst : Field K] {a b : K} (w z : QuadraticAlgebra K a b), w / z = w * z⁻¹
-- Mathlib.Algebra.Lie.Basic
LieEquiv.mk.congr_simp : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] (toLieHom toLieHom_1 : L →ₗ⁅R⁆ L')
  (e_toLieHom : toLieHom = toLieHom_1) (invFun invFun_1 : L' → L) (e_invFun : invFun = invFun_1)
  (left_inv : Function.LeftInverse invFun (↑toLieHom).toFun)
  (right_inv : Function.RightInverse invFun (↑toLieHom).toFun),
  { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_ext_iff : ∀ {A B : ProfiniteGrp.{u}} {f g : A ⟶ B}, f = g ↔ ProfiniteGrp.Hom.hom f = ProfiniteGrp.Hom.hom g
-- Lean.Parser.Do
Lean.Parser.Term.leftArrow : Lean.Parser.Parser
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.completeDigraph_eq_top : ∀ (V : Type u_3), Digraph.completeDigraph V = ⊤
-- Mathlib.SetTheory.Ordinal.Basic
linearOrder_toType : (o : Ordinal.{u_1}) → LinearOrder o.ToType
-- Mathlib.RingTheory.Flat.Rank
Module.rankAtStalk_le_one_iff_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], (∀ (p : PrimeSpectrum R), Module.rankAtStalk S p ≤ 1) ↔ Function.Surjective ⇑(algebraMap R S)
-- Lean.Data.KVMap
Lean.KVMap.setBool : Lean.KVMap → Lean.Name → Bool → Lean.KVMap
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.restrictMonoidHom.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y] {V : Set X}
  (h : V ⊆ U), Function.locallyFinsuppWithin.restrictMonoidHom h = Function.locallyFinsuppWithin.restrictMonoidHom h
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.Equation.map : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {S : Type s} [inst_1 : CommRing S] (f : R →+* S)
  {P : Fin 3 → R}, W'.Equation P → (W'.map f).Equation (⇑f ∘ P)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_obj_grp_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.MonObj.mul)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.order_abs : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : LinearOrder R] [inst_2 : AddCommGroup R]
  [IsOrderedAddMonoid R] [inst_4 : Zero Γ] (x : Lex (HahnSeries Γ R)), (ofLex |x|).order = (ofLex x).order
-- Mathlib.NumberTheory.AlmostPrime
Nat.IsAlmostPrime.mul : ∀ {k l m n : ℕ}, k.IsAlmostPrime m → l.IsAlmostPrime n → (k + l).IsAlmostPrime (m * n)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The `E₂` homological spectral sequence indexed by `ℕ × ℕ` attached to
a third quadrant spectral object indexed by `EInt`.  -/
CategoryTheory.Abelian.SpectralObject.E₂HomologicalSpectralSequenceNat : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Y : CategoryTheory.Abelian.SpectralObject C EInt) →
        [Y.IsThirdQuadrant] →
          CategoryTheory.SpectralSequence C (fun r => ComplexShape.spectralSequenceNat (-r, r - 1)) 2
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {m n : WithTop ℕ∞} [CompleteSpace E]
  [inst_7 : IsManifold I 1 M] {V : (x : M) → TangentSpace I x},
  ContMDiffWithinAt I I.tangent m (fun x => ⟨x, V x⟩) s x →
    UniqueMDiff[s] →
      x ∈ s →
        m + 1 ≤ n →
          ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent m
            (fun x_1 =>
              ⟨x_1,
                VectorField.mpullbackWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) V (Set.range ↑I) x_1⟩)
            ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
-- Mathlib.Data.Finset.PImage
Part.mem_toFinset : ∀ {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] {x : α}, x ∈ o.toFinset ↔ x ∈ o
-- Mathlib.Algebra.Polynomial.Div
/-- An algorithm for deciding polynomial divisibility.
Prefer `Classical.dec`, as the algorithm relies on `%ₘ` and so is `noncomputable`.
 -/
Polynomial.decidableDvdMonic : {R : Type u} → [inst : Ring R] → {q : Polynomial R} → [DecidableEq R] → (p : Polynomial R) → q.Monic → Decidable (q ∣ p)
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform.subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.mulDysonETransform e x).1 * (Finset.mulDysonETransform e x).2 ⊆ x.1 * x.2
-- Mathlib.Analysis.RCLike.Basic
RCLike.nnnorm_ofNat : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ) [inst_1 : n.AtLeastTwo], ‖OfNat.ofNat n‖₊ = OfNat.ofNat n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_squareLeft : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B),
  (CategoryTheory.Limits.CatCospanTransform.id F G).squareLeft = inferInstance
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasFDerivWithinAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x
-- Mathlib.Analysis.Calculus.Deriv.Inv
/-- Eta-expanded form of `HasDerivWithinAt.inv` -/
HasDerivWithinAt.fun_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivWithinAt c c' s x → c x ≠ 0 → HasDerivWithinAt (fun i => (c i)⁻¹) (-c' / c x ^ 2) s x
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.ofAscListAux₂.eq_def : ∀ {α : Type u_1} (x : List α),
  Ordnode.ofAscListAux₂ x =
    match (motive := List α → Ordnode α → ℕ → Ordnode α) x with
    | [] => fun t x => t
    | x :: xs => fun l s =>
      match Ordnode.ofAscListAux₁ xs s with
      | (r, ⟨ys, h⟩) =>
        have this := ⋯;
        Ordnode.ofAscListAux₂ ys (l.link x r) (s <<< 1)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coe_posPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)),
  ↑(MeasureTheory.Lp.posPart f) = (↑f).posPart
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.eval_pappAck_step_zero : ∀ (c : Nat.Partrec.Code), (Nat.Partrec.Code.pappAck.step c).eval 0 = c.eval 1
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- If `f` is a collection of linear maps, then the construction `MultilinearMap.compLinearMap`
sending a multilinear map `g` to `g (f₁ ⬝ , ..., fₙ ⬝ )` is linear in `g`.  -/
MultilinearMap.compLinearMapₗ : {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)] →
                        ((i : ι) → M₁ i →ₗ[R] M₁' i) → MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.mk : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  (∀ (i : ℕ) (h : i < rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]) →
    RingTheory.Sequence.IsWeaklyRegular M rs
-- Lean.MetavarContext
Lean.getExprMVarAssignment? : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m (Option Lean.Expr)
-- Mathlib.Data.Matrix.Mul
instIsDedekindFiniteMonoidOfIsStablyFiniteRing : ∀ (R : Type u_10) [inst : NonAssocSemiring R] [IsStablyFiniteRing R], IsDedekindFiniteMonoid R
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.mk' : ∀ {l r : List Char},
  String.Legacy.Iterator.ValidFor l r
    { s := String.ofList (l.reverse ++ r), i := { byteIdx := String.utf8Len l.reverse } }
-- Mathlib.FieldTheory.Finite.Basic
/-- The sum of a subgroup of the units of a field is 1 if the subgroup is trivial and 1 otherwise  -/
FiniteField.sum_subgroup_units : ∀ {K : Type u_1} [inst : Ring K] [NoZeroDivisors K] {G : Subgroup Kˣ} [inst_2 : Fintype ↥G]
  [inst_3 : Decidable (G = ⊥)], ∑ x, ↑↑x = if G = ⊥ then 1 else 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instPartialOrder.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instPartialOrder = PartialOrder.ofSetLike (SubAddAction R M) M
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.locallyOfFinitePresentation_of_isOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.LocallyOfFinitePresentation f
-- Mathlib.LinearAlgebra.Complex.Module
ComplexStarModule.ext_iff : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x y : A}, x = y ↔ realPart x = realPart y ∧ imaginaryPart x = imaginaryPart y
-- Std.Http.Protocol.H1.Parser
/-- Parses a single chunk in chunked transfer encoding.
 -/
Std.Http.Protocol.H1.parseChunkPartial : Std.Http.Protocol.H1.Config →
  Std.Internal.Parsec.ByteArray.Parser
    (Option (ℕ × Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue) × ByteSlice))
-- Init.Control.Except
Except.map.eq_2 : ∀ {ε : Type u} {α : Type u_1} {β : Type u_2} (f : α → β) (v : α), Except.map f (Except.ok v) = Except.ok (f v)
-- Init.Data.String.Lemmas.Iterate
String.Slice.toList_revChars : ∀ {s : String.Slice}, s.revChars.toList = s.copy.toList.reverse
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.instIsIsoEqToHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y),
  CategoryTheory.IsIso (CategoryTheory.eqToHom h)
-- Mathlib.Data.Finset.Option
Finset.coe_eraseNone : ∀ {α : Type u_1} (s : Finset (Option α)), ↑(Finset.eraseNone s) = some ⁻¹' ↑s
-- Init.Data.UInt.Lemmas
System.Platform.two_pow_numBits_ne_zero : 2 ^ System.Platform.numBits ≠ 0
-- Mathlib.RingTheory.Bialgebra.TensorProduct
/-- The base ring is a right identity for the tensor product of bialgebras, up to
bialgebra equivalence.  -/
Bialgebra.TensorProduct.rid : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Bialgebra S A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra R S] → [inst_6 : IsScalarTower R S A] → TensorProduct R A R ≃ₐc[S] A
-- Mathlib.CategoryTheory.Subobject.Basic
/-- The category of subobjects of `X : C`, defined as isomorphism classes of monomorphisms into `X`.
 -/
CategoryTheory.Subobject : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Type (max u₁ v₁)
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.LocalPredicate.mk.sizeOf_spec : ∀ {X : TopCat} {T : ↑X → Type u_1} [inst : (a : ↑X) → SizeOf (T a)] (toPrelocalPredicate : TopCat.PrelocalPredicate T)
  (locality :
    ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
      (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate.pred fun x => f (i x)) → toPrelocalPredicate.pred f),
  sizeOf { toPrelocalPredicate := toPrelocalPredicate, locality := locality } = 1 + sizeOf toPrelocalPredicate
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Init.Data.UInt.Bitwise
instAssociativeUInt8HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.RingTheory.Jacobson.Ring
/-- General form of the Nullstellensatz for Jacobson rings, since in a Jacobson ring we have
`Inf {P maximal | P ≥ I} = Inf {P prime | P ≥ I} = I.radical`. Fields are always Jacobson,
and in that special case this is (most of) the classical Nullstellensatz,
since `I(V(I))` is the intersection of maximal ideals containing `I`, which is then `I.radical`  -/
MvPolynomial.isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} [Finite ι] [IsJacobsonRing R], IsJacobsonRing (MvPolynomial ι R)
-- Mathlib.Data.Set.Image
Subtype.map.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f f_1 : α → β) (e_f : f = f_1)
  (h : ∀ (a : α), p a → q (f a)) (a a_1 : Subtype p), a = a_1 → Subtype.map f h a = Subtype.map f_1 ⋯ a_1
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGT? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option ((a : α) × β a)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.mod_two_eq_one_iff_testBit_zero : ∀ {x : ℕ}, x % 2 = 1 ↔ x.testBit 0 = true
-- Mathlib.Order.Filter.Partial
Filter.tendsto_iff_ptendsto_univ : ∀ {α : Type u} {β : Type v} (l₁ : Filter α) (l₂ : Filter β) (f : α → β),
  Filter.Tendsto f l₁ l₂ ↔ Filter.PTendsto (PFun.res f Set.univ) l₁ l₂
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toOpposite_apply : ∀ (R : Type u_4) [inst : NonUnitalCommSemiring R] (r : R), (RingEquiv.toOpposite R) r = MulOpposite.op r
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map.eq_1 : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  SemidirectProduct.map fn fg h = { toFun := fun x => ⟨fn x.left, fg x.right⟩, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Probability.Process.LocalProperty
/-- Auxiliary definition for `isPreLocalizingSequence_of_isLocalizingSequence` which constructs a
strictly increasing sequence from a given sequence.  -/
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux : (ℕ → ℕ) → ℕ → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An initial object is terminal in the opposite category.  -/
CategoryTheory.Limits.IsInitial.op : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsTerminal (Opposite.op X)
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.instIsDominantHomRepresentativeOfIsDominant : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y) [f.IsDominant],
  AlgebraicGeometry.IsDominant f.representative.hom
-- Mathlib.CategoryTheory.Abelian.LeftDerived
/-- The left derived functors of an additive functor.  -/
CategoryTheory.Functor.leftDerived : {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] →
          [CategoryTheory.HasProjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) → [F.Additive] → ℕ → CategoryTheory.Functor C D
-- Lean.Elab.Binders
Lean.Elab.Term.elabArrow : Lean.Elab.Term.TermElab
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_neg_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {G : Type u_4} [inst : InvolutiveNeg G] [inst_1 : MeasurableSpace G]
  [MeasurableNeg G] {f : α → G}, (Measurable fun x => -f x) ↔ Measurable f
-- Mathlib.Analysis.Normed.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
ESeminormedCommMonoid.mul_comm : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ESeminormedCommMonoid E] (a b : E), a * b = b * a
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.le_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {K₁ K₂ : CategoryTheory.Pretopology C}, K₁ ≤ K₂ ↔ K₁.coverings ≤ K₂.coverings
-- Mathlib.Data.Multiset.Defs
/-- Lift of the list `pmap` operation. Map a partial function `f` over a multiset
`s` whose elements are all in the domain of `f`.  -/
Multiset.pmap : {α : Type u_1} → {β : Type v} → {p : α → Prop} → ((a : α) → p a → β) → (s : Multiset α) → (∀ a ∈ s, p a) → Multiset β
-- Std.Data.HashMap.Raw
/-- The notation `m[a]?` is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.HashMap.Raw.get? : {α : Type u} → {β : Type v} → [beq : BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → Option β
-- Mathlib.Data.ENNReal.Inv
ENNReal.orderIsoIicOneBirational_symm_apply : ∀ (x : ↑(Set.Iic 1)), ENNReal.orderIsoIicOneBirational.symm x = ((↑x)⁻¹ - 1)⁻¹
-- Mathlib.Analysis.Normed.Group.AddTorsor
NormedAddTorsor.toAddTorsor : {V : outParam (Type u_1)} →
  {P : Type u_2} →
    {inst : SeminormedAddCommGroup V} → {inst_1 : PseudoMetricSpace P} → [self : NormedAddTorsor V P] → AddTorsor V P
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The cosine of the angle between three points is 0 if and only if the angle is π / 2.  -/
EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_assoc_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X)
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffWithinAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.cos (f x)) s x
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
TopCat.Opens.coverDense_iff_isBasis : ∀ {X : TopCat} {ι : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} ι]
  (B : CategoryTheory.Functor ι (TopologicalSpace.Opens ↑X)),
  B.IsCoverDense (Opens.grothendieckTopology ↑X) ↔ TopologicalSpace.Opens.IsBasis (Set.range B.obj)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.isLink_iff : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β},
  G.IsLink e x y → ∀ {x' y' : α}, G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
LinearIsometryEquiv.contDiffPointwiseHolderAt_left_comp : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} (g : F ≃ₗᵢ[ℝ] G),
  ContDiffPointwiseHolderAt k α (⇑g ∘ f) a ↔ ContDiffPointwiseHolderAt k α f a