mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The underlying `ContinuousAddMonoidHom`.  -/
ProfiniteAddGrp.Hom.hom : {M N : ProfiniteAddGrp.{u}} → M.Hom N → ↑M.toProfinite.toTop →ₜ+ ↑N.toProfinite.toTop
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_surjective : ∀ {σ : Type u_1} (R : Type u_3) {n : ℕ} [inst : Fintype σ] [inst_1 : CommRing R],
  Fintype.card σ ≤ n → Function.Surjective ⇑(MvPolynomial.esymmAlgHom σ R n)
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense.  -/
contMDiffAt_vectorSpace_iff_contDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {x : E},
  ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n (fun x => ⟨x, V x⟩) x ↔ ContDiffAt 𝕜 n V x
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instReprExtTheorem : Repr Lean.Meta.Ext.ExtTheorem
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.zero_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α], 0 ≠ ⊤
-- Init.Grind.Order
Lean.Grind.Order.lt_eq_true_of_le_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k₁ k₂ : ℤ},
  k₁.blt' k₂ = true → a ≤ b + ↑k₁ → (a < b + ↑k₂) = True
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.erase : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.GroupTheory.Index
Subgroup.index_inf_ne_zero : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.index ≠ 0 → K.index ≠ 0 → (H ⊓ K).index ≠ 0
-- Init.Data.UInt.Bitwise
UInt8.toNat_not : ∀ (a : UInt8), (~~~a).toNat = UInt8.size - 1 - a.toNat
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasPullback_over_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.HasPullback 0 0
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_sdiff : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s t : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G]
  {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s →
    MeasurableSet t →
      μ.IntegrableOn f s →
        t ⊆ s → ∫ᵛ (x : X) in s \ t, f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ] - ∫ᵛ (x : X) in t, f x ∂[B; μ]
-- Mathlib.Data.Finset.Fold
Finset.le_fold_max : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  c ≤ Finset.fold max b f s ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.toList.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → t.toList = t_1.toList
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.nhds_top_basis : (nhds ⊤).HasBasis (fun x => True) fun x => Set.Ioi ↑x
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
norm_iteratedFDerivWithin_prod_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_2} {A' : Type u_4} [inst_3 : NormedCommRing A']
  [inst_4 : NormedAlgebra 𝕜 A'] [inst_5 : DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'}
  {N : WithTop ℕ∞},
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    UniqueDiffOn 𝕜 s →
      ∀ {x : E},
        x ∈ s →
          ∀ {n : ℕ},
            ↑n ≤ N →
              ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j ∈ u, f j x) s x‖ ≤
                ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
-- Mathlib.Algebra.Group.End
Equiv.permCongrHom_trans : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} (e : α ≃ β) (e' : β ≃ γ),
  e.permCongrHom.trans e'.permCongrHom = (e.trans e').permCongrHom
-- Mathlib.Analysis.Normed.Module.RCLike.Real
frontier_sphere' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] (x : E) (r : ℝ),
  frontier (Metric.sphere x r) = Metric.sphere x r
-- Mathlib.RingTheory.OreLocalization.NonZeroDivisors
OreLocalization.nontrivial_of_nonZeroDivisorsRight : ∀ {R : Type u_1} [inst : MonoidWithZero R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] [Nontrivial R],
  S ≤ nonZeroDivisorsRight R → Nontrivial (OreLocalization S R)
-- Lean.Meta.LetToHave
/-- Returns `true` if there are any `letE (nondep := false)` subexpressions.
If true, then we must be sure to visit the subexpression.
If false, then we might still need to visit the subexpression,
but if we are not currently under any nondependent lets it is safe to skip it.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.hasDepLet : Lean.Expr → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyDₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  Std.DTreeMap.Internal.Impl.getKeyDₘ k l fallback = (l.getKey?ₘ k).getD fallback
-- Mathlib.Analysis.Complex.Angle
/-- The angle between two non-zero complex numbers is the absolute value of the argument of their
quotient.

Note that this does not hold when `x` or `y` is `0` as the LHS is `π / 2` while the RHS is `0`.  -/
Complex.angle_eq_abs_arg : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → InnerProductGeometry.angle x y = |(x / y).arg|
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 0.  -/
Finset.sum_smul_const_vsub_eq_neg_weightedVSub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P),
  ∑ i ∈ s, w i = 0 → ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = -(s.weightedVSub p₂) w
