mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.BinomialHeap.Basic
/-- `O(n log n)`. Construct a heap from a list by inserting all the elements.  -/
Batteries.BinomialHeap.ofList : {α : Type u} → (le : α → α → Bool) → List α → Batteries.BinomialHeap α le
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.comp_homEquiv_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (Opposite.op X')) (f : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp f (e.homEquiv.symm x) =
    e.homEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f.op)) x)
-- Mathlib.Topology.Compactness.Compact
isCompact_iUnion : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [Finite ι],
  (∀ (i : ι), IsCompact (f i)) → IsCompact (⋃ i, f i)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.match_1.eq_2 : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {n : Type u_1 → Type u_3} (γ : Type u_1) (Pl : α → γ → ForInStep γ → Prop)
  (motive :
    (it : Std.IterM Id α) → ((b : α) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (Pl b c))) → Sort u_2)
  (upperBound : α)
  (f :
    (b : α) →
      { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
        (c : γ) → n (Subtype (Pl b c)))
  (h_1 :
    (next upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := some next, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := some next, upperBound := upperBound } } f)
  (h_2 :
    (upperBound : α) →
      (f :
          (b : α) →
            { internalState := { next := none, upperBound := upperBound } }.IsPlausibleIndirectOutput b →
              (c : γ) → n (Subtype (Pl b c))) →
        motive { internalState := { next := none, upperBound := upperBound } } f),
  (match { internalState := { next := none, upperBound := upperBound } }, f with
    | { internalState := { next := some next, upperBound := upperBound } }, f => h_1 next upperBound f
    | { internalState := { next := none, upperBound := upperBound } }, f => h_2 upperBound f) =
    h_2 upperBound f
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coneOfConeUncurry_pt : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCones F}
  (Q : (j : J) → CategoryTheory.Limits.IsLimit (D.obj j))
  (c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.uncurry.obj F)),
  (CategoryTheory.Limits.coneOfConeUncurry Q c).pt = c.pt
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_mul : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Mul γ] [inst_3 : ContinuousMul γ] (f g : α →ₘ[μ] γ), ↑(f * g) =ᵐ[μ] ↑f * ↑g
-- Init.Data.UInt.Lemmas
UInt32.lt_ofNat_iff : ∀ {n : UInt32} {m : ℕ}, m < UInt32.size → (n < UInt32.ofNat m ↔ n.toNat < m)
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose₄ : ∀ {p q : Prop}, (q → p) → ¬p → ¬q
-- Mathlib.Analysis.Calculus.FDeriv.Pow
/-- Eta-expanded form of `fderivWithin_pow` -/
fderivWithin_fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    ∀ (n : ℕ),
      DifferentiableWithinAt 𝕜 f s x →
        fderivWithin 𝕜 (fun i => f i ^ n) s x = (n • f x ^ (n - 1)) • fderivWithin 𝕜 f s x
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- An equivalence between the type of `WalkingIso`s in `C` and the type of isomorphisms in `C`.  -/
CategoryTheory.WalkingIso.equiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor CategoryTheory.WalkingIso C ≃ (X : C) × (Y : C) × (X ≅ Y)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k k' : α} {f : Option β → Option β}
  {h : k' ∈ Std.ExtDHashMap.Const.alter m k f},
  (Std.ExtDHashMap.Const.alter m k f).getKey k' h = if heq : (k == k') = true then k else m.getKey k' ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonAssocSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M],
  MonoidAlgebra.nonAssocSemiring =
    { toNonUnitalNonAssocSemiring := MonoidAlgebra.nonUnitalNonAssocSemiring, toOne := MonoidAlgebra.one, one_mul := ⋯,
      mul_one := ⋯, natCast := fun n => MonoidAlgebra.single 1 ↑n, natCast_zero := ⋯, natCast_succ := ⋯ }
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.map_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (R' : Type u_6)
  {M' : Type u_7} [inst_3 : CommRing R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] [inst_6 : Module R M']
  [inst_7 : Algebra R R'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (p : Polynomial R) (q : PolynomialModule R M),
  (PolynomialModule.map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (PolynomialModule.map R' f) q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.iterateDerivativeC.eq_1 : ∀ (n k : ℕ) (x : ℝ) (i : ℕ),
  Polynomial.Chebyshev.iterateDerivativeC✝ n k x i =
    ↑k.factorial *
        (∏ j ∈ (Finset.range (n + 1)).erase i, (Polynomial.Chebyshev.node n i - Polynomial.Chebyshev.node n j))⁻¹ *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - Polynomial.Chebyshev.node n a)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.cpow_mul_ofReal_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ) (z : ℂ), ↑x ^ (↑y * z) = ↑(x ^ y) ^ z
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.IsTriangularizable.maxGenEigenspace_eq_top : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  [self : LieModule.IsTriangularizable R L M] (x : L), ⨆ φ, ((LieModule.toEnd R L M) x).maxGenEigenspace φ = ⊤
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {g : β →CO γ} {f₁ f₂ : α →CO β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass Mᵒᵈ N α
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Pull back the metric structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
algebra homomorphism `Unitization.splitMul 𝕜 A`, but replace the bornology and the uniformity so
that they coincide with `𝕜 × A`.  -/
Unitization.instMetricSpace : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] → [RegularNormedAlgebra 𝕜 A] → MetricSpace (Unitization 𝕜 A)
-- Mathlib.Algebra.MonoidAlgebra.Support
/-- **Alias** of `MonoidAlgebra.support_coeff_single_mul`. -/
MonoidAlgebra.support_single_mul : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : IsLeftCancelMul G] (f : MonoidAlgebra k G)
  (r : k),
  (∀ (y : k), r * y = 0 ↔ y = 0) →
    ∀ (x : G), (MonoidAlgebra.single x r * f).coeff.support = Finset.map (mulLeftEmbedding x) f.coeff.support
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.uniqueOfRight : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            [inst_2 : TopologicalSpace M₁] →
              [inst_3 : AddCommMonoid M₁] →
                {M₂ : Type u_6} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R₁ M₁] → [inst_7 : Module R₂ M₂] → [Subsingleton M₂] → Unique (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Topology.Category.CompHaus.Frm
topCatOpToFrm_obj_coe : ∀ (X : TopCatᵒᵖ), ↑(topCatOpToFrm.obj X) = TopologicalSpace.Opens ↑(Opposite.unop X)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_inv : ∀ {α : Type u_2} [inst : Inv α] {s t : Set α}, (s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹
-- Qq.ForLean.ToExpr
toExprLevel : Lean.Level → Lean.Expr
-- Lean.Structure
Lean.StructureResolutionOrderResult : Type
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey?.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.leaf.maxKey? = none
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Run the `CoherenceM ρ` monad.  -/
Mathlib.Tactic.BicategoryLike.CoherenceM.run : {α ρ : Type} →
  Mathlib.Tactic.BicategoryLike.CoherenceM ρ α → ρ → optParam Mathlib.Tactic.BicategoryLike.State { } → Lean.MetaM α
-- Mathlib.Data.List.Defs
List.map₂Left.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.map₂Left f (a :: as) (b :: bs) = f a (some b) :: List.map₂Left f as bs
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
/-- The natural embedding of the free additive semigroup into the
free additive monoid. This is injective (`FreeAddSemigroup.toFreeAddMonoid_injective`), and its
image consists of all non-`0` elements of the free additive monoid
(`FreeAddSemigroup.eq_zero_or_toFreeAddMonoid`).  -/
FreeAddSemigroup.toFreeAddMonoid : {α : Type u_1} → FreeAddSemigroup α →ₙ+ FreeAddMonoid α
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.IsPartial.mk : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R}
  {f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)},
  StrictMono ↑f →
    seed.baseEmbedding ≤ f →
      (∀ (x : ↥f.domain) (c : FiniteArchimedeanClass M),
          toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑f x))) ∈ f.toFun.range) →
        HahnEmbedding.IsPartial seed f
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The map that appears in Behrend's bound on Roth numbers.  -/
Behrend.map : {n : ℕ} → ℕ → (Fin n → ℕ) →+ ℕ
-- Init.Data.Array.BasicAux
/-- Applies a function to each element of an array, returning the array of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new array if the result of each function call is
pointer-equal to its argument.
 -/
