mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Subgroup
SubgroupClass.seminormedCommGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] {S : Type u_2} [inst_1 : SetLike S E] [inst_2 : SubgroupClass S E]
  (s : S),
  SubgroupClass.seminormedCommGroup s =
    { toNorm := (SubgroupClass.seminormedGroup s).toNorm, toCommGroup := SubgroupClass.toCommGroup s,
      toPseudoMetricSpace := Subtype.pseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.instHasLimitsOfShapeOfHasCountableLimitsOfCountableCategory : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u_2)
  [CategoryTheory.Limits.HasCountableLimits C] [inst_2 : CategoryTheory.Category.{v, u_2} J]
  [CategoryTheory.CountableCategory J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).maxKey? = some k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.coe_inj : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)}
  {f g : BoxIntegral.BoxAdditiveMap ι M I₀}, ⇑f = ⇑g ↔ f = g
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.unknownErrorCode : Lean.JsonRpc.ErrorCode
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ofList_eq_insertMany_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {l : List (α × β)}, Std.TreeMap.Raw.ofList l cmp = ∅.insertMany l
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.union_right_iff : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t u : Set α},
  MeasureTheory.AEDisjoint μ s (t ∪ u) ↔ MeasureTheory.AEDisjoint μ s t ∧ MeasureTheory.AEDisjoint μ s u
-- Std.Do.WP.Sound
/-- A `wp`-provable postcondition refines the post-run computation `prog.run s : m (α × σ)`
via `Internal.Ensures`.
 -/
Std.Do.StateT.ensures_of_wp_run : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WP m ps] [Std.Do.WPSound m ps]
  {α σ : Type u} {prog : StateT σ m α} (s : σ) (P : α × σ → Prop),
  (⊢ₛ (Std.Do.wp prog).apply (Std.Do.PostCond.noThrow fun a s' => ⌜P (a, s')⌝) s) →
    Std.Do.Internal.Ensures P (prog.run s)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData) {Z : C} (h_1 : h.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom (CategoryTheory.CategoryStruct.comp h.ι h_1) =
    CategoryTheory.CategoryStruct.comp S.homologyι (CategoryTheory.CategoryStruct.comp h.opcyclesIso.hom h_1)
-- Init.Data.Rat.Lemmas
Rat.ofScientific_false_def : ∀ {m e : ℕ}, Rat.ofScientific m false e = ↑(m * 10 ^ e)
-- Mathlib.CategoryTheory.Join.Basic
/-- Precomposing `mkFunctor F G α` with the left inclusion gives back `F`.  -/
CategoryTheory.Join.mkFunctorLeft : {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 E) →
              (G : CategoryTheory.Functor D E) →
                (α : (CategoryTheory.Prod.fst C D).comp F ⟶ (CategoryTheory.Prod.snd C D).comp G) →
                  (CategoryTheory.Join.inclLeft C D).comp (CategoryTheory.Join.mkFunctor F G α) ≅ F
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_pos_iff : ∀ {a : ENNReal}, 0 < a.toReal ↔ 0 < a ∧ a < ⊤
-- Lean.Parser.Types
_private.Lean.Parser.Types.0.Lean.Parser.SyntaxStack.drop : Lean.Parser.SyntaxStack → ℕ
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- The negation of an element `a` of a semigroup with a distributive negation divides another
element `b` iff `a` divides `b`.  -/
neg_dvd : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, -a ∣ b ↔ a ∣ b
-- Mathlib.MeasureTheory.Measure.WithDensityFinite
MeasureTheory.Measure.toFiniteAux.congr_simp : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [inst : MeasureTheory.SFinite μ], μ.toFiniteAux = μ_1.toFiniteAux
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.under_asIdeal : ∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] {B : Type u_6} [inst_2 : CommRing B] [inst_3 : IsDomain B]
  [inst_4 : Algebra A B] [inst_5 : Algebra.IsIntegral A B] (w : IsDedekindDomain.HeightOneSpectrum B),
  (IsDedekindDomain.HeightOneSpectrum.under A w).asIdeal = Ideal.under A w.asIdeal
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.colimit_ι_zero_cokernel_desc_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.CategoryStruct.comp f g = 0)
  [inst_2 : CategoryTheory.Limits.HasCokernel f] {Z_1 : C} (h_1 : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f 0)
        CategoryTheory.Limits.WalkingParallelPair.zero)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc f g h) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Init.Data.SInt.Lemmas