-- Lean.Parser.Extension
Lean.Parser.withOpen : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.pow : ∀ {n a b : ℕ} (m : ℕ), a ≡ b [MOD n] → a ^ m ≡ b ^ m [MOD n]
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sSup_toSubmodule_eq_iSup : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set (LieSubmodule R L M)), ↑(sSup S) = ⨆ N ∈ S, ↑N
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofBitVec : ∀ {b : BitVec 32}, { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Icc : ∀ {a b : ℝ}, 0 < a → a ≤ b → Real.log '' Set.Icc a b = Set.Icc (Real.log a) (Real.log b)
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.isUnit_of_coeff_zero_ne_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [CharP k p] (x : WittVector p k),
  x.coeff 0 ≠ 0 → IsUnit x
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- A variant of `IsConjRoot.iff_eq_zero`. `0` is a conjugate root of `x` if and only if `x = 0`.
 -/
isConjRoot_zero_iff_eq_zero' : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {x : S},
  IsConjRoot K x 0 ↔ x = 0
-- Mathlib.Algebra.Ring.Parity
even_add_one : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Even (a + 1) ↔ Odd a
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.whiskerLeft_zero : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C},
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft X 0 = 0
-- Std.Http.Data.Chunk
/-- The proof that it's a valid extension name.
 -/
Std.Http.Chunk.ExtensionName.isValidExtensionName : ∀ (self : Std.Http.Chunk.ExtensionName), Std.Http.Chunk.IsValidExtensionName self.value
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Spec is fully faithful  -/
AlgebraicGeometry.Spec.homEquiv : {R S : CommRingCat} → (AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R) ≃ (R ⟶ S)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
primitiveRoots.congr_simp : ∀ (k k_1 : ℕ),
  k = k_1 → ∀ (R : Type u_7) [inst : CommRing R] [inst_1 : IsDomain R], primitiveRoots k R = primitiveRoots k_1 R
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.maxKey?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction : ∀ {R : CommRingCat}, CategoryTheory.IsIso AlgebraicGeometry.tilde.adjunction.unit
-- Lean.Elab.Tactic.Doc
/-- The name of the canonical parser for the tactic  -/
Lean.Elab.Tactic.Doc.TacticDoc.internalName : Lean.Elab.Tactic.Doc.TacticDoc → Lean.Name
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousNeg.of_nhds_zero : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  Filter.Tendsto (fun x => -x) (nhds 0) (nhds 0) →
    (∀ (x₀ : G), nhds x₀ = Filter.map (fun x => x₀ + x) (nhds 0)) →
      (∀ (x₀ : G), Filter.Tendsto (fun x => x₀ + x + -x₀) (nhds 0) (nhds 0)) → ContinuousNeg G
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  k' ∈ Std.ExtDHashMap.Const.alter m k f ↔
    if (k == k') = true then (f (Std.ExtDHashMap.Const.get? m k)).isSome = true else k' ∈ m
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_lt_one_iff₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀}
  [ZeroLEOneClass M₀], 0 ≤ a → (a ^ 2 < 1 ↔ a < 1)
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `replaceF`.  -/
List.replaceFTR : {α : Type u_1} → (α → Option α) → List α → List α
-- Mathlib.Logic.Embedding.Set
/-- Equivalence between embeddings of `Option α` and a sigma type over the embeddings of `α`.  -/
Function.Embedding.optionEmbeddingEquiv : (α : Type u_1) → (β : Type u_2) → (Option α ↪ β) ≃ (f : α ↪ β) × ↑(Set.range ⇑f)ᶜ
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.rank_eq_lift : ∀ {σ : Type u} {K : Type v} [inst : CommRing K] [Nontrivial K],
  Module.rank K (MvPolynomial σ K) = Cardinal.lift.{v, u} (Cardinal.mk (σ →₀ ℕ))
-- Lean.Elab.Tactic.Induction
/-- Return `inductionAlt` name. It assumes `alt` does not have multiple `inductionAltLHS`. Returns `none` if the name is missing.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltName? : Lean.Syntax → Option Lean.Name
-- Mathlib.Topology.Instances.Discrete
LinearOrder.bot_topologicalSpace_eq_preorderTopology : ∀ {α : Type u_2} [inst : LinearOrder α] [PredOrder α] [SuccOrder α], ⊥ = Preorder.topology α
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.abs_integral_le_integral_abs : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  |∫ (a : α), f a ∂μ| ≤ ∫ (a : α), |f a| ∂μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l →
            k ∈ l → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKey? k' = some k
-- Mathlib.Data.Quot
Quotient.lift_comp_mk : ∀ {α : Sort u_1} {β : Sort u_2} {x : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b),
  Quotient.lift f h ∘ Quotient.mk x = f
-- Aesop.Forward.State
/-- A hypothesis that has not yet been matched against a premise, or a rule
pattern substitution.  -/
Aesop.RawHyp : Type
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The forgetful map from `NonUnitalSubalgebra` to `NonUnitalSubsemiring` as an
`OrderEmbedding`  -/
NonUnitalSubalgebra.toNonUnitalSubring' : {R : Type u} →
  {A : Type v} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalNonAssocRing A] → [inst_2 : Module R A] → NonUnitalSubalgebra R A ↪o NonUnitalSubring A
