mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Parsec.Basic
/-- Peeks at the next element, returns `some` if exists else `none`, does not consume input.
 -/
Std.Internal.Parsec.peek? : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι (Option elem)
-- Mathlib.Data.NNRat.Defs
NNRat.coe_sub : ∀ {p q : ℚ≥0}, q ≤ p → ↑(p - q) = ↑p - ↑q
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.centerToAddOpposite.eq_1 : ∀ {M : Type u_2} [inst : AddZeroClass M], AddSubmonoid.centerToAddOpposite = AddSubsemigroup.centerToAddOpposite
-- Mathlib.LinearAlgebra.Prod
Submodule.ker_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inr R M M₂).ker = ⊥
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_iff_getElem_le_getElem_of_le`. -/
List.sortedLE_of_getElem_le_getElem_of_le : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i ≤ j → l[i] ≤ l[j]) → l.SortedLE
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_inl_normalizationCoprodIso_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom h)) =
    CategoryTheory.CategoryStruct.comp iU
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) h)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ),
  t.truncGELTToLTGE a b = t.truncGELTToLTGE a b
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_top_le_iff : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {K : TopologicalSpace.Compacts E} {C : ℝ},
  0 ≤ C →
    ∀ (i : ℕ) (f : ContDiffMapSupportedIn E F ⊤ K),
      (ContDiffMapSupportedIn.seminorm 𝕜 E F ⊤ K i) f ≤ C ↔ ∀ x ∈ K, ‖iteratedFDeriv ℝ i (⇑f) x‖ ≤ C
-- Mathlib.Topology.NhdsKer
nhdsKer_sUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : Set (Set X)), nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.headD.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a : α) (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.headD le a (Batteries.BinomialHeap.Imp.Heap.cons rank val c s) =
    Batteries.BinomialHeap.Imp.Heap.headD le (if le a val = true then a else val) s
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) → [inst_2 : CategoryTheory.AddMonObj A] → Inhabited (CategoryTheory.AddMod C A)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.map_id : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Projectivization.map LinearMap.id ⋯ = id
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.isClosed' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.Closeds α), IsClosed self.carrier
-- Std.Do.SPred.SPred
Std.Do.SPred.pure_cons : ∀ {σs : List (Type u)} {σ : Type u} {P : Prop}, ⌜P⌝ = fun x => ⌜P⌝
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield inherits a division ring structure  -/
SubfieldClass.toDivisionRing : {K : Type u} →
  [inst : DivisionRing K] →
    {S : Type u_1} → [inst_1 : SetLike S K] → [h : SubfieldClass S K] → (s : S) → DivisionRing ↥s
-- Init.Prelude
decide_eq_true : ∀ {p : Prop} [inst : Decidable p], p → decide p = true
-- Init.Data.List.SplitOn.Lemmas
/-- When a list of the form `[...xs, sep, ...as]` is split at `a`,
the result is the concatenation of `splitOnP` called on `xs` and `as`  -/
List.splitOn_append_cons_self : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a : α} (xs as : List α),
  List.splitOn a (xs ++ a :: as) = List.splitOn a xs ++ List.splitOn a as
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.restrict : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α}, AEMeasurable f μ → ∀ {s : Set α}, AEMeasurable f (μ.restrict s)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mk.inj : ∀ {ι : Type u_1} {X : Type u_2} {inst : TopologicalSpace X} {s : Set X} {toFun : ι → C(X, ℝ)}
  {locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)} {nonneg' : 0 ≤ toFun}
  {sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1} {sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), (toFun i) x ≤ 1}
  {toFun_1 : ι → C(X, ℝ)} {locallyFinite'_1 : LocallyFinite fun i => Function.support ⇑(toFun_1 i)}
  {nonneg'_1 : 0 ≤ toFun_1} {sum_eq_one'_1 : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun_1 i) x = 1}
  {sum_le_one'_1 : ∀ (x : X), ∑ᶠ (i : ι), (toFun_1 i) x ≤ 1},
  { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
      { toFun := toFun_1, locallyFinite' := locallyFinite'_1, nonneg' := nonneg'_1, sum_eq_one' := sum_eq_one'_1,
        sum_le_one' := sum_le_one'_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The product of `Submonoid`s is isomorphic to their product as `Monoid`s.  -/
Submonoid.prodEquiv : {N : Type u_2} →
  [inst : MulOneClass N] →
    {M : Type u_5} → [inst_1 : MulOneClass M] → (s : Submonoid M) → (t : Submonoid N) → ↥(s.prod t) ≃* ↥s × ↥t
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.trunc.eq_1 : ∀ {R : Type u_1} [inst : Semiring R],
  LaurentPolynomial.trunc =
    (Polynomial.toFinsuppIso R).symm.toAddMonoidHom.comp
      (AddMonoidAlgebra.comapDomainAddMonoidHom Nat.cast LaurentPolynomial.trunc._proof_1)
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_pair : ∀ {X : Type u_2} {x y : X} [inst : PseudoEMetricSpace X], Metric.ediam {x, y} = edist x y
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.measurableSet_bliminf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : ℕ → Set α} {p : ℕ → Prop},
  (∀ (n : ℕ), p n → MeasurableSet (s n)) → MeasurableSet (Filter.bliminf s Filter.atTop p)
-- Mathlib.Order.CompleteLattice.Basic
iInf_image : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {f : β → γ} {g : γ → α} {t : Set β},
  ⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b)
-- Mathlib.Topology.AlexandrovDiscrete
closure_iUnion : ∀ {ι : Sort u_1} {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (f : ι → Set α),
  closure (⋃ i, f i) = ⋃ i, closure (f i)
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- The next fixed point function, the least fixed point of the normal function `f`, at least `a`.

This is defined as `nfpFamily` applied to a family consisting only of `f`.  -/
Ordinal.nfp : (Ordinal.{u_1} → Ordinal.{u_1}) → Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.baseChange_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (P : Fin 3 → A), (W'.baseChange B).Nonsingular (⇑f ∘ P) ↔ (W'.baseChange A).Nonsingular P
-- Mathlib.Tactic.Find
/-- `#find t` finds definitions and theorems whose result type matches the term `t`, and prints them as
info lines. Use holes in `t` to indicate arbitrary subexpressions, for example `#find _ ∧ _` will
match any conjunction. `#find` is also available as a command.
`#find` will not affect the goal by itself and should be removed from the finished proof.