Array.mapMono : {α : Type u_1} → Array α → (α → α) → Array α
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_three : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a : A),
  autoParam (0 ≤ a) CFC.nnrpow_three._auto_1 → a ^ 3 = a * a * a
-- Mathlib.CategoryTheory.Sites.Plus
CategoryTheory.GrothendieckTopology.diagramNatTrans_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) (P : CategoryTheory.Functor Cᵒᵖ D),
  J.diagramNatTrans (CategoryTheory.CategoryStruct.id P) X = CategoryTheory.CategoryStruct.id (J.diagram P X)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} [inst_3 : Inhabited (β k)] {f : β k → β k}, m.WF → (m.modify k f).get! k = (Option.map f (m.get? k)).get!
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.elabAtom : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiag : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {F : CategoryTheory.Functor C FintypeCat} →
      [inst_1 : CategoryTheory.GaloisCategory C] →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {V U : OpenSubgroup (CategoryTheory.Aut F)} →
            (h : (↑U).Normal) →
              {A : C} →
                (u :
                    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
                      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F)
                        (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U))) →
                  U ≤ V →
                    CategoryTheory.Limits.Cocone
                      ((CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).comp
                        (CategoryTheory.PreGaloisCategory.functorToAction F))
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.tail_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → s.tail ~ʷ t.tail
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCloseds_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : T2Space α]
  [inst_3 : T2Space β] (K : TopologicalSpace.NonemptyCompacts α) (L : TopologicalSpace.NonemptyCompacts β),
  (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds
-- Mathlib.Order.CompleteBooleanAlgebra
/-- **Alias** of `Function.frameMinimalAxioms`.

---

Pullback an `Order.Frame.MinimalAxioms` along an injection.  -/
Function.Injective.frameMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  Order.Frame.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) →
        (∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) → (∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a) → Order.Frame.MinimalAxioms α
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙHom : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus 𝕜 A p] {a : A}
  (ha : p a), NonUnitalStarAlgHom.range (cfcₙHom ha) = NonUnitalStarAlgebra.elemental 𝕜 a