-- Std.Data.TreeMap.Raw.Basic
/-- Tree maps without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `TreeMap`
over `TreeMap.Raw`. Lemmas about the operations on `Std.TreeMap.Raw` are available in the
module `Std.Data.TreeMap.Raw.Lemmas`.

A tree map stores an assignment of keys to values. It depends on a comparator function that
defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval
of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function `cmp` should satisfy
certain laws that ensure a consistent ordering:

* If `a` is less than (or equal) to `b`, then `b` is greater than (or equal) to `a`
and vice versa (see the `OrientedCmp` typeclass).
* If `a` is less than or equal to `b` and `b` is, in turn, less than or equal to `c`, then `a`
is less than or equal to `c` (see the `TransCmp` typeclass).

Keys for which `cmp a b = Ordering.eq` are considered the same, i.e., there can be only one entry
with key either `a` or `b` in a tree map. Looking up either `a` or `b` always yields the same entry,
if any is present.

To avoid expensive copies, users should make sure that the tree map is used linearly.

Internally, the tree maps are represented as size-bounded trees, a type of self-balancing binary
search tree with efficient order statistic lookups.
 -/
Std.TreeMap.Raw : (α : Type u) → Type v → autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1 → Type (max u v)
-- Lean.Declaration
Lean.QuotVal.toConstantVal : Lean.QuotVal → Lean.ConstantVal
-- Init.Data.String.Basic
String.Pos.Raw.isValid_push : ∀ {s : String} {c : Char} {p : String.Pos.Raw},
  String.Pos.Raw.IsValid (s.push c) p ↔ String.Pos.Raw.IsValid s p ∨ p = s.rawEndPos + c
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If the pairwise pullbacks exist, this is the pre-`1`-hypercover where the covers
by the pullbacks are given by the pullbacks themselves.  -/
CategoryTheory.PreZeroHypercover.toPreOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → [E.HasPullbacks] → CategoryTheory.PreOneHypercover S
-- Mathlib.Data.Finset.Option
Finset.eraseNone_map_some : ∀ {α : Type u_1} (s : Finset α), Finset.eraseNone (Finset.map Function.Embedding.some s) = s
-- Init.Data.SInt.Lemmas
ISize.ofIntTruncate_toInt : ∀ (x : ISize), ISize.ofIntClamp x.toInt = x
-- Mathlib.Data.Seq.Defs
/-- Get the tail of a sequence (or `nil` if the sequence is `nil`)  -/
Stream'.Seq.tail : {α : Type u} → Stream'.Seq α → Stream'.Seq α
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectMonomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [∀ (i : I), CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (F i)]
      [CategoryTheory.Limits.HasPullbacks C], CategoryTheory.JointlyReflectMonomorphisms F