UInt64.toBitVec_toInt64 : ∀ (x : UInt64), x.toInt64.toBitVec = x.toBitVec
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initiallySmall_of_small_weakly_initial_set : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (s : Set J)
  [Small.{v, u} ↑s], (∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)) → CategoryTheory.InitiallySmall J
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁IsoOfIsTrivial.congr_simp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) [hA : A.IsTrivial],
  groupCohomology.cocycles₁IsoOfIsTrivial A = groupCohomology.cocycles₁IsoOfIsTrivial A
-- Mathlib.Data.PFunctor.Multivariate.M
/-- A path from the root of a tree to one of its node  -/
MvPFunctor.M.Path : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → P.last.M → Fin2 n → Type u
-- Mathlib.Order.Interval.Basic
NonemptyInterval.fst_dual : ∀ {α : Type u_1} [inst : LE α] (s : NonemptyInterval α),
  (NonemptyInterval.dual s).toProd.1 = OrderDual.toDual s.toProd.2
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.supp_def : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R), x ∈ ValuativeRel.supp R ↔ x ≤ᵥ 0
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_le_mk_iff_lt : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  a ≠ 0 → (ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b ↔ ∃ n, |b| < n • |a|)
-- Batteries.Tactic.Lint.Misc
/-- A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such
variables should be implicit instead.
 -/
Batteries.Tactic.Lint.explicitVarsOfIff : Batteries.Tactic.Lint.Linter
-- Mathlib.Topology.Compactification.StoneCech
/-- `pure : α → Ultrafilter α` defines a dense embedding of `α` in `Ultrafilter α`.  -/
isDenseEmbedding_pure : ∀ {α : Type u}, IsDenseEmbedding pure
-- Mathlib.Tactic.Translate.UnfoldBoundary
_private.Mathlib.Tactic.Translate.UnfoldBoundary.0.Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.insert : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries →
  Mathlib.Tactic.UnfoldBoundary.UnfoldEntry → Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion g],
  AlgebraicGeometry.IsPreimmersion (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Meta.SynthInstance
/-- Returns `{ type, cacheKeyType, hasOutParams }`, where `type` is the normalized type, and `cacheKeyType`
is part of the key for the type class resolution cache. If the class associated with `type`
does not have output parameters, then, `cacheKeyType` is `type`.
If it has, we replace arguments corresponding with output parameters with wildcard terms.

For example, the cache key for a query like
`HAppend.{0, 0, ?u} (BitVec 8) (BitVec 8) ?m` should be independent of the specific
metavariable IDs in output parameter positions. To achieve this, output parameter arguments
are erased from the cache key. However, universe levels that only appear in output parameter
types (e.g., `?u` corresponding to the result type's universe) must also be erased to avoid
cache misses when the same query is issued with different universe metavariable IDs.
 -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocess : Lean.Expr → Lean.MetaM Lean.Meta.PreprocessResult✝
-- Mathlib.Algebra.Group.Defs
inv_inv : ∀ {G : Type u_1} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_of_injective : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ {p : Polynomial R}, (Polynomial.map f p).Monic → p.Monic
-- Mathlib.LinearAlgebra.Multilinear.Curry
LinearMap.uncurryMid_apply : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1))
  (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) (m : (i : Fin n.succ) → M i),
  (LinearMap.uncurryMid p f) m = (f (m p)) (p.removeNth m)
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → (∀ x ∈ s, g x ≠ 0) → ContDiffOn 𝕜 n (f / g) s
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (b : β),
  ⇑e ⁻¹' Set.Iic b = Set.Iic (e.symm b)
-- Aesop.Search.SearchM
Aesop.SearchM.instInhabitedState : {a : Type} → [Inhabited a] → {a_1 : Aesop.Queue a} → Inhabited (Aesop.SearchM.State a)
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.toList.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Std.DHashMap.Internal.AssocList α β → Sort u_3)
  (h_1 : Unit → motive Std.DHashMap.Internal.AssocList.nil)
  (h_2 :
    (a : α) →
      (b : β a) → (es : Std.DHashMap.Internal.AssocList α β) → motive (Std.DHashMap.Internal.AssocList.cons a b es)),
  (match Std.DHashMap.Internal.AssocList.nil with
    | Std.DHashMap.Internal.AssocList.nil => h_1 ()
    | Std.DHashMap.Internal.AssocList.cons a b es => h_2 a b es) =
    h_1 ()