-- Mathlib.Topology.EMetricSpace.Diam
/-- The diameter of a set in a pseudoemetric space as an extended nonnegative real number.  -/
Metric.ediam : {X : Type u_2} → [PseudoEMetricSpace X] → Set X → ENNReal
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  (t.erase k).isEmpty = false →
    ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSemilatticeSupFiniteIndexNormalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instSemilatticeSupFiniteIndexNormalAddSubgroup =
    Function.Injective.semilatticeSup (fun H => H.toAddSubgroup) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β},
  Function.LeftInverse f g → Function.LeftInverse h i → Function.LeftInverse (h ∘ f) (g ∘ i)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.add : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, f.NeBot → g.NeBot → (f + g).NeBot
-- Mathlib.Analysis.Normed.Affine.AddTorsor
dist_left_midpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] {𝕜 : Type u_5} [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 V]
  [inst_5 : Invertible 2] (p₁ p₂ : P), dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The "smoothing function" is defined as `1 / log n`. This is defined as an `ℝ → ℝ` function
as opposed to `ℕ → ℝ` since this is more convenient for the proof, where we need to e.g. take
derivatives.  -/
AkraBazziRecurrence.smoothingFn : ℝ → ℝ
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.id_ε_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Comonad.id C).ε.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.toAddMonoidHom_fromCompletion : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  [inst_12 : T0Space β] [inst_13 : CompleteSpace β] (f : α →SL[σ] β),
  (↑f.fromCompletion).toAddMonoidHom = (↑f).toAddMonoidHom.extension ⋯
