mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.updateAlts : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Cases pu → Array (Lean.Compiler.LCNF.Alt pu) → Lean.Compiler.LCNF.Cases pu
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.refoldFun : Mathlib.Tactic.Translate.CastKind✝
-- Lean.Expr
_private.Lean.Expr.0.Lean.natSubFn : Lean.Expr
-- ProofWidgets.Component.Basic
ProofWidgets.MarkdownDisplay.instFromJsonProps : Lean.FromJson ProofWidgets.MarkdownDisplay.Props
-- Mathlib.Topology.ContinuousMap.Polynomial
Polynomial.toContinuousMapOn_X_eq_restrict_id : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : IsTopologicalSemiring R] (s : Set R),
  Polynomial.X.toContinuousMapOn s = ContinuousMap.restrict s (ContinuousMap.id R)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_epsilon_pos : 0 < ArchimedeanClass.mk Hyperreal.epsilon
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquiv_apply : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (M : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : ι → M) (b : ι₂ → M),
  (PiTensorProduct.tmulEquiv R M)
      (((PiTensorProduct.tprod R) fun i => a i) ⊗ₜ[R] (PiTensorProduct.tprod R) fun i => b i) =
    (PiTensorProduct.tprod R) fun i => Sum.elim a b i
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearEquiv.coe_withLpCongr : ∀ (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [inst : Semiring K] [inst_1 : Semiring K']
  {σ : K →+* K'} {σ' : K' →+* K} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] [inst_4 : AddCommGroup V]
  [inst_5 : Module K V] [inst_6 : AddCommGroup V'] [inst_7 : Module K' V'] (f : V ≃ₛₗ[σ] V'),
  ⇑(LinearEquiv.withLpCongr p f) = WithLp.map p ⇑f
-- Mathlib.RingTheory.OreLocalization.OreSet
OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors : ∀ {R : Type u_1} [inst : Ring R] [NoZeroDivisors R] {S : Submonoid R},
  Nonempty (OreLocalization.OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.Header.mk.injEq : ∀ (version : UInt8) (isutcnt isstdcnt leapcnt timecnt typecnt charcnt : UInt32) (version_1 : UInt8)
  (isutcnt_1 isstdcnt_1 leapcnt_1 timecnt_1 typecnt_1 charcnt_1 : UInt32),
  ({ version := version, isutcnt := isutcnt, isstdcnt := isstdcnt, leapcnt := leapcnt, timecnt := timecnt,
        typecnt := typecnt, charcnt := charcnt } =
      { version := version_1, isutcnt := isutcnt_1, isstdcnt := isstdcnt_1, leapcnt := leapcnt_1, timecnt := timecnt_1,
        typecnt := typecnt_1, charcnt := charcnt_1 }) =
    (version = version_1 ∧
      isutcnt = isutcnt_1 ∧
        isstdcnt = isstdcnt_1 ∧ leapcnt = leapcnt_1 ∧ timecnt = timecnt_1 ∧ typecnt = typecnt_1 ∧ charcnt = charcnt_1)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.analyticWithinAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E}, HasFPowerSeriesWithinAt f p s x → AnalyticWithinAt 𝕜 f s x
-- Init.Data.SInt.Basic
/-- Multiplies two 32-bit signed integers, wrapping around on over- or underflow.  Usually accessed via
the `*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.mul : Int32 → Int32 → Int32
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.sub : {R : Type u_1} →
  [inst : Ring R] →
    {R₂ : Type u_2} →
      [inst_1 : Ring R₂] →
        {M : Type u_4} →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : AddCommGroup M] →
              {M₂ : Type u_5} →
                [inst_4 : TopologicalSpace M₂] →
                  [inst_5 : AddCommGroup M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R₂ M₂] → {σ₁₂ : R →+* R₂} → [IsTopologicalAddGroup M₂] → Sub (M →SL[σ₁₂] M₂)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Exact.from_tautology : ∀ {σs : List (Type u)} {φ : Prop} {P T : Std.Do.SPred σs} [Std.Do.SPred.Tactic.PropAsSPredTautology φ T], φ → P ⊢ₛ T
-- Init.Data.UInt.Basic
/-- Bitwise and for word-sized unsigned integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
USize.land : USize → USize → USize
-- Mathlib.Logic.Basic
/-- **Alias** of `iff_congr`. -/
Iff.iff : ∀ {p₁ p₂ q₁ q₂ : Prop}, (p₁ ↔ p₂) → (q₁ ↔ q₂) → ((p₁ ↔ q₁) ↔ (p₂ ↔ q₂))
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_nil : ∀ {α : Type u} {β : Type v} (f : α → β), Stream'.Seq.map f Stream'.Seq.nil = Stream'.Seq.nil
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- If `f` is continuous, then so is its proximitiy function at `⊤`.
 -/
ValueDistribution.continuous_proximity_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E}, Continuous f → Continuous (ValueDistribution.proximity f ⊤)
-- Batteries.Data.AssocList
Batteries.AssocList.findEntryP?_eq : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (l : Batteries.AssocList α β),
  Batteries.AssocList.findEntryP? p l =
    List.find?
      (fun x =>
        match x with
        | (a, b) => p a b)
      l.toList
-- Std.Time.Format.DateFormat
Std.Time.DateFormat.mk.sizeOf_spec : ∀ (firstDayOfWeek : Std.Time.Weekday) (minimalDaysInFirstWeek : Std.Time.Internal.Bounded.LE 0 6)
  (symbols : Std.Time.DateFormatSymbols),
  sizeOf { firstDayOfWeek := firstDayOfWeek, minimalDaysInFirstWeek := minimalDaysInFirstWeek, symbols := symbols } =
    1 + sizeOf firstDayOfWeek + sizeOf minimalDaysInFirstWeek + sizeOf symbols
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.NatTrans.commShiftPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  {F : CategoryTheory.Functor C D} [inst_6 : F.CommShift B] {G : CategoryTheory.Functor C D} [inst_7 : G.CommShift B]
  (τ : F ⟶ G) [CategoryTheory.NatTrans.CommShift τ B],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.PullbackShift.natTrans φ τ) A
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) {Z' : C}
  (P' : CategoryTheory.ProjectiveResolution Z') {f : Z ⟶ Z'} (φ : P.Hom P' f) {Z_1 : ChainComplex C ℕ}
  (h : (ChainComplex.single₀ C).obj Z' ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp P'.π h) =
    CategoryTheory.CategoryStruct.comp P.π (CategoryTheory.CategoryStruct.comp ((ChainComplex.single₀ C).map f) h)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rio_add_add_eq_append : ∀ {m n : ℕ}, (*...m + n).toArray = (*...m).toArray ++ (m...m + n).toArray
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.length_eq_fold : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] [inst_4 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = Std.Iter.fold (fun acc x => acc + 1) 0 it
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.restrictScalars_symm_apply : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A ≃ₐ[S] B) (x : B), (AlgEquiv.restrictScalars R f).symm x = f.symm x
-- Mathlib.Data.Set.Lattice
Set.biUnion_and : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι → Prop) (q : ι → ι' → Prop)
  (s : (x : ι) → (y : ι') → p x ∧ q x y → Set α),
  ⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯
-- Mathlib.Analysis.Convex.Strict
StrictConvex.add : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [ContinuousAdd E] {s t : Set E},
  StrictConvex 𝕜 s → StrictConvex 𝕜 t → StrictConvex 𝕜 (s + t)
-- Mathlib.Data.Stream.Init
Stream'.append_right_injective : ∀ {α : Type u} (x : List α) (a b : Stream' α), x ++ₛ a = x ++ₛ b → a = b
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.takeWhile.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α), Array.takeWhile p as = Array.takeWhile.go✝ p as 0 #[]
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.min_order_le_order_add : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : Zero Γ] [inst_2 : LinearOrder Γ] {x y : HahnSeries Γ R},
  x + y ≠ 0 → min x.order y.order ≤ (x + y).order
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.toOpens_injective : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α}, Function.Injective TopologicalSpace.OpenNhdsOf.toOpens
-- Mathlib.Analysis.Calculus.ContDiff.Bounds
/-- Bounding the norm of the iterated derivative of `B (f x) (g x)` within a set in terms of the
iterated derivatives of `f` and `g` when `B` is bilinear of norm at most `1`:
`‖D^n (x ↦ B (f x) (g x))‖ ≤ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖`  -/
ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {F : Type uF}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {G : Type uG} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} {s : Set D} {x : D},
  ContDiffOn 𝕜 N f s →
    ContDiffOn 𝕜 N g s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ∀ {n : ℕ},
            ↑n ≤ N →
              ‖B‖ ≤ 1 →
                ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
                  ∑ i ∈ Finset.range (n + 1),
                    ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
-- Init.Control.Lawful.MonadLift.Instances
_private.Init.Control.Lawful.MonadLift.Instances.0.ExceptT.bindCont.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero_real : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0) →
      ∀ {t : Set α}, MeasurableSet t → μ t ≠ ⊤ → f =ᵐ[μ.restrict t] 0
-- Mathlib.LinearAlgebra.Matrix.StdBasis
Module.Basis.matrix_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {m : Type u_4} {n : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M) (i : m) (j : n)
  (k : ι) [inst_5 : DecidableEq m] [inst_6 : DecidableEq n],
  (Module.Basis.matrix m n b) (i, j, k) = Matrix.single i j (b k)
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_sub_left : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd G G] [IsIsometricVAdd Gᵃᵒᵖ G]
  (a b c : G), edist (a - b) (a - c) = edist b c
-- Std.Async.Basic
/-- Creates a new `BaseAsync` out of a `Task`.
 -/
Std.Async.BaseAsync.ofTask : {α : Type} → Task α → Std.Async.BaseAsync α
-- Mathlib.Algebra.Homology.ShortComplex.Ab
/-- The canonical additive morphism `S.X₁ →+ AddMonoidHom.ker S.g` induced by `S.f`.  -/
CategoryTheory.ShortComplex.abToCycles : (S : CategoryTheory.ShortComplex Ab) → ↑S.X₁ →+ ↥(AddCommGrpCat.Hom.hom S.g).ker
-- Mathlib.Data.Int.Cast.Lemmas
/-- This version is primed so that the `RingHomClass` versions aren't.  -/
map_intCast' : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroupWithOne α] [inst_1 : AddGroupWithOne β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (f : F), f 1 = 1 → ∀ (n : ℤ), f ↑n = ↑n
-- Batteries.Data.UInt
USize.pred_toNat : ∀ {i : USize}, 0 < i → (i - 1).toNat = i.toNat - 1
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- If any parameter to the series is a sufficiently large nonpositive integer, then the series
term is zero.  -/
ordinaryHypergeometricSeries_eq_zero_of_neg_nat : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) {n k : ℕ},
  ↑k = -a ∨ ↑k = -b ∨ ↑k = -c → k < n → ordinaryHypergeometricSeries 𝔸 a b c n = 0
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- An induction principle for additive closure membership for predicates with two arguments.  -/
AddSubmonoid.closure_induction₂ : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M}
  {motive : (x y : M) → x ∈ AddSubmonoid.closure s → y ∈ AddSubmonoid.closure s → Prop},
  (∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯) →
    (∀ (x : M) (hx : x ∈ AddSubmonoid.closure s), motive 0 x ⋯ hx) →
      (∀ (x : M) (hx : x ∈ AddSubmonoid.closure s), motive x 0 hx ⋯) →
        (∀ (x y z : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s)
            (hz : z ∈ AddSubmonoid.closure s), motive x z hx hz → motive y z hy hz → motive (x + y) z ⋯ hz) →
          (∀ (x y z : M) (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s)
              (hz : z ∈ AddSubmonoid.closure s), motive z x hz hx → motive z y hz hy → motive z (x + y) hz ⋯) →
            ∀ {x y : M} (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s), motive x y hx hy
-- Init.Data.Iterators.Producers.Monadic.List
Std.Iterators.Types.ListIterator.instIterator.eq_1 : ∀ {m : Type w → Type w'} {α : Type w} [inst : Pure m],
  Std.Iterators.Types.ListIterator.instIterator =
    {
      IsPlausibleStep := fun it x =>
        match x with
        | Std.IterStep.yield it' out => it.internalState.list = out :: it'.internalState.list
        | Std.IterStep.skip it => False
        | Std.IterStep.done => it.internalState.list = [],
      step := fun it =>
        pure
          (match it with
          | { internalState := { list := [] } } => Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩
          | { internalState := { list := x :: xs } } =>
            Std.Shrink.deflate ⟨Std.IterStep.yield { internalState := { list := xs } } x, ⋯⟩) }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k fallback : α},
        (m₁.inter m₂).getKeyD k fallback = if m₂.contains k = true then m₁.getKeyD k fallback else fallback
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.insphere.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → s.insphere = s_1.insphere
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- Character on a product of `ZMod`s given by `x ↦ ∏ i, e ^ (2 * π * I * x i * y / n)`.  -/
_private.Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality.0.AddChar.mkZModAux : {ι : Type u_2} →
  [DecidableEq ι] →
    (n : ι → ℕ) → [∀ (i : ι), NeZero (n i)] → ((i : ι) → ZMod (n i)) → AddChar (DirectSum ι fun i => ZMod (n i)) Circle
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toMulEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ↑e.symm = (↑e).symm
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntryIfNew_le_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k kmi : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l),
  (Std.Internal.List.minKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi → (compare kmi k).isLE = true
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.toMultiplicative.eq_1 : ∀ (R : Type u_3) (M : Type u_6) [inst : Semiring R] [inst_1 : Add M],
  AddMonoidAlgebra.toMultiplicative R M =
    { toFun := fun x => MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff),
      invFun := fun x => AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.Balanced.depth_bound : ∀ {α : Type u_1} {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ}, t.Balanced c n → t.depth ≤ 2 * (t.size + 1).log2
-- Mathlib.Data.Set.Opposite
/-- The opposite of a set `s` is the set obtained by taking the opposite of each member of `s`.  -/
Set.op : {α : Type u_1} → Set α → Set αᵒᵖ
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.secondCountableTopology : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [Countable ι] [inst : (i : ι) → TopologicalSpace (β i)]
  [∀ (i : ι), SecondCountableTopology (β i)], SecondCountableTopology (PiLp p β)
-- Mathlib.Algebra.Group.Basic
div_eq_of_eq_mul'' : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = c * b → a / b = c
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.regular.inj : ∀ {result result_1 : Aesop.RuleResult},
  Aesop.SafeRuleResult.regular result = Aesop.SafeRuleResult.regular result_1 → result = result_1
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.lift.congr_simp : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g g_1 : A →+* L} (e_g : g = g_1) (hg : Function.Injective ⇑g),
  IsFractionRing.lift hg = IsFractionRing.lift ⋯
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (J : Type u_2) [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  [CategoryTheory.Limits.HasColimitsOfShape J C], (CochainComplex.plus C).IsClosedUnderColimitsOfShape J
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instModule : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : Module R ENNReal] → [IsScalarTower R ENNReal ENNReal] → Module R (MeasureTheory.OuterMeasure α)
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.concreteCategory : CategoryTheory.ConcreteCategory FinBoolAlg fun x1 x2 => BoundedLatticeHom ↑x1.toBoolAlg ↑x2.toBoolAlg
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- The possibilities we distinguish to delaborate the finset indexing a big operator, including
filters.
* `{finset := s, filter = none}` represents `∑ x ∈ s, f x`;
* `{finset := s, filter = some p}` represents `∑ x ∈ s with p, f x`.
 -/
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetFilterResult : Type
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_apply_eq_ofReal_integral' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (f : α → ℝ),
  MeasurableSet s → (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instLocallySmallFunctor : ∀ {A : Type u'} [inst : CategoryTheory.Category.{v', u'} A] [CategoryTheory.LocallySmall.{w, v', u'} A] (C : Type w)
  [inst_2 : CategoryTheory.SmallCategory C],
  CategoryTheory.LocallySmall.{w, max v' w, max (max (max u' w) v') w} (CategoryTheory.Functor C A)
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- If `P` is a morphism property affine locally defined by `affineAnd Q`, `P` is stable under
composition if `Q` is.  -/
AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) → P.IsStableUnderComposition
-- Mathlib.Topology.Order.OrderClosed
/-- The limit of a collection of functions that is frequently monotone is monotone.  -/
monotone_of_frequently_monotone_of_tendsto : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {ι : Type u_1}
  {l : Filter ι} [inst_2 : Preorder β] {F : ι → β → α} {f : β → α},
  (∃ᶠ (i : ι) in l, Monotone (F i)) → (∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) → Monotone f
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.ringHomComp_inv : ∀ {R' : Type u_2} [inst : CommRing R'] {R'' : Type u_3} [inst_1 : CommRing R''] {R : Type u_4}
  [inst_2 : CommMonoidWithZero R] (χ : MulChar R R') (f : R' →+* R''), (χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_eq_mk_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {g₁ g₂ : GL n R},
  Matrix.ProjGenLinGroup.mk g₁ = Matrix.ProjGenLinGroup.mk g₂ ↔ ∃ u, g₁ * (Matrix.GeneralLinearGroup.scalar n) u = g₂
-- Std.Time.Format.Modifier
/-- `Year` represents different year formatting styles based on the number of pattern letters.
 -/
Std.Time.Year : Type
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_div_left : ∀ {m n a : ℕ}, m.Coprime n → a ∣ m → (m / a).Coprime n
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.RingTheory.TotallySplit
Algebra.IsFiniteSplit.instEtale : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsFiniteSplit R S], Algebra.Etale R S
-- Aesop.Index
_private.Aesop.Index.0.Aesop.Index.trace.traceArray : {α : Type} → [ToString (Aesop.Rule α)] → Aesop.TraceOption → Array (Aesop.Rule α) → Lean.CoreM Unit
-- Mathlib.Order.Filter.Cofinite
Filter.cofinite_inf_principal_neBot_iff : ∀ {α : Type u_2} {s : Set α}, (Filter.cofinite ⊓ Filter.principal s).NeBot ↔ s.Infinite
-- Mathlib.Analysis.Oscillation
/-- The oscillation of `f : E → F` at `x`.  -/
oscillation : {E : Type u} → {F : Type v} → [PseudoEMetricSpace F] → [TopologicalSpace E] → (E → F) → E → ENNReal
-- Init.Data.List.Sublist
List.IsInfix.eq_of_length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₂.length ≤ l₁.length → l₁ = l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_δ_self'_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)},
  j = i.castSucc →
    ∀ (x : S.obj (Opposite.op { len := n + 2 })),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j)) x) =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
          ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.succ)) x)