-- Mathlib.GroupTheory.Finiteness
AddMonoid.FG.mk : ∀ {M : Type u_3} [inst : AddMonoid M], ⊤.FG → AddMonoid.FG M
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_leftUnitor : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.leftUnitor F) = F.toFunctor.leftUnitor
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.erase.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l.size - 1) l.size → Sort u_3)
  (l' : Std.DTreeMap.Internal.Impl α β) (hl'₁ : l'.Balanced) (hl'₂ : l.size - 1 ≤ l'.size) (hl'₃ : l'.size ≤ l.size)
  (h_1 :
    (l' : Std.DTreeMap.Internal.Impl α β) →
      (hl'₁ : l'.Balanced) →
        (hl'₂ : l.size - 1 ≤ l'.size) →
          (hl'₃ : l'.size ≤ l.size) →
            motive { impl := l', balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ }),
  (match { impl := l', balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } with
    | { impl := l', balanced_impl := hl'₁, lb_le_size_impl := hl'₂, size_impl_le_ub := hl'₃ } =>
      h_1 l' hl'₁ hl'₂ hl'₃) =
    h_1 l' hl'₁ hl'₂ hl'₃
-- Mathlib.Order.Basic
Pi.instCompl : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → Compl (π i)] → Compl ((i : ι) → π i)
-- Mathlib.Topology.Path
Path.bijective_cast : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y x' y' : X} (hx : x' = x) (hy : y' = y),
  Function.Bijective fun x_1 => x_1.cast hx hy
-- Mathlib.Data.NNRat.Defs
NNRat.coprime_num_den : ∀ (q : ℚ≥0), q.num.Coprime q.den
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
`T` is a homeomorphism from `T` to itself.  -/
Homeomorph.smul : {α : Type u_2} →
  {G : Type u_4} →
    [inst : TopologicalSpace α] → [inst_1 : Group G] → [inst_2 : MulAction G α] → [ContinuousConstSMul G α] → G → α ≃ₜ α
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.empty_or_nonempty_of_hausdorffEDist_ne_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist s t ≠ ⊤ → s = ∅ ∧ t = ∅ ∨ s.Nonempty ∧ t.Nonempty
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.instContainsIdentitiesInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.ContainsIdentities],
  P.ind.ContainsIdentities
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The forgetful map from subalgebras to non-unital subalgebras, as an order embedding.  -/
Subalgebra.toNonUnitalSubalgebraOrderEmbedding : {R : Type uR} →
  {A : Type uA} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Subalgebra R A ↪o NonUnitalSubalgebra R A
-- Mathlib.Topology.Path
Path.cast_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a₁ a₂ b₁ b₂ c₁ c₂ : X} (γ : Path a₂ b₂) (γ' : Path b₂ c₂) (ha : a₁ = a₂)
  (hb : b₁ = b₂) (hc : c₁ = c₂), (γ.trans γ').cast ha hc = (γ.cast ha hb).trans (γ'.cast hb hc)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.con_mono : ∀ {G : Type u_1} [inst : Group G] {N M : Subgroup G} [hN : N.Normal] [hM : M.Normal],
  N ≤ M → QuotientGroup.con N ≤ QuotientGroup.con M
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_snd : ∀ {𝕜 : 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'] {x : M × M'}, MDiffAt Prod.snd x
-- Mathlib.Data.Num.Basic
Num.instSub : Sub Num
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized
/-- Constants are majorized with exponent `exp = 0` by any functions which tends to infinity.  -/
Tactic.ComputeAsymptotics.Majorized.const : ∀ {b : ℝ → ℝ},
  Filter.Tendsto b Filter.atTop Filter.atTop → ∀ {c : ℝ}, Tactic.ComputeAsymptotics.Majorized (fun x => c) b 0
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : PartialOrder β] → PartialOrder (α →Co β)
-- Init.Data.Nat.Basic
Nat.eq_of_lt_succ_of_not_lt : ∀ {m n : ℕ}, m < n + 1 → ¬m < n → m = n
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- **Alias** of `LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete`. -/
LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Nontrivial G] (g : G),
  ({x | x ≤ g}.WellFoundedOn fun x1 x2 => x1 > x2) ↔ Nonempty (G ≃+o ℤ)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_inter_eq_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.RingTheory.RegularLocalRing.Polynomial
Polynomial.isRegularRing_of_isRegularRing : ∀ (R : Type u_1) [inst : CommRing R] [IsRegularRing R], IsRegularRing (Polynomial R)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.reverse_single : ∀ {n : ℕ} (hn : 0 < n), (Composition.single n hn).reverse = Composition.single n hn
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.exists_isConj : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K] [Algebra.IsAlgebraic ℚ K]
  (φ : K →+* ℂ), ∃ σ, NumberField.ComplexEmbedding.IsConj φ σ
-- Mathlib.Data.List.Cycle
Cycle.fintypeNodupNontrivialCycle : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Fintype { s // s.Nodup ∧ s.Nontrivial }
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- The map `CardinalDirectedPoset κ → CardinalDirectedPoset κ` which sends
a partially ordered `κ`-filtered type `J` to `WithTop J`.  -/
CategoryTheory.CardinalDirectedPoset.withTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] → CategoryTheory.CardinalDirectedPoset κ → CategoryTheory.CardinalDirectedPoset κ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.whiskering_obj_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) {X Y : CategoryTheory.Functor SimplexCategory C} (α : X ⟶ Y) (X_1 : SimplexCategory),
  (((CategoryTheory.CosimplicialObject.whiskering C D).obj H).map α).app X_1 = H.map (α.app X_1)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.evaluation_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C) (F : CategoryTheory.Functor C D), ((CategoryTheory.evaluation C D).obj X).obj F = F.obj X
-- Mathlib.Data.Set.Monotone
/-- **Alias** of `StrictMono.of_domRestrict`.

---

**Alias** of the forward direction of `strictMono_domRestrict`. -/
StrictMono.of_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMono (s.domRestrict f) → StrictMonoOn f s
-- Init.Data.List.Lemmas
List.reverse_append : ∀ {α : Type u_1} {as bs : List α}, (as ++ bs).reverse = bs.reverse ++ as.reverse
-- Mathlib.RingTheory.IntegralDomain
/-- A finite subgroup of the units of an integral domain is cyclic.  -/
isCyclic_subgroup_units : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (S : Subgroup Rˣ) [Finite ↥S], IsCyclic ↥S
-- Mathlib.Data.ZMod.Basic
ZMod.lift_comp_castAddHom : ∀ (n : ℕ) {A : Type u_2} [inst : AddGroup A] (f : { f // f ↑n = 0 }),
  ((ZMod.lift n) f).comp (Int.castAddHom (ZMod n)) = ↑f