mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together on `s`. Stated by permuting the entries of `g`.  -/
AntivaryOn.sum_mul_le_sum_mul_comp_perm : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {s : Finset ι} {σ : Equiv.Perm ι} {f g : ι → α},
  AntivaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, f i * g (σ i)
-- Lean.Data.PrefixTree
Lean.instInhabitedPrefixTree : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → Inhabited (Lean.PrefixTree α β p)
-- Init.Data.List.TakeDrop
List.drop_drop : ∀ {α : Type u_1} {i j : ℕ} {l : List α}, List.drop i (List.drop j l) = List.drop (j + i) l
-- Init.Data.SInt.Lemmas
instLawfulIdentityISizeHAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- ε-δ characterization of uniform continuity on pseudoemetric spaces  -/
EMetric.uniformContinuous_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε
-- Mathlib.CategoryTheory.SingleObj
/-- A monoid homomorphism `f: M → End X` into the endomorphisms of an object `X` of a category `C`
induces a functor `SingleObj M ⥤ C`.  -/
CategoryTheory.SingleObj.functor : {M : Type u} →
  [inst : Monoid M] →
    {C : Type v} →
      [inst_1 : CategoryTheory.Category.{w, v} C] →
        {X : C} → (M →* CategoryTheory.End X) → CategoryTheory.Functor (CategoryTheory.SingleObj M) C
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
/-- The canonical isomorphism `(K ⊞ L).X i ≅ (K.X i) ⊞ (L.X i)`.  -/
HomologicalComplex.biprodXIso : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Preadditive C] →
        {c : ComplexShape ι} →
          (K L : HomologicalComplex C c) →
            [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] →
              (i : ι) → (K ⊞ L).X i ≅ K.X i ⊞ L.X i
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.zsmul : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (n : ℤ), Function.HasFiniteSupport (n • f)
-- Mathlib.Topology.Defs.Induced
Topology.IsEmbedding.mk : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → Function.Injective f → Topology.IsEmbedding f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKeyD k' fallback =
      if (k == k') = true then if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then k else fallback
      else m.getKeyD k' fallback
-- Lean.Elab.App
Lean.Elab.Term.getElabElimExprInfo : Lean.Expr → Lean.MetaM Lean.Elab.Term.ElabElimInfo
-- Init.Data.List.Lemmas
List.flatMap_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α} {β : Type u_2} {f : α → List β},
  List.flatMap f (List.replicate n a) = (List.replicate n (f a)).flatten
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.liminf_eq_sSup_univ_of_empty : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι}, v.HasBasis p s → ∀ (i : ι'), p i → s i = ∅ → Filter.liminf f v = sSup Set.univ
-- Init.Data.Array.Zip
Array.zipWithAll_map_left : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {as : Array α} {bs : Array β} {f : α → α'}
  {g : Option α' → Option β → γ},
  Array.zipWithAll g (Array.map f as) bs = Array.zipWithAll (fun a b => g (f <$> a) b) as bs
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_dvd_of_dvd : ∀ {m n : ℤ}, m ∣ n → n / m ∣ n
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.map_fst : ∀ {X Y : Bipointed} (self : X.Hom Y), self.toFun X.toProd.1 = Y.toProd.1
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.coe_one : ∀ {M : Type u_1} [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A], ⇑1 = id
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.comp_surjective : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ {g : ι' → ι}, Function.Surjective g → l.HasBasis (p ∘ g) (s ∘ g)
-- Mathlib.Order.Hom.Basic
OrderIso.trans_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ] (e : α ≃o β) (e' : β ≃o γ)
  (x : α), (e.trans e') x = e' (e x)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k k' fallback : α}, (k == k') = true → m.getKeyD k fallback = m.getKeyD k' fallback
-- Batteries.Data.List.Basic
/-- Returns the longest initial prefix of two lists such that they are pairwise related by `R`.
```
takeWhile₂ (· < ·) [1, 2, 4, 5] [5, 4, 3, 6] = ([1, 2], [5, 4])
```
 -/
List.takeWhile₂ : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → List α → List β → List α × List β
-- Mathlib.RingTheory.IsTensorProduct
_private.Mathlib.RingTheory.IsTensorProduct.0.IsTensorProduct.assocAux_symm_tmul : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] (f : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂)
  (hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃) (hg : IsTensorProduct g)
  (x₁ : M₁) (x₂ : M₂) (x₃ : M₃), (IsTensorProduct.assocAux✝ f hf g hg).symm (x₁ ⊗ₜ[R] (g x₂) x₃) = (f x₁) x₂ ⊗ₜ[S] x₃
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_neg_cancel_right : ∀ {α : Type u} [inst : AddMonoid α] (a : α) (b : AddUnits α), a + ↑b + ↑(-b) = a
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.continuous : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {s : Set E} {c : NNReal}, ApproximatesLinearOn f f' s c → Continuous (s.domRestrict f)
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_eq_image : ∀ (n : ℕ), Finset.HasAntidiagonal.antidiagonal n = Finset.image (fun i => (i, n - i)) (Finset.range (n + 1))
-- Mathlib.NumberTheory.ModularForms.QExpansion
CuspFormClass.exp_decay_atImInfty : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [CuspFormClass F Γ k],
  0 < h → h ∈ Γ.strictPeriods → ⇑f =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-2 * Real.pi * τ.im / h)
-- Mathlib.Data.Finset.SymmDiff
Finset.coe_symmDiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, ↑(symmDiff s t) = symmDiff ↑s ↑t
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasDerivWithinAt_congr_set`. -/
HasDerivWithinAt.congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜},
  s =ᶠ[nhds x] t → HasDerivWithinAt f f' s x → HasDerivWithinAt f f' t x
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- The norm on the infinite adele ring is given by the product of the normalized norms
across infinite places. The normalized norm is the real norm at real places and the
square of the complex norm at complex places.  -/
NumberField.InfiniteAdeleRing.instNorm : (K : Type u_1) → [inst : Field K] → [NumberField K] → Norm (NumberField.InfiniteAdeleRing K)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X), S.preOneHypercover.I₀ = S.Arrow
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence'_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence'.functor = CategoryTheory.Square.toArrowArrowFunctor'
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_smul_addMonoidHom_apply : ∀ {A : Type u_5} {B : Type u_6} {M : Type u_7} [inst : AddMonoid A] [inst_1 : DistribSMul M A] [inst_2 : AddZeroClass B]
  (c : M) (f : A →+ B) (a : A), (DomMulAct.mk c • f) a = f (c • a)
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_comm : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (n : ℕ),
  ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = ∑ i ∈ Finset.range n, y ^ i * x ^ (n - 1 - i)
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- A type alias for a group `G`. `ConjAct G` acts on `G` by conjugation  -/
ConjAct : Type u_3 → Type u_3
-- Mathlib.Topology.ContinuousMap.Compact
/-- When `α` is compact, and `β` is a metric space, the bounded continuous maps `α →ᵇ β` are
isometric to `C(α, β)`.
 -/
ContinuousMap.isometryEquivBoundedOfCompact : (α : Type u_1) →
  (β : Type u_2) →
    [inst : TopologicalSpace α] →
      [inst_1 : CompactSpace α] → [inst_2 : PseudoMetricSpace β] → C(α, β) ≃ᵢ BoundedContinuousFunction α β
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.Algebra.Group.End
/-- If `M` is a type with multiplicative, then multiplicative automorphisms of `M` have the
structure of a group.  -/
MulAut.instGroup : (M : Type u_2) → [inst : Mul M] → Group (MulAut M)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.toList_intermediateZip_of_finite : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] [inst_1 : Std.Iterator α₂ Id β₂] {it₁ : Std.Iter β₁}
  {memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }} {it₂ : Std.Iter β₂} [Std.Iterators.Finite α₁ Id]
  [Std.Iterators.Finite α₂ Id],
  (Std.Iter.Intermediate.zip it₁ memo it₂).toList = ((Option.map Subtype.val memo).toList ++ it₁.toList).zip it₂.toList
-- Mathlib.Analysis.Convex.Deriv
/-- If `f : ℝ → ℝ` is strictly convex on `S` and differentiable at `y ∈ S`, then the slope of any
secant line with right endpoint at `y` is strictly less than the left derivative at `y`.  -/
StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConvexOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' (Set.Iio y) y → slope f x y < f'
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.induct_unfolding : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s })
  (motive : γ → (next : α) → LargeEnough next → n γ → Prop),
  (∀ (acc : γ) (next : α) (h : LargeEnough next) (h_1 : next ≤ upperBound),
      (∀ (acc' : γ),
          Pl next acc (ForInStep.yield acc') →
            ∀ (next' : α) (hs : Std.PRange.succ? next = some next'),
              motive acc' next' ⋯
                (Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f)) →
        motive acc next h do
          let __do_lift ← f next h h_1 acc
          match __do_lift with
            | ⟨ForInStep.yield acc', property⟩ =>
              match hs : Std.PRange.succ? next with
              | some next' =>
                Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
              | none => pure acc'
            | ⟨ForInStep.done acc', property⟩ => pure acc') →
    (∀ (acc : γ) (next : α) (h : LargeEnough next), ¬next ≤ upperBound → motive acc next h (pure acc)) →
      ∀ (acc : γ) (next : α) (h : LargeEnough next),
        motive acc next h (Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
/-- Given a family of elements of a monoid, a member is said to be indecomposable if it cannot be
written as a product of two others in a non-trivial way.  -/
IsMulIndecomposable : {ι : Type u_1} → {M : Type u_2} → [Monoid M] → (ι → M) → Set ι → ι → Prop
-- Mathlib.Data.Fintype.Quotient
Quotient.hrecOn.congr_simp : ∀ {α : Sort u} {s : Setoid α} {motive : Quotient s → Sort v} (q : Quotient s) (f f_1 : (a : α) → motive ⟦a⟧)
  (e_f : f = f_1) (c : ∀ (a b : α), a ≈ b → f a ≍ f b), Quotient.hrecOn q f c = Quotient.hrecOn q f_1 ⋯
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate Value Theorem** for continuous functions on closed intervals, case
`f a ≥ t ≥ f b`.  -/
intermediate_value_Icc' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Icc (f b) (f a) ⊆ f '' Set.Icc a b
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSubtype.match_3.eq_2 : ∀ (motive : (n : ℕ) → (P : Fin n → Prop) → DecidablePred P → { i // P i } → Sort u_1) (n : ℕ) (P : Fin (n + 1) → Prop)
  (inst : DecidablePred P) (i : ℕ) (hi : i + 1 < n + 1) (hp : P ⟨i + 1, hi⟩)
  (h_1 : (n : ℕ) → (P : Fin (n + 1) → Prop) → (inst : DecidablePred P) → (hp : P 0) → motive n.succ P inst ⟨⟨0, ⋯⟩, hp⟩)
  (h_2 :
    (n : ℕ) →
      (P : Fin (n + 1) → Prop) →
        (inst : DecidablePred P) →
          (i : ℕ) → (hi : i + 1 < n + 1) → (hp : P ⟨i + 1, hi⟩) → motive n.succ P inst ⟨⟨i.succ, hi⟩, hp⟩),
  (match n.succ, P, inst, ⟨⟨i.succ, hi⟩, hp⟩ with
    | n.succ, P, inst, ⟨⟨0, ⋯⟩, hp⟩ => h_1 n P inst hp
    | n.succ, P, inst, ⟨⟨i.succ, hi⟩, hp⟩ => h_2 n P inst i hi hp) =
    h_2 n P inst i hi hp
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.congr_set : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → s =ᶠ[nhds x] t → ContMDiffWithinAt I I' n f t x
-- Init.Data.List.Count
List.count_eq_length_filter : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l = (List.filter (fun x => x == a) l).length
-- Mathlib.RingTheory.Artinian.Module
Ideal.quotientEquivAlgOfEq.congr_simp : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J),
  Ideal.quotientEquivAlgOfEq R₁ h = Ideal.quotientEquivAlgOfEq R₁ h
-- Mathlib.Order.Antisymmetrization
AntisymmRel.symmGen_congr_right : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) b c →
    (Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a b ↔ Relation.SymmGen (fun x1 x2 => x1 ≤ x2) a c)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalRingOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] → NonUnitalRing (DirectLimit G f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
unitary_iff_isStarNormal_and_spectrum_subset_unitary : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A}, u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `initial_of_initial_comp` below.  -/
CategoryTheory.Functor.initial_of_equivalence_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.IsEquivalence] [(F.comp G).Initial], G.Initial
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Control of the variation of the vector measure which appears in the integral of a vector
function with respect to a signed measure.  -/
MeasureTheory.VectorMeasure.variation_transpose_lsmul_flip : ∀ {X : Type u_2} {E : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [Nontrivial E] {μ : MeasureTheory.SignedMeasure X},
  (MeasureTheory.VectorMeasure.transpose μ (ContinuousLinearMap.lsmul ℝ ℝ).flip).variation =
    MeasureTheory.VectorMeasure.variation μ
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeSmallCategory : (J : Type v₁) → [CategoryTheory.SmallCategory J] → CategoryTheory.SmallCategory (CategoryTheory.Bicone J)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.asFiber.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  AlgebraicGeometry.Scheme.Hom.asFiber f x = (AlgebraicGeometry.Scheme.Hom.fiberHomeo f (f x)).symm ⟨x, ⋯⟩
-- Init.Data.List.Nat.Count
List.IsInfix.le_countP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <:+: l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
-- Mathlib.Data.Finsupp.Fin
/-- `tail` for maps `Fin (n + 1) →₀ M`. See `Fin.tail` for more details.  -/
Finsupp.tail : {n : ℕ} → {M : Type u_1} → [inst : Zero M] → (Fin (n + 1) →₀ M) → Fin n →₀ M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.congr : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α},
  BaireMeasurableSet s → s =ᶠ[residual α] t → BaireMeasurableSet t
-- Mathlib.Data.Nat.Factorization.Induction
/-- For any multiplicative function `f` with `f 1 = 1` and `f 0 = 1`,
we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`  -/
Nat.multiplicative_factorization' : ∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
  (∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) →
    f 0 = 1 → f 1 = 1 → f n = n.factorization.prod fun p k => f (p ^ k)
-- Mathlib.GroupTheory.Congruence.Defs
Con.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Con.instInhabited = { default := conGen emptyRelation }
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- The canonical isomorphism `G/⊥ ≃* G`.  -/
QuotientGroup.quotientBot : {G : Type u} → [inst : Group G] → G ⧸ ⊥ ≃* G
-- Lean.Meta.Tactic.Cases
Lean.Meta.CasesSubgoal.mk : Lean.Meta.InductionSubgoal → Option Lean.Name → Lean.Meta.CasesSubgoal
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldRedeclInfo.inj : ∀ {i i_1 : Lean.Elab.FieldRedeclInfo},
  Lean.Elab.Info.ofFieldRedeclInfo i = Lean.Elab.Info.ofFieldRedeclInfo i_1 → i = i_1
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_nsmul_add' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoMod hp (m • p + a) b = m • p + toIcoMod hp a b
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.mul_equiv_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (g : CauSeq β abv) {f : CauSeq β abv},
  f ≈ 0 → g * f ≈ 0
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.wellFoundedLT' : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), IsBotZeroClass (α i)] [∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Π₀ (i : ι), α i)
-- Init.Data.Slice.List.Lemmas
ListSlice.instLawfulSliceSizeTakeListIteratorIdListSliceData : ∀ {α : Type u_1}, Std.Slice.LawfulSliceSize (Std.Slice.Internal.ListSliceData α)
-- Std.Async.Process
Std.IO.Process.instInhabitedResourceUsageStats.default : Std.IO.Process.ResourceUsageStats
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurable_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : PartialOrder α]
  [OrderClosedTopology α] [SecondCountableTopology α], Measurable fun p => p.1 ≤ p.2
-- Mathlib.FieldTheory.Fixed
/-- Bijection between `G` and algebra automorphisms of `F` that fix the fixed points.  -/
FixedPoints.toAlgAutMulEquiv : (G : Type u_2) →
  (F : Type u_3) →
    [inst : Group G] →
      [inst_1 : Field F] →
        [inst_2 : MulSemiringAction G F] → [Finite G] → [FaithfulSMul G F] → G ≃* Gal(F/↥(FixedPoints.subfield G F))
-- Init.Control.Except
_private.Init.Control.Except.0.Except.map.match_1.eq_2 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (v : α) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.ok v with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_2 v
-- Mathlib.Order.Filter.Pi
Filter.le_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {g : Filter ((i : ι) → α i)},
  g ≤ Filter.pi f ↔ ∀ (i : ι), Filter.Tendsto (Function.eval i) g (f i)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.get? a = none
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` and `y` are both separable elements, then `F⟮x, y⟯ / F` is a separable extension.
As a consequence, any rational function of `x` and `y` is also a separable element.  -/
IntermediateField.isSeparable_adjoin_pair_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x y : E},
  IsSeparable F x → IsSeparable F y → Algebra.IsSeparable F ↥F⟮x, y⟯
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.sigmaMk_apply : ∀ {I : Type u_5} {X : I → Type u_7} [inst : (i : I) → TopologicalSpace (X i)] (i : I) (snd : X i),
  (ContinuousMap.sigmaMk i) snd = ⟨i, snd⟩
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that the slice formed by `startPos` and `endPos` contains a match
of `pat` in `s` and it is longest among matches starting at `startPos`.
 -/
String.Slice.Pattern.Model.IsLongestMatchAt : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → s.Pos → Prop