There is also the `find` tactic which looks for lemmas which are `apply`able against the current
goal.

Examples:
```lean
#find _ + _ = _ + _
#find ?n + _ = _ + ?n
#find (_ : Nat) + _ = _ + _
#find Nat → Nat
```
 -/
Mathlib.Tactic.Find.«tactic#find_» : Lean.ParserDescr
-- Mathlib.RingTheory.Perfection
ModP.preVal_add : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} (x y : ModP O p), ModP.preVal K v O p (x + y) ≤ max (ModP.preVal K v O p x) (ModP.preVal K v O p y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).getKey? k' =
        if compare k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.instMonadCacheOfMonad : {α β : Type} →
  {m : Type → Type} →
    [inst : BEq α] → [inst_1 : Hashable α] → [Monad m] → [Lean.MonadHashMapCacheAdapter α β m] → Lean.MonadCache α β m
-- Mathlib.LinearAlgebra.Multilinear.Finsupp
/-- The linear equivalence of multilinear maps on free modules over `R` indexed by `fun i => κ i` on
the domain and `ι'` on the codomain and the finitely supported maps from
`(Π i, κ i) × ι'` into `R`.

This is the `Finsupp` version of `MultilinearMap.freeDFinsuppEquiv`.
 -/
MultilinearMap.freeFinsuppEquiv : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      {κ : ι → Type u_4} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [DecidableEq R] →
                [DecidableEq ι'] →
                  [(i : ι) → Fintype (κ i)] →
                    [(i : ι) → DecidableEq (κ i)] →
                      (((i : ι) → κ i) × ι' →₀ R) ≃ₗ[R] MultilinearMap R (fun i => κ i →₀ R) (ι' →₀ R)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : CategoryTheory.AddGrp C), (CategoryTheory.AddGrp.forget C).obj X = X.X
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.lift_addCommutator_eq_add_add_neg_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] (f₁ f₂ : X ⟶ G),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.AddGrpObj.addCommutator G) =
    f₁ + f₂ + -f₁ + -f₂
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.isFiniteMeasureAdd : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.IsFiniteMeasure (μ + ν)
-- Init.Data.String.Basic
String.lt_next' : ∀ (s : String) (p : String.Pos.Raw), p < String.Pos.Raw.next s p
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_sSup : ∀ {M : Type u_2} [inst : Mul M] (S : Set (Subsemigroup M)), (sSup S).op = sSup (Subsemigroup.unop ⁻¹' S)
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- Point below which the recurrence is in the base case  -/
AkraBazziRecurrence.n₀ : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : Nonempty α] →
      {T : ℕ → ℝ} → {g : ℝ → ℝ} → {a b : α → ℝ} → {r : α → ℕ → ℕ} → AkraBazziRecurrence T g a b r → ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.CallHierarchyPrepareParams
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z),
  ↑(e.transHomeomorph f').symm = ↑e.symm ∘ ⇑f'.symm
-- Mathlib.Algebra.Homology.Factorizations.CM5a
CochainComplex.Plus.modelCategoryQuillen.exists_quasiIso_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) [CategoryTheory.EnoughInjectives C] (n : ℤ) [K.IsStrictlyGE n],
  ∃ L i, ∃ (_ : QuasiIso i) (_ : ∀ (n : ℤ), CategoryTheory.Injective (L.X n)), L.IsStrictlyGE n
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ‖OfNat.ofNat n‖ = OfNat.ofNat n
-- Mathlib.Data.Sym.Basic
Sym.map_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (n : ℕ), Function.Injective (Sym.map f)
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.instSmallD₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W]
  [CategoryTheory.LocallySmall.{w, v, u} C], Small.{w, max u v} (CategoryTheory.OrthogonalReflection.D₂ W Z)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isNone_minEntry?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.minEntry? l).isNone = l.isEmpty
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.LawfulEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, k ∈ t.keysArray ↔ k ∈ t
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.restrictPreimage_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) (s : Set β)
  (a : ↑(⇑f ⁻¹' s)), (f.restrictPreimage s) a = s.restrictPreimage (⇑f) a
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_eq_zero_iff : ∀ {R : Type u_1} (n : ℕ) [inst : Semiring R] (t : R), (SkewPolynomial.monomial n) t = 0 ↔ t = 0
-- Lean.Parser.Basic
Lean.Parser.scientificLitFn : Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.Group.Synonym
toLex_div : ∀ {α : Type u_1} [inst : Div α] (a b : α), toLex (a / b) = toLex a / toLex b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.iCycles_mk : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {m n : ℕ}
  (h : (ComplexShape.down ℕ).next m = n) (f : (Fin m → G) →₀ ↑A)
  (hf : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains A).d m n)) f = 0),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A m)) (groupHomology.cyclesMk m n h f hf) = f
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X Y : C)
  [HomotopicalAlgebra.IsFibrant Y], Equivalence HomotopicalAlgebra.RightHomotopyRel
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Useful to use together with `Continuous.comp₂`.  -/
ContinuousLinearMap.continuous₂ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G),
  Continuous (Function.uncurry fun x y => (f x) y)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_const : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} (b : β), MeasurableSpace.map (fun _a => b) m = ⊤
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.isoMk_hom_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom),
  (CategoryTheory.Bicategory.InducedBicategory.isoMk φ).hom.hom = φ.hom
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.unit_pushforwardComp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g]
  [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).unit
      ((CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.comp f g)).whiskerLeft
        (CategoryTheory.ExponentiableMorphism.pushforwardComp f g).hom) =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g)).unit