-- Init.Data.Array.Basic
/-- See comment at `forIn'Unsafe`  -/
Array.foldlMUnsafe : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (β → α → m β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m β
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.iUnion : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_5} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) → MeasureTheory.NullMeasurableSet (⋃ i, s i) μ
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1_mono : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {hm : m ≤ m0}
  [inst : MeasureTheory.SigmaFinite (μ.trim hm)] {E : Type u_7} [inst_1 : NormedAddCommGroup E]
  [inst_2 : PartialOrder E] [ClosedIciTopology E] [IsOrderedAddMonoid E] [inst_5 : NormedSpace ℝ E]
  [IsOrderedModule ℝ E] {f g : α → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ →
      f ≤ᵐ[μ] g → ↑↑(MeasureTheory.condExpL1 hm μ f) ≤ᵐ[μ] ↑↑(MeasureTheory.condExpL1 hm μ g)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.IntermediateField.isAlgebraic_X : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → IsAlgebraic (↥E) RatFunc.X
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- Upper exponential growth as a `SupBotHom`.  -/
ExpGrowth.expGrowthSupBotHom : SupBotHom (ℕ → ENNReal) EReal
-- Mathlib.Analysis.Calculus.FDeriv.Basic
hasFDerivWithinAt_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  t ∈ nhds x → (HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x)
-- Mathlib.Data.PNat.Defs
PNat.coe_lt_coe : ∀ (n k : ℕ+), ↑n < ↑k ↔ n < k
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.Q_map_eq_of_homotopy : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {K L : CochainComplex C ℤ} {f g : K ⟶ L} (h : Homotopy f g),
  DerivedCategory.Q.map f = DerivedCategory.Q.map g
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
AddActionHom.zeroEmbeddingMap.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {one : Type u_5} [inst_2 : Unique one],
  AddActionHom.zeroEmbeddingMap = { toFun := Function.Embedding.oneEmbeddingEquiv.toFun, map_vadd' := ⋯ }
-- Mathlib.Data.Prod.Basic
Prod.instIsTransLex : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsTrans α r] [IsTrans β s],
  IsTrans (α × β) (Prod.Lex r s)
-- Lean.Parser.Do
Lean.Parser.Term.doPatDecl : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.instTrans : {α : Type u} →
  {β : α → Type v} →
    Trans Std.DTreeMap.Internal.Impl.Equiv Std.DTreeMap.Internal.Impl.Equiv Std.DTreeMap.Internal.Impl.Equiv
-- Mathlib.Topology.MetricSpace.Bounded
Metric.hasAntitoneBasis_cobounded_compl_closedBall : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  (Bornology.cobounded α).HasAntitoneBasis fun r => (Metric.closedBall c r)ᶜ
-- Mathlib.Data.Int.ModEq
Int.ModEq.mul_left' : ∀ {n a b c : ℤ}, a ≡ b [ZMOD n] → c * a ≡ c * b [ZMOD c * n]
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : AddCommMonoid B} {inst_4 : Module R B} {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B}
  {toLinearMap : A →ₗ[R] B} {counit_comp : CoalgebraStruct.counit ∘ₗ toLinearMap = CoalgebraStruct.counit}
  {map_comp_comul :
    TensorProduct.map toLinearMap toLinearMap ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap}
  {toLinearMap_1 : A →ₗ[R] B} {counit_comp_1 : CoalgebraStruct.counit ∘ₗ toLinearMap_1 = CoalgebraStruct.counit}
  {map_comp_comul_1 :
    TensorProduct.map toLinearMap_1 toLinearMap_1 ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ toLinearMap_1},
  { toLinearMap := toLinearMap, counit_comp := counit_comp, map_comp_comul := map_comp_comul } =
      { toLinearMap := toLinearMap_1, counit_comp := counit_comp_1, map_comp_comul := map_comp_comul_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.Order.Defs.LinearOrder
gt_trichotomy : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), b < a ∨ a = b ∨ a < b
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The inverse of the structure map of a terminal coalgebra  -/
CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {A : CategoryTheory.Endofunctor.Coalgebra F} → CategoryTheory.Limits.IsTerminal A → (F.obj A.V ⟶ A.V)
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMaxOrderElemIoo : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x y : α}, NoMaxOrder ↑(Set.Ioo y x)