-- Init.Prelude
/-- A decidable predicate.

A predicate is decidable if the corresponding proposition is `Decidable` for each possible argument.
 -/
DecidablePred : {α : Sort u} → (α → Prop) → Sort (max 1 u)
-- Mathlib.LinearAlgebra.SymplecticGroup
/-- The group of symplectic matrices over a ring `R`.  -/
Matrix.symplecticGroup : (l : Type u_1) →
  (R : Type u_2) →
    [inst : DecidableEq l] → [inst_1 : CommRing R] → [inst_2 : Fintype l] → Submonoid (Matrix (l ⊕ l) (l ⊕ l) R)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_eq_false' : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.isUnsatDvd k p = true → (k ∣ Int.Internal.Linear.Poly.denote' ctx p) = False
-- Mathlib.Order.Antisymmetrization
/-- **Alias** of `lt_of_antisymmRel_of_lt`. -/
AntisymmRel.trans_lt : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → b < c → a < c
-- Std.Time.DateTime.Timestamp
/-- Fetches the current duration from the system.
 -/
Std.Time.Timestamp.now : IO Std.Time.Timestamp
-- Mathlib.GroupTheory.Nilpotent
/-- The `n+1`st term of the upper central series `H i` has underlying set equal to
the `x` such that `⁅x,G⁆ ⊆ H n`.  -/
AddSubgroup.mem_upperCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : AddGroup G] {n : ℕ} {x : G},
  x ∈ AddSubgroup.upperCentralSeries G (n + 1) ↔ ∀ (y : G), ⁅x, y⁆ ∈ AddSubgroup.upperCentralSeries G n
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_pos : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    (Polynomial.aeval a) F ≠ 0 → T_gen✝ p F a > 0
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.unop_top : ∀ {M : Type u_2} [inst : Mul M], ⊤.unop = ⊤
-- Init.Data.Iterators.Combinators.Monadic.Take
Std.Iterators.Types.Take.mk.inj : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {countdown : ℕ} {inner : Std.IterM m β}
  {finite : countdown > 0 ∨ Std.Iterators.Finite α m} {countdown_1 : ℕ} {inner_1 : Std.IterM m β}
  {finite_1 : countdown_1 > 0 ∨ Std.Iterators.Finite α m},
  { countdown := countdown, inner := inner, finite := finite } =
      { countdown := countdown_1, inner := inner_1, finite := finite_1 } →
    countdown = countdown_1 ∧ inner = inner_1
-- Mathlib.Data.Matrix.Mul
Matrix.smul_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : AddCommMonoid α] [inst_1 : Mul α]
  [inst_2 : Fintype n] [inst_3 : Monoid R] [inst_4 : DistribMulAction R α] [IsScalarTower R α α] (a : R)
  (M : Matrix m n α) (N : Matrix n l α), a • M * N = a • (M * N)
-- Mathlib.Tactic.FieldSimp
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), recursively construct a proof that in the field `$M`, the quotient
of the "multiplicative linear combinations" represented by `l₁` and `l₂` is the multiplicative
linear combination represented by `FieldSimp.qNF.div l₁ l₁`.  -/
Mathlib.Tactic.FieldSimp.qNF.mkDivProof : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
        have a := (l₁.div l₂).toNF;
        have a_1 := l₂.toNF;
        have a_2 := l₁.toNF;
        Q(«$a_2».eval / «$a_1».eval = «$a».eval)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₃.f =
    CategoryTheory.Limits.cokernel.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) g
      ⋯