-- Init.Data.List.Nat.TakeDrop
List.head?_take : ∀ {α : Type u_1} {l : List α} {i : ℕ}, (List.take i l).head? = if i = 0 then none else l.head?
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mul_nc.eq_1 : ∀ (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.mul_nc p₂ = Lean.Grind.CommRing.Poly.mul_nc.go p₂ p₁ (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.ext : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {f g : A →A[R] B}, (∀ (x : A), f x = g x) → f = g
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_cons_eq_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.containsKey a (⟨k, v⟩ :: l) = true ↔ (k == a) = true ∨ Std.Internal.List.containsKey a l = true
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.toMeasure_injective : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω], Function.Injective MeasureTheory.FiniteMeasure.toMeasure
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- The natural isomorphism
`F.mapShortComplex ⋙ cyclesFunctor D ≅ cyclesFunctor C ⋙ F`
for a functor `F : C ⥤ D` which preserves homology.  -/
CategoryTheory.ShortComplex.cyclesFunctorIso : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.PreservesZeroMorphisms] →
                [inst_5 : CategoryTheory.Limits.HasKernels C] →
                  [inst_6 : CategoryTheory.Limits.HasCokernels C] →
                    [inst_7 : CategoryTheory.Limits.HasKernels D] →
                      [inst_8 : CategoryTheory.Limits.HasCokernels D] →
                        [F.PreservesHomology] →
                          F.mapShortComplex.comp (CategoryTheory.ShortComplex.cyclesFunctor D) ≅
                            (CategoryTheory.ShortComplex.cyclesFunctor C).comp F
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I : Ideal S} [IsDomain S]
  {r : S},
  r ≠ 0 →
    r ∈ I → ∀ {p : Polynomial R}, p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ Ideal.comap f I
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.mk_neg : ∀ (z : ℂ) (hz : ‖-z‖ ≤ 1), Complex.UnitClosedDisc.mk (-z) hz = -Complex.UnitClosedDisc.mk z ⋯
-- Aesop.Rule
Aesop.NormRuleInfo.mk.inj : ∀ {penalty penalty_1 : ℤ}, { penalty := penalty } = { penalty := penalty_1 } → penalty = penalty_1
-- Mathlib.Algebra.Module.SnakeLemma
/-- Suppose we have an exact commutative diagram
```
                K₃
                |
                ι₃
                ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|       |
π₁      π₂
↓       ↓
C₁ -G-→ C₂

```
such that `f₂` is surjective, `g₁` is injective, and `π₁` is surjective,
then `K₃ -δ→ C₁ -G→ C₂` is exact.
 -/
SnakeLemma.exact_δ'_left : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) {K₃ : Type u_9} {C₁ : Type u_10} {C₂ : Type u_11}
  [inst_13 : AddCommGroup K₃] [inst_14 : Module R K₃] [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁]
  [inst_17 : AddCommGroup C₂] [inst_18 : Module R C₂] (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
  (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⇑i₁ ⇑π₁) (π₂ : N₂ →ₗ[R] C₂),
  Function.Exact ⇑i₂ ⇑π₂ →
    ∀ (hf₂ : Function.Surjective ⇑f₂) (hg₁ : Function.Injective ⇑g₁) (G : C₁ →ₗ[R] C₂), ⋯ = ⋯ → ⋯ → ⋯
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Implementation of `for x in (b : BinomialHeap α le) ...` notation,
which iterates over the elements in the heap in increasing order.
 -/
Batteries.BinomialHeap.forIn : {α : Type u} →
  {le : α → α → Bool} →
    {m : Type u_1 → Type u_2} →
      {β : Type u_1} → [Monad m] → Batteries.BinomialHeap α le → β → (α → β → m (ForInStep β)) → m β
-- Mathlib.Data.Sign.Defs
/-- Turn a `SignType` into zero, one, or minus one. This is a coercion instance.  -/
SignType.cast : {α : Type u_1} → [Zero α] → [One α] → [Neg α] → SignType → α
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (pres : CategoryTheory.Limits.LimitPresentation J X) {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (pres.π.app i) (pres.diag.map f) = pres.π.app j
-- Std.Http.Data.Headers.Name
Std.Http.Header.Name.beq_eq : ∀ {x y : Std.Http.Header.Name}, (x == y) = (x.value == y.value)