-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkGateCached.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput) (idx : ℕ)
  (h1 : idx < (Std.Sat.AIG.mkGateCached.go aig input).aig.decls.size) (h2 : idx < aig.decls.size),
  (Std.Sat.AIG.mkGateCached.go aig input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- The linear equivalence between the fractional ideal `I` and the integral ideal `I.num`
defined by mapping `x` to `I.den • x`.  -/
FractionalIdeal.equivNum : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            [IsDomain R] →
              [Module.IsTorsionFree R P] → [Nontrivial P] → {I : FractionalIdeal S P} → ↑I.den ≠ 0 → ↥↑I ≃ₗ[R] ↥I.num
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.filter : {α : Type u} →
  {β : α → Type v} → ((a : α) → β a → Bool) → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃` and types `I` and `J`, this is the obvious
functor `GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃`.  -/
CategoryTheory.GradedObject.mapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃) →
              (I : Type u_4) →
                (J : Type u_5) →
                  CategoryTheory.Functor (CategoryTheory.GradedObject I C₁)
                    (CategoryTheory.Functor (CategoryTheory.GradedObject J C₂) (CategoryTheory.GradedObject (I × J) C₃))
-- Mathlib.Tactic.Simps.Basic
/-- A Boolean specifying whether `simp` lemmas are generated for this projection by default.  -/
Simps.ProjectionData.isDefault : Simps.ProjectionData → Bool
-- Mathlib.Order.Monotone.Defs
Monotone.comp_le_comp_left : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {g h : γ → β},
  Monotone f → g ≤ h → f ∘ g ≤ f ∘ h
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.independent_genEigenspace : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M) (k : ℕ∞), iSupIndep fun x => (f.genEigenspace x) k
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.iso₀_hom_naturality_assoc : ∀ {R : Type u} [inst : CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : ModuleCat.of R R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map f 0)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.iso₀ N).hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.iso₀ M).hom h
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime_apply_coe : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {a n : ℕ} (h : a.Coprime n) [inst_2 : NeZero n]
  (x : ↥(primitiveRoots n R)), ↑((IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime h) x) = ↑x ^ a
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.cmp.match_1.splitter : (motive : ONote → ONote → Sort u_1) →
  (x x_1 : ONote) →
    (Unit → motive ONote.zero ONote.zero) →
      ((x : ONote) → (x = ONote.zero → False) → motive x ONote.zero) →
        ((x : ONote) → (x = ONote.zero → False) → motive ONote.zero x) →
          ((e₁ : ONote) →
              (n₁ : ℕ+) → (a₁ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)) →
            motive x x_1
-- Init.Data.Char.Basic
/-- Returns `true` if the character is a uppercase ASCII letter.

The uppercase ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZ`.
 -/
Char.isUpper : Char → Bool
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopEquiv_unitIso_hom_app_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C), ((MonObj.mopEquiv C).unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ▷ f`.  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight : (Type → Type) → Type
-- Mathlib.Analysis.Normed.Group.Continuity
NormedGroup.toENormedMonoid.eq_1 : ∀ {F : Type u_7} [inst : NormedGroup F],
  NormedGroup.toENormedMonoid =
    { toContinuousENorm := SeminormedGroup.toContinuousENorm, toMonoid := inst.toMonoid, enorm_zero := ⋯,
      enorm_mul_le := ⋯, enorm_eq_zero := ⋯ }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.DTreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_eq_right : ∀ {a b : ByteArray} {i j : ℕ}, i = a.size → j = a.size + b.size → (a ++ b).extract i j = b
-- Aesop.Options.Internal
Aesop.Options'.toOptions : Aesop.Options' → Aesop.Options
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_2 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (isLt : 0 < n + 1 + 1) (isLt_1 : 1 < n + 1 + 1)
  (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩)
  (h_1 : (isLt isLt_2 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_2⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_2 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_2⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_2⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨0, isLt⟩, ⟨1, isLt_1⟩, x with
    | ⟨0, isLt⟩, ⟨0, isLt_2⟩, x => h_1 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨1, isLt_2⟩, x => h_2 isLt isLt_2 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_2 isLt isLt_1 x
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.isLeftQuasiInverse_congr : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u' ≈ u → v' ≈ v → (u.IsLeftQuasiInverse v ↔ u'.IsLeftQuasiInverse v')
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat.eq_2 : ∀ (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst_1 : Infinite ↑s] (n : ℕ),
  Nat.Subtype.ofNat s n.succ = Nat.Subtype.succ (Nat.Subtype.ofNat s n)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.smul_inv_mul_eq_inv_mul_opSMul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  ↑(A * A).card < 3 / 2 * ↑A.card → a ∈ A → a • (A⁻¹ * A) = MulOpposite.op a • (A⁻¹ * A)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.mkOfSMul_smul : ∀ {R : Type u} [inst : Ring R] {A : AddCommGrpCat} (φ : R →+* CategoryTheory.End A) (r : R),
  (ModuleCat.mkOfSMul φ).smul r = φ r
-- Init.Data.Iterators.Lemmas.Combinators.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Append.0.Std.IterM.step_append.match_1.eq_1 : ∀ {α₁ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (out : β)
  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' out, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' out h
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.fold.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.node c l v r with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_2 